[]: Open (size=23, cost=0, time=0, max=0, total=8.10623e-06, pending=1)
[0]: Open (size=23, cost=23, time=0.690166, max=0.690166, total=0.708903, pending=1)
[1]: Open (size=23, cost=23, time=0.0185699, max=0.0185699, total=0.728535, pending=1)
[0]: Open (size=23, cost=23, time=0.709602, max=0.690166, total=0.758001, pending=1)
[1]: Open (size=25, cost=25, time=0.0478258, max=0.0292559, total=0.841274, pending=2)
[10]: Open (size=27, cost=47, time=0.137487, max=0.0481069, total=0.971485, pending=3)
[00]: Open (size=23, cost=49, time=0.769196, max=0.690166, total=1.07056, pending=3)
[10]: Open (size=48, cost=104, time=0.234612, max=0.0506101, total=1.15982, pending=3)
[100]: Open (size=80, cost=100, time=0.302196, max=0.0675838, total=1.26898, pending=4)
[01]: Open (size=23, cost=109, time=0.768023, max=0.690166, total=1.3925, pending=4)
[010]: Open (size=90, cost=100, time=0.855141, max=0.690166, total=1.51175, pending=5)
[11]: Open (size=27, cost=113, time=0.128954, max=0.041554, total=1.61187, pending=5)
[011]: Open (size=92, cost=114, time=0.844597, max=0.690166, total=1.76595, pending=5)
[101]: Open (size=79, cost=117, time=0.275442, max=0.0506101, total=1.80953, pending=5)
[00]: Open (size=60, cost=125, time=0.856749, max=0.690166, total=1.84765, pending=5)
[001]: Open (size=89, cost=108, time=0.923007, max=0.690166, total=1.94204, pending=6)
[000]: Open (size=95, cost=111, time=0.91973, max=0.690166, total=1.99149, pending=6)
[001]: Open (size=89, cost=123, time=0.97154, max=0.690166, total=2.06403, pending=6)
[000]: Open (size=95, cost=126, time=0.991466, max=0.690166, total=2.11136, pending=7)
[0010]: Open (size=90, cost=131, time=0.993828, max=0.690166, total=2.15301, pending=7)
[000]: Open (size=95, cost=133, time=1.03188, max=0.690166, total=2.26766, pending=7)
[100]: Open (size=80, cost=134, time=0.424244, max=0.071923, total=2.47148, pending=7)
[0010]: Open (size=90, cost=135, time=1.10658, max=0.690166, total=2.57607, pending=7)
[101]: Open (size=79, cost=137, time=0.312577, max=0.0506101, total=2.80032, pending=7)
[0011]: Open (size=88, cost=142, time=0.995189, max=0.690166, total=2.90683, pending=7)
[000]: Open (size=82, cost=165, time=1.23337, max=0.690166, total=3.08317, pending=7)
[0001]: Open (size=94, cost=159, time=1.30725, max=0.690166, total=3.20211, pending=8)
[0000]: Open (size=82, cost=172, time=1.27656, max=0.690166, total=3.36678, pending=8)
[100]: Open (size=78, cost=176, time=0.526425, max=0.102181, total=3.46381, pending=8)
[0010]: Open (size=86, cost=179, time=1.32694, max=0.690166, total=3.50499, pending=8)
[101]: Open (size=77, cost=183, time=0.416953, max=0.104376, total=3.83361, pending=8)
[0010]: Open (size=88, cost=184, time=1.37354, max=0.690166, total=3.85954, pending=8)
[00100]: Open (size=88, cost=174, time=1.42056, max=0.690166, total=3.92838, pending=9)
[00101]: Open (size=100, cost=175, time=1.39286, max=0.690166, total=3.96759, pending=9)
[0011]: Open (size=84, cost=185, time=1.1678, max=0.690166, total=4.00527, pending=9)
[0001]: Open (size=94, cost=186, time=1.46888, max=0.690166, total=4.04114, pending=9)
[11]: Open (size=84, cost=187, time=0.279258, max=0.0956321, total=4.12806, pending=9)
[00101]: Open (size=93, cost=195, time=1.42784, max=0.690166, total=4.26956, pending=9)
[0001]: Open (size=94, cost=222, time=1.55178, max=0.690166, total=4.33667, pending=9)
[00101]: Open (size=85, cost=223, time=1.4907, max=0.690166, total=4.38955, pending=9)
[010]: Open (size=90, cost=245, time=0.952201, max=0.690166, total=4.47843, pending=9)
[011]: Open (size=92, cost=337, time=0.886117, max=0.690166, total=4.51514, pending=9)
[010]: Open (size=90, cost=355, time=0.979336, max=0.690166, total=4.54626, pending=9)
[0101]: Open (size=111, cost=325, time=1.06374, max=0.690166, total=4.67952, pending=10)
[0100]: Open (size=105, cost=357, time=1.05478, max=0.690166, total=4.74855, pending=10)
[01001]: Open (size=92, cost=351, time=1.06976, max=0.690166, total=4.80222, pending=11)
[01000]: Open (size=91, cost=367, time=1.07758, max=0.690166, total=4.89056, pending=12)
[0101]: Open (size=105, cost=377, time=1.11811, max=0.690166, total=6.43254, pending=13)
[010010]: Open (size=92, cost=391, time=1.10199, max=0.690166, total=6.57768, pending=13)
[0000]: Open (size=80, cost=399, time=1.36589, max=0.690166, total=7.10148, pending=14)
[11]: Open (size=84, cost=400, time=0.415973, max=0.136715, total=7.35012, pending=14)
[0101]: Open (size=95, cost=407, time=1.22708, max=0.690166, total=7.55009, pending=15)
[00100]: Open (size=80, cost=409, time=1.45236, max=0.690166, total=7.76028, pending=15)
[010000]: Open (size=91, cost=411, time=1.22217, max=0.690166, total=7.84166, pending=15)
[0000]: Open (size=134, cost=412, time=1.56429, max=0.690166, total=8.31435, pending=16)
[00100]: Open (size=134, cost=422, time=1.50911, max=0.690166, total=8.54374, pending=16)
[0011]: Open (size=82, cost=428, time=1.19707, max=0.690166, total=8.62826, pending=16)
[00110]: Open (size=124, cost=420, time=1.22576, max=0.690166, total=8.68771, pending=17)
[001100]: Open (size=91, cost=352, time=1.36229, max=0.690166, total=8.96477, pending=18)
[001101]: Open (size=86, cost=371, time=1.35656, max=0.690166, total=9.03399, pending=19)
[0011000]: Open (size=86, cost=391, time=1.40758, max=0.690166, total=9.068, pending=19)
[0011001]: Open (size=98, cost=398, time=1.399, max=0.690166, total=9.13451, pending=19)
[101]: Open (size=77, cost=436, time=0.437398, max=0.104376, total=9.33073, pending=19)
[1011]: Open (size=81, cost=384, time=0.587887, max=0.104376, total=9.59917, pending=20)
[00111]: Open (size=134, cost=438, time=1.22631, max=0.690166, total=9.92891, pending=20)
[111]: Open (size=122, cost=438, time=0.504361, max=0.136715, total=10.0348, pending=21)
[1110]: Open (size=79, cost=436, time=0.52929, max=0.136715, total=10.1714, pending=22)
[0011000]: Open (size=152, cost=449, time=1.4526, max=0.690166, total=10.2197, pending=22)
[0001]: Open (size=74, cost=451, time=1.59464, max=0.690166, total=10.2868, pending=22)
[0011001]: Open (size=151, cost=453, time=1.52792, max=0.690166, total=10.3618, pending=22)
[0100000]: Open (size=164, cost=455, time=1.39633, max=0.690166, total=10.3725, pending=22)
[001101]: Open (size=162, cost=460, time=1.37657, max=0.690166, total=10.6462, pending=23)
[01000000]: Open (size=113, cost=460, time=1.41655, max=0.690166, total=10.9381, pending=23)
[00101]: Open (size=74, cost=461, time=1.56128, max=0.690166, total=11.3026, pending=24)
[110]: Open (size=122, cost=461, time=0.518812, max=0.136715, total=11.4232, pending=24)
[1100]: Open (size=128, cost=452, time=0.535046, max=0.136715, total=11.4618, pending=25)
[1010]: Open (size=81, cost=462, time=0.548919, max=0.104376, total=11.581, pending=26)
[100]: Open (size=78, cost=463, time=0.56173, max=0.102181, total=11.6051, pending=26)
[0000]: Open (size=90, cost=465, time=1.7744, max=0.690166, total=11.7911, pending=26)
[1011]: Open (size=174, cost=469, time=0.668211, max=0.104376, total=11.8333, pending=26)
[010000000]: Open (size=113, cost=473, time=1.49025, max=0.690166, total=11.8603, pending=26)
[010011]: Open (size=98, cost=474, time=1.11232, max=0.690166, total=11.9163, pending=26)
[00100]: Open (size=90, cost=475, time=1.57033, max=0.690166, total=11.9609, pending=26)
[0100100]: Open (size=114, cost=475, time=1.19597, max=0.690166, total=11.9955, pending=26)
[001110]: Open (size=135, cost=476, time=1.26585, max=0.690166, total=12.045, pending=26)
[1010]: Open (size=81, cost=478, time=0.565304, max=0.104376, total=12.069, pending=26)
[0011000]: Open (size=90, cost=488, time=1.49916, max=0.690166, total=12.4431, pending=26)
[010011]: Open (size=98, cost=492, time=1.14132, max=0.690166, total=12.4811, pending=26)
[001110]: Open (size=137, cost=492, time=1.28247, max=0.690166, total=12.5265, pending=26)
[0011101]: Open (size=98, cost=444, time=1.33156, max=0.690166, total=12.6183, pending=27)
[0011100]: Open (size=101, cost=503, time=1.3277, max=0.690166, total=12.7602, pending=27)
[1011]: Open (size=174, cost=510, time=0.685649, max=0.104376, total=13.0641, pending=27)
[11001]: Open (size=96, cost=513, time=0.629971, max=0.136715, total=13.1407, pending=27)
[001111]: Open (size=132, cost=513, time=1.28564, max=0.690166, total=13.2331, pending=27)
[010000000]: Open (size=182, cost=515, time=1.51033, max=0.690166, total=13.2585, pending=27)
[0100000001]: Open (size=201, cost=463, time=1.53211, max=0.690166, total=13.3223, pending=28)
[010001]: Open (size=97, cost=518, time=2.49293, max=1.37469, total=13.4297, pending=29)
[0100101]: Open (size=113, cost=521, time=1.49186, max=0.690166, total=14.0115, pending=29)
[1010]: Open (size=174, cost=523, time=0.703558, max=0.104376, total=14.6333, pending=29)
[010011]: Open (size=98, cost=526, time=1.16753, max=0.690166, total=14.7065, pending=29)
[0100100]: Open (size=222, cost=529, time=1.22161, max=0.690166, total=14.7588, pending=29)
[1101]: Open (size=128, cost=529, time=0.533534, max=0.136715, total=14.8054, pending=29)
[001111]: Open (size=134, cost=529, time=1.30273, max=0.690166, total=14.8909, pending=29)
[0011111]: Open (size=98, cost=447, time=1.64371, max=0.690166, total=15.604, pending=30)
[0011110]: Open (size=101, cost=494, time=1.65923, max=0.690166, total=16.1446, pending=30)
[0011111]: Open (size=174, cost=501, time=1.86923, max=0.690166, total=16.5964, pending=30)
[0011110]: Open (size=140, cost=502, time=1.82804, max=0.690166, total=16.7463, pending=30)
[0011101]: Open (size=174, cost=531, time=1.39346, max=0.690166, total=17.2366, pending=30)
[0011111]: Open (size=174, cost=534, time=2.00045, max=0.690166, total=17.3187, pending=30)
[01000000010]: Open (size=186, cost=536, time=1.58497, max=0.690166, total=17.3985, pending=30)
[010000000100]: Open (size=172, cost=525, time=1.61045, max=0.690166, total=19.6802, pending=31)
[01000000011]: Open (size=186, cost=536, time=1.58908, max=0.690166, total=19.8221, pending=31)
[010000000110]: Open (size=170, cost=520, time=1.68385, max=0.690166, total=20.286, pending=32)
[010000000111]: Open (size=188, cost=532, time=1.93761, max=0.690166, total=26.0744, pending=32)
[001101]: Open (size=113, cost=538, time=1.6376, max=0.690166, total=26.5421, pending=32)
[010000000100]: Open (size=163, cost=538, time=1.70615, max=0.690166, total=26.6001, pending=32)
[01000001]: Open (size=115, cost=539, time=1.6164, max=0.690166, total=32.0372, pending=32)
[11000]: Open (size=94, cost=541, time=0.550729, max=0.136715, total=32.4054, pending=32)
[1110]: Open (size=79, cost=542, time=0.566974, max=0.136715, total=32.4694, pending=33)
[0100000000]: Open (size=180, cost=543, time=1.53115, max=0.690166, total=32.5718, pending=33)
[01000000000]: Open (size=145, cost=506, time=1.5749, max=0.690166, total=32.6885, pending=34)
[01000000001]: Open (size=148, cost=519, time=1.57233, max=0.690166, total=33.2683, pending=35)
[1101]: Open (size=128, cost=545, time=0.611827, max=0.136715, total=33.3566, pending=36)
[010000000100]: Open (size=118, cost=550, time=1.75507, max=0.690166, total=36.4249, pending=37)
[010000000110]: Open (size=118, cost=550, time=1.83859, max=0.690166, total=36.5128, pending=37)
[010000000111]: Open (size=188, cost=550, time=2.38729, max=0.690166, total=36.6057, pending=37)
[010000000000]: Open (size=141, cost=550, time=1.59462, max=0.690166, total=36.8797, pending=37)
[010000000010]: Open (size=138, cost=550, time=1.60262, max=0.690166, total=37.0346, pending=38)
[010001]: Open (size=97, cost=552, time=3.04144, max=1.37469, total=37.1785, pending=39)
[1111]: Open (size=77, cost=553, time=0.602949, max=0.136715, total=37.5055, pending=39)
[011]: Open (size=94, cost=554, time=0.912152, max=0.690166, total=37.962, pending=39)
[1011]: Open (size=127, cost=557, time=0.737068, max=0.104376, total=38.0078, pending=39)
[011]: Open (size=75, cost=557, time=0.950299, max=0.690166, total=38.0587, pending=39)
[0100001]: Open (size=188, cost=562, time=1.55504, max=0.690166, total=38.1882, pending=39)
[01000001]: Open (size=157, cost=565, time=1.76071, max=0.690166, total=38.3132, pending=39)
[010001]: Open (size=97, cost=570, time=3.34247, max=1.37469, total=38.9151, pending=39)
[1010]: Open (size=127, cost=570, time=0.745059, max=0.104376, total=39.5532, pending=39)
[110000]: Open (size=103, cost=571, time=0.573879, max=0.136715, total=39.6016, pending=39)
[0100000000000]: Open (size=162, cost=574, time=1.61389, max=0.690166, total=39.6385, pending=39)
[0011101]: Open (size=127, cost=578, time=1.44012, max=0.690166, total=39.7152, pending=39)
[010011]: Open (size=111, cost=579, time=1.18589, max=0.690166, total=39.7847, pending=39)
[0100101]: Open (size=255, cost=583, time=2.04147, max=0.690166, total=39.8712, pending=39)
[010000000110]: Open (size=131, cost=587, time=1.86599, max=0.690166, total=39.9777, pending=39)
[010000000100]: Open (size=131, cost=587, time=1.77833, max=0.690166, total=40.1045, pending=39)
[1111]: Open (size=229, cost=588, time=1.03504, max=0.269971, total=40.3145, pending=39)
[010011]: Open (size=209, cost=592, time=1.22479, max=0.690166, total=40.395, pending=39)
[010000000111]: Open (size=179, cost=600, time=2.63462, max=0.690166, total=40.5133, pending=39)
[010011]: Open (size=136, cost=600, time=1.29134, max=0.690166, total=41.6411, pending=40)
[11011]: Open (size=95, cost=603, time=3.64655, max=3.03472, total=41.69, pending=40)
[0100001]: Open (size=178, cost=614, time=1.66941, max=0.690166, total=43.783, pending=40)
[010001]: Open (size=153, cost=616, time=3.59931, max=1.37469, total=44.3122, pending=40)
[11001]: Open (size=96, cost=619, time=0.710915, max=0.136715, total=45.0453, pending=40)
[0100000001111]: Open (size=142, cost=620, time=3.02034, max=0.690166, total=45.4078, pending=40)
[01000000011110]: Open (size=142, cost=623, time=3.53607, max=0.690166, total=46.8486, pending=41)
[110000]: Open (size=209, cost=625, time=0.593264, max=0.136715, total=47.6268, pending=41)
[010000000101]: Open (size=188, cost=628, time=3.81387, max=2.2289, total=47.9363, pending=41)
[11010]: Open (size=94, cost=634, time=0.634994, max=0.136715, total=49.304, pending=41)
[0000]: Open (size=94, cost=634, time=1.79257, max=0.690166, total=49.339, pending=41)
[0100000000101]: Open (size=170, cost=635, time=1.67756, max=0.690166, total=49.3753, pending=41)
[0100001]: Open (size=149, cost=635, time=2.14711, max=0.690166, total=49.5547, pending=41)
[0100000000000]: Open (size=294, cost=636, time=1.63321, max=0.690166, total=55.1864, pending=42)
[010000000110]: Open (size=218, cost=640, time=1.92085, max=0.690166, total=55.3075, pending=42)
[00100]: Open (size=94, cost=644, time=1.58545, max=0.690166, total=55.5816, pending=42)
[0100101]: Open (size=242, cost=654, time=2.12601, max=0.690166, total=55.625, pending=42)
[0011111]: Open (size=127, cost=655, time=2.04752, max=0.690166, total=55.767, pending=42)
[110001]: Open (size=103, cost=656, time=0.575391, max=0.136715, total=55.846, pending=42)
[0100000001110]: Open (size=134, cost=656, time=3.34673, max=0.712112, total=55.895, pending=42)
[0011000]: Open (size=94, cost=657, time=1.51505, max=0.690166, total=57.0323, pending=42)
[110000]: Open (size=171, cost=659, time=0.70191, max=0.136715, total=57.0827, pending=42)
[11010]: Open (size=113, cost=666, time=0.65154, max=0.136715, total=57.1522, pending=42)
[0100000000100]: Open (size=173, cost=680, time=1.62172, max=0.690166, total=57.221, pending=43)
[01000001]: Open (size=234, cost=681, time=2.08051, max=0.690166, total=57.8242, pending=43)
[0100000000101]: Open (size=291, cost=686, time=1.7972, max=0.690166, total=58.0638, pending=43)
[0100100]: Open (size=220, cost=687, time=1.24129, max=0.690166, total=58.2437, pending=43)
[110101]: Open (size=103, cost=691, time=0.673434, max=0.136715, total=58.304, pending=43)
[0100000000100]: Open (size=202, cost=693, time=1.65116, max=0.690166, total=58.3488, pending=43)
[11011]: Open (size=95, cost=695, time=5.72242, max=3.03472, total=58.9769, pending=43)
[010000000011]: Open (size=150, cost=697, time=1.59033, max=0.690166, total=60.935, pending=43)
[01000000011111]: Open (size=148, cost=699, time=3.88876, max=0.86842, total=61.2832, pending=43)
[11011]: Open (size=188, cost=700, time=7.64999, max=3.03472, total=61.6568, pending=43)
[110100]: Open (size=103, cost=703, time=0.67282, max=0.136715, total=63.7924, pending=43)
[01000010]: Open (size=218, cost=713, time=2.44095, max=0.690166, total=63.9704, pending=43)
[010001]: Open (size=218, cost=719, time=4.26417, max=1.37469, total=69.3905, pending=43)
[0100000000001]: Open (size=165, cost=719, time=1.68114, max=0.690166, total=69.5463, pending=43)
[01000011]: Open (size=219, cost=721, time=7.13323, max=4.75562, total=70.0498, pending=43)
[110101]: Open (size=207, cost=723, time=0.696112, max=0.136715, total=80.3534, pending=43)
[0101]: Open (size=128, cost=724, time=1.37856, max=0.690166, total=80.6623, pending=43)
[010011]: Open (size=252, cost=724, time=1.30723, max=0.690166, total=80.7645, pending=43)
[010000001]: Open (size=123, cost=727, time=1.63798, max=0.690166, total=80.9456, pending=43)
[0100000000100]: Open (size=290, cost=728, time=1.70084, max=0.690166, total=81.0835, pending=43)
[010000000001]: Open (size=153, cost=730, time=2.08063, max=0.690166, total=81.214, pending=43)
[110100]: Open (size=111, cost=730, time=0.713942, max=0.136715, total=82.3539, pending=43)
[01000000011110]: Open (size=142, cost=738, time=4.25017, max=0.714098, total=82.4105, pending=43)
[0000]: Open (size=194, cost=739, time=1.80746, max=0.690166, total=83.1343, pending=43)
[0100101]: Open (size=207, cost=739, time=2.23707, max=0.690166, total=83.1876, pending=43)
[001101]: Open (size=128, cost=740, time=1.66602, max=0.690166, total=83.2858, pending=43)
[110001]: Open (size=103, cost=741, time=0.600598, max=0.136715, total=83.3308, pending=43)
[110100]: Open (size=238, cost=741, time=0.73658, max=0.136715, total=83.378, pending=43)
[0100000000001]: Open (size=205, cost=743, time=1.74514, max=0.690166, total=83.5468, pending=43)
[1011]: Open (size=127, cost=744, time=0.755867, max=0.104376, total=84.1437, pending=43)
[010000001]: Open (size=123, cost=745, time=1.73583, max=0.690166, total=84.1908, pending=43)
[110001]: Open (size=155, cost=750, time=0.623462, max=0.136715, total=84.6263, pending=43)
[010000000001]: Open (size=262, cost=750, time=3.07102, max=0.690166, total=84.9058, pending=43)
[1010]: Open (size=127, cost=757, time=0.762506, max=0.104376, total=85.1433, pending=43)
[11011]: Open (size=184, cost=762, time=9.76945, max=3.03472, total=85.1975, pending=43)
[0011000]: Open (size=194, cost=762, time=1.53874, max=0.690166, total=91.7811, pending=43)
[110101]: Open (size=171, cost=763, time=0.804993, max=0.136715, total=91.9016, pending=43)
[0011101]: Open (size=127, cost=765, time=1.46945, max=0.690166, total=92.0116, pending=43)
[110000]: Open (size=280, cost=768, time=0.727719, max=0.136715, total=92.0808, pending=43)
[1100000]: Open (size=234, cost=728, time=0.753181, max=0.136715, total=92.5746, pending=44)
[0011111]: Open (size=127, cost=768, time=2.08096, max=0.690166, total=98.3094, pending=44)
[11011]: Open (size=346, cost=775, time=16.3036, max=3.03472, total=98.3708, pending=44)
[0100000000001]: Open (size=293, cost=778, time=1.86903, max=0.690166, total=102.467, pending=44)
[0101]: Open (size=139, cost=782, time=1.41138, max=0.690166, total=102.677, pending=44)
[11011]: Open (size=292, cost=793, time=20.3728, max=3.03472, total=102.723, pending=44)
[1100001]: Open (size=240, cost=796, time=1.16191, max=0.434191, total=104.752, pending=44)
[010000000001]: Open (size=238, cost=796, time=3.25659, max=0.690166, total=105.823, pending=45)
[00100]: Open (size=178, cost=797, time=1.60173, max=0.690166, total=106.087, pending=45)
[1100000]: Open (size=165, cost=805, time=0.84167, max=0.136715, total=106.168, pending=45)
[01000001]: Open (size=264, cost=809, time=2.26105, max=0.690166, total=106.246, pending=45)
[01000000011111]: Open (size=148, cost=814, time=4.22543, max=0.86842, total=106.347, pending=45)
[01000000011110]: Open (size=210, cost=814, time=4.87939, max=0.714098, total=106.875, pending=45)
[11000010]: Open (size=238, cost=827, time=1.71692, max=0.55501, total=112.911, pending=45)
[010001]: Open (size=205, cost=834, time=4.39161, max=1.37469, total=118.932, pending=45)
[0101]: Open (size=125, cost=835, time=1.42814, max=0.690166, total=119.237, pending=45)
[010000001]: Open (size=192, cost=846, time=2.0066, max=0.690166, total=124.649, pending=45)
[01000000011111]: Open (size=196, cost=859, time=4.66775, max=0.86842, total=124.774, pending=45)
[01000010]: Open (size=286, cost=869, time=2.56873, max=0.690166, total=127.574, pending=45)
[110101]: Open (size=280, cost=872, time=0.852691, max=0.136715, total=128.038, pending=45)
[1101010]: Open (size=234, cost=832, time=0.881936, max=0.136715, total=128.608, pending=46)
[11010100]: Open (size=167, cost=871, time=0.935053, max=0.136715, total=133.887, pending=47)
[11000010]: Open (size=176, cost=877, time=2.41097, max=0.69405, total=134.175, pending=47)
[01000001]: Open (size=251, cost=891, time=2.33015, max=0.690166, total=141.617, pending=47)
[010000000110]: Open (size=149, cost=894, time=2.06941, max=0.690166, total=141.765, pending=47)
[01000010]: Open (size=198, cost=894, time=2.87366, max=0.690166, total=141.875, pending=47)
[110001]: Open (size=280, cost=896, time=0.725704, max=0.136715, total=147.34, pending=47)
[001101]: Open (size=248, cost=902, time=1.68097, max=0.690166, total=147.442, pending=47)
[1110]: Open (size=210, cost=907, time=0.632611, max=0.136715, total=147.485, pending=47)
[1100000]: Open (size=351, cost=908, time=0.867994, max=0.136715, total=147.55, pending=47)
[110001]: Open (size=180, cost=909, time=0.781562, max=0.136715, total=147.647, pending=47)
[1100010]: Open (size=183, cost=863, time=0.808029, max=0.136715, total=147.991, pending=48)
[11000010]: Open (size=418, cost=917, time=4.40077, max=0.760343, total=148.167, pending=48)
[1100011]: Open (size=193, cost=925, time=1.0536, max=0.272034, total=148.839, pending=48)
[01000010]: Open (size=264, cost=930, time=3.00337, max=0.690166, total=149.556, pending=49)
[1011]: Open (size=478, cost=932, time=0.773324, max=0.104376, total=155.316, pending=49)
[1010]: Open (size=485, cost=952, time=0.783313, max=0.104376, total=155.371, pending=49)
[0011101]: Open (size=485, cost=960, time=1.48964, max=0.690166, total=155.43, pending=49)
[11010100]: Open (size=165, cost=961, time=0.963933, max=0.136715, total=155.491, pending=49)
[010000000100]: Open (size=173, cost=962, time=1.87308, max=0.690166, total=155.592, pending=49)
[010000000110]: Open (size=152, cost=963, time=2.09474, max=0.690166, total=155.723, pending=49)
[0011111]: Open (size=485, cost=963, time=2.10244, max=0.690166, total=161.574, pending=49)
[1010]: Open (size=431, cost=976, time=0.804309, max=0.104376, total=161.629, pending=49)
[1100010]: Open (size=246, cost=983, time=0.834594, max=0.136715, total=161.692, pending=49)
[11000100]: Open (size=225, cost=936, time=0.880364, max=0.136715, total=166.589, pending=50)
[1101011]: Open (size=248, cost=984, time=1.35673, max=0.504044, total=167.188, pending=50)
[0011101]: Open (size=431, cost=984, time=1.51147, max=0.690166, total=167.704, pending=50)
[0100000000000]: Open (size=185, cost=993, time=1.67836, max=0.690166, total=167.767, pending=50)
[1101011]: Open (size=184, cost=996, time=1.83633, max=0.504044, total=167.886, pending=50)
[11000011]: Open (size=248, cost=1003, time=1.65047, max=0.488562, total=173.644, pending=50)
[011]: Open (size=171, cost=1007, time=1.03595, max=0.690166, total=174.161, pending=50)
[010000000100]: Open (size=163, cost=1012, time=1.89851, max=0.690166, total=174.209, pending=50)
[11000011]: Open (size=184, cost=1015, time=2.13146, max=0.488562, total=179.799, pending=50)
[11000110]: Open (size=191, cost=1026, time=1.40293, max=0.349334, total=185.734, pending=50)
[010011]: Open (size=183, cost=1045, time=1.39701, max=0.690166, total=191.725, pending=50)
[01000010]: Open (size=369, cost=1049, time=3.19831, max=0.690166, total=191.806, pending=50)
[11010100]: Open (size=351, cost=1050, time=0.997503, max=0.136715, total=208.409, pending=50)
[11000110]: Open (size=175, cost=1050, time=2.14229, max=0.441935, total=208.505, pending=50)
[001101]: Open (size=246, cost=1056, time=1.69656, max=0.690166, total=217.82, pending=50)
[0100000000000]: Open (size=188, cost=1059, time=1.70067, max=0.690166, total=217.871, pending=50)
[11000011]: Open (size=181, cost=1059, time=2.81822, max=0.686759, total=217.956, pending=50)
[01000010]: Open (size=284, cost=1065, time=3.46173, max=0.690166, total=224.125, pending=50)
[01000001]: Open (size=214, cost=1069, time=2.43689, max=0.690166, total=229.571, pending=50)
[01000010]: Open (size=221, cost=1083, time=3.52074, max=0.690166, total=229.704, pending=50)
[1101011]: Open (size=194, cost=1085, time=2.35842, max=0.522093, total=229.931, pending=50)
[11000011]: Open (size=194, cost=1089, time=3.6353, max=0.817077, total=230.506, pending=50)
[0000]: Open (size=134, cost=1100, time=1.82897, max=0.690166, total=231.371, pending=50)
[00000]: Open (size=186, cost=278, time=1.86205, max=0.690166, total=231.474, pending=51)
******* COMPLETION *******
inverse(multiply(X0,Y0)) -> multiply(inverse(Y0),inverse(X0))
multiply(X2,inverse(X2)) -> identity
inverse(inverse(X2)) -> X2
multiply(X0,identity) -> X0
b -> inverse(c)
multiply(identity,X0) -> X0
multiply(inverse(X0),X0) -> identity
multiply(multiply(X0,Y0),Z0) -> multiply(X0,multiply(Y0,Z0))
multiply(inverse(X0),multiply(X0,Z1)) -> Z1
inverse(identity) -> identity
multiply(X2,multiply(inverse(X2),Z1)) -> Z1
**************************
On branch: [00000]
With size, cost: 61, 153
Orientations: 984
Calls to AProVE (all, T, NT, ?): 604, 534, 47, 23
Time (all, branch, AProVE): 231.476, 1.86205, 218.367
Time/call in AProVE (Avg, Min, Max): 0.361536, 5.5635, 0.00516796
Time/T-call in AProVE (Avg, Min, Max): 0.169666, 5.072, 0.690166
All conjectures solved.