[]: Open (size=71, cost=0, time=0, max=0, total=1.09673e-05, pending=1)
[0]: Open (size=71, cost=71, time=0.819302, max=0.819302, total=0.845217, pending=1)
[1]: Open (size=71, cost=71, time=0.025686, max=0.025686, total=0.933894, pending=2)
[01]: Open (size=71, cost=71, time=0.843199, max=0.819302, total=0.990547, pending=3)
[11]: Open (size=71, cost=71, time=0.0625539, max=0.0368679, total=1.08023, pending=3)
[01]: Open (size=71, cost=71, time=0.932375, max=0.819302, total=1.11766, pending=3)
[11]: Open (size=71, cost=71, time=0.0997829, max=0.0372291, total=1.17789, pending=3)
[01]: Open (size=71, cost=71, time=0.992276, max=0.819302, total=1.23074, pending=3)
[11]: Open (size=71, cost=71, time=0.152327, max=0.0525441, total=1.26875, pending=3)
[01]: Open (size=71, cost=71, time=1.02989, max=0.819302, total=1.30235, pending=3)
[11]: Open (size=71, cost=71, time=0.185488, max=0.0525441, total=1.3537, pending=3)
[01]: Open (size=71, cost=71, time=1.08071, max=0.819302, total=1.40355, pending=3)
[11]: Open (size=71, cost=71, time=0.234801, max=0.0525441, total=1.52842, pending=4)
[011]: Open (size=71, cost=71, time=1.13006, max=0.819302, total=1.61682, pending=5)
[111]: Open (size=71, cost=71, time=0.279903, max=0.0525441, total=1.76051, pending=6)
[00]: Open (size=71, cost=71, time=0.883866, max=0.819302, total=1.89173, pending=7)
[010]: Open (size=71, cost=71, time=1.15544, max=0.819302, total=1.94599, pending=7)
[110]: Open (size=71, cost=71, time=0.277213, max=0.0525441, total=2.18395, pending=8)
[00]: Open (size=71, cost=71, time=0.937884, max=0.819302, total=2.3859, pending=9)
[10]: Open (size=71, cost=71, time=0.0452542, max=0.025686, total=2.46002, pending=9)
[00]: Open (size=71, cost=71, time=1.01169, max=0.819302, total=2.54238, pending=9)
[10]: Open (size=71, cost=71, time=0.127383, max=0.082129, total=2.65357, pending=9)
[00]: Open (size=71, cost=71, time=1.12237, max=0.819302, total=2.68361, pending=9)
[10]: Open (size=71, cost=71, time=0.15712, max=0.082129, total=2.70908, pending=9)
[00]: Open (size=71, cost=71, time=1.14717, max=0.819302, total=2.7332, pending=9)
[10]: Open (size=71, cost=71, time=0.180783, max=0.082129, total=2.85771, pending=10)
[000]: Open (size=71, cost=71, time=1.23764, max=0.819302, total=2.90379, pending=10)
[001]: Open (size=71, cost=71, time=1.18047, max=0.819302, total=3.04631, pending=11)
[10]: Open (size=71, cost=71, time=0.226298, max=0.082129, total=3.13246, pending=12)
[0000]: Open (size=71, cost=71, time=1.28409, max=0.819302, total=3.24848, pending=13)
[0010]: Open (size=71, cost=71, time=1.23666, max=0.819302, total=3.35557, pending=13)
[0000]: Open (size=71, cost=71, time=1.38994, max=0.819302, total=3.38309, pending=13)
[100]: Open (size=71, cost=71, time=0.260545, max=0.082129, total=4.12802, pending=14)
[101]: Open (size=71, cost=71, time=0.307273, max=0.082129, total=4.41681, pending=15)
[00000]: Open (size=71, cost=71, time=1.94723, max=0.819302, total=4.52637, pending=16)
[000000]: Open (size=71, cost=71, time=2.84315, max=0.895914, total=6.22214, pending=17)
******* COMPLETION *******
dfib(s(s(X0))) -> plus(dfib(s(X0)),plus(dfib(X0),dfib(X0)))
fib(s(s(X0))) -> plus(fib(s(X0)),fib(X0))
minus(s(X0),s(Y0)) -> minus(X0,Y0)
plus(X0,s(Y0)) -> s(plus(X0,Y0))
p(X0) -> minus(X0,s(zero))
fib(s(zero)) -> s(zero)
dfib(s(zero)) -> s(zero)
dfib(zero) -> s(zero)
minus(X0,zero) -> X0
plus(X0,zero) -> X0
fib(zero) -> s(zero)
**************************
On branch: [000000]
With size, cost: 71, 71
Orientations: 70
Calls to AProVE (all, T, NT, ?): 52, 52, 0, 0
Time (all, branch, AProVE): 6.22763, 2.84315, 6.18703
Time/call in AProVE (Avg, Min, Max): 0.118981, 0.895631, 0.019531
Time/T-call in AProVE (Avg, Min, Max): 0.118981, 0.895631, 0.895914
All conjectures solved.