[]: Open (size=54, cost=0, time=0, max=0, total=9.05991e-06, pending=1)
[0]: Open (size=54, cost=54, time=0.77566, max=0.77566, total=0.808594, pending=1)
[1]: Open (size=54, cost=54, time=0.0327129, max=0.0327129, total=0.891032, pending=2)
[00]: Open (size=54, cost=54, time=0.824744, max=0.77566, total=0.950407, pending=3)
[10]: Open (size=54, cost=54, time=0.0535209, max=0.0327129, total=0.978445, pending=3)
[00]: Open (size=55, cost=55, time=0.852535, max=0.77566, total=1.07806, pending=4)
[01]: Open (size=54, cost=72, time=0.808767, max=0.77566, total=1.15245, pending=5)
[010]: Open (size=54, cost=72, time=0.84849, max=0.77566, total=1.22515, pending=6)
[11]: Open (size=54, cost=84, time=0.0707619, max=0.038049, total=1.35455, pending=7)
[110]: Open (size=53, cost=81, time=0.143347, max=0.0725851, total=1.45235, pending=8)
[0101]: Open (size=53, cost=85, time=0.933745, max=0.77566, total=1.52249, pending=9)
[111]: Open (size=54, cost=85, time=0.0956399, max=0.038049, total=1.83488, pending=10)
[011]: Open (size=54, cost=86, time=0.841406, max=0.77566, total=2.00958, pending=11)
[100]: Open (size=53, cost=90, time=0.112096, max=0.034539, total=2.10556, pending=12)
[000]: Open (size=55, cost=101, time=0.88963, max=0.77566, total=2.22493, pending=13)
[1101]: Open (size=52, cost=108, time=0.189352, max=0.0725851, total=2.43092, pending=14)
[0100]: Open (size=53, cost=111, time=0.892086, max=0.77566, total=2.49413, pending=15)
[1111]: Open (size=53, cost=114, time=0.186682, max=0.091042, total=2.661, pending=16)
[0111]: Open (size=53, cost=115, time=0.882568, max=0.77566, total=2.74988, pending=17)
[101]: Open (size=53, cost=122, time=0.117896, max=0.040339, total=2.93005, pending=18)
[1110]: Open (size=53, cost=124, time=0.178721, max=0.083081, total=3.08257, pending=19)
[0110]: Open (size=53, cost=125, time=0.895588, max=0.77566, total=7.20241, pending=20)
[1100]: Open (size=52, cost=129, time=0.166972, max=0.0725851, total=7.34616, pending=21)
[001]: Open (size=55, cost=138, time=0.88922, max=0.77566, total=7.53083, pending=22)
[11010]: Open (size=52, cost=138, time=0.232988, max=0.0725851, total=7.85732, pending=23)
[11110]: Open (size=55, cost=152, time=0.226107, max=0.091042, total=8.12213, pending=24)
[01110]: Open (size=55, cost=153, time=0.974579, max=0.77566, total=8.33954, pending=25)
[1000]: Open (size=56, cost=153, time=0.184033, max=0.0719371, total=8.64044, pending=26)
[10001]: Open (size=68, cost=110, time=0.254852, max=0.0719371, total=9.80218, pending=27)
[11000]: Open (size=52, cost=159, time=0.249887, max=0.0829148, total=10.7898, pending=28)
[100010]: Open (size=72, cost=162, time=0.595882, max=0.179974, total=11.1593, pending=28)
[1000100]: Open (size=72, cost=114, time=0.919334, max=0.323452, total=11.6819, pending=29)
******* COMPLETION *******
d(d(d(d(d(X0))))) -> d(d(d(d(X0))))
d(d(d(c(X0)))) -> d(d(d(d(X0))))
e(d(X0)) -> d(d(d(d(e(X0)))))
e(c(X0)) -> d(d(d(d(e(X0)))))
c(d(X0)) -> d(d(d(d(X0))))
b(X0) -> d(d(X0))
a(X0) -> d(d(d(d(X0))))
c(c(X0)) -> d(d(d(X0)))
**************************
On branch: [1000100]
With size, cost: 66, 78
Orientations: 68
Calls to AProVE (all, T, NT, ?): 65, 63, 1, 1
Time (all, branch, AProVE): 35.5658, 1.26264, 35.4788
Time/call in AProVE (Avg, Min, Max): 0.545828, 23.5047, 0.018528
Time/T-call in AProVE (Avg, Min, Max): 0.185929, 3.99379, 0.343303
All conjectures solved.