[]: Open (size=68, cost=0, time=0, max=0, total=1.00136e-05, pending=1)
[0]: Open (size=68, cost=68, time=0.962976, max=0.764061, total=0.997412, pending=1)
[00]: Open (size=68, cost=68, time=1.0859, max=0.764061, total=1.16605, pending=2)
[1]: Open (size=68, cost=73, time=0.94552, max=0.764061, total=1.30133, pending=2)
[01]: Open (size=68, cost=84, time=1.06921, max=0.764061, total=1.37659, pending=2)
[1]: Open (size=68, cost=89, time=1.01999, max=0.764061, total=1.43465, pending=2)
[10]: Open (size=68, cost=105, time=1.05468, max=0.764061, total=1.54803, pending=3)
[11]: Open (size=68, cost=105, time=1.09742, max=0.764061, total=1.60682, pending=3)
[00]: Open (size=68, cost=140, time=1.21927, max=0.764061, total=1.66279, pending=3)
[01]: Open (size=68, cost=156, time=1.12537, max=0.764061, total=2.01461, pending=4)
[000]: Open (size=68, cost=168, time=1.31582, max=0.764061, total=2.17533, pending=5)
[11]: Open (size=68, cost=177, time=1.15121, max=0.764061, total=2.38366, pending=6)
[10]: Open (size=68, cost=177, time=1.11133, max=0.764061, total=2.51862, pending=7)
[0000]: Open (size=68, cost=196, time=1.38013, max=0.764061, total=2.70498, pending=8)
[011]: Open (size=68, cost=204, time=1.21251, max=0.764061, total=2.86349, pending=8)
[111]: Open (size=68, cost=205, time=1.21672, max=0.764061, total=3.04419, pending=9)
[010]: Open (size=68, cost=212, time=1.19601, max=0.764061, total=3.2599, pending=10)
[0001]: Open (size=68, cost=214, time=1.45626, max=0.764061, total=3.42207, pending=11)
[00011]: Open (size=117, cost=180, time=1.60898, max=0.764061, total=4.24893, pending=12)
[001]: Open (size=68, cost=216, time=1.47169, max=0.764061, total=4.92771, pending=13)
[000111]: Open (size=117, cost=216, time=1.70265, max=0.764061, total=5.23244, pending=14)
[100]: Open (size=68, cost=225, time=1.23207, max=0.764061, total=10.8045, pending=14)
[101]: Open (size=68, cost=233, time=1.17374, max=0.764061, total=10.9525, pending=15)
[0111]: Open (size=68, cost=250, time=1.32562, max=0.764061, total=11.2325, pending=16)
[01110]: Open (size=110, cost=245, time=1.5412, max=0.764061, total=11.5995, pending=17)
[011100]: Open (size=102, cost=241, time=1.68524, max=0.764061, total=11.9477, pending=18)
[1111]: Open (size=68, cost=251, time=1.30053, max=0.764061, total=12.1881, pending=18)
[11111]: Open (size=122, cost=183, time=1.51858, max=0.764061, total=12.4533, pending=19)
[111111]: Open (size=114, cost=199, time=1.65788, max=0.764061, total=12.6254, pending=20)
[111110]: Open (size=114, cost=207, time=1.58709, max=0.764061, total=12.6687, pending=20)
[11110]: Open (size=108, cost=246, time=1.52534, max=0.764061, total=12.7409, pending=20)
[111100]: Open (size=98, cost=240, time=1.60354, max=0.764061, total=12.8452, pending=21)
[110]: Open (size=68, cost=253, time=1.21739, max=0.764061, total=12.9208, pending=21)
[0101]: Open (size=68, cost=258, time=1.28854, max=0.764061, total=13.0344, pending=22)
[111100]: Open (size=114, cost=260, time=1.67373, max=0.764061, total=13.4284, pending=23)
[011100]: Open (size=118, cost=261, time=1.92101, max=0.764061, total=13.4836, pending=23)
[0011]: Open (size=68, cost=262, time=1.65198, max=0.764061, total=13.5684, pending=23)
[00110]: Open (size=104, cost=223, time=1.69657, max=0.764061, total=13.7639, pending=24)
[001101]: Open (size=82, cost=259, time=1.75402, max=0.764061, total=14.1773, pending=25)
[111100]: Open (size=213, cost=268, time=1.72428, max=0.764061, total=14.4658, pending=26)
[00111]: Open (size=104, cost=269, time=1.79426, max=0.764061, total=19.9216, pending=26)
[1001]: Open (size=68, cost=271, time=1.34374, max=0.764061, total=20.832, pending=27)
[1000]: Open (size=68, cost=271, time=1.26399, max=0.764061, total=20.972, pending=27)
[01011]: Open (size=92, cost=271, time=1.41021, max=0.764061, total=21.087, pending=27)
[0100]: Open (size=68, cost=272, time=1.26203, max=0.764061, total=21.2077, pending=27)
[01011]: Open (size=191, cost=272, time=1.52283, max=0.764061, total=21.3297, pending=27)
[011101]: Open (size=102, cost=275, time=1.74119, max=0.764061, total=21.7012, pending=28)
[01111]: Open (size=110, cost=275, time=1.59694, max=0.764061, total=27.0201, pending=28)
[0010]: Open (size=68, cost=276, time=1.59203, max=0.764061, total=27.4083, pending=29)
[0011010]: Open (size=96, cost=277, time=1.84493, max=0.764061, total=27.506, pending=29)
[1011]: Open (size=68, cost=279, time=1.34573, max=0.764061, total=28.0027, pending=30)
[10110]: Open (size=136, cost=197, time=1.54504, max=0.764061, total=28.2679, pending=31)
[101101]: Open (size=128, cost=213, time=1.65395, max=0.764061, total=28.412, pending=32)
[101100]: Open (size=128, cost=221, time=1.63322, max=0.764061, total=28.5806, pending=32)
[10111]: Open (size=122, cost=248, time=1.4875, max=0.764061, total=28.7126, pending=32)
[011100]: Open (size=217, cost=282, time=2.00241, max=0.764061, total=28.9225, pending=33)
[010111]: Open (size=151, cost=288, time=1.55453, max=0.764061, total=34.2212, pending=33)
[001100]: Open (size=82, cost=291, time=2.04939, max=0.764061, total=39.5184, pending=33)
[011110]: Open (size=100, cost=293, time=1.62203, max=0.764061, total=45.1812, pending=33)
[0111100]: Open (size=124, cost=293, time=1.75325, max=0.764061, total=46.1214, pending=34)
[00110101]: Open (size=155, cost=294, time=1.95637, max=0.764061, total=46.2088, pending=34)
[011101]: Open (size=118, cost=295, time=1.77525, max=0.764061, total=51.6913, pending=34)
[0110]: Open (size=68, cost=296, time=1.27601, max=0.764061, total=51.7645, pending=34)
[101111]: Open (size=100, cost=296, time=1.50849, max=0.764061, total=51.8357, pending=34)
[011101]: Open (size=217, cost=296, time=1.84334, max=0.764061, total=57.2777, pending=34)
[1101]: Open (size=68, cost=299, time=1.30163, max=0.764061, total=62.6997, pending=34)
[0111100]: Open (size=239, cost=301, time=1.83656, max=0.764061, total=62.7479, pending=34)
[1001]: Open (size=76, cost=302, time=1.47003, max=0.764061, total=68.1133, pending=34)
[10011]: Open (size=110, cost=265, time=1.51327, max=0.764061, total=68.1874, pending=35)
[100110]: Open (size=136, cost=203, time=1.53486, max=0.764061, total=68.2381, pending=36)
[100111]: Open (size=118, cost=237, time=1.53948, max=0.764061, total=70.6053, pending=36)
[1001111]: Open (size=143, cost=211, time=1.58454, max=0.764061, total=70.8894, pending=37)
[10011111]: Open (size=143, cost=247, time=1.68624, max=0.764061, total=71.1989, pending=38)
[1101]: Open (size=76, cost=306, time=1.34045, max=0.764061, total=76.4355, pending=38)
[11011]: Open (size=110, cost=267, time=1.3591, max=0.764061, total=76.4974, pending=39)
[110111]: Open (size=138, cost=205, time=1.3972, max=0.764061, total=76.5679, pending=40)
[110110]: Open (size=120, cost=251, time=1.38866, max=0.764061, total=78.6583, pending=40)
[1101101]: Open (size=98, cost=287, time=1.40591, max=0.764061, total=78.9454, pending=41)
[11011010]: Open (size=110, cost=303, time=1.4506, max=0.764061, total=79.062, pending=42)
[0000]: Open (size=77, cost=306, time=1.52636, max=0.764061, total=84.2496, pending=42)
[1010]: Open (size=68, cost=311, time=1.2774, max=0.764061, total=84.2871, pending=42)
[01010]: Open (size=92, cost=311, time=1.63098, max=0.764061, total=84.3331, pending=42)
[100110]: Open (size=136, cost=313, time=1.65424, max=0.764061, total=85.193, pending=43)
[1001100]: Open (size=138, cost=223, time=1.68096, max=0.764061, total=85.2688, pending=44)
[10011001]: Open (size=130, cost=291, time=1.7306, max=0.764061, total=85.3751, pending=45)
[1110]: Open (size=68, cost=315, time=1.34442, max=0.764061, total=85.6239, pending=45)
[1010]: Open (size=86, cost=316, time=1.31085, max=0.764061, total=85.6549, pending=45)
[1000]: Open (size=86, cost=316, time=1.36755, max=0.764061, total=85.7397, pending=45)
******* COMPLETION *******
g(X1,X0) -> X1
cons(X0,nil) -> X0
cdr(nil) -> nil
f(X0,nil) -> nil
**************************
On branch: [1000]
With size, cost: 15, 63
Orientations: 248
Calls to AProVE (all, T, NT, ?): 183, 169, 2, 12
Time (all, branch, AProVE): 85.8192, 1.43776, 85.1045
Time/call in AProVE (Avg, Min, Max): 0.465052, 5.36039, 0.0164311
Time/T-call in AProVE (Avg, Min, Max): 0.108937, 0.796633, 0.764061
All conjectures solved.