[]: Open (size=19, cost=0, time=0, max=0, total=1.00136e-05, pending=1)
[1]: Open (size=19, cost=19, time=0.852395, max=0.793397, total=0.8844, pending=1)
[0]: Open (size=19, cost=29, time=0.825098, max=0.793397, total=0.940239, pending=1)
[01]: Open (size=20, cost=25, time=0.867936, max=0.793397, total=1.04156, pending=2)
[010]: Open (size=21, cost=26, time=0.920256, max=0.793397, total=1.27752, pending=3)
[011]: Open (size=21, cost=26, time=1.05127, max=0.793397, total=1.33022, pending=3)
[00]: Open (size=19, cost=29, time=0.883139, max=0.793397, total=1.44231, pending=3)
[001]: Open (size=21, cost=25, time=0.942178, max=0.793397, total=1.55755, pending=4)
[1]: Open (size=20, cost=32, time=0.907911, max=0.793397, total=1.66172, pending=4)
[001]: Open (size=21, cost=53, time=1.04582, max=0.793397, total=1.7366, pending=4)
[000]: Open (size=19, cost=53, time=0.938992, max=0.793397, total=1.977, pending=5)
[0000]: Open (size=27, cost=46, time=0.994912, max=0.793397, total=2.12145, pending=6)
[0001]: Open (size=24, cost=48, time=1.02696, max=0.793397, total=2.24405, pending=6)
[011]: Open (size=21, cost=54, time=1.16291, max=0.793397, total=2.34814, pending=7)
[010]: Open (size=21, cost=54, time=0.972532, max=0.793397, total=2.60868, pending=8)
[0101]: Open (size=27, cost=40, time=1.08047, max=0.793397, total=2.84857, pending=9)
[0011]: Open (size=27, cost=55, time=1.11709, max=0.793397, total=3.03366, pending=9)
[0111]: Open (size=27, cost=56, time=1.31509, max=0.793397, total=3.16167, pending=9)
[00010]: Open (size=36, cost=56, time=1.09109, max=0.793397, total=3.30168, pending=9)
[000100]: Open (size=36, cost=55, time=1.25365, max=0.793397, total=3.61676, pending=10)
[1]: Open (size=21, cost=61, time=0.982351, max=0.793397, total=3.94605, pending=11)
[11]: Open (size=41, cost=49, time=1.09938, max=0.793397, total=4.14651, pending=12)
[111]: Open (size=41, cost=49, time=1.30485, max=0.793397, total=4.47911, pending=13)
[1111]: Open (size=41, cost=41, time=1.43634, max=0.793397, total=4.72492, pending=14)
******* COMPLETION *******
d(a(a(X0))) -> a(d(a(X0)))
c(a(X0)) -> a(c(X0))
b(a(X0)) -> a(c(X0))
b(d(X0)) -> X0
e(X0) -> d(a(X0))
c(d(a(X0))) -> a(X0)
d(a(c(X0))) -> a(X0)
**************************
On branch: [1111]
With size, cost: 41, 41
Orientations: 50
Calls to AProVE (all, T, NT, ?): 39, 39, 0, 0
Time (all, branch, AProVE): 4.72551, 1.43634, 4.70781
Time/call in AProVE (Avg, Min, Max): 0.120713, 0.793193, 0.031646
Time/T-call in AProVE (Avg, Min, Max): 0.120713, 0.793193, 0.793397
All conjectures solved.