[]: Open (size=48, cost=0, time=0, max=0, total=9.05991e-06, pending=1)
[1]: Open (size=48, cost=48, time=0.847498, max=0.798497, total=0.879805, pending=1)
[10]: Open (size=48, cost=48, time=0.878145, max=0.798497, total=0.953822, pending=2)
[11]: Open (size=48, cost=78, time=0.890005, max=0.798497, total=1.6566, pending=2)
[0]: Open (size=48, cost=114, time=0.83034, max=0.798497, total=2.84307, pending=2)
[01]: Open (size=48, cost=78, time=0.930371, max=0.798497, total=3.01539, pending=3)
[10]: Open (size=48, cost=148, time=0.95098, max=0.798497, total=8.47543, pending=3)
[101]: Open (size=46, cost=180, time=1.01276, max=0.798497, total=8.63555, pending=4)
[00]: Open (size=48, cost=198, time=0.901847, max=0.798497, total=8.90469, pending=5)
[100]: Open (size=49, cost=221, time=1.04705, max=0.798497, total=14.1559, pending=5)
[1000]: Open (size=52, cost=223, time=1.09976, max=0.798497, total=14.6266, pending=6)
[1010]: Open (size=47, cost=255, time=1.13058, max=0.798497, total=17.4284, pending=7)
[10101]: Open (size=55, cost=256, time=1.37934, max=0.798497, total=17.8742, pending=8)
[00]: Open (size=48, cost=266, time=0.930363, max=0.798497, total=18.3624, pending=9)
[000]: Open (size=48, cost=179, time=1.01532, max=0.798497, total=18.5203, pending=10)
[0001]: Open (size=49, cost=149, time=1.50951, max=0.798497, total=19.0613, pending=11)
[00010]: Open (size=52, cost=241, time=2.75935, max=1.10308, total=21.1284, pending=12)
[101011]: Open (size=78, cost=271, time=1.68397, max=0.798497, total=28.2499, pending=12)
[10100]: Open (size=54, cost=286, time=1.43687, max=0.798497, total=28.3888, pending=13)
[101010]: Open (size=78, cost=287, time=1.67913, max=0.798497, total=34.5477, pending=13)
[10000]: Open (size=53, cost=294, time=2.25159, max=1.15183, total=34.84, pending=14)
[10100]: Open (size=63, cost=299, time=1.59453, max=0.798497, total=41.1591, pending=14)
[1011]: Open (size=45, cost=306, time=1.1616, max=0.798497, total=41.1975, pending=14)
[10111]: Open (size=53, cost=285, time=1.19747, max=0.798497, total=41.2622, pending=15)
[0000]: Open (size=48, cost=331, time=1.06049, max=0.798497, total=41.326, pending=15)
[10100]: Open (size=95, cost=333, time=1.62591, max=0.798497, total=41.3748, pending=16)
[10111]: Open (size=53, cost=359, time=1.25738, max=0.798497, total=41.9768, pending=17)
[101001]: Open (size=126, cost=360, time=1.78915, max=0.798497, total=42.2814, pending=17)
[001]: Open (size=46, cost=364, time=1.00142, max=0.798497, total=42.409, pending=18)
[101000]: Open (size=126, cost=367, time=1.78791, max=0.798497, total=42.5189, pending=18)
[10111]: Open (size=123, cost=372, time=1.3165, max=0.798497, total=42.6358, pending=19)
[10110]: Open (size=52, cost=375, time=1.18574, max=0.798497, total=42.8203, pending=19)
[10111]: Open (size=116, cost=377, time=1.38932, max=0.798497, total=48.5893, pending=19)
******* COMPLETION *******
b(a(a(c(X0)))) -> b(a(a(a(X0))))
a(a(a(a(X0)))) -> a(a(a(X0)))
c(a(a(a(X0)))) -> a(a(a(X0)))
c(a(c(X0))) -> a(a(c(X0)))
a(c(a(X0))) -> a(a(a(X0)))
a(b(a(a(X0)))) -> c(a(a(X0)))
b(a(b(X0))) -> b(X0)
c(b(X0)) -> a(a(b(X0)))
a(a(b(a(X0)))) -> a(a(X0))
c(c(X0)) -> c(a(a(X0)))
c(a(a(c(X0)))) -> a(a(a(X0)))
a(a(a(c(X0)))) -> a(a(a(X0)))
b(c(a(a(X0)))) -> b(a(a(X0)))
**************************
On branch: [10111]
With size, cost: 108, 138
Orientations: 94
Calls to AProVE (all, T, NT, ?): 85, 64, 15, 6
Time (all, branch, AProVE): 50.4662, 1.71136, 50.1527
Time/call in AProVE (Avg, Min, Max): 0.590032, 5.98244, 0.0187328
Time/T-call in AProVE (Avg, Min, Max): 0.187701, 1.78699, 0.798497
All conjectures solved.