[]: Open (size=159, cost=0, time=0, max=0, total=1.21593e-05, pending=1)
[0]: Open (size=1299, cost=10933, time=13.4525, max=0.66532, total=16.126, pending=1)
[00]: Open (size=1299, cost=6135, time=13.6118, max=0.66532, total=16.8924, pending=2)
[000]: Open (size=1299, cost=3457, time=13.775, max=0.66532, total=17.4152, pending=3)
[0000]: Open (size=1299, cost=2702, time=13.9136, max=0.66532, total=17.8175, pending=4)
[00000]: Open (size=1299, cost=2347, time=14.0486, max=0.66532, total=18.1683, pending=5)
[000000]: Open (size=1299, cost=2260, time=14.1823, max=0.66532, total=18.5509, pending=6)
[0000000]: Open (size=1295, cost=2256, time=14.3198, max=0.66532, total=18.904, pending=7)
[0000001]: Open (size=1295, cost=2256, time=14.391, max=0.66532, total=19.3434, pending=8)
[00000000]: Open (size=1295, cost=2256, time=14.5104, max=0.66532, total=19.6859, pending=9)
[00000001]: Open (size=1295, cost=2256, time=14.5604, max=0.66532, total=20.0304, pending=10)
[000000001]: Open (size=1295, cost=2256, time=14.7188, max=0.66532, total=20.3684, pending=11)
[0000000011]: Open (size=1212, cost=2180, time=14.9709, max=0.66532, total=20.7813, pending=12)
******* COMPLETION *******
f3(f3(f3(f3(X0)))) -> f3(X0)
f3(j(Z0)) -> f3(f3(Z0))
g(X0,Z1) -> f3(Z1)
f4(Y0) -> f3(Y0)
f10(Y0) -> f3(Y0)
f5(Y0) -> f3(Y0)
f1(Y0) -> f3(Y0)
f7(Y0) -> f3(Y0)
f8(Y0) -> f3(Y0)
f6(Y0) -> f3(Y0)
f2(Y0) -> f3(Y0)
f9(Y0) -> f3(Y0)
**************************
On branch: [0000000011]
With size, cost: 54, 1022
Orientations: 254
Calls to AProVE (all, T, NT, ?): 139, 139, 0, 0
Time (all, branch, AProVE): 20.9767, 15.1296, 17.4662
Time/call in AProVE (Avg, Min, Max): 0.125656, 0.665118, 0.019181
Time/T-call in AProVE (Avg, Min, Max): 0.125656, 0.665118, 0.66532
All conjectures solved.