[]: Open (size=66, cost=0, time=0, max=0, total=1.71661e-05, pending=1)
[0]: Open (size=66, cost=66, time=0.949296, max=0.76515, total=1.00343, pending=1)
[1]: Open (size=66, cost=66, time=0.941054, max=0.76515, total=1.14958, pending=2)
[00]: Open (size=66, cost=66, time=1.03284, max=0.76515, total=1.25814, pending=3)
[11]: Open (size=66, cost=66, time=1.00064, max=0.76515, total=1.36846, pending=4)
[000]: Open (size=66, cost=66, time=1.10065, max=0.76515, total=1.47911, pending=5)
[10]: Open (size=66, cost=66, time=0.989504, max=0.76515, total=1.65775, pending=6)
[0000]: Open (size=66, cost=66, time=1.17231, max=0.76515, total=1.80659, pending=7)
[001]: Open (size=67, cost=71, time=1.07461, max=0.76515, total=2.0622, pending=8)
[101]: Open (size=67, cost=71, time=1.03021, max=0.76515, total=2.19493, pending=8)
[001]: Open (size=67, cost=71, time=1.20662, max=0.76515, total=2.28025, pending=8)
[111]: Open (size=67, cost=71, time=1.0421, max=0.76515, total=2.4431, pending=9)
[0010]: Open (size=69, cost=73, time=1.27631, max=0.76515, total=2.47452, pending=9)
[110]: Open (size=66, cost=76, time=1.06916, max=0.76515, total=2.61423, pending=10)
[100]: Open (size=66, cost=76, time=1.09686, max=0.76515, total=2.80651, pending=11)
[1100]: Open (size=66, cost=76, time=1.19282, max=0.76515, total=2.86011, pending=12)
[1000]: Open (size=66, cost=76, time=1.1197, max=0.76515, total=3.47658, pending=12)
[101]: Open (size=67, cost=81, time=1.11479, max=0.76515, total=3.80754, pending=12)
[111]: Open (size=67, cost=81, time=1.07278, max=0.76515, total=3.85742, pending=13)
[01]: Open (size=66, cost=82, time=1.01139, max=0.76515, total=3.91861, pending=14)
[010]: Open (size=66, cost=82, time=1.03744, max=0.76515, total=3.97389, pending=15)
[0100]: Open (size=66, cost=82, time=1.09758, max=0.76515, total=4.102, pending=16)
[1010]: Open (size=69, cost=83, time=1.13674, max=0.76515, total=4.18237, pending=17)
[1110]: Open (size=69, cost=83, time=1.09765, max=0.76515, total=4.61405, pending=17)
[01000]: Open (size=74, cost=86, time=1.12947, max=0.76515, total=4.93966, pending=17)
[010000]: Open (size=74, cost=86, time=1.16159, max=0.76515, total=5.00171, pending=18)
[00000]: Open (size=75, cost=87, time=1.2947, max=0.76515, total=5.80081, pending=19)
[011]: Open (size=67, cost=87, time=1.03977, max=0.76515, total=6.15461, pending=20)
[000000]: Open (size=75, cost=87, time=1.55654, max=0.76515, total=6.24658, pending=20)
[011]: Open (size=67, cost=87, time=1.13073, max=0.76515, total=6.95592, pending=21)
[0000000]: Open (size=75, cost=87, time=1.90627, max=0.76515, total=7.1785, pending=22)
******* COMPLETION *******
f(s(s(Z0))) -> p(f(s(Z0)),f(Z0))
n(b(X0,Y0)) -> b(p(X0,Y0),X0)
p(X0,s(Y0)) -> s(p(X0,Y0))
g(X0) -> b(f(s(X0)),f(X0))
u(b(X0,Y0)) -> p(X0,Y0)
f(s(zero)) -> s(zero)
p(X0,zero) -> X0
f(zero) -> zero
**************************
On branch: [0000000]
With size, cost: 54, 66
Orientations: 66
Calls to AProVE (all, T, NT, ?): 59, 55, 4, 0
Time (all, branch, AProVE): 7.18078, 1.90627, 7.13334
Time/call in AProVE (Avg, Min, Max): 0.120904, 0.764763, 0.021733
Time/T-call in AProVE (Avg, Min, Max): 0.104444, 0.764763, 0.76515
All conjectures solved.