[]: Open (size=25, cost=0, time=0, max=0, total=7.86781e-06, pending=1)
[0]: Open (size=25, cost=25, time=0.735087, max=0.607327, total=0.767676, pending=1)
[1]: Open (size=25, cost=25, time=0.726743, max=0.607327, total=0.831189, pending=2)
[00]: Open (size=25, cost=59, time=0.766081, max=0.607327, total=0.908617, pending=3)
[10]: Open (size=25, cost=59, time=0.761232, max=0.607327, total=0.975006, pending=3)
[01]: Open (size=25, cost=115, time=0.766682, max=0.607327, total=1.05136, pending=3)
[11]: Open (size=25, cost=115, time=0.768678, max=0.607327, total=1.17828, pending=3)
[00]: Open (size=66, cost=119, time=0.83089, max=0.607327, total=1.30078, pending=3)
[10]: Open (size=66, cost=119, time=0.836157, max=0.607327, total=1.38367, pending=4)
[001]: Open (size=56, cost=131, time=0.876368, max=0.607327, total=1.49853, pending=5)
[000]: Open (size=56, cost=131, time=0.867299, max=0.607327, total=1.90678, pending=5)
[100]: Open (size=56, cost=131, time=0.888723, max=0.607327, total=1.99174, pending=5)
[101]: Open (size=56, cost=131, time=0.897369, max=0.607327, total=2.08144, pending=5)
[100]: Open (size=90, cost=141, time=0.975848, max=0.607327, total=2.34798, pending=5)
[000]: Open (size=90, cost=141, time=0.949532, max=0.607327, total=2.43787, pending=5)
[001]: Open (size=88, cost=163, time=1.2799, max=0.607327, total=2.53167, pending=5)
[101]: Open (size=88, cost=163, time=1.15887, max=0.607327, total=2.58995, pending=5)
[100]: Open (size=88, cost=174, time=1.06255, max=0.607327, total=2.64965, pending=5)
[000]: Open (size=88, cost=174, time=1.03992, max=0.607327, total=2.72138, pending=5)
[01]: Open (size=94, cost=179, time=0.890741, max=0.607327, total=2.86496, pending=5)
[11]: Open (size=94, cost=179, time=0.888067, max=0.607327, total=2.94483, pending=5)
[01]: Open (size=94, cost=327, time=0.958224, max=0.607327, total=3.04581, pending=5)
[11]: Open (size=94, cost=327, time=0.984661, max=0.607327, total=3.27578, pending=6)
[010]: Open (size=75, cost=376, time=1.07255, max=0.607327, total=3.52349, pending=7)
[110]: Open (size=75, cost=376, time=1.08043, max=0.607327, total=3.64581, pending=7)
[010]: Open (size=112, cost=379, time=1.17312, max=0.607327, total=3.67939, pending=7)
[110]: Open (size=112, cost=379, time=1.10517, max=0.607327, total=3.85307, pending=7)
[111]: Open (size=75, cost=421, time=1.12585, max=0.607327, total=3.94192, pending=7)
[011]: Open (size=75, cost=421, time=1.06717, max=0.607327, total=3.9954, pending=7)
[111]: Open (size=112, cost=424, time=1.17082, max=0.607327, total=4.06577, pending=7)
[011]: Open (size=112, cost=424, time=1.12922, max=0.607327, total=9.51485, pending=7)
[010]: Open (size=172, cost=439, time=1.33012, max=0.607327, total=15.3098, pending=7)
[110]: Open (size=172, cost=439, time=1.17681, max=0.607327, total=15.3482, pending=7)
[011]: Open (size=170, cost=450, time=1.42691, max=0.607327, total=15.3817, pending=7)
[111]: Open (size=170, cost=450, time=1.42556, max=0.607327, total=15.4233, pending=7)
[001]: Open (size=77, cost=499, time=1.33012, max=0.607327, total=15.4658, pending=7)
[101]: Open (size=77, cost=499, time=1.21041, max=0.607327, total=15.561, pending=7)
[100]: Open (size=77, cost=501, time=1.12681, max=0.607327, total=15.633, pending=7)
[000]: Open (size=77, cost=501, time=1.17401, max=0.607327, total=15.7128, pending=7)
[001]: Open (size=145, cost=534, time=1.40382, max=0.607327, total=15.7936, pending=7)
[101]: Open (size=145, cost=534, time=1.25353, max=0.607327, total=15.9033, pending=7)
[000]: Open (size=156, cost=567, time=1.22957, max=0.607327, total=16.0259, pending=7)
[100]: Open (size=156, cost=567, time=1.18063, max=0.607327, total=16.1269, pending=7)
[101]: Open (size=110, cost=702, time=1.34915, max=0.607327, total=16.2109, pending=7)
[001]: Open (size=110, cost=702, time=1.48754, max=0.607327, total=16.2589, pending=7)
[100]: Open (size=121, cost=735, time=1.22821, max=0.607327, total=16.3069, pending=7)
[000]: Open (size=121, cost=735, time=1.2948, max=0.607327, total=16.3575, pending=7)
[110]: Open (size=149, cost=805, time=1.1929, max=0.607327, total=16.4161, pending=7)
[010]: Open (size=149, cost=805, time=1.35081, max=0.607327, total=16.4762, pending=7)
[011]: Open (size=158, cost=894, time=1.44847, max=0.607327, total=16.5357, pending=7)
[111]: Open (size=158, cost=894, time=1.44796, max=0.607327, total=16.6047, pending=7)
[101]: Open (size=125, cost=980, time=1.36924, max=0.607327, total=16.6676, pending=7)
[001]: Open (size=125, cost=980, time=1.50795, max=0.607327, total=16.9789, pending=8)
[100]: Open (size=136, cost=1003, time=1.24366, max=0.607327, total=17.1887, pending=9)
[1001]: Open (size=226, cost=963, time=1.26484, max=0.607327, total=17.2901, pending=10)
[000]: Open (size=136, cost=1003, time=1.31974, max=0.607327, total=17.3425, pending=10)
[0001]: Open (size=226, cost=963, time=1.34076, max=0.607327, total=17.4538, pending=11)
[1011]: Open (size=239, cost=1016, time=1.41447, max=0.607327, total=17.511, pending=11)
[0011]: Open (size=239, cost=1016, time=1.5352, max=0.607327, total=17.5634, pending=11)
[1001]: Open (size=220, cost=1111, time=1.28332, max=0.607327, total=17.6162, pending=11)
[0001]: Open (size=220, cost=1111, time=1.36542, max=0.607327, total=17.7034, pending=11)
[0011]: Open (size=217, cost=1177, time=1.55801, max=0.607327, total=17.7744, pending=11)
[00110]: Open (size=194, cost=1084, time=1.60289, max=0.607327, total=17.9028, pending=12)
[001101]: Open (size=189, cost=1146, time=1.69475, max=0.607327, total=18.0975, pending=13)
[1011]: Open (size=217, cost=1177, time=1.43736, max=0.607327, total=18.2391, pending=13)
[10110]: Open (size=194, cost=1084, time=1.49246, max=0.607327, total=18.4108, pending=14)
[101101]: Open (size=189, cost=1146, time=1.5183, max=0.607327, total=18.5251, pending=15)
[0000]: Open (size=244, cost=1178, time=1.36971, max=0.607327, total=18.5986, pending=15)
[1000]: Open (size=244, cost=1178, time=1.28468, max=0.607327, total=18.6714, pending=15)
[0000]: Open (size=247, cost=1248, time=1.41027, max=0.607327, total=18.7385, pending=15)
[1000]: Open (size=247, cost=1248, time=1.32061, max=0.607327, total=19.0655, pending=15)
[1010]: Open (size=281, cost=1249, time=1.60417, max=0.607327, total=19.3778, pending=15)
[0010]: Open (size=281, cost=1249, time=1.65986, max=0.607327, total=19.5242, pending=15)
[10111]: Open (size=209, cost=1255, time=1.52284, max=0.607327, total=19.6988, pending=15)
[00111]: Open (size=209, cost=1255, time=1.62713, max=0.607327, total=19.8159, pending=15)
[010]: Open (size=149, cost=1278, time=1.37181, max=0.607327, total=19.8961, pending=15)
[110]: Open (size=149, cost=1278, time=1.21781, max=0.607327, total=19.9743, pending=15)
[10111]: Open (size=212, cost=1378, time=1.59777, max=0.607327, total=20.053, pending=15)
[101111]: Open (size=210, cost=1223, time=1.70885, max=0.607327, total=20.291, pending=16)
[00111]: Open (size=212, cost=1378, time=1.67459, max=0.607327, total=20.4597, pending=16)
[001111]: Open (size=210, cost=1223, time=1.83097, max=0.607327, total=20.7943, pending=17)
[001100]: Open (size=207, cost=1380, time=1.66518, max=0.607327, total=20.9147, pending=17)
[101100]: Open (size=207, cost=1380, time=1.5494, max=0.607327, total=21.0023, pending=17)
[111]: Open (size=119, cost=1419, time=1.47567, max=0.607327, total=21.0759, pending=17)
[011]: Open (size=119, cost=1419, time=1.47662, max=0.607327, total=21.1557, pending=17)
[1010]: Open (size=288, cost=1439, time=1.70354, max=0.607327, total=21.2435, pending=17)
[0010]: Open (size=288, cost=1439, time=1.80072, max=0.607327, total=21.4582, pending=17)
[001100]: Open (size=210, cost=1453, time=1.71883, max=0.607327, total=21.625, pending=17)
[101100]: Open (size=210, cost=1453, time=1.58945, max=0.607327, total=21.8943, pending=17)
[111]: Open (size=246, cost=1504, time=1.49582, max=0.607327, total=22.1876, pending=17)
[011]: Open (size=246, cost=1504, time=1.49885, max=0.607327, total=22.3345, pending=17)
[101110]: Open (size=210, cost=1513, time=1.73523, max=0.607327, total=22.4057, pending=17)
[001110]: Open (size=210, cost=1513, time=1.87989, max=0.607327, total=22.6796, pending=17)
[0000]: Open (size=186, cost=1525, time=1.62632, max=0.607327, total=22.948, pending=17)
[1000]: Open (size=186, cost=1525, time=1.50831, max=0.607327, total=23.5281, pending=17)
[0000]: Open (size=170, cost=1561, time=1.81473, max=0.607327, total=23.9761, pending=17)
[1000]: Open (size=170, cost=1561, time=1.6477, max=0.607327, total=24.3014, pending=17)
[1001]: Open (size=183, cost=1591, time=1.3134, max=0.607327, total=24.7341, pending=17)
[10010]: Open (size=176, cost=295, time=1.62079, max=0.607327, total=25.4215, pending=18)
******* COMPLETION *******
inverse(multiply(X0,Y0)) -> multiply(inverse(Y0),inverse(X0))
d -> b
multiply(X2,inverse(X2)) -> identity
inverse(inverse(X0)) -> X0
inverse(identity) -> identity
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
multiply(X0,identity) -> X0
multiply(X0,multiply(inverse(X0),Z3)) -> Z3
**************************
On branch: [10010]
With size, cost: 60, 179
Orientations: 328
Calls to AProVE (all, T, NT, ?): 193, 180, 11, 2
Time (all, branch, AProVE): 25.4238, 1.62079, 21.4199
Time/call in AProVE (Avg, Min, Max): 0.110984, 5.46461, 0.014081
Time/T-call in AProVE (Avg, Min, Max): 0.0542824, 0.607132, 0.607327
All conjectures solved.