[]: Open (size=34, cost=0, time=0, max=0, total=7.86781e-06, pending=1)
[0]: Open (size=34, cost=34, time=0.666158, max=0.666158, total=0.680129, pending=1)
[1]: Open (size=34, cost=34, time=0.0137179, max=0.0137179, total=0.717445, pending=1)
[10]: Open (size=33, cost=33, time=0.0657799, max=0.035383, total=0.794849, pending=2)
[0]: Open (size=35, cost=35, time=0.703218, max=0.666158, total=0.858562, pending=2)
[00]: Open (size=35, cost=35, time=0.7547, max=0.666158, total=0.950273, pending=3)
[11]: Open (size=33, cost=73, time=0.0552871, max=0.0248902, total=0.996756, pending=3)
[01]: Open (size=35, cost=97, time=0.743006, max=0.666158, total=1.03246, pending=3)
[10]: Open (size=31, cost=239, time=0.128206, max=0.0624261, total=1.08082, pending=3)
[11]: Open (size=30, cost=256, time=0.0896881, max=0.0344009, total=1.29046, pending=3)
[110]: Open (size=56, cost=188, time=0.138444, max=0.0344009, total=1.40354, pending=4)
[111]: Open (size=56, cost=274, time=0.178688, max=0.0615201, total=1.44222, pending=4)
[110]: Open (size=50, cost=293, time=0.174839, max=0.0363951, total=1.49433, pending=4)
[01]: Open (size=33, cost=305, time=0.789752, max=0.666158, total=1.68153, pending=4)
[110]: Open (size=188, cost=314, time=0.355286, max=0.09286, total=1.76162, pending=4)
[00]: Open (size=35, cost=341, time=0.799457, max=0.666158, total=1.80082, pending=4)
[10]: Open (size=110, cost=346, time=0.333732, max=0.109015, total=1.90048, pending=4)
[01]: Open (size=59, cost=361, time=0.865406, max=0.666158, total=1.93529, pending=4)
[111]: Open (size=50, cost=386, time=0.228256, max=0.0615201, total=2.00035, pending=5)
[010]: Open (size=59, cost=411, time=0.905635, max=0.666158, total=2.05328, pending=5)
[111]: Open (size=74, cost=413, time=0.276984, max=0.0615201, total=2.19991, pending=5)
[1110]: Open (size=74, cost=415, time=0.317285, max=0.0615201, total=2.29759, pending=6)
[00]: Open (size=145, cost=471, time=0.893465, max=0.666158, total=3.27653, pending=6)
[011]: Open (size=59, cost=491, time=0.886443, max=0.666158, total=3.30479, pending=6)
[1111]: Open (size=74, cost=498, time=0.330381, max=0.0615201, total=3.36611, pending=6)
[11111]: Open (size=75, cost=514, time=0.359448, max=0.0615201, total=3.42246, pending=7)
[110]: Open (size=188, cost=515, time=0.391618, max=0.09286, total=3.46032, pending=7)
[11111]: Open (size=83, cost=515, time=0.390594, max=0.0615201, total=3.48592, pending=7)
[010]: Open (size=79, cost=517, time=1.04648, max=0.666158, total=3.58545, pending=7)
[11110]: Open (size=74, cost=562, time=0.352951, max=0.0615201, total=3.9752, pending=7)
[011]: Open (size=89, cost=599, time=0.942396, max=0.666158, total=4.12148, pending=7)
[11111]: Open (size=102, cost=621, time=0.477405, max=0.0637839, total=4.15883, pending=7)
[10]: Open (size=110, cost=625, time=0.364738, max=0.109015, total=4.20879, pending=7)
[11110]: Open (size=110, cost=636, time=0.479984, max=0.068666, total=4.24569, pending=7)
[1110]: Open (size=264, cost=675, time=0.590841, max=0.0845311, total=4.6679, pending=7)
[011]: Open (size=89, cost=681, time=0.973002, max=0.666158, total=4.71277, pending=7)
[110]: Open (size=188, cost=683, time=0.411923, max=0.09286, total=4.83838, pending=7)
[11110]: Open (size=175, cost=702, time=0.838131, max=0.10142, total=4.86353, pending=7)
[010]: Open (size=237, cost=717, time=1.41595, max=0.666158, total=4.98514, pending=7)
[00]: Open (size=145, cost=747, time=0.916305, max=0.666158, total=5.02659, pending=7)
[11110]: Open (size=416, cost=766, time=0.937845, max=0.10142, total=5.0588, pending=7)
[11111]: Open (size=102, cost=808, time=0.515442, max=0.0637839, total=5.11733, pending=7)
[1110]: Open (size=264, cost=886, time=0.628956, max=0.0845311, total=5.31908, pending=7)
[011]: Open (size=193, cost=899, time=1.07191, max=0.666158, total=5.3463, pending=7)
[110]: Open (size=188, cost=936, time=0.428549, max=0.09286, total=5.38834, pending=7)
[11111]: Open (size=197, cost=952, time=0.6547, max=0.0637839, total=5.42019, pending=7)
[010]: Open (size=237, cost=967, time=1.44945, max=0.666158, total=5.48172, pending=7)
[11110]: Open (size=411, cost=982, time=0.983746, max=0.10142, total=5.52253, pending=7)
[1110]: Open (size=264, cost=1086, time=0.646513, max=0.0845311, total=5.57521, pending=7)
[011]: Open (size=131, cost=1103, time=1.09991, max=0.666158, total=5.62033, pending=7)
[110]: Open (size=188, cost=1234, time=0.448045, max=0.09286, total=5.70673, pending=7)
[11110]: Open (size=411, cost=1237, time=1.0206, max=0.10142, total=5.7483, pending=7)
[11111]: Open (size=173, cost=1319, time=0.685435, max=0.0637839, total=5.82659, pending=7)
[1110]: Open (size=264, cost=1376, time=0.678014, max=0.0845311, total=6.1266, pending=7)
[011]: Open (size=165, cost=1461, time=1.15378, max=0.666158, total=6.1684, pending=7)
[11110]: Open (size=411, cost=1480, time=1.0753, max=0.10142, total=6.2771, pending=7)
[10]: Open (size=110, cost=1482, time=0.391268, max=0.109015, total=6.3426, pending=7)
[11110]: Open (size=411, cost=1624, time=1.11587, max=0.10142, total=6.37696, pending=7)
[11111]: Open (size=229, cost=1665, time=0.843514, max=0.0637839, total=6.4531, pending=7)
[011]: Open (size=337, cost=1921, time=1.21194, max=0.666158, total=6.7342, pending=7)
[1110]: Open (size=264, cost=1963, time=0.698642, max=0.0845311, total=6.80603, pending=7)
[010]: Open (size=237, cost=1977, time=1.47392, max=0.666158, total=6.90673, pending=7)
[00]: Open (size=145, cost=1989, time=0.935339, max=0.666158, total=6.95722, pending=7)
[1110]: Open (size=255, cost=2004, time=0.764163, max=0.0845311, total=6.99666, pending=7)
[11110]: Open (size=411, cost=2056, time=1.15792, max=0.10142, total=7.05311, pending=7)
[110]: Open (size=157, cost=2125, time=0.46969, max=0.09286, total=7.13868, pending=7)
[011]: Open (size=511, cost=2345, time=1.2463, max=0.666158, total=7.19057, pending=7)
[11111]: Open (size=577, cost=2350, time=0.965563, max=0.0637839, total=7.25359, pending=7)
[010]: Open (size=237, cost=2375, time=1.50016, max=0.666158, total=7.36084, pending=7)
[10]: Open (size=110, cost=2601, time=0.405582, max=0.109015, total=7.41793, pending=7)
[010]: Open (size=237, cost=2765, time=1.52601, max=0.666158, total=7.46696, pending=7)
[011]: Open (size=505, cost=2791, time=1.28, max=0.666158, total=7.53175, pending=7)
[11111]: Open (size=572, cost=2803, time=1.01121, max=0.0637839, total=7.59541, pending=7)
[11110]: Open (size=411, cost=2809, time=1.19968, max=0.10142, total=7.70492, pending=7)
[00]: Open (size=145, cost=2971, time=0.951045, max=0.666158, total=7.88018, pending=7)
[011]: Open (size=501, cost=3051, time=1.30882, max=0.666158, total=7.95252, pending=7)
[110]: Open (size=157, cost=3060, time=0.488273, max=0.09286, total=8.06003, pending=7)
[10]: Open (size=122, cost=3156, time=0.422486, max=0.109015, total=8.1331, pending=7)
[1110]: Open (size=219, cost=3213, time=0.785296, max=0.0845311, total=8.22236, pending=7)
[11111]: Open (size=572, cost=3268, time=1.05113, max=0.0637839, total=8.29568, pending=7)
[10]: Open (size=198, cost=3463, time=0.458437, max=0.109015, total=8.40736, pending=7)
[011]: Open (size=501, cost=3535, time=1.37019, max=0.666158, total=8.46494, pending=7)
[110]: Open (size=168, cost=3537, time=0.508902, max=0.09286, total=8.54709, pending=7)
[11111]: Open (size=572, cost=3734, time=1.08842, max=0.0637839, total=8.66663, pending=7)
[110]: Open (size=261, cost=3779, time=0.554127, max=0.09286, total=8.80202, pending=7)
[010]: Open (size=185, cost=3951, time=1.54632, max=0.666158, total=8.87998, pending=7)
[110]: Open (size=261, cost=4077, time=0.57549, max=0.09286, total=9.02999, pending=7)
[11111]: Open (size=572, cost=4084, time=1.1299, max=0.0637839, total=9.12324, pending=7)
[10]: Open (size=198, cost=4177, time=0.473965, max=0.109015, total=9.27602, pending=7)
[011]: Open (size=501, cost=4203, time=1.40136, max=0.666158, total=9.35297, pending=7)
[11110]: Open (size=366, cost=4387, time=1.28728, max=0.10142, total=9.45916, pending=7)
[1110]: Open (size=203, cost=4437, time=0.805338, max=0.0845311, total=9.61102, pending=7)
[010]: Open (size=213, cost=4507, time=1.6, max=0.666158, total=9.78211, pending=7)
[11111]: Open (size=572, cost=4513, time=1.17686, max=0.0637839, total=9.88311, pending=7)
[110]: Open (size=241, cost=4683, time=0.603199, max=0.09286, total=10.0518, pending=7)
[010]: Open (size=213, cost=4751, time=1.62668, max=0.666158, total=10.1416, pending=7)
[110]: Open (size=241, cost=5004, time=0.622656, max=0.09286, total=10.3456, pending=7)
[1110]: Open (size=218, cost=5035, time=0.859799, max=0.0845311, total=10.442, pending=7)
[00]: Open (size=145, cost=5131, time=0.976899, max=0.666158, total=10.6429, pending=7)
[010]: Open (size=325, cost=5149, time=1.68, max=0.666158, total=10.733, pending=7)
[110]: Open (size=238, cost=5242, time=0.64406, max=0.09286, total=10.8495, pending=7)
[10]: Open (size=197, cost=5258, time=0.492419, max=0.109015, total=11.0348, pending=7)
[1110]: Open (size=331, cost=5307, time=0.91281, max=0.0845311, total=11.1152, pending=7)
[110]: Open (size=266, cost=5412, time=0.694464, max=0.09286, total=11.2416, pending=7)
[010]: Open (size=315, cost=5433, time=1.70669, max=0.666158, total=11.3569, pending=7)
[11110]: Open (size=334, cost=5491, time=1.33999, max=0.10142, total=11.4847, pending=7)
[10]: Open (size=192, cost=5542, time=0.510565, max=0.109015, total=11.6482, pending=7)
[11111]: Open (size=572, cost=5627, time=1.2253, max=0.0637839, total=11.7523, pending=7)
[1110]: Open (size=331, cost=5649, time=0.949193, max=0.0845311, total=11.9298, pending=7)
[110]: Open (size=257, cost=5738, time=0.716225, max=0.09286, total=13.3061, pending=7)
[010]: Open (size=315, cost=5761, time=1.73507, max=0.666158, total=13.5286, pending=7)
[10]: Open (size=206, cost=5768, time=0.528618, max=0.109015, total=13.799, pending=7)
[11111]: Open (size=563, cost=5791, time=1.27073, max=0.0637839, total=14.0109, pending=7)
[00]: Open (size=173, cost=5913, time=0.993519, max=0.666158, total=14.2776, pending=7)
[011]: Open (size=501, cost=5915, time=1.43299, max=0.666158, total=14.3651, pending=7)
[1110]: Open (size=331, cost=5965, time=1.05488, max=0.105685, total=14.5018, pending=7)
[10]: Open (size=205, cost=6341, time=0.582189, max=0.109015, total=14.7092, pending=7)
[110]: Open (size=257, cost=6347, time=0.766668, max=0.09286, total=14.8376, pending=7)
[00]: Open (size=173, cost=6441, time=1.01071, max=0.666158, total=15.0899, pending=7)
[010]: Open (size=315, cost=6485, time=1.79953, max=0.666158, total=15.2083, pending=7)
[011]: Open (size=501, cost=6573, time=1.47995, max=0.666158, total=15.3648, pending=7)
[110]: Open (size=328, cost=6604, time=0.823297, max=0.09286, total=15.514, pending=7)
[1110]: Open (size=312, cost=6715, time=1.10797, max=0.105685, total=15.674, pending=7)
[00]: Open (size=249, cost=6759, time=1.02747, max=0.666158, total=15.8299, pending=7)
[010]: Open (size=275, cost=6795, time=1.82961, max=0.666158, total=15.943, pending=7)
[1110]: Open (size=273, cost=6962, time=1.13936, max=0.105685, total=16.1461, pending=7)
[010]: Open (size=359, cost=6975, time=1.85922, max=0.666158, total=17.1551, pending=7)
[011]: Open (size=501, cost=7091, time=1.52219, max=0.666158, total=17.3956, pending=7)
[010]: Open (size=359, cost=7153, time=1.89415, max=0.666158, total=17.5673, pending=7)
[110]: Open (size=299, cost=7172, time=0.849368, max=0.09286, total=17.7616, pending=7)
[11110]: Open (size=316, cost=7177, time=1.38087, max=0.10142, total=17.9369, pending=7)
[1110]: Open (size=335, cost=7209, time=1.25566, max=0.105685, total=18.249, pending=7)
[010]: Open (size=359, cost=7271, time=1.93504, max=0.666158, total=18.4413, pending=7)
[10]: Open (size=205, cost=7335, time=0.620269, max=0.109015, total=18.7211, pending=7)
[101]: Open (size=268, cost=3617, time=0.643159, max=0.109015, total=18.8804, pending=8)
[100]: Open (size=282, cost=4908, time=0.653909, max=0.109015, total=19.0559, pending=8)
[101]: Open (size=247, cost=5122, time=0.709133, max=0.109015, total=19.2965, pending=8)
[100]: Open (size=238, cost=5396, time=0.759542, max=0.109015, total=19.5254, pending=8)
[101]: Open (size=236, cost=5469, time=0.789415, max=0.109015, total=19.6558, pending=8)
[100]: Open (size=225, cost=5972, time=0.787528, max=0.109015, total=19.7993, pending=8)
[101]: Open (size=183, cost=6917, time=0.817271, max=0.109015, total=19.9865, pending=8)
[100]: Open (size=211, cost=7069, time=0.852569, max=0.109015, total=20.2612, pending=8)
[00]: Open (size=247, cost=7493, time=1.04522, max=0.666158, total=26.4755, pending=8)
[000]: Open (size=247, cost=5253, time=1.07457, max=0.666158, total=26.636, pending=9)
[1110]: Open (size=335, cost=7548, time=1.29498, max=0.105685, total=26.9791, pending=9)
[11110]: Open (size=331, cost=7639, time=1.44972, max=0.10142, total=27.2769, pending=9)
[010]: Open (size=327, cost=7697, time=2.00025, max=0.666158, total=27.7148, pending=9)
[11111]: Open (size=527, cost=7716, time=1.31863, max=0.0637839, total=27.9306, pending=9)
[110]: Open (size=299, cost=7763, time=0.875427, max=0.09286, total=28.1867, pending=9)
[1100]: Open (size=346, cost=5450, time=1.03891, max=0.163483, total=28.5713, pending=10)
[1101]: Open (size=332, cost=6265, time=0.910875, max=0.09286, total=29.1479, pending=10)
[1100]: Open (size=299, cost=6462, time=1.39941, max=0.163483, total=29.3144, pending=10)
[1101]: Open (size=332, cost=6851, time=0.937697, max=0.09286, total=29.5825, pending=10)
[11011]: Open (size=470, cost=805, time=0.9717, max=0.09286, total=29.7487, pending=11)
[1100]: Open (size=299, cost=7013, time=1.50344, max=0.163483, total=30.5039, pending=11)
[11010]: Open (size=332, cost=7492, time=0.96554, max=0.09286, total=31.2169, pending=11)
[11011]: Open (size=391, cost=7505, time=1.33222, max=0.09286, total=31.4205, pending=11)
[1100]: Open (size=346, cost=7538, time=1.84817, max=0.163483, total=31.7227, pending=11)
[101]: Open (size=197, cost=7906, time=0.869846, max=0.109015, total=37.598, pending=11)
[11110]: Open (size=468, cost=7909, time=1.54861, max=0.10142, total=37.831, pending=11)
[101]: Open (size=205, cost=7981, time=0.895569, max=0.109015, total=41.2858, pending=11)
[1100]: Open (size=347, cost=8061, time=2.19656, max=0.19595, total=42.1659, pending=11)
[11001]: Open (size=355, cost=7421, time=2.3367, max=0.19595, total=42.6874, pending=12)
[11000]: Open (size=345, cost=7704, time=2.3674, max=0.19595, total=43.5984, pending=12)
[11001]: Open (size=355, cost=7797, time=2.85309, max=0.257603, total=44.0819, pending=12)
[001]: Open (size=247, cost=8095, time=1.07533, max=0.666158, total=44.6945, pending=12)
[11110]: Open (size=468, cost=8118, time=1.58916, max=0.10142, total=44.849, pending=12)
[11000]: Open (size=345, cost=8136, time=2.61571, max=0.248307, total=45.0834, pending=12)
[11001]: Open (size=355, cost=8194, time=3.10361, max=0.257603, total=45.4687, pending=12)
[11010]: Open (size=332, cost=8276, time=0.997547, max=0.09286, total=45.917, pending=12)
[1110]: Open (size=307, cost=8323, time=1.37115, max=0.105685, total=46.1377, pending=12)
[010]: Open (size=315, cost=8353, time=2.03307, max=0.666158, total=46.5316, pending=12)
[100]: Open (size=237, cost=8382, time=1.2924, max=0.180243, total=46.7819, pending=12)
[11000]: Open (size=345, cost=8400, time=2.7476, max=0.248307, total=47.065, pending=12)
[001]: Open (size=247, cost=8405, time=1.10132, max=0.666158, total=47.4838, pending=12)
[11000]: Open (size=345, cost=8595, time=2.88724, max=0.248307, total=47.674, pending=12)
[11110]: Open (size=468, cost=8614, time=1.62545, max=0.10142, total=48.1228, pending=12)
[1110]: Open (size=397, cost=8662, time=1.43985, max=0.105685, total=48.3903, pending=12)
[11010]: Open (size=332, cost=8805, time=1.03036, max=0.09286, total=48.6453, pending=12)
[000]: Open (size=247, cost=8993, time=1.18432, max=0.666158, total=49.8888, pending=12)
[11010]: Open (size=307, cost=8998, time=1.30909, max=0.09286, total=50.0952, pending=12)
[101]: Open (size=200, cost=9131, time=1.19331, max=0.109015, total=50.5001, pending=12)
[011]: Open (size=449, cost=9189, time=1.55501, max=0.666158, total=50.9083, pending=12)
[1110]: Open (size=349, cost=9290, time=1.47686, max=0.105685, total=51.1148, pending=12)
[11010]: Open (size=310, cost=9395, time=1.35244, max=0.09286, total=51.394, pending=12)
[11011]: Open (size=383, cost=9467, time=1.36925, max=0.09286, total=51.9421, pending=12)
[101]: Open (size=210, cost=9498, time=1.22793, max=0.109015, total=52.3274, pending=12)
[000]: Open (size=241, cost=9511, time=1.21631, max=0.666158, total=52.6786, pending=12)
[11110]: Open (size=468, cost=9562, time=1.66505, max=0.10142, total=52.9185, pending=12)
[11010]: Open (size=332, cost=9617, time=1.42617, max=0.09286, total=53.3315, pending=12)
[11001]: Open (size=355, cost=9655, time=3.24078, max=0.257603, total=57.1981, pending=12)
[100]: Open (size=237, cost=9656, time=1.3422, max=0.180243, total=57.7471, pending=12)
[101]: Open (size=281, cost=9783, time=1.26535, max=0.109015, total=58.1308, pending=12)
[11110]: Open (size=386, cost=9804, time=1.75138, max=0.10142, total=58.4348, pending=12)
[11111]: Open (size=477, cost=9933, time=1.36541, max=0.0637839, total=58.9721, pending=12)
[1110]: Open (size=349, cost=10031, time=1.51457, max=0.105685, total=59.2949, pending=12)
[11100]: Open (size=412, cost=5467, time=1.71578, max=0.201208, total=59.8277, pending=13)
[111001]: Open (size=408, cost=4973, time=2.25224, max=0.237044, total=60.8116, pending=14)
[111000]: Open (size=398, cost=5531, time=2.21811, max=0.202912, total=67.2726, pending=14)
[111001]: Open (size=390, cost=5662, time=3.23761, max=0.320462, total=72.82, pending=14)
[111000]: Open (size=378, cost=5842, time=2.42763, max=0.20952, total=73.2706, pending=14)
[111001]: Open (size=391, cost=5987, time=3.49721, max=0.320462, total=73.6666, pending=14)
[111000]: Open (size=378, cost=6294, time=2.64137, max=0.213739, total=74.1152, pending=14)
[111001]: Open (size=382, cost=6308, time=3.72549, max=0.320462, total=76.0177, pending=14)
[11101]: Open (size=394, cost=8793, time=1.57254, max=0.105685, total=77.9685, pending=14)
[111001]: Open (size=371, cost=9760, time=4.94264, max=0.320462, total=78.363, pending=14)
[11101]: Open (size=394, cost=9837, time=1.64565, max=0.105685, total=78.9974, pending=14)
[11000]: Open (size=345, cost=10063, time=3.01214, max=0.248307, total=79.2428, pending=14)
[11110]: Open (size=459, cost=10097, time=1.8432, max=0.10142, total=79.686, pending=14)
[100]: Open (size=296, cost=10393, time=1.38423, max=0.180243, total=80.034, pending=14)
[11001]: Open (size=355, cost=10477, time=3.41163, max=0.257603, total=80.3502, pending=14)
[111001]: Open (size=371, cost=10477, time=5.17716, max=0.320462, total=80.9757, pending=14)
[100]: Open (size=284, cost=10512, time=1.43067, max=0.180243, total=81.8923, pending=14)
[11010]: Open (size=376, cost=10535, time=2.52147, max=0.09286, total=82.2645, pending=14)
[001]: Open (size=247, cost=10737, time=1.12541, max=0.666158, total=82.7495, pending=14)
[101]: Open (size=254, cost=10746, time=1.31007, max=0.109015, total=82.9762, pending=14)
[1010]: Open (size=264, cost=8491, time=1.36171, max=0.109015, total=83.4371, pending=15)
[1011]: Open (size=250, cost=10479, time=1.34802, max=0.109015, total=84.0006, pending=15)
[1010]: Open (size=228, cost=10575, time=1.45756, max=0.109015, total=84.4165, pending=15)
[111001]: Open (size=398, cost=10773, time=5.40617, max=0.320462, total=85.9462, pending=15)
[11001]: Open (size=400, cost=10838, time=3.53334, max=0.257603, total=86.6341, pending=15)
[11010]: Open (size=360, cost=10863, time=2.56974, max=0.09286, total=87.2539, pending=15)
[110100]: Open (size=410, cost=6296, time=2.63785, max=0.09286, total=88.062, pending=16)
[1011]: Open (size=325, cost=10984, time=1.38995, max=0.109015, total=92.7295, pending=16)
[10111]: Open (size=318, cost=8221, time=1.49026, max=0.109015, total=93.2409, pending=17)
[11110]: Open (size=410, cost=10988, time=1.89588, max=0.10142, total=93.8256, pending=17)
[110101]: Open (size=368, cost=10989, time=2.62395, max=0.09286, total=99.8015, pending=17)
[110100]: Open (size=497, cost=11098, time=3.48484, max=0.09286, total=100.519, pending=17)
[1101001]: Open (size=683, cost=1716, time=3.62753, max=0.14269, total=101.351, pending=18)
[111001]: Open (size=388, cost=11141, time=5.62654, max=0.320462, total=134.532, pending=18)
[110101]: Open (size=482, cost=11173, time=2.68605, max=0.09286, total=135.255, pending=18)
[1101011]: Open (size=475, cost=9749, time=2.73908, max=0.09286, total=135.835, pending=19)
[000]: Open (size=233, cost=11227, time=1.24724, max=0.666158, total=137.36, pending=19)
[11001]: Open (size=399, cost=11241, time=3.72401, max=0.257603, total=137.711, pending=19)
[011]: Open (size=331, cost=11247, time=1.58939, max=0.666158, total=138.3, pending=19)
[001]: Open (size=241, cost=11275, time=1.14939, max=0.666158, total=138.875, pending=19)
[011]: Open (size=349, cost=11297, time=1.7039, max=0.666158, total=139.18, pending=19)
[11110]: Open (size=490, cost=11308, time=2.09256, max=0.152716, total=139.627, pending=19)
[10111]: Open (size=226, cost=11329, time=1.6105, max=0.109015, total=140.026, pending=19)
[011]: Open (size=545, cost=11379, time=1.74352, max=0.666158, total=140.964, pending=19)
[000]: Open (size=307, cost=11393, time=1.28241, max=0.666158, total=141.269, pending=19)
[1101011]: Open (size=558, cost=11449, time=2.96291, max=0.09286, total=141.549, pending=19)
[1010]: Open (size=367, cost=11487, time=1.67489, max=0.109015, total=142.135, pending=19)
[1101000]: Open (size=495, cost=11661, time=3.5798, max=0.0949581, total=142.633, pending=19)
[11110]: Open (size=490, cost=11685, time=2.15807, max=0.152716, total=143.618, pending=19)
[10111]: Open (size=341, cost=11757, time=1.73305, max=0.109015, total=149.697, pending=19)
[011]: Open (size=545, cost=11807, time=1.7829, max=0.666158, total=151.107, pending=19)
[1101001]: Open (size=704, cost=12019, time=8.75587, max=0.232695, total=151.597, pending=19)
[1101010]: Open (size=472, cost=12031, time=2.74465, max=0.09286, total=158.234, pending=19)
[11110]: Open (size=456, cost=12064, time=2.38685, max=0.152716, total=158.99, pending=19)
[10110]: Open (size=302, cost=12072, time=1.42805, max=0.109015, total=159.458, pending=19)
[101101]: Open (size=324, cost=5557, time=1.5032, max=0.109015, total=159.863, pending=20)
[1011011]: Open (size=507, cost=6782, time=2.06371, max=0.11601, total=161.899, pending=21)
[1011010]: Open (size=503, cost=6811, time=2.10585, max=0.158146, total=162.298, pending=21)
[1011011]: Open (size=507, cost=7777, time=2.13591, max=0.11601, total=167.715, pending=21)
[11111]: Open (size=383, cost=12109, time=1.41072, max=0.0637839, total=168.767, pending=21)
[11011]: Open (size=375, cost=12233, time=1.40709, max=0.09286, total=170.481, pending=21)
[1101011]: Open (size=556, cost=12273, time=3.02245, max=0.09286, total=170.938, pending=21)
[1101000]: Open (size=483, cost=12328, time=3.65168, max=0.0949581, total=171.562, pending=21)
[1101010]: Open (size=587, cost=12346, time=2.80353, max=0.09286, total=172.639, pending=21)
[11010100]: Open (size=474, cost=12305, time=2.91029, max=0.10676, total=173.356, pending=22)
[1010]: Open (size=340, cost=12377, time=1.72639, max=0.109015, total=174.024, pending=22)
[001]: Open (size=283, cost=12413, time=1.17753, max=0.666158, total=174.589, pending=22)
[100]: Open (size=284, cost=12583, time=1.4787, max=0.180243, total=174.858, pending=22)
[011]: Open (size=535, cost=12595, time=1.8677, max=0.666158, total=175.412, pending=22)
[11111]: Open (size=602, cost=12597, time=1.70485, max=0.0637839, total=175.79, pending=22)
[11010101]: Open (size=468, cost=12607, time=2.86228, max=0.09286, total=176.265, pending=22)
[000]: Open (size=267, cost=12773, time=1.31328, max=0.666158, total=176.937, pending=22)
[0001]: Open (size=321, cost=7305, time=4.01369, max=2.70041, total=180.035, pending=23)
[0000]: Open (size=321, cost=12855, time=1.4054, max=0.666158, total=194.45, pending=23)
[1010]: Open (size=335, cost=12868, time=1.78023, max=0.109015, total=194.925, pending=23)
[10100]: Open (size=550, cost=3483, time=4.98144, max=0.318228, total=204.133, pending=24)
[10101]: Open (size=550, cost=4149, time=4.98821, max=0.324994, total=205.282, pending=24)
[10100]: Open (size=480, cost=4681, time=5.54014, max=0.318228, total=206.974, pending=24)
[10101]: Open (size=482, cost=4992, time=5.89425, max=0.337867, total=207.768, pending=24)
[10100]: Open (size=450, cost=5517, time=5.81697, max=0.318228, total=209.236, pending=24)
[10101]: Open (size=440, cost=5820, time=6.47698, max=0.337867, total=210.193, pending=24)
[10100]: Open (size=420, cost=6226, time=6.11124, max=0.318228, total=212.486, pending=24)
[10101]: Open (size=384, cost=6227, time=7.32932, max=0.337867, total=213.549, pending=24)
[10100]: Open (size=420, cost=6852, time=6.39964, max=0.318228, total=214.909, pending=24)
[10101]: Open (size=348, cost=7354, time=7.62791, max=0.337867, total=216.735, pending=24)
[10100]: Open (size=334, cost=8646, time=6.97814, max=0.318228, total=219.091, pending=24)
[10101]: Open (size=326, cost=9987, time=8.21222, max=0.337867, total=221.62, pending=24)
******* COMPLETION *******
double_divide(double_divide(double_divide(C15,inverse(A0)),A26),A0) -> double_divide(inverse(A26),C15)
double_divide(A0,double_divide(C13,A13)) -> double_divide(double_divide(A13,inverse(A0)),inverse(C13))
double_divide(double_divide(C1,A0),C1) -> A0
double_divide(inverse(A0),A0) -> identity
inverse(inverse(A0)) -> A0
double_divide(identity,A0) -> inverse(A0)
inverse(identity) -> identity
multiply(A0,B0) -> double_divide(inverse(A0),inverse(B0))
double_divide(A0,inverse(A0)) -> identity
double_divide(A0,identity) -> inverse(A0)
inverse(double_divide(B5,A0)) -> double_divide(inverse(A0),inverse(B5))
double_divide(double_divide(double_divide(C1,A0),A12),inverse(A0)) -> double_divide(inverse(A12),C1)
**************************
On branch: [10101]
With size, cost: 86, 1235
Orientations: 1144
Calls to AProVE (all, T, NT, ?): 622, 586, 28, 8
Time (all, branch, AProVE): 241.107, 12.2842, 116.551
Time/call in AProVE (Avg, Min, Max): 0.18738, 5.34326, 0.013679
Time/T-call in AProVE (Avg, Min, Max): 0.103026, 2.86519, 0.443825
All conjectures solved.