[]: Open (size=42, cost=0, time=0, max=0, total=1.00136e-05, pending=1)
[0]: Open (size=42, cost=66, time=1.47579, max=0.939308, total=1.54141, pending=1)
[1]: Open (size=42, cost=66, time=1.4431, max=0.939308, total=1.74804, pending=2)
[01]: Open (size=42, cost=90, time=1.5426, max=0.939308, total=1.9997, pending=3)
[00]: Open (size=42, cost=90, time=1.61451, max=0.939308, total=2.41516, pending=4)
[10]: Open (size=42, cost=90, time=1.5456, max=0.939308, total=2.73193, pending=5)
[11]: Open (size=42, cost=106, time=1.5912, max=0.939308, total=3.11547, pending=6)
[010]: Open (size=42, cost=114, time=1.75349, max=0.939308, total=3.58408, pending=7)
[000]: Open (size=42, cost=114, time=1.77301, max=0.939308, total=3.77034, pending=7)
[001]: Open (size=42, cost=114, time=1.77143, max=0.939308, total=3.9869, pending=7)
[0010]: Open (size=60, cost=98, time=1.94018, max=0.939308, total=4.34029, pending=8)
[0011]: Open (size=68, cost=100, time=1.95323, max=0.939308, total=4.57489, pending=8)
[100]: Open (size=42, cost=114, time=1.71236, max=0.939308, total=5.10826, pending=8)
[0010]: Open (size=60, cost=128, time=2.17362, max=0.939308, total=5.30802, pending=8)
[100]: Open (size=60, cost=130, time=1.90909, max=0.939308, total=5.48829, pending=8)
[011]: Open (size=42, cost=130, time=1.74573, max=0.939308, total=5.86648, pending=9)
[0111]: Open (size=68, cost=100, time=1.92697, max=0.939308, total=6.2346, pending=10)
[0110]: Open (size=60, cost=106, time=1.92957, max=0.939308, total=6.48756, pending=10)
[0111]: Open (size=68, cost=106, time=2.1793, max=0.939308, total=6.79809, pending=10)
[010]: Open (size=60, cost=130, time=1.93667, max=0.939308, total=7.13195, pending=10)
[101]: Open (size=42, cost=130, time=1.76093, max=0.939308, total=7.44838, pending=11)
[1011]: Open (size=68, cost=100, time=1.85419, max=0.939308, total=7.65007, pending=12)
[1010]: Open (size=60, cost=106, time=1.86626, max=0.939308, total=7.73375, pending=12)
[1011]: Open (size=68, cost=106, time=1.93725, max=0.939308, total=7.8357, pending=12)
[000]: Open (size=60, cost=130, time=1.98647, max=0.939308, total=8.02712, pending=12)
[110]: Open (size=42, cost=130, time=1.82659, max=0.939308, total=8.16762, pending=13)
[0011]: Open (size=66, cost=134, time=2.48499, max=0.939308, total=8.23471, pending=13)
[0111]: Open (size=66, cost=134, time=2.51172, max=0.939308, total=8.46015, pending=14)
[1011]: Open (size=66, cost=134, time=2.12728, max=0.939308, total=8.69594, pending=15)
[0110]: Open (size=60, cost=136, time=2.23896, max=0.939308, total=8.99847, pending=16)
[1010]: Open (size=60, cost=136, time=1.96709, max=0.939308, total=9.06581, pending=16)
[1000]: Open (size=66, cost=138, time=2.10158, max=0.939308, total=9.32109, pending=17)
[0100]: Open (size=66, cost=138, time=2.14338, max=0.939308, total=9.4158, pending=17)
[0000]: Open (size=66, cost=138, time=2.07332, max=0.939308, total=9.50787, pending=17)
[00001]: Open (size=54, cost=108, time=2.2225, max=0.939308, total=9.79044, pending=18)
[110]: Open (size=60, cost=146, time=1.8907, max=0.939308, total=9.85849, pending=18)
[00000]: Open (size=54, cost=148, time=2.24236, max=0.939308, total=9.95458, pending=19)
[1000]: Open (size=54, cost=148, time=2.19489, max=0.939308, total=10.024, pending=19)
[10000]: Open (size=54, cost=144, time=2.25536, max=0.939308, total=10.2074, pending=20)
[10001]: Open (size=54, cost=144, time=2.31569, max=0.939308, total=10.328, pending=20)
[0100]: Open (size=54, cost=148, time=2.23416, max=0.939308, total=10.481, pending=20)
[01001]: Open (size=54, cost=144, time=2.32731, max=0.939308, total=10.691, pending=21)
[010011]: Open (size=88, cost=140, time=2.40947, max=0.939308, total=10.8213, pending=22)
[010010]: Open (size=72, cost=146, time=2.37349, max=0.939308, total=10.8914, pending=22)
[010011]: Open (size=88, cost=146, time=2.47866, max=0.939308, total=10.9974, pending=22)
[10101]: Open (size=88, cost=152, time=2.13612, max=0.939308, total=11.0642, pending=22)
[010011]: Open (size=88, cost=152, time=2.54445, max=0.939308, total=11.1297, pending=22)
[1100]: Open (size=66, cost=154, time=1.93581, max=0.939308, total=11.1951, pending=22)
[10101]: Open (size=88, cost=158, time=2.20057, max=0.939308, total=11.2397, pending=22)
[1001]: Open (size=60, cost=160, time=2.09359, max=0.939308, total=11.2968, pending=22)
[10011]: Open (size=80, cost=144, time=2.15417, max=0.939308, total=11.4236, pending=23)
[0001]: Open (size=60, cost=160, time=2.03877, max=0.939308, total=11.4801, pending=23)
[0101]: Open (size=60, cost=160, time=2.04512, max=0.939308, total=11.5578, pending=23)
[10110]: Open (size=58, cost=162, time=2.25089, max=0.939308, total=11.6218, pending=23)
[111]: Open (size=42, cost=162, time=1.82289, max=0.939308, total=11.6848, pending=23)
[1111]: Open (size=68, cost=100, time=1.86917, max=0.939308, total=11.7704, pending=24)
[1110]: Open (size=60, cost=130, time=1.85911, max=0.939308, total=11.9102, pending=24)
[1111]: Open (size=66, cost=134, time=2.00741, max=0.939308, total=11.9641, pending=24)
[1110]: Open (size=60, cost=160, time=1.91182, max=0.939308, total=12.1257, pending=25)
[11101]: Open (size=88, cost=152, time=1.94806, max=0.939308, total=12.2481, pending=26)
[10111]: Open (size=58, cost=162, time=2.3045, max=0.939308, total=12.3702, pending=26)
[00111]: Open (size=58, cost=162, time=2.57327, max=0.939308, total=12.5038, pending=26)
[11111]: Open (size=58, cost=162, time=2.07737, max=0.939308, total=12.5831, pending=26)
[111111]: Open (size=82, cost=142, time=2.26316, max=0.939308, total=12.9045, pending=27)
[00110]: Open (size=58, cost=162, time=2.62071, max=0.939308, total=13.2758, pending=27)
[01110]: Open (size=58, cost=162, time=2.57944, max=0.939308, total=13.3132, pending=27)
[011101]: Open (size=82, cost=142, time=2.82231, max=0.939308, total=13.5925, pending=28)
[01000]: Open (size=54, cost=164, time=2.34874, max=0.939308, total=14.5744, pending=28)
[010001]: Open (size=88, cost=140, time=2.43384, max=0.939308, total=14.7344, pending=29)
[10100]: Open (size=80, cost=166, time=2.0517, max=0.939308, total=14.9538, pending=29)
[10011]: Open (size=80, cost=166, time=2.20947, max=0.939308, total=15.0094, pending=29)
[0010]: Open (size=72, cost=174, time=2.35205, max=0.939308, total=15.0912, pending=29)
[010011]: Open (size=86, cost=174, time=2.60849, max=0.939308, total=15.1643, pending=30)
[111110]: Open (size=68, cost=174, time=2.21093, max=0.939308, total=15.2315, pending=30)
[011100]: Open (size=68, cost=174, time=2.61383, max=0.939308, total=15.3169, pending=30)
[010001]: Open (size=86, cost=174, time=2.65105, max=0.939308, total=15.3814, pending=30)
[011101]: Open (size=80, cost=176, time=3.80291, max=0.939308, total=15.513, pending=30)
[1101]: Open (size=60, cost=176, time=1.94054, max=0.939308, total=15.7521, pending=30)
[11011]: Open (size=80, cost=144, time=1.98047, max=0.939308, total=15.8274, pending=31)
[010010]: Open (size=72, cost=176, time=2.47744, max=0.939308, total=16.1129, pending=31)
[111111]: Open (size=80, cost=176, time=2.63311, max=0.939308, total=16.2441, pending=31)
[010000]: Open (size=72, cost=176, time=2.42125, max=0.939308, total=16.3935, pending=31)
[1100]: Open (size=54, cost=180, time=1.97891, max=0.939308, total=16.4584, pending=31)
[11000]: Open (size=54, cost=176, time=2.0177, max=0.939308, total=16.5789, pending=32)
[110001]: Open (size=88, cost=140, time=2.14179, max=0.939308, total=16.8079, pending=33)
[00001]: Open (size=72, cost=180, time=2.28818, max=0.939308, total=17.4101, pending=33)
[000010]: Open (size=82, cost=172, time=2.42058, max=0.939308, total=17.5939, pending=34)
[110000]: Open (size=72, cost=180, time=2.12031, max=0.939308, total=17.6585, pending=34)
[11101]: Open (size=88, cost=180, time=2.06826, max=0.939308, total=17.7639, pending=34)
[10101]: Open (size=88, cost=180, time=2.2562, max=0.939308, total=17.8763, pending=34)
[0110]: Open (size=72, cost=182, time=2.3044, max=0.939308, total=17.9489, pending=34)
[10010]: Open (size=72, cost=182, time=2.15823, max=0.939308, total=18.1194, pending=35)
[11110]: Open (size=58, cost=182, time=2.09749, max=0.939308, total=18.1764, pending=35)
[111101]: Open (size=82, cost=142, time=2.18406, max=0.939308, total=18.3631, pending=36)
[11100]: Open (size=80, cost=182, time=1.99635, max=0.939308, total=18.8396, pending=36)
[01111]: Open (size=58, cost=182, time=2.67814, max=0.939308, total=18.8679, pending=36)
[011111]: Open (size=82, cost=142, time=2.76061, max=0.939308, total=19.0259, pending=37)
[00100]: Open (size=78, cost=182, time=2.38878, max=0.939308, total=19.3941, pending=37)
[111100]: Open (size=68, cost=184, time=2.19519, max=0.939308, total=19.473, pending=37)
[011110]: Open (size=68, cost=184, time=2.75162, max=0.939308, total=19.5545, pending=37)
[00100]: Open (size=66, cost=184, time=2.46551, max=0.939308, total=19.6411, pending=37)
[001001]: Open (size=78, cost=178, time=2.50723, max=0.939308, total=19.7367, pending=38)
[0010011]: Open (size=66, cost=152, time=2.55326, max=0.939308, total=19.8343, pending=39)
[00100110]: Open (size=80, cost=164, time=2.62076, max=0.939308, total=20.0454, pending=40)
[001000]: Open (size=78, cost=180, time=2.51683, max=0.939308, total=20.1292, pending=40)
[0010000]: Open (size=72, cost=174, time=2.5655, max=0.939308, total=20.2264, pending=41)
[0010010]: Open (size=66, cost=182, time=2.55591, max=0.939308, total=20.3698, pending=42)
[00100111]: Open (size=80, cost=182, time=2.69374, max=0.939308, total=20.6811, pending=43)
[10101]: Open (size=86, cost=186, time=2.3272, max=0.939308, total=20.9164, pending=44)
[000010]: Open (size=70, cost=186, time=2.48279, max=0.939308, total=21.0642, pending=45)
[11101]: Open (size=86, cost=186, time=2.17888, max=0.939308, total=21.1427, pending=45)
[0010001]: Open (size=72, cost=186, time=2.56253, max=0.939308, total=21.3509, pending=46)
[00100010]: Open (size=86, cost=178, time=2.64821, max=0.939308, total=21.4914, pending=47)
[00100000]: Open (size=86, cost=186, time=2.6434, max=0.939308, total=21.6535, pending=47)
[01100]: Open (size=78, cost=190, time=2.39221, max=0.939308, total=21.7488, pending=47)
[11010]: Open (size=72, cost=190, time=1.97417, max=0.939308, total=21.7881, pending=47)
[11011]: Open (size=78, cost=194, time=2.26319, max=0.939308, total=21.8573, pending=47)
[00100100]: Open (size=80, cost=194, time=2.80225, max=0.939308, total=22.2372, pending=48)
[10011]: Open (size=78, cost=194, time=2.28894, max=0.939308, total=22.3505, pending=48)
[001001111]: Open (size=82, cost=194, time=2.87047, max=0.939308, total=22.4873, pending=49)
[11001]: Open (size=54, cost=196, time=2.05826, max=0.939308, total=23.0719, pending=50)
[110011]: Open (size=88, cost=140, time=2.11345, max=0.939308, total=23.1826, pending=51)
[110010]: Open (size=72, cost=190, time=2.11171, max=0.939308, total=23.618, pending=51)
[10100]: Open (size=80, cost=196, time=2.1057, max=0.939308, total=23.7408, pending=51)
[0001]: Open (size=72, cost=198, time=2.11457, max=0.939308, total=23.9812, pending=52)
[0101]: Open (size=72, cost=198, time=2.10734, max=0.939308, total=24.0761, pending=53)
[00010]: Open (size=78, cost=198, time=2.15152, max=0.939308, total=24.1763, pending=54)
[01010]: Open (size=78, cost=198, time=2.15696, max=0.939308, total=24.2272, pending=54)
[101001]: Open (size=74, cost=202, time=2.18471, max=0.939308, total=24.3218, pending=54)
[001001110]: Open (size=80, cost=204, time=2.74913, max=0.939308, total=24.5513, pending=55)
[111111]: Open (size=72, cost=204, time=2.78087, max=0.939308, total=24.6479, pending=55)
[011101]: Open (size=72, cost=204, time=4.04046, max=0.939308, total=24.7533, pending=55)
[00100001]: Open (size=86, cost=204, time=2.6269, max=0.939308, total=24.8416, pending=55)
[011111]: Open (size=72, cost=204, time=3.12658, max=0.939308, total=25.0448, pending=56)
[011100]: Open (size=68, cost=204, time=2.6765, max=0.939308, total=25.217, pending=56)
[111110]: Open (size=68, cost=204, time=2.29447, max=0.939308, total=25.2673, pending=56)
[1010010]: Open (size=94, cost=204, time=2.34481, max=0.939308, total=25.3641, pending=56)
[10100100]: Open (size=88, cost=188, time=2.41365, max=0.939308, total=25.4884, pending=57)
[101001001]: Open (size=108, cost=198, time=2.47459, max=0.939308, total=25.6022, pending=58)
[111101]: Open (size=72, cost=204, time=2.65816, max=0.939308, total=25.6717, pending=58)
[010000]: Open (size=72, cost=206, time=2.4837, max=0.939308, total=25.792, pending=58)
[00100011]: Open (size=86, cost=206, time=2.61307, max=0.939308, total=25.8448, pending=58)
[01100]: Open (size=66, cost=208, time=2.42961, max=0.939308, total=25.9543, pending=59)
[011000]: Open (size=78, cost=204, time=2.47715, max=0.939308, total=26.0528, pending=60)
[0110000]: Open (size=72, cost=198, time=2.55619, max=0.939308, total=26.2012, pending=61)
[00010]: Open (size=66, cost=208, time=2.20038, max=0.939308, total=26.3309, pending=62)
[00100110]: Open (size=86, cost=210, time=2.69917, max=0.939308, total=26.4635, pending=63)
[110000]: Open (size=72, cost=210, time=2.22319, max=0.939308, total=26.6711, pending=64)
[000011]: Open (size=72, cost=210, time=2.33743, max=0.939308, total=26.7423, pending=64)
[01100000]: Open (size=86, cost=210, time=2.62425, max=0.939308, total=26.7966, pending=64)
[01100001]: Open (size=86, cost=212, time=2.61373, max=0.939308, total=26.8798, pending=64)
[101000]: Open (size=74, cost=212, time=2.26422, max=0.939308, total=27.0649, pending=65)
[10010]: Open (size=72, cost=212, time=2.21089, max=0.939308, total=27.1614, pending=66)
[00101]: Open (size=72, cost=212, time=2.38681, max=0.939308, total=27.1986, pending=66)
[11100]: Open (size=80, cost=212, time=2.02286, max=0.939308, total=27.2396, pending=66)
[000100]: Open (size=78, cost=212, time=2.26972, max=0.939308, total=27.3757, pending=67)
[0001000]: Open (size=72, cost=206, time=2.3138, max=0.939308, total=27.4894, pending=68)
[00010000]: Open (size=86, cost=186, time=2.52168, max=0.939308, total=27.7469, pending=69)
[111011]: Open (size=78, cost=214, time=2.30577, max=0.939308, total=28.6317, pending=69)
[110001]: Open (size=70, cost=214, time=2.74024, max=0.939308, total=28.9799, pending=69)
[1010001]: Open (size=94, cost=214, time=2.31931, max=0.939308, total=29.126, pending=69)
[10100010]: Open (size=88, cost=202, time=2.39482, max=0.939308, total=29.2602, pending=70)
[101000101]: Open (size=94, cost=198, time=2.51235, max=0.939308, total=29.454, pending=71)
[101000100]: Open (size=94, cost=208, time=2.46761, max=0.939308, total=29.6834, pending=71)
[1010001000]: Open (size=88, cost=202, time=2.71633, max=0.939308, total=30.0275, pending=72)
[010001]: Open (size=70, cost=214, time=2.78044, max=0.939308, total=30.2095, pending=73)
[101010]: Open (size=78, cost=214, time=2.38053, max=0.939308, total=30.3015, pending=73)
[110011]: Open (size=70, cost=214, time=2.5452, max=0.939308, total=30.3678, pending=73)
[010011]: Open (size=70, cost=214, time=2.67351, max=0.939308, total=30.5143, pending=73)
[00010001]: Open (size=86, cost=216, time=2.35845, max=0.939308, total=30.6078, pending=73)
[10001]: Open (size=72, cost=216, time=2.4659, max=0.939308, total=30.7318, pending=74)
[100010]: Open (size=82, cost=192, time=2.5356, max=0.939308, total=30.8483, pending=75)
[10100010001]: Open (size=102, cost=216, time=2.79962, max=0.939308, total=30.9659, pending=75)
[000100011]: Open (size=86, cost=216, time=2.41261, max=0.939308, total=31.8382, pending=76)
[10000]: Open (size=72, cost=216, time=2.37314, max=0.939308, total=31.9194, pending=76)
[100000]: Open (size=82, cost=172, time=2.45001, max=0.939308, total=32.0394, pending=77)
[000101]: Open (size=78, cost=218, time=2.26056, max=0.939308, total=32.2145, pending=77)
[0001011]: Open (size=66, cost=202, time=2.32516, max=0.939308, total=32.3379, pending=78)
[00010110]: Open (size=80, cost=162, time=2.42446, max=0.939308, total=32.5431, pending=79)
[00010111]: Open (size=80, cost=182, time=2.42779, max=0.939308, total=32.6413, pending=79)
[000101110]: Open (size=80, cost=174, time=2.59207, max=0.939308, total=33.0414, pending=80)
[00010110]: Open (size=86, cost=200, time=2.51966, max=0.939308, total=33.225, pending=80)
[000100010]: Open (size=86, cost=218, time=2.42397, max=0.939308, total=33.3682, pending=81)
[011001]: Open (size=78, cost=218, time=2.47781, max=0.939308, total=33.421, pending=81)
[0110010]: Open (size=66, cost=202, time=2.56533, max=0.939308, total=33.5542, pending=82)
[0110011]: Open (size=66, cost=212, time=2.52024, max=0.939308, total=33.6859, pending=83)
[01100100]: Open (size=80, cost=214, time=2.62339, max=0.939308, total=33.865, pending=84)
[11010]: Open (size=72, cost=220, time=2.04134, max=0.939308, total=33.9425, pending=84)
[110101]: Open (size=104, cost=180, time=2.07944, max=0.939308, total=34.0492, pending=85)
[110010]: Open (size=72, cost=220, time=2.232, max=0.939308, total=34.4149, pending=86)
[01101]: Open (size=72, cost=220, time=2.38519, max=0.939308, total=34.4779, pending=86)
[011011]: Open (size=104, cost=180, time=2.42163, max=0.939308, total=34.5717, pending=87)
[1010011]: Open (size=94, cost=220, time=2.24988, max=0.939308, total=34.7222, pending=87)
[110000]: Open (size=86, cost=220, time=2.29112, max=0.939308, total=34.8757, pending=88)
[00000]: Open (size=72, cost=220, time=2.30925, max=0.939308, total=35.0833, pending=89)
[000000]: Open (size=82, cost=192, time=2.43636, max=0.939308, total=35.3107, pending=90)
[1100000]: Open (size=90, cost=220, time=2.39545, max=0.939308, total=35.4808, pending=90)
[11000000]: Open (size=88, cost=216, time=2.53028, max=0.939308, total=35.8045, pending=91)
[100010]: Open (size=70, cost=222, time=2.65107, max=0.939308, total=35.8939, pending=91)
[010010]: Open (size=86, cost=222, time=2.60522, max=0.939308, total=35.9784, pending=91)
[0100101]: Open (size=90, cost=222, time=2.66698, max=0.939308, total=36.1058, pending=92)
[01100110]: Open (size=80, cost=224, time=2.58916, max=0.939308, total=36.2502, pending=93)
[011101]: Open (size=72, cost=224, time=4.12655, max=0.939308, total=36.3419, pending=93)
[011111]: Open (size=72, cost=224, time=3.29639, max=0.939308, total=36.8418, pending=94)
[01010]: Open (size=66, cost=224, time=2.24933, max=0.939308, total=37.2986, pending=95)
[010101]: Open (size=78, cost=218, time=2.29161, max=0.939308, total=37.3822, pending=96)
[0101011]: Open (size=66, cost=222, time=2.351, max=0.939308, total=37.4962, pending=97)
[01010110]: Open (size=80, cost=182, time=2.41455, max=0.939308, total=37.6312, pending=98)
[01010111]: Open (size=80, cost=218, time=2.41897, max=0.939308, total=37.9329, pending=99)
[010101110]: Open (size=80, cost=210, time=2.53076, max=0.939308, total=38.2269, pending=100)
[111101]: Open (size=72, cost=224, time=2.77611, max=0.939308, total=38.3331, pending=100)
[111111]: Open (size=72, cost=224, time=2.88395, max=0.939308, total=38.6859, pending=101)
[111011]: Open (size=66, cost=226, time=2.65033, max=0.939308, total=39.1258, pending=102)
[000101110]: Open (size=100, cost=226, time=2.77058, max=0.939308, total=39.4363, pending=103)
[00111]: Open (size=68, cost=226, time=2.64983, max=0.939308, total=39.6685, pending=103)
[001110]: Open (size=80, cost=182, time=2.69454, max=0.939308, total=39.7775, pending=104)
[101010]: Open (size=66, cost=226, time=2.44366, max=0.939308, total=39.9942, pending=104)
[000101111]: Open (size=80, cost=226, time=2.6601, max=0.939308, total=40.1343, pending=105)
[01100111]: Open (size=80, cost=226, time=2.62674, max=0.939308, total=40.2447, pending=105)
[011001111]: Open (size=82, cost=218, time=2.69491, max=0.939308, total=40.378, pending=106)
[10110]: Open (size=68, cost=226, time=2.31106, max=0.939308, total=40.6613, pending=107)
[101100]: Open (size=80, cost=182, time=2.39488, max=0.939308, total=40.8159, pending=108)
[101000100011]: Open (size=102, cost=226, time=3.56754, max=0.939308, total=41.0804, pending=108)
[111110]: Open (size=66, cost=226, time=2.38838, max=0.939308, total=41.8575, pending=108)
[1111100]: Open (size=76, cost=208, time=2.5663, max=0.939308, total=42.1147, pending=109)
[011100]: Open (size=66, cost=226, time=2.72384, max=0.939308, total=42.31, pending=110)
[0111000]: Open (size=76, cost=208, time=2.81958, max=0.939308, total=42.4897, pending=111)
[001000010]: Open (size=86, cost=226, time=2.68822, max=0.939308, total=42.6347, pending=112)
[10100110]: Open (size=88, cost=228, time=2.33365, max=0.939308, total=42.7049, pending=112)
[101001101]: Open (size=94, cost=224, time=2.42481, max=0.939308, total=42.8785, pending=113)
[010100]: Open (size=78, cost=228, time=2.28764, max=0.939308, total=42.981, pending=113)
[0101000]: Open (size=72, cost=222, time=2.33089, max=0.939308, total=43.0834, pending=114)
[01010000]: Open (size=86, cost=202, time=2.5118, max=0.939308, total=43.3712, pending=115)
[00110]: Open (size=68, cost=230, time=2.65551, max=0.939308, total=43.8616, pending=115)
[001100]: Open (size=80, cost=182, time=2.92216, max=0.939308, total=44.1601, pending=116)
[011011]: Open (size=102, cost=230, time=2.56939, max=0.939308, total=45.0724, pending=116)
[10100010000]: Open (size=102, cost=230, time=2.80883, max=0.939308, total=45.2353, pending=117)
[00100100]: Open (size=86, cost=230, time=2.91144, max=0.939308, total=50.4887, pending=117)
[10111]: Open (size=68, cost=230, time=2.43495, max=0.939308, total=50.6308, pending=118)
[101110]: Open (size=80, cost=182, time=2.51145, max=0.939308, total=50.7801, pending=119)
[0110001]: Open (size=72, cost=230, time=2.54365, max=0.939308, total=51.8235, pending=119)
[01100010]: Open (size=86, cost=222, time=2.61612, max=0.939308, total=51.9806, pending=120)
[0010011110]: Open (size=84, cost=230, time=3.05256, max=0.939308, total=52.0494, pending=120)
[01100000]: Open (size=92, cost=232, time=2.70303, max=0.939308, total=52.2345, pending=120)
[00100101]: Open (size=80, cost=232, time=2.61731, max=0.939308, total=52.3979, pending=121)
[001001011]: Open (size=82, cost=194, time=2.73911, max=0.939308, total=52.5729, pending=122)
[0010010111]: Open (size=84, cost=230, time=3.08671, max=0.939308, total=53.0641, pending=123)
[00010000]: Open (size=92, cost=232, time=3.40133, max=0.939308, total=53.4461, pending=123)
[010000]: Open (size=86, cost=232, time=2.53288, max=0.939308, total=59.5047, pending=123)
[01010000]: Open (size=92, cost=232, time=2.98913, max=0.939308, total=59.6936, pending=124)
[010100000]: Open (size=90, cost=228, time=3.22185, max=0.939308, total=60.17, pending=125)
[0100001]: Open (size=90, cost=232, time=2.60774, max=0.939308, total=60.4222, pending=125)
[011000010]: Open (size=86, cost=234, time=2.67723, max=0.939308, total=60.6209, pending=126)
[111001]: Open (size=74, cost=234, time=2.11386, max=0.939308, total=60.6932, pending=126)
[010011]: Open (size=70, cost=234, time=2.76404, max=0.939308, total=60.8065, pending=127)
[1101010]: Open (size=86, cost=234, time=2.35709, max=0.939308, total=61.0209, pending=128)
[11010101]: Open (size=94, cost=216, time=2.42854, max=0.939308, total=61.1628, pending=129)
[1110111]: Open (size=70, cost=234, time=2.78926, max=0.939308, total=61.238, pending=129)
[1010101]: Open (size=70, cost=234, time=2.5016, max=0.939308, total=61.6969, pending=130)
[1010100]: Open (size=70, cost=234, time=2.52173, max=0.939308, total=61.8833, pending=131)
[1110110]: Open (size=70, cost=234, time=2.81771, max=0.939308, total=62.0279, pending=132)
[010001]: Open (size=70, cost=234, time=2.8694, max=0.939308, total=62.4163, pending=133)
[10100010000]: Open (size=106, cost=234, time=2.8735, max=0.939308, total=62.9156, pending=134)
[011110]: Open (size=68, cost=234, time=2.83593, max=0.939308, total=62.9938, pending=134)
[111100]: Open (size=68, cost=234, time=2.27432, max=0.939308, total=63.0766, pending=134)
[01100010]: Open (size=92, cost=234, time=2.6802, max=0.939308, total=63.1603, pending=134)
[01100011]: Open (size=86, cost=234, time=2.6238, max=0.939308, total=63.405, pending=135)
[00100010]: Open (size=84, cost=236, time=2.80606, max=0.939308, total=63.5861, pending=136)
[01100101]: Open (size=80, cost=236, time=2.63542, max=0.939308, total=63.6736, pending=136)
[011001011]: Open (size=82, cost=218, time=2.70061, max=0.939308, total=63.8157, pending=137)
[01100100]: Open (size=94, cost=236, time=2.6974, max=0.939308, total=64.1399, pending=138)
[01001011]: Open (size=88, cost=236, time=2.72715, max=0.939308, total=64.2705, pending=139)
[010010111]: Open (size=90, cost=228, time=2.83576, max=0.939308, total=64.4482, pending=140)
[01100110]: Open (size=94, cost=236, time=2.67717, max=0.939308, total=64.7267, pending=141)
[00011]: Open (size=72, cost=236, time=2.17068, max=0.939308, total=64.867, pending=142)
[01011]: Open (size=72, cost=236, time=2.15608, max=0.939308, total=64.9036, pending=142)
[010111]: Open (size=96, cost=172, time=2.18546, max=0.939308, total=64.9657, pending=143)
[001000011]: Open (size=86, cost=236, time=2.76446, max=0.939308, total=65.1939, pending=144)
[1110010]: Open (size=94, cost=236, time=2.17934, max=0.939308, total=65.2656, pending=144)
[11100100]: Open (size=88, cost=220, time=2.23455, max=0.939308, total=65.3809, pending=145)
[111001001]: Open (size=108, cost=230, time=2.41795, max=0.939308, total=65.6466, pending=146)
[1110010011]: Open (size=142, cost=222, time=2.5069, max=0.939308, total=65.8691, pending=147)
[1010001001]: Open (size=88, cost=238, time=2.55849, max=0.939308, total=66.0611, pending=147)
[0100110]: Open (size=70, cost=238, time=2.85684, max=0.939308, total=66.2032, pending=148)
[01001100]: Open (size=78, cost=230, time=3.04595, max=0.939308, total=66.5762, pending=149)
[0100011]: Open (size=70, cost=238, time=2.96085, max=0.939308, total=66.7859, pending=149)
[01000110]: Open (size=78, cost=230, time=3.12744, max=0.939308, total=67.0951, pending=150)
[1110010010]: Open (size=122, cost=238, time=2.54712, max=0.939308, total=67.2816, pending=150)
[11000001]: Open (size=88, cost=238, time=2.58052, max=0.939308, total=67.3828, pending=150)
[110000011]: Open (size=90, cost=220, time=2.63664, max=0.939308, total=67.537, pending=151)
[01001010]: Open (size=88, cost=238, time=2.74761, max=0.939308, total=67.7668, pending=152)
[000011]: Open (size=78, cost=240, time=2.38843, max=0.939308, total=67.9697, pending=152)
[0000111]: Open (size=90, cost=228, time=2.44754, max=0.939308, total=68.0909, pending=153)
[00001110]: Open (size=88, cost=188, time=2.58207, max=0.939308, total=68.2911, pending=154)
[00001111]: Open (size=88, cost=220, time=2.50983, max=0.939308, total=68.4062, pending=154)
[000011110]: Open (size=88, cost=232, time=2.6472, max=0.939308, total=68.7256, pending=155)
[0000111101]: Open (size=108, cost=230, time=2.81332, max=0.939308, total=69.025, pending=156)
[0000111100]: Open (size=108, cost=234, time=2.77466, max=0.939308, total=69.2711, pending=156)
[00001111000]: Open (size=104, cost=230, time=2.94499, max=0.939308, total=69.5822, pending=157)
[1100001]: Open (size=90, cost=240, time=2.39003, max=0.939308, total=70.4747, pending=158)
[00010000]: Open (size=88, cost=240, time=4.32652, max=0.939308, total=70.7975, pending=159)
[001001100]: Open (size=80, cost=242, time=2.83621, max=0.939308, total=71.7041, pending=159)
[10100010011]: Open (size=102, cost=242, time=2.61866, max=0.939308, total=71.8048, pending=159)
[00001110]: Open (size=102, cost=242, time=2.69382, max=0.939308, total=75.293, pending=160)
[110100]: Open (size=92, cost=242, time=2.1078, max=0.939308, total=75.5579, pending=161)
[0100100]: Open (size=90, cost=242, time=2.66673, max=0.939308, total=75.6264, pending=161)
[01001000]: Open (size=88, cost=238, time=2.75551, max=0.939308, total=75.8558, pending=162)
[011010]: Open (size=92, cost=242, time=2.44011, max=0.939308, total=75.9595, pending=162)
[0101010]: Open (size=66, cost=242, time=2.34304, max=0.939308, total=76.0181, pending=162)
[01010100]: Open (size=80, cost=222, time=2.41359, max=0.939308, total=76.216, pending=163)
[01010101]: Open (size=80, cost=238, time=2.46657, max=0.939308, total=76.2927, pending=163)
[001000110]: Open (size=86, cost=242, time=2.66817, max=0.939308, total=76.5534, pending=164)
[111000]: Open (size=74, cost=244, time=2.06528, max=0.939308, total=76.6106, pending=164)
[000011111]: Open (size=88, cost=244, time=2.68837, max=0.939308, total=76.7309, pending=165)
[101001000]: Open (size=108, cost=244, time=2.4615, max=0.939308, total=77.1136, pending=166)
[1010010000]: Open (size=102, cost=238, time=2.55883, max=0.939308, total=77.4121, pending=167)
[10100100000]: Open (size=124, cost=242, time=2.90034, max=0.939308, total=77.85, pending=168)
[00100000]: Open (size=84, cost=244, time=2.73427, max=0.939308, total=83.3443, pending=168)
[011000011]: Open (size=86, cost=244, time=2.73128, max=0.939308, total=83.4852, pending=168)
[101011]: Open (size=78, cost=244, time=2.41949, max=0.939308, total=83.5793, pending=168)
[111010]: Open (size=78, cost=244, time=2.25778, max=0.939308, total=83.6607, pending=168)
[100001]: Open (size=72, cost=246, time=2.41387, max=0.939308, total=83.7508, pending=168)
[1000010]: Open (size=90, cost=238, time=2.64491, max=0.939308, total=84.1474, pending=169)
[10000100]: Open (size=88, cost=218, time=2.75712, max=0.939308, total=84.3258, pending=170)
[10000101]: Open (size=88, cost=226, time=2.70725, max=0.939308, total=84.4065, pending=170)
[100011]: Open (size=72, cost=246, time=2.51061, max=0.939308, total=84.8004, pending=171)
[10100010010]: Open (size=102, cost=246, time=2.63451, max=0.939308, total=84.904, pending=171)
[000101101]: Open (size=80, cost=246, time=2.58282, max=0.939308, total=90.7574, pending=171)
[100001011]: Open (size=88, cost=246, time=3.02543, max=0.939308, total=91.0761, pending=171)
[010101110]: Open (size=100, cost=246, time=2.63207, max=0.939308, total=91.516, pending=172)
[10100111]: Open (size=88, cost=246, time=2.31604, max=0.939308, total=91.8101, pending=172)
[0001001]: Open (size=72, cost=248, time=2.33608, max=0.939308, total=92.021, pending=173)
[00010010]: Open (size=86, cost=228, time=2.38277, max=0.939308, total=92.1336, pending=174)
[00010011]: Open (size=86, cost=238, time=2.39797, max=0.939308, total=92.2017, pending=174)
[000101110]: Open (size=106, cost=248, time=2.99747, max=0.939308, total=92.3599, pending=175)
[0001011101]: Open (size=108, cost=242, time=4.31887, max=1.3214, total=93.8073, pending=176)
[00010111011]: Open (size=100, cost=226, time=6.78756, max=2.46869, total=98.6991, pending=177)
[00010111010]: Open (size=100, cost=246, time=6.7357, max=2.41683, total=101.43, pending=177)
[001001100]: Open (size=96, cost=248, time=2.9317, max=0.939308, total=103.913, pending=177)
[0010011000]: Open (size=108, cost=200, time=3.02622, max=0.939308, total=104.086, pending=178)
[00100110000]: Open (size=118, cost=174, time=3.121, max=0.939308, total=104.297, pending=179)
[00100110001]: Open (size=118, cost=174, time=3.13518, max=0.939308, total=109.615, pending=179)
[001001100011]: Open (size=146, cost=200, time=4.16464, max=1.02946, total=110.764, pending=180)
******* COMPLETION *******
b(c(X0)) -> c(c(b(w(X0))))
b(w(w(X0))) -> w(w(b(X0)))
b(w(b(X0))) -> w(X0)
w(u(X0)) -> u(c(X0))
b(a(X0)) -> u(b(X0))
c(u(X0)) -> u(w(X0))
w(a(X0)) -> a(c(X0))
b(u(X0)) -> a(b(X0))
c(a(X0)) -> a(w(X0))
u(a(X0)) -> X0
a(u(X0)) -> X0
w(c(X0)) -> X0
c(w(X0)) -> X0
v(X0) -> c(b(w(X0)))
**************************
On branch: [001001100011]
With size, cost: 80, 134
Orientations: 796
Calls to AProVE (all, T, NT, ?): 583, 578, 0, 5
Time (all, branch, AProVE): 110.766, 4.16464, 108.616
Time/call in AProVE (Avg, Min, Max): 0.186306, 5.77928, 0.0256581
Time/T-call in AProVE (Avg, Min, Max): 0.141972, 3.40672, 1.02946
All conjectures solved.