[]: Open (size=26, cost=0, time=0, max=0, total=8.82149e-06, pending=1)
[0]: Open (size=26, cost=26, time=0.738009, max=0.612318, total=0.766563, pending=1)
[00]: Open (size=26, cost=40, time=0.775681, max=0.612318, total=0.842203, pending=2)
[1]: Open (size=26, cost=70, time=0.727591, max=0.612318, total=0.899913, pending=2)
[01]: Open (size=26, cost=96, time=0.774942, max=0.612318, total=0.963824, pending=3)
[00]: Open (size=57, cost=103, time=0.832245, max=0.612318, total=1.06256, pending=3)
[10]: Open (size=26, cost=146, time=0.763613, max=0.612318, total=1.32704, pending=3)
[101]: Open (size=56, cost=68, time=0.783793, max=0.612318, total=1.37024, pending=4)
[100]: Open (size=54, cost=92, time=0.784656, max=0.612318, total=1.54125, pending=4)
[101]: Open (size=41, cost=133, time=0.951913, max=0.612318, total=1.68121, pending=4)
[100]: Open (size=101, cost=155, time=0.922784, max=0.612318, total=1.73453, pending=4)
[11]: Open (size=26, cost=158, time=0.754203, max=0.612318, total=1.79602, pending=5)
[111]: Open (size=56, cost=76, time=0.772967, max=0.612318, total=1.85122, pending=6)
[110]: Open (size=54, cost=98, time=0.788661, max=0.612318, total=1.91446, pending=6)
[111]: Open (size=41, cost=121, time=0.834427, max=0.612318, total=1.97947, pending=6)
[110]: Open (size=107, cost=128, time=0.851523, max=0.612318, total=2.01041, pending=6)
[111]: Open (size=41, cost=137, time=0.863557, max=0.612318, total=2.03205, pending=6)
[01]: Open (size=85, cost=170, time=0.870863, max=0.612318, total=2.18473, pending=6)
[101]: Open (size=99, cost=177, time=1.00209, max=0.612318, total=2.29332, pending=6)
[1001]: Open (size=91, cost=191, time=0.952126, max=0.612318, total=2.49558, pending=7)
[10010]: Open (size=90, cost=195, time=1.0513, max=0.612318, total=2.6806, pending=8)
[1011]: Open (size=97, cost=197, time=1.10197, max=0.612318, total=2.9938, pending=8)
[110]: Open (size=106, cost=203, time=0.87175, max=0.612318, total=3.07844, pending=8)
[10010]: Open (size=104, cost=207, time=1.35585, max=0.612318, total=3.1413, pending=8)
[10011]: Open (size=90, cost=209, time=1.03511, max=0.612318, total=3.18479, pending=8)
[1010]: Open (size=97, cost=217, time=1.10287, max=0.612318, total=3.37487, pending=8)
[111]: Open (size=111, cost=225, time=1.01191, max=0.612318, total=3.42732, pending=8)
[10010]: Open (size=104, cost=238, time=1.39365, max=0.612318, total=3.49033, pending=8)
[1010]: Open (size=97, cost=261, time=1.15268, max=0.612318, total=3.56653, pending=8)
[10011]: Open (size=114, cost=270, time=1.21807, max=0.612318, total=3.61812, pending=8)
[1000]: Open (size=91, cost=301, time=0.953375, max=0.612318, total=3.66349, pending=8)
[10001]: Open (size=90, cost=291, time=0.97624, max=0.612318, total=3.72075, pending=9)
[10011]: Open (size=112, cost=301, time=1.25834, max=0.612318, total=3.74492, pending=9)
[01]: Open (size=85, cost=309, time=0.976021, max=0.612318, total=3.77548, pending=9)
[10001]: Open (size=114, cost=313, time=0.995861, max=0.612318, total=3.89311, pending=9)
[10000]: Open (size=90, cost=330, time=0.984249, max=0.612318, total=3.9174, pending=9)
[01]: Open (size=152, cost=330, time=1.07946, max=0.612318, total=3.95902, pending=9)
[1011]: Open (size=97, cost=337, time=1.18289, max=0.612318, total=3.9918, pending=9)
[00]: Open (size=72, cost=339, time=1.09165, max=0.612318, total=4.02007, pending=9)
[10011]: Open (size=112, cost=340, time=1.28209, max=0.612318, total=4.06386, pending=9)
[10000]: Open (size=114, cost=360, time=1.02071, max=0.612318, total=4.11034, pending=9)
[10001]: Open (size=114, cost=362, time=1.01571, max=0.612318, total=4.14606, pending=9)
[1011]: Open (size=129, cost=367, time=1.20603, max=0.612318, total=4.18486, pending=9)
[110]: Open (size=106, cost=377, time=0.931031, max=0.612318, total=4.24647, pending=9)
[00]: Open (size=129, cost=379, time=1.12525, max=0.612318, total=4.32276, pending=10)
[10000]: Open (size=114, cost=393, time=1.05153, max=0.612318, total=4.40555, pending=10)
[111]: Open (size=97, cost=401, time=1.07064, max=0.612318, total=4.43032, pending=10)
[1100]: Open (size=86, cost=401, time=0.973452, max=0.612318, total=4.56748, pending=11)
[1010]: Open (size=97, cost=417, time=1.19968, max=0.612318, total=4.61715, pending=11)
[1011]: Open (size=129, cost=427, time=1.25867, max=0.612318, total=4.69172, pending=11)
[1110]: Open (size=85, cost=427, time=1.16907, max=0.612318, total=4.71992, pending=11)
[10001]: Open (size=114, cost=448, time=1.04886, max=0.612318, total=4.81189, pending=11)
[1111]: Open (size=85, cost=453, time=1.10244, max=0.612318, total=4.83654, pending=11)
[10000]: Open (size=104, cost=456, time=1.07007, max=0.612318, total=4.86704, pending=11)
[00]: Open (size=94, cost=457, time=1.19093, max=0.612318, total=4.90401, pending=11)
[1111]: Open (size=85, cost=457, time=1.12514, max=0.612318, total=4.94371, pending=11)
[1010]: Open (size=91, cost=467, time=1.26374, max=0.612318, total=4.9785, pending=11)
[1100]: Open (size=141, cost=468, time=1.01571, max=0.612318, total=5.03997, pending=11)
[1110]: Open (size=137, cost=469, time=1.24673, max=0.612318, total=5.12182, pending=11)
[10000]: Open (size=104, cost=478, time=1.10005, max=0.612318, total=5.15749, pending=11)
[1100]: Open (size=161, cost=481, time=1.08069, max=0.612318, total=5.18976, pending=11)
[1101]: Open (size=86, cost=510, time=0.95143, max=0.612318, total=5.28159, pending=11)
[1111]: Open (size=115, cost=521, time=1.14841, max=0.612318, total=5.34992, pending=11)
[10001]: Open (size=112, cost=529, time=1.06688, max=0.612318, total=5.52551, pending=11)
[1011]: Open (size=129, cost=533, time=1.28027, max=0.612318, total=5.58561, pending=11)
[1100]: Open (size=141, cost=539, time=1.157, max=0.612318, total=5.68514, pending=11)
[11000]: Open (size=109, cost=406, time=1.24549, max=0.612318, total=5.83154, pending=12)
[11001]: Open (size=109, cost=462, time=1.22922, max=0.612318, total=5.98996, pending=12)
[1010]: Open (size=139, cost=541, time=1.30905, max=0.612318, total=6.17435, pending=12)
[10010]: Open (size=93, cost=558, time=1.45918, max=0.612318, total=6.26609, pending=12)
[10001]: Open (size=112, cost=559, time=1.11841, max=0.612318, total=6.40982, pending=12)
[1101]: Open (size=141, cost=561, time=1.01065, max=0.612318, total=6.46561, pending=12)
[1110]: Open (size=135, cost=563, time=1.27414, max=0.612318, total=6.49219, pending=12)
[10010]: Open (size=182, cost=571, time=1.56147, max=0.612318, total=6.52499, pending=12)
[1111]: Open (size=107, cost=573, time=1.29185, max=0.612318, total=6.57791, pending=12)
[1101]: Open (size=140, cost=573, time=1.02922, max=0.612318, total=6.61254, pending=12)
[1010]: Open (size=135, cost=597, time=1.37533, max=0.612318, total=6.71515, pending=12)
[1101]: Open (size=169, cost=605, time=1.0999, max=0.612318, total=6.77929, pending=12)
[10010]: Open (size=149, cost=613, time=1.59614, max=0.612318, total=6.81693, pending=12)
[100101]: Open (size=119, cost=220, time=1.61373, max=0.612318, total=6.86777, pending=13)
[1001010]: Open (size=96, cost=269, time=1.74216, max=0.612318, total=7.11868, pending=14)
[1001011]: Open (size=96, cost=375, time=1.78333, max=0.612318, total=7.24211, pending=14)
[10010110]: Open (size=86, cost=467, time=1.85453, max=0.612318, total=7.38043, pending=15)
[10010111]: Open (size=84, cost=487, time=1.83783, max=0.612318, total=7.55908, pending=15)
[1001010]: Open (size=54, cost=507, time=1.85662, max=0.612318, total=7.61182, pending=15)
[100100]: Open (size=103, cost=560, time=1.61399, max=0.612318, total=7.76679, pending=15)
[1001010]: Open (size=113, cost=570, time=1.98321, max=0.612318, total=7.8134, pending=15)
[1111]: Open (size=101, cost=625, time=1.31171, max=0.612318, total=7.86682, pending=15)
[1011]: Open (size=125, cost=629, time=1.3706, max=0.612318, total=7.91105, pending=15)
[00]: Open (size=109, cost=637, time=1.2131, max=0.612318, total=7.93797, pending=15)
[1111]: Open (size=115, cost=643, time=1.33181, max=0.612318, total=7.97288, pending=15)
[11111]: Open (size=97, cost=257, time=1.38034, max=0.612318, total=8.05432, pending=16)
[111111]: Open (size=79, cost=317, time=1.48881, max=0.612318, total=8.21359, pending=17)
[111110]: Open (size=79, cost=373, time=1.48508, max=0.612318, total=8.27595, pending=17)
[11110]: Open (size=77, cost=443, time=1.37953, max=0.612318, total=8.44116, pending=17)
[111111]: Open (size=235, cost=513, time=1.5351, max=0.612318, total=8.62889, pending=17)
[11110]: Open (size=81, cost=559, time=1.52664, max=0.612318, total=8.67383, pending=17)
[01]: Open (size=140, cost=656, time=1.09862, max=0.612318, total=8.79726, pending=17)
[1110]: Open (size=119, cost=661, time=1.29737, max=0.612318, total=8.83425, pending=17)
[1011]: Open (size=125, cost=665, time=1.38748, max=0.612318, total=8.8662, pending=17)
[10011]: Open (size=101, cost=670, time=1.31545, max=0.612318, total=8.89946, pending=17)
[11001]: Open (size=152, cost=695, time=1.35916, max=0.612318, total=9.10163, pending=17)
[10011]: Open (size=173, cost=703, time=1.46399, max=0.612318, total=9.16277, pending=17)
[11110]: Open (size=157, cost=709, time=1.62619, max=0.612318, total=9.20019, pending=17)
[11000]: Open (size=132, cost=723, time=1.38077, max=0.612318, total=9.258, pending=17)
[1001010]: Open (size=111, cost=730, time=2.0118, max=0.612318, total=9.32126, pending=17)
[00]: Open (size=198, cost=731, time=1.22765, max=0.612318, total=9.3992, pending=17)
[111111]: Open (size=175, cost=753, time=1.56864, max=0.612318, total=9.443, pending=17)
[111110]: Open (size=65, cost=773, time=1.61598, max=0.612318, total=9.5054, pending=17)
[10011]: Open (size=159, cost=797, time=1.48144, max=0.612318, total=9.68777, pending=17)
[100111]: Open (size=145, cost=262, time=1.52119, max=0.612318, total=9.767, pending=18)
[1001111]: Open (size=96, cost=258, time=1.60282, max=0.612318, total=9.87076, pending=19)
[1001110]: Open (size=96, cost=387, time=1.57809, max=0.612318, total=9.90468, pending=19)
[10011100]: Open (size=98, cost=491, time=1.59425, max=0.612318, total=9.96291, pending=20)
[1001111]: Open (size=54, cost=496, time=1.62876, max=0.612318, total=10.0247, pending=20)
[10011101]: Open (size=98, cost=590, time=1.60667, max=0.612318, total=10.2116, pending=20)
[100110]: Open (size=127, cost=742, time=1.49637, max=0.612318, total=10.2889, pending=20)
[1001111]: Open (size=111, cost=746, time=1.77394, max=0.612318, total=10.3369, pending=20)
[10000]: Open (size=93, cost=799, time=1.11877, max=0.612318, total=10.4039, pending=20)
[100001]: Open (size=118, cost=212, time=1.20023, max=0.612318, total=10.5633, pending=21)
[1000010]: Open (size=97, cost=236, time=1.31658, max=0.612318, total=10.7107, pending=22)
[1000011]: Open (size=97, cost=340, time=1.31317, max=0.612318, total=10.74, pending=22)
[10000110]: Open (size=84, cost=420, time=1.33166, max=0.612318, total=10.8101, pending=23)
[10000111]: Open (size=86, cost=431, time=1.3542, max=0.612318, total=10.8529, pending=23)
[1000010]: Open (size=54, cost=473, time=1.33866, max=0.612318, total=10.914, pending=23)
[100000]: Open (size=103, cost=577, time=1.19825, max=0.612318, total=11.0839, pending=23)
[1000010]: Open (size=111, cost=723, time=1.47225, max=0.612318, total=11.1176, pending=23)
[100000]: Open (size=203, cost=723, time=1.21378, max=0.612318, total=11.1767, pending=23)
[1000000]: Open (size=125, cost=778, time=1.72346, max=0.612318, total=11.7417, pending=24)
[11110]: Open (size=225, cost=817, time=1.65611, max=0.612318, total=12.0638, pending=24)
[10000110]: Open (size=77, cost=818, time=1.35707, max=0.612318, total=12.1144, pending=24)
[1110]: Open (size=103, cost=843, time=1.31547, max=0.612318, total=12.1773, pending=24)
[111110]: Open (size=299, cost=859, time=1.72603, max=0.612318, total=12.2296, pending=24)
[1110]: Open (size=121, cost=873, time=1.33918, max=0.612318, total=12.2871, pending=24)
[11101]: Open (size=129, cost=299, time=1.3958, max=0.612318, total=12.3905, pending=25)
[111010]: Open (size=123, cost=479, time=1.54196, max=0.612318, total=12.5892, pending=26)
[111011]: Open (size=123, cost=591, time=1.53872, max=0.612318, total=12.6339, pending=26)
[111010]: Open (size=123, cost=689, time=1.57239, max=0.612318, total=12.6987, pending=26)
[11100]: Open (size=97, cost=691, time=1.39966, max=0.612318, total=12.9338, pending=26)
[111010]: Open (size=169, cost=771, time=1.75861, max=0.612318, total=12.9791, pending=26)
[11100]: Open (size=97, cost=789, time=1.42807, max=0.612318, total=13.0485, pending=26)
[1010]: Open (size=115, cost=875, time=1.41838, max=0.612318, total=13.3316, pending=26)
[10101]: Open (size=209, cost=361, time=1.60112, max=0.612318, total=13.6016, pending=27)
[101011]: Open (size=177, cost=503, time=1.72323, max=0.612318, total=13.7795, pending=28)
[101010]: Open (size=177, cost=685, time=1.71638, max=0.612318, total=13.8311, pending=28)
[101011]: Open (size=91, cost=767, time=1.75095, max=0.612318, total=13.9875, pending=28)
[10100]: Open (size=177, cost=823, time=1.59958, max=0.612318, total=14.0675, pending=28)
[101000]: Open (size=127, cost=767, time=1.93132, max=0.612318, total=14.5245, pending=29)
[101010]: Open (size=129, cost=873, time=1.80517, max=0.612318, total=15.4712, pending=29)
[10000111]: Open (size=86, cost=877, time=1.39187, max=0.612318, total=15.8169, pending=29)
[1101]: Open (size=150, cost=899, time=1.11848, max=0.612318, total=15.8962, pending=29)
[10010111]: Open (size=77, cost=903, time=1.86842, max=0.612318, total=15.942, pending=29)
[1000010]: Open (size=231, cost=904, time=1.49611, max=0.612318, total=16.0141, pending=29)
[100100]: Open (size=136, cost=904, time=1.6299, max=0.612318, total=16.0669, pending=29)
[1001010]: Open (size=231, cost=911, time=2.0494, max=0.612318, total=16.1219, pending=29)
[10000110]: Open (size=100, cost=913, time=1.38361, max=0.612318, total=16.176, pending=29)
[10001]: Open (size=101, cost=916, time=1.15798, max=0.612318, total=16.2392, pending=29)
[1101]: Open (size=142, cost=917, time=1.13489, max=0.612318, total=16.3598, pending=29)
[11011]: Open (size=134, cost=281, time=1.16787, max=0.612318, total=16.4308, pending=30)
[110111]: Open (size=104, cost=426, time=1.28544, max=0.612318, total=16.5798, pending=31)
[110110]: Open (size=104, cost=530, time=1.27347, max=0.612318, total=16.7401, pending=31)
[11010]: Open (size=116, cost=742, time=1.1705, max=0.612318, total=16.787, pending=31)
[110111]: Open (size=153, cost=779, time=1.40634, max=0.612318, total=16.8258, pending=31)
[1101111]: Open (size=137, cost=579, time=1.46107, max=0.612318, total=16.922, pending=32)
******* COMPLETION *******
div(i(Y0),div(Y15,div(Y0,X11))) -> div(i(X11),Y15)
div(X3,div(Y15,div(i(X3),X5))) -> div(i(X5),Y15)
div(div(X5,Y0),Y3) -> div(X5,div(Y3,i(Y0)))
div(i(Y0),div(X11,Y0)) -> i(X11)
i(div(X5,Y6)) -> div(Y6,X5)
div(X3,div(X5,i(X3))) -> i(X5)
times(X1,Y0) -> div(X1,i(Y0))
div(Y0,one) -> Y0
i(one) -> one
div(Y0,Y0) -> one
i(i(Y0)) -> Y0
div(one,Y1) -> i(Y1)
**************************
On branch: [1101111]
With size, cost: 85, 334
Orientations: 588
Calls to AProVE (all, T, NT, ?): 326, 326, 0, 0
Time (all, branch, AProVE): 18.8594, 3.28544, 15.1302
Time/call in AProVE (Avg, Min, Max): 0.0464116, 0.612135, 0.0119421
Time/T-call in AProVE (Avg, Min, Max): 0.0464116, 0.612135, 0.612318
All conjectures solved.