[]: Open (size=74, cost=0, time=0, max=0, total=1.50204e-05, pending=1)
[0]: Open (size=74, cost=74, time=0.823765, max=0.7908, total=0.889211, pending=1)
[1]: Open (size=74, cost=74, time=0.855927, max=0.7908, total=0.997431, pending=2)
[01]: Open (size=74, cost=74, time=0.876431, max=0.7908, total=1.10473, pending=3)
[11]: Open (size=74, cost=74, time=0.90716, max=0.7908, total=1.29804, pending=4)
[011]: Open (size=74, cost=74, time=0.980986, max=0.7908, total=1.3768, pending=5)
[111]: Open (size=74, cost=74, time=0.938225, max=0.7908, total=1.58952, pending=6)
[10]: Open (size=74, cost=74, time=0.911743, max=0.7908, total=1.8096, pending=7)
[101]: Open (size=74, cost=74, time=1.03572, max=0.7908, total=2.03742, pending=8)
[1010]: Open (size=74, cost=74, time=1.17007, max=0.7908, total=2.2646, pending=9)
[1011]: Open (size=74, cost=74, time=1.12806, max=0.7908, total=2.44299, pending=10)
[10100]: Open (size=74, cost=74, time=1.28454, max=0.7908, total=2.57958, pending=11)
[10101]: Open (size=74, cost=74, time=1.23332, max=0.7908, total=2.83294, pending=12)
[1111]: Open (size=75, cost=75, time=1.04728, max=0.7908, total=3.12614, pending=13)
[0111]: Open (size=75, cost=75, time=1.109, max=0.7908, total=3.38969, pending=14)
[1110]: Open (size=75, cost=75, time=1.04866, max=0.7908, total=3.64183, pending=15)
[11100]: Open (size=75, cost=75, time=1.1558, max=0.7908, total=3.86078, pending=16)
[11101]: Open (size=75, cost=75, time=1.15978, max=0.7908, total=4.16208, pending=17)
[101001]: Open (size=76, cost=76, time=1.41261, max=0.7908, total=4.52459, pending=18)
[10110]: Open (size=76, cost=76, time=1.18958, max=0.7908, total=4.75048, pending=19)
[10111]: Open (size=76, cost=76, time=1.20243, max=0.7908, total=4.92891, pending=20)
[101011]: Open (size=76, cost=76, time=1.37437, max=0.7908, total=5.10894, pending=21)
[111011]: Open (size=77, cost=77, time=1.33187, max=0.7908, total=5.40823, pending=22)
[01111]: Open (size=77, cost=77, time=1.22615, max=0.7908, total=5.68272, pending=23)
[111001]: Open (size=77, cost=77, time=1.30396, max=0.7908, total=5.86671, pending=24)
[01110]: Open (size=77, cost=77, time=1.24326, max=0.7908, total=5.96242, pending=25)
[011111]: Open (size=77, cost=77, time=1.28823, max=0.7908, total=6.25758, pending=26)
[0111110]: Open (size=67, cost=69, time=1.41891, max=0.7908, total=6.52128, pending=27)
[011101]: Open (size=77, cost=77, time=1.43465, max=0.7908, total=6.89485, pending=28)
[0111010]: Open (size=69, cost=77, time=1.60418, max=0.7908, total=7.12634, pending=29)
[01110100]: Open (size=67, cost=75, time=1.69094, max=0.7908, total=7.31436, pending=30)
[01110101]: Open (size=67, cost=75, time=1.70423, max=0.7908, total=7.63809, pending=31)
[11111]: Open (size=78, cost=78, time=1.18417, max=0.7908, total=7.81695, pending=32)
[101111]: Open (size=78, cost=78, time=1.30117, max=0.7908, total=7.96729, pending=33)
[1011110]: Open (size=68, cost=70, time=1.35406, max=0.7908, total=8.06859, pending=34)
[11110]: Open (size=78, cost=78, time=1.17319, max=0.7908, total=8.18271, pending=35)
[101101]: Open (size=78, cost=78, time=1.25247, max=0.7908, total=8.25732, pending=36)
[1011010]: Open (size=70, cost=78, time=1.3195, max=0.7908, total=8.41246, pending=37)
[10110100]: Open (size=68, cost=76, time=1.42409, max=0.7908, total=8.54535, pending=38)
[10110101]: Open (size=68, cost=76, time=1.34659, max=0.7908, total=8.66144, pending=39)
[1010010]: Open (size=68, cost=80, time=1.56469, max=0.7908, total=8.83347, pending=40)
[111111]: Open (size=80, cost=80, time=1.24555, max=0.7908, total=8.96946, pending=41)
[1111110]: Open (size=70, cost=73, time=1.27876, max=0.7908, total=9.02941, pending=42)
[111101]: Open (size=80, cost=80, time=1.20706, max=0.7908, total=9.16987, pending=43)
[1111010]: Open (size=72, cost=81, time=1.2486, max=0.7908, total=9.23544, pending=44)
[11110100]: Open (size=70, cost=79, time=1.30702, max=0.7908, total=9.34432, pending=45)
[11110101]: Open (size=70, cost=79, time=1.29784, max=0.7908, total=9.46267, pending=46)
[1110010]: Open (size=70, cost=82, time=1.34166, max=0.7908, total=9.5644, pending=47)
[1010111]: Open (size=68, cost=84, time=1.56656, max=0.7908, total=9.64799, pending=48)
[1010110]: Open (size=68, cost=84, time=1.48021, max=0.7908, total=9.69796, pending=49)
[1010011]: Open (size=68, cost=84, time=1.48521, max=0.7908, total=9.77104, pending=50)
[0111111]: Open (size=69, cost=85, time=1.41994, max=0.7908, total=9.83852, pending=51)
[0111011]: Open (size=69, cost=85, time=1.49548, max=0.7908, total=9.93075, pending=52)
[01111111]: Open (size=69, cost=85, time=1.47692, max=0.7908, total=9.99782, pending=53)
******* COMPLETION *******
d(g(c(Z0))) -> e(g(c(Z0)))
x1(h(j(g(Z0)))) -> x1(h(Z0))
w(i(g(c(Z0)))) -> h(c(Z0))
x1(w(i(Z0))) -> x1(w(d(Z0)))
j(f(Z0)) -> Z0
y1(b(Z0)) -> g(Z0)
a(Z0) -> i(y1(Z0))
o(Z0) -> x1(h(c(Z0)))
w(e(Z0)) -> h(j(Z0))
u(Z0) -> x1(w(d(y1(Z0))))
e(f(c(Z0))) -> i(g(c(Z0)))
**************************
On branch: [01111111]
With size, cost: 73, 75
Orientations: 112
Calls to AProVE (all, T, NT, ?): 110, 109, 1, 0
Time (all, branch, AProVE): 10.8115, 1.65648, 10.7051
Time/call in AProVE (Avg, Min, Max): 0.0973192, 0.790603, 0.021898
Time/T-call in AProVE (Avg, Min, Max): 0.0924368, 0.790603, 0.7908
All conjectures solved.