[]: Open (size=38, cost=0, time=0, max=0, total=1.50204e-05, pending=1)
[1]: Open (size=38, cost=38, time=0.024735, max=0.024735, total=0.832455, pending=1)
[11]: Open (size=38, cost=38, time=0.0433691, max=0.024735, total=0.915684, pending=2)
[0]: Open (size=38, cost=56, time=0.807463, max=0.807463, total=1.0043, pending=3)
[111]: Open (size=38, cost=62, time=0.106021, max=0.0626521, total=1.04363, pending=4)
[10]: Open (size=38, cost=62, time=0.089083, max=0.064348, total=1.3892, pending=5)
[100]: Open (size=38, cost=62, time=0.17346, max=0.0843771, total=1.54493, pending=6)
[101]: Open (size=38, cost=62, time=0.160113, max=0.0710299, total=1.91836, pending=7)
[01]: Open (size=38, cost=70, time=0.824679, max=0.807463, total=2.24029, pending=8)
[110]: Open (size=38, cost=70, time=0.0686669, max=0.0252979, total=2.37948, pending=9)
[00]: Open (size=38, cost=80, time=0.829325, max=0.807463, total=2.5122, pending=10)
[1010]: Open (size=39, cost=83, time=0.25529, max=0.0951769, total=2.67677, pending=11)
[1110]: Open (size=39, cost=83, time=0.268965, max=0.162944, total=2.83018, pending=11)
[1010]: Open (size=41, cost=83, time=0.40698, max=0.15169, total=3.09452, pending=11)
[1110]: Open (size=41, cost=83, time=0.53144, max=0.262475, total=3.40412, pending=12)
[1100]: Open (size=39, cost=91, time=0.110727, max=0.0420599, total=3.76344, pending=13)
[011]: Open (size=38, cost=92, time=0.881182, max=0.807463, total=3.91552, pending=13)
[000]: Open (size=38, cost=92, time=0.908617, max=0.807463, total=4.07826, pending=14)
[001]: Open (size=38, cost=92, time=0.914074, max=0.807463, total=4.1352, pending=15)
[1000]: Open (size=39, cost=103, time=0.346064, max=0.172604, total=4.19711, pending=16)
[0001]: Open (size=37, cost=105, time=0.926725, max=0.807463, total=4.50527, pending=17)
[0010]: Open (size=37, cost=107, time=0.939614, max=0.807463, total=4.65236, pending=18)
[0110]: Open (size=37, cost=107, time=0.987277, max=0.807463, total=4.80088, pending=19)
[0000]: Open (size=37, cost=107, time=0.946843, max=0.807463, total=4.95096, pending=20)
[1100]: Open (size=41, cost=115, time=0.260905, max=0.150178, total=5.12161, pending=21)
[010]: Open (size=38, cost=116, time=0.906877, max=0.807463, total=5.28386, pending=22)
[0100]: Open (size=37, cost=115, time=1.00759, max=0.807463, total=5.43628, pending=23)
[00011]: Open (size=36, cost=120, time=0.966154, max=0.807463, total=5.6901, pending=24)
[00001]: Open (size=36, cost=120, time=1.05281, max=0.807463, total=6.59393, pending=25)
[0011]: Open (size=37, cost=121, time=0.949719, max=0.807463, total=6.8465, pending=26)
[0111]: Open (size=37, cost=121, time=0.937195, max=0.807463, total=7.11765, pending=27)
[01101]: Open (size=36, cost=136, time=1.03555, max=0.807463, total=7.3655, pending=28)
[00101]: Open (size=36, cost=136, time=0.982946, max=0.807463, total=7.5142, pending=29)
[00111]: Open (size=36, cost=136, time=1.05774, max=0.807463, total=7.68204, pending=30)
[01111]: Open (size=36, cost=136, time=1.08112, max=0.807463, total=7.83467, pending=31)
[11100]: Open (size=42, cost=137, time=0.667263, max=0.262475, total=8.0244, pending=32)
[10100]: Open (size=42, cost=140, time=0.596836, max=0.189856, total=8.23533, pending=33)
[101001]: Open (size=50, cost=137, time=0.679274, max=0.189856, total=8.35536, pending=34)
[00100]: Open (size=36, cost=141, time=1.04383, max=0.807463, total=8.43941, pending=34)
[00000]: Open (size=36, cost=141, time=1.01066, max=0.807463, total=8.51491, pending=35)
[01100]: Open (size=36, cost=141, time=1.08815, max=0.807463, total=8.59191, pending=36)
[00010]: Open (size=36, cost=144, time=1.03339, max=0.807463, total=8.67607, pending=37)
[01001]: Open (size=36, cost=144, time=1.13371, max=0.807463, total=14.3163, pending=37)
[0101]: Open (size=37, cost=145, time=0.957939, max=0.807463, total=14.4413, pending=38)
[01011]: Open (size=36, cost=144, time=0.985651, max=0.807463, total=14.4935, pending=39)
[1011]: Open (size=39, cost=149, time=0.386104, max=0.225991, total=14.5193, pending=40)
[1001]: Open (size=39, cost=149, time=0.373554, max=0.200094, total=14.567, pending=40)
[01000]: Open (size=36, cost=149, time=1.1342, max=0.807463, total=14.6392, pending=40)
[1111]: Open (size=39, cost=149, time=0.287901, max=0.18188, total=14.7292, pending=41)
[111001]: Open (size=50, cost=154, time=0.805643, max=0.262475, total=14.7803, pending=41)
[10000]: Open (size=42, cost=160, time=0.513778, max=0.172604, total=24.9594, pending=41)
[100001]: Open (size=50, cost=124, time=0.548726, max=0.172604, total=25.0372, pending=42)
[00110]: Open (size=36, cost=160, time=1.11183, max=0.807463, total=25.2155, pending=42)
[01110]: Open (size=36, cost=160, time=1.04013, max=0.807463, total=30.9232, pending=42)
[101001]: Open (size=59, cost=163, time=0.758159, max=0.189856, total=31.7152, pending=43)
[101000]: Open (size=50, cost=164, time=0.628824, max=0.189856, total=37.4379, pending=43)
[100000]: Open (size=50, cost=167, time=0.551278, max=0.172604, total=37.4781, pending=43)
[000110]: Open (size=36, cost=168, time=1.77248, max=0.807463, total=43.5788, pending=44)
[000010]: Open (size=36, cost=168, time=1.1754, max=0.807463, total=53.4714, pending=44)
[1101]: Open (size=39, cost=177, time=0.158574, max=0.0899072, total=53.6962, pending=45)
[1001]: Open (size=41, cost=179, time=0.443493, max=0.200094, total=53.7317, pending=45)
[1111]: Open (size=41, cost=179, time=0.336284, max=0.18188, total=59.4696, pending=45)
[100001]: Open (size=70, cost=183, time=0.610949, max=0.172604, total=65.1771, pending=45)
[011110]: Open (size=36, cost=184, time=1.24473, max=0.807463, total=75.7056, pending=45)
[0111101]: Open (size=48, cost=161, time=1.47259, max=0.807463, total=76.5555, pending=46)
[01010]: Open (size=36, cost=184, time=0.981517, max=0.807463, total=96.6558, pending=46)
[011010]: Open (size=36, cost=184, time=1.0859, max=0.807463, total=96.6797, pending=47)
[0110101]: Open (size=48, cost=161, time=1.13937, max=0.807463, total=96.8238, pending=48)
[01101011]: Open (size=71, cost=146, time=1.25378, max=0.807463, total=96.9729, pending=49)
[01101010]: Open (size=71, cost=147, time=1.20464, max=0.807463, total=97.0531, pending=49)
[01101011]: Open (size=70, cost=165, time=1.32993, max=0.807463, total=97.0851, pending=49)
[01101010]: Open (size=70, cost=169, time=1.2327, max=0.807463, total=120.881, pending=49)
[011010101]: Open (size=88, cost=143, time=1.36841, max=0.807463, total=123.122, pending=50)
[011010100]: Open (size=88, cost=165, time=3.4094, max=2.09451, total=128.872, pending=50)
[001010]: Open (size=36, cost=184, time=1.07912, max=0.807463, total=136.288, pending=50)
[0010101]: Open (size=50, cost=182, time=1.13123, max=0.807463, total=136.453, pending=51)
[001110]: Open (size=36, cost=184, time=1.17902, max=0.807463, total=142.224, pending=51)
[0011101]: Open (size=50, cost=182, time=1.36066, max=0.807463, total=146.419, pending=52)
[11000]: Open (size=42, cost=188, time=0.373329, max=0.150178, total=152.259, pending=52)
[110000]: Open (size=58, cost=169, time=0.420096, max=0.150178, total=152.339, pending=53)
[1100001]: Open (size=58, cost=162, time=0.482395, max=0.150178, total=152.436, pending=54)
[1100000]: Open (size=58, cost=177, time=0.451096, max=0.150178, total=158.076, pending=54)
[000000]: Open (size=36, cost=189, time=1.05463, max=0.807463, total=174.727, pending=54)
[0000001]: Open (size=42, cost=132, time=1.07116, max=0.807463, total=174.767, pending=55)
[00000011]: Open (size=50, cost=152, time=1.09874, max=0.807463, total=174.821, pending=56)
[000000111]: Open (size=56, cost=134, time=1.14201, max=0.807463, total=174.893, pending=57)
******* COMPLETION *******
b(d(a(d(X0)))) -> b(c(X0))
d(d(X0)) -> b(a(c(X0)))
b(d(c(X0))) -> b(c(X0))
d(b(X0)) -> b(d(X0))
c(b(X0)) -> b(c(X0))
c(d(X0)) -> d(c(X0))
b(b(X0)) -> b(c(X0))
c(c(X0)) -> b(X0)
a(a(X0)) -> d(c(X0))
a(b(X0)) -> b(c(X0))
b(c(a(X0))) -> b(c(X0))
b(d(a(c(X0)))) -> b(c(X0))
a(d(c(X0))) -> d(c(a(X0)))
d(c(a(c(X0)))) -> b(c(X0))
d(c(a(d(X0)))) -> b(c(X0))
**************************
On branch: [000000111]
With size, cost: 102, 111
Orientations: 232
Calls to AProVE (all, T, NT, ?): 207, 173, 7, 27
Time (all, branch, AProVE): 203.691, 1.47509, 203.264
Time/call in AProVE (Avg, Min, Max): 0.98195, 16.6021, 0.00799012
Time/T-call in AProVE (Avg, Min, Max): 0.172751, 3.74253, 0.807463
All conjectures solved.