[]: Open (size=38, cost=0, time=0, max=0, total=1.00136e-05, pending=1)
[0]: Open (size=38, cost=38, time=0.714443, max=0.714443, total=0.737964, pending=1)
[1]: Open (size=38, cost=38, time=0.023145, max=0.023145, total=0.773792, pending=1)
[10]: Open (size=37, cost=37, time=0.0785329, max=0.038691, total=0.85422, pending=2)
[0]: Open (size=39, cost=39, time=0.750014, max=0.714443, total=0.916574, pending=2)
[00]: Open (size=39, cost=39, time=0.813257, max=0.714443, total=1.03774, pending=3)
[11]: Open (size=37, cost=77, time=0.064455, max=0.0246131, total=1.10292, pending=3)
[01]: Open (size=39, cost=101, time=0.807501, max=0.714443, total=1.16967, pending=3)
[10]: Open (size=30, cost=176, time=0.139928, max=0.0613952, total=1.21742, pending=3)
[11]: Open (size=30, cost=331, time=0.129518, max=0.065063, total=1.41943, pending=3)
[110]: Open (size=56, cost=224, time=0.181294, max=0.065063, total=1.52938, pending=4)
[111]: Open (size=56, cost=370, time=0.21085, max=0.065063, total=1.73225, pending=4)
[110]: Open (size=214, cost=401, time=0.375794, max=0.0811231, total=1.82365, pending=4)
[00]: Open (size=35, cost=427, time=0.876388, max=0.714443, total=1.88448, pending=4)
[111]: Open (size=50, cost=440, time=0.299336, max=0.088486, total=2.02853, pending=4)
[1110]: Open (size=74, cost=411, time=0.346849, max=0.088486, total=2.10927, pending=5)
[110]: Open (size=213, cost=541, time=0.433321, max=0.0811231, total=2.95864, pending=5)
[1110]: Open (size=307, cost=562, time=0.68459, max=0.088486, total=3.05994, pending=5)
[1111]: Open (size=74, cost=562, time=0.34891, max=0.088486, total=3.15932, pending=5)
[11111]: Open (size=75, cost=582, time=0.415972, max=0.088486, total=3.33942, pending=6)
[11110]: Open (size=74, cost=626, time=0.448522, max=0.099612, total=3.65262, pending=6)
[11111]: Open (size=102, cost=671, time=0.712677, max=0.109309, total=3.78521, pending=6)
[01]: Open (size=35, cost=673, time=0.852146, max=0.714443, total=3.8448, pending=6)
[11110]: Open (size=110, cost=682, time=0.560635, max=0.099612, total=3.94702, pending=7)
[110]: Open (size=201, cost=685, time=0.529051, max=0.0957298, total=4.76908, pending=7)
[010]: Open (size=61, cost=685, time=0.921597, max=0.714443, total=4.89337, pending=7)
[10]: Open (size=93, cost=698, time=0.336878, max=0.114419, total=4.96833, pending=7)
[1110]: Open (size=306, cost=728, time=0.779038, max=0.0944481, total=4.99732, pending=7)
[11110]: Open (size=460, cost=734, time=1.28807, max=0.154819, total=5.0322, pending=7)
[010]: Open (size=81, cost=781, time=0.980385, max=0.714443, total=5.08611, pending=7)
[011]: Open (size=61, cost=809, time=0.917512, max=0.714443, total=5.17133, pending=7)
[11111]: Open (size=102, cost=824, time=0.761059, max=0.109309, total=5.21549, pending=7)
[11110]: Open (size=458, cost=874, time=1.33015, max=0.154819, total=5.51962, pending=7)
[11111]: Open (size=197, cost=895, time=0.997189, max=0.109309, total=5.57977, pending=7)
[011]: Open (size=91, cost=907, time=0.952492, max=0.714443, total=5.64674, pending=7)
[1110]: Open (size=294, cost=920, time=0.806368, max=0.0944481, total=5.6742, pending=7)
[00]: Open (size=179, cost=931, time=1.01346, max=0.714443, total=5.71492, pending=7)
[011]: Open (size=91, cost=993, time=0.969856, max=0.714443, total=5.74403, pending=7)
[110]: Open (size=170, cost=1062, time=0.642988, max=0.113937, total=5.81748, pending=7)
[11110]: Open (size=457, cost=1070, time=1.3757, max=0.154819, total=5.85208, pending=7)
[011]: Open (size=195, cost=1187, time=1.01573, max=0.714443, total=5.91775, pending=7)
[010]: Open (size=389, cost=1213, time=1.04885, max=0.714443, total=5.95963, pending=7)
[11111]: Open (size=173, cost=1220, time=1.03071, max=0.109309, total=5.99184, pending=7)
[1110]: Open (size=294, cost=1277, time=0.832676, max=0.0944481, total=6.29475, pending=7)
[11110]: Open (size=445, cost=1316, time=1.41849, max=0.154819, total=6.34913, pending=7)
[011]: Open (size=133, cost=1327, time=1.04013, max=0.714443, total=6.44678, pending=7)
[10]: Open (size=81, cost=1367, time=0.358349, max=0.114419, total=6.53824, pending=7)
[11111]: Open (size=229, cost=1515, time=1.18717, max=0.109309, total=6.58185, pending=7)
[010]: Open (size=389, cost=1573, time=1.07096, max=0.714443, total=7.01059, pending=7)
[1110]: Open (size=279, cost=1588, time=0.850565, max=0.0944481, total=7.05145, pending=7)
[110]: Open (size=170, cost=1656, time=0.661089, max=0.113937, total=7.09865, pending=7)
[011]: Open (size=167, cost=1663, time=1.097, max=0.714443, total=7.14596, pending=7)
[00]: Open (size=179, cost=1779, time=1.0312, max=0.714443, total=7.31845, pending=7)
[011]: Open (size=347, cost=1799, time=1.18938, max=0.714443, total=7.37461, pending=7)
[11110]: Open (size=445, cost=1853, time=1.47871, max=0.154819, total=7.46169, pending=7)
[11111]: Open (size=587, cost=1932, time=1.39585, max=0.109309, total=7.54674, pending=7)
[10]: Open (size=143, cost=1949, time=0.382447, max=0.114419, total=7.81976, pending=7)
[011]: Open (size=673, cost=2021, time=1.22412, max=0.714443, total=7.84975, pending=7)
[1110]: Open (size=279, cost=2172, time=0.870056, max=0.0944481, total=7.92672, pending=7)
[10]: Open (size=135, cost=2177, time=0.395376, max=0.114419, total=7.98559, pending=7)
[11110]: Open (size=430, cost=2238, time=1.52145, max=0.154819, total=8.02423, pending=7)
[10]: Open (size=129, cost=2477, time=0.412433, max=0.114419, total=8.11879, pending=7)
[110]: Open (size=170, cost=2510, time=0.682924, max=0.113937, total=8.16105, pending=7)
[010]: Open (size=375, cost=2601, time=1.09142, max=0.714443, total=8.21819, pending=7)
[011]: Open (size=671, cost=2739, time=1.25625, max=0.714443, total=8.27519, pending=7)
[11111]: Open (size=575, cost=2742, time=1.53846, max=0.109309, total=8.36406, pending=7)
[11110]: Open (size=430, cost=2860, time=1.55799, max=0.154819, total=8.55099, pending=7)
[10]: Open (size=116, cost=2876, time=0.42937, max=0.114419, total=8.69548, pending=7)
[1110]: Open (size=263, cost=2877, time=0.888913, max=0.0944481, total=9.59991, pending=7)
[10]: Open (size=263, cost=3077, time=0.930854, max=0.114419, total=9.71367, pending=7)
[101]: Open (size=138, cost=699, time=1.00437, max=0.114419, total=9.93826, pending=8)
[100]: Open (size=149, cost=725, time=1.06178, max=0.114419, total=9.98189, pending=8)
[101]: Open (size=112, cost=901, time=1.02853, max=0.114419, total=10.0461, pending=8)
[100]: Open (size=97, cost=1429, time=1.09218, max=0.114419, total=10.1159, pending=8)
[101]: Open (size=104, cost=1905, time=1.06144, max=0.114419, total=10.5152, pending=8)
[1010]: Open (size=165, cost=1631, time=1.15905, max=0.114419, total=10.7585, pending=9)
[100]: Open (size=167, cost=2133, time=1.27813, max=0.114419, total=16.196, pending=9)
[1010]: Open (size=165, cost=2256, time=1.23186, max=0.114419, total=16.6115, pending=9)
[1011]: Open (size=165, cost=2494, time=1.13893, max=0.114419, total=16.9043, pending=9)
[100]: Open (size=167, cost=2548, time=1.39522, max=0.117092, total=22.522, pending=9)
[1011]: Open (size=165, cost=3013, time=1.2093, max=0.114419, total=22.9894, pending=9)
[100]: Open (size=197, cost=3063, time=1.49071, max=0.117092, total=28.6186, pending=9)
[1011]: Open (size=231, cost=3188, time=1.26278, max=0.114419, total=29.4529, pending=9)
[100]: Open (size=227, cost=3380, time=1.6279, max=0.137188, total=35.136, pending=9)
[1011]: Open (size=231, cost=3404, time=1.33014, max=0.114419, total=35.5605, pending=9)
[11111]: Open (size=560, cost=3408, time=1.59959, max=0.109309, total=35.9358, pending=9)
[110]: Open (size=169, cost=3423, time=0.701895, max=0.113937, total=36.1254, pending=9)
[011]: Open (size=671, cost=3465, time=1.28921, max=0.714443, total=36.1965, pending=9)
[1010]: Open (size=151, cost=3535, time=1.35229, max=0.120434, total=36.3043, pending=9)
[110]: Open (size=256, cost=3626, time=0.714798, max=0.113937, total=36.4613, pending=9)
[1010]: Open (size=241, cost=3633, time=1.38426, max=0.120434, total=36.5259, pending=9)
[010]: Open (size=375, cost=3661, time=1.11469, max=0.714443, total=41.9119, pending=9)
[1011]: Open (size=377, cost=3686, time=1.36509, max=0.114419, total=41.9798, pending=9)
[10111]: Open (size=371, cost=1863, time=1.74165, max=0.376558, total=42.7567, pending=10)
[11110]: Open (size=414, cost=3711, time=1.62467, max=0.154819, total=43.7454, pending=10)
[100]: Open (size=227, cost=3763, time=1.65995, max=0.137188, total=43.8661, pending=10)
[10111]: Open (size=296, cost=3804, time=2.52916, max=0.376558, total=44.3599, pending=10)
[11110]: Open (size=404, cost=3824, time=1.66051, max=0.154819, total=44.7401, pending=10)
[10110]: Open (size=371, cost=4106, time=1.641, max=0.275903, total=44.8818, pending=10)
[1110]: Open (size=248, cost=4120, time=0.929439, max=0.0944481, total=45.2773, pending=10)
[100]: Open (size=257, cost=4123, time=1.69094, max=0.137188, total=45.3791, pending=10)
[11111]: Open (size=560, cost=4294, time=1.64275, max=0.109309, total=45.839, pending=10)
[010]: Open (size=375, cost=4363, time=1.13569, max=0.714443, total=46.0533, pending=10)
[110]: Open (size=256, cost=4368, time=0.728095, max=0.113937, total=46.145, pending=10)
[00]: Open (size=179, cost=4447, time=1.0577, max=0.714443, total=46.2614, pending=10)
[1010]: Open (size=217, cost=4474, time=1.44022, max=0.120434, total=46.3341, pending=10)
[10111]: Open (size=279, cost=4501, time=2.72827, max=0.376558, total=51.7732, pending=10)
[100]: Open (size=257, cost=4598, time=1.72373, max=0.137188, total=52.2225, pending=10)
[110]: Open (size=239, cost=4834, time=0.757088, max=0.113937, total=52.864, pending=10)
[011]: Open (size=657, cost=4859, time=1.32125, max=0.714443, total=52.9506, pending=10)
[100]: Open (size=457, cost=4953, time=1.75581, max=0.137188, total=53.091, pending=10)
[11110]: Open (size=399, cost=4996, time=1.69697, max=0.154819, total=53.6534, pending=10)
[10110]: Open (size=349, cost=5177, time=1.84152, max=0.275903, total=53.819, pending=10)
[1110]: Open (size=231, cost=5244, time=0.950766, max=0.0944481, total=54.2761, pending=10)
[100]: Open (size=457, cost=5279, time=1.78884, max=0.137188, total=54.4133, pending=10)
[1001]: Open (size=457, cost=1880, time=2.03743, max=0.248592, total=55.1559, pending=11)
[1000]: Open (size=457, cost=3178, time=1.95992, max=0.171081, total=62.0517, pending=11)
******* COMPLETION *******
double_divide(inverse(C2),double_divide(C21,double_divide(C2,C38))) -> double_divide(C38,inverse(C21))
double_divide(double_divide(C0,C17),B18) -> double_divide(inverse(C17),double_divide(inverse(B18),C0))
double_divide(C0,double_divide(A0,C0)) -> A0
double_divide(identity,B4) -> inverse(B4)
inverse(inverse(C2)) -> C2
double_divide(A0,identity) -> inverse(A0)
double_divide(A0,inverse(A0)) -> identity
multiply(A0,B0) -> double_divide(inverse(A0),inverse(B0))
inverse(identity) -> identity
double_divide(inverse(C2),C2) -> identity
inverse(double_divide(C2,C7)) -> double_divide(inverse(C7),inverse(C2))
double_divide(B37,double_divide(C2,double_divide(inverse(B37),C19))) -> double_divide(C19,inverse(C2))
**************************
On branch: [1000]
With size, cost: 86, 523
Orientations: 398
Calls to AProVE (all, T, NT, ?): 220, 210, 2, 8
Time (all, branch, AProVE): 69.5612, 3.84388, 56.7579
Time/call in AProVE (Avg, Min, Max): 0.25799, 5.42978, 0.011122
Time/T-call in AProVE (Avg, Min, Max): 0.0657886, 0.714229, 0.436865
All conjectures solved.