[]: Open (size=19, cost=0, time=0, max=0, total=1.21593e-05, pending=1)
[1]: Open (size=19, cost=65, time=0.729661, max=0.616392, total=0.755405, pending=1)
[0]: Open (size=19, cost=81, time=0.733577, max=0.616392, total=0.917366, pending=1)
[1]: Open (size=63, cost=126, time=0.888709, max=0.616392, total=1.03834, pending=1)
[0]: Open (size=73, cost=183, time=0.85236, max=0.616392, total=1.15329, pending=1)
[1]: Open (size=57, cost=237, time=0.999005, max=0.616392, total=1.19118, pending=1)
[10]: Open (size=122, cost=166, time=1.03839, max=0.616392, total=1.27141, pending=2)
[0]: Open (size=71, cost=246, time=0.88846, max=0.616392, total=1.47361, pending=2)
[00]: Open (size=91, cost=242, time=0.944072, max=0.616392, total=1.6034, pending=3)
[11]: Open (size=122, cost=251, time=1.0367, max=0.616392, total=1.65878, pending=3)
[01]: Open (size=91, cost=267, time=0.959936, max=0.616392, total=1.72188, pending=3)
[10]: Open (size=122, cost=273, time=1.23829, max=0.616392, total=1.79713, pending=3)
[101]: Open (size=107, cost=187, time=1.36312, max=0.616392, total=2.01472, pending=4)
[01]: Open (size=85, cost=328, time=1.03193, max=0.616392, total=2.09009, pending=4)
[101]: Open (size=76, cost=355, time=1.42508, max=0.616392, total=2.15207, pending=4)
[100]: Open (size=107, cost=381, time=1.40042, max=0.616392, total=2.33936, pending=4)
[00]: Open (size=66, cost=386, time=0.994721, max=0.616392, total=2.47512, pending=4)
[001]: Open (size=79, cost=389, time=1.18434, max=0.616392, total=2.77598, pending=5)
[101]: Open (size=140, cost=471, time=1.56437, max=0.616392, total=3.11814, pending=5)
[11]: Open (size=89, cost=487, time=1.09228, max=0.616392, total=3.21204, pending=5)
[000]: Open (size=79, cost=536, time=1.18026, max=0.616392, total=3.34152, pending=5)
[11]: Open (size=102, cost=547, time=1.19946, max=0.616392, total=3.46091, pending=5)
[111]: Open (size=102, cost=368, time=1.31881, max=0.616392, total=3.63904, pending=6)
[110]: Open (size=102, cost=493, time=1.24577, max=0.616392, total=3.81635, pending=6)
[101]: Open (size=94, cost=578, time=1.63179, max=0.616392, total=3.90277, pending=6)
[110]: Open (size=145, cost=579, time=1.29723, max=0.616392, total=3.97839, pending=6)
[000]: Open (size=72, cost=579, time=1.28929, max=0.616392, total=4.07485, pending=6)
[01]: Open (size=85, cost=601, time=1.08619, max=0.616392, total=4.1735, pending=6)
[011]: Open (size=90, cost=408, time=1.21982, max=0.616392, total=4.40335, pending=7)
[111]: Open (size=106, cost=644, time=1.46095, max=0.616392, total=4.79854, pending=7)
[001]: Open (size=85, cost=664, time=1.49023, max=0.616392, total=5.12958, pending=7)
[101]: Open (size=176, cost=684, time=1.67902, max=0.616392, total=5.22655, pending=7)
[111]: Open (size=107, cost=687, time=1.72113, max=0.616392, total=5.27601, pending=7)
[001]: Open (size=95, cost=687, time=1.55787, max=0.616392, total=5.35171, pending=7)
[100]: Open (size=107, cost=694, time=1.49423, max=0.616392, total=5.39157, pending=7)
[111]: Open (size=115, cost=705, time=1.75133, max=0.616392, total=5.4753, pending=7)
[100]: Open (size=107, cost=707, time=1.5313, max=0.616392, total=5.55124, pending=7)
[001]: Open (size=282, cost=724, time=1.57692, max=0.616392, total=5.60988, pending=7)
[101]: Open (size=154, cost=728, time=1.70115, max=0.616392, total=5.65076, pending=7)
[010]: Open (size=90, cost=729, time=1.18661, max=0.616392, total=5.71977, pending=7)
[000]: Open (size=85, cost=739, time=1.36627, max=0.616392, total=5.83033, pending=7)
[100]: Open (size=117, cost=746, time=1.55546, max=0.616392, total=5.93087, pending=7)
[001]: Open (size=212, cost=759, time=1.59693, max=0.616392, total=5.99058, pending=7)
[000]: Open (size=212, cost=759, time=1.41852, max=0.616392, total=6.04431, pending=7)
[011]: Open (size=115, cost=769, time=1.53934, max=0.616392, total=6.1254, pending=7)
[111]: Open (size=136, cost=823, time=1.77313, max=0.616392, total=6.23154, pending=7)
[010]: Open (size=129, cost=854, time=1.25013, max=0.616392, total=6.33697, pending=7)
[110]: Open (size=124, cost=863, time=1.35915, max=0.616392, total=6.42635, pending=7)
[100]: Open (size=247, cost=869, time=1.57808, max=0.616392, total=6.81484, pending=7)
[011]: Open (size=244, cost=869, time=1.58377, max=0.616392, total=6.88008, pending=7)
[101]: Open (size=143, cost=969, time=1.73522, max=0.616392, total=6.96324, pending=7)
[110]: Open (size=212, cost=1094, time=1.57302, max=0.616392, total=7.04502, pending=7)
[111]: Open (size=212, cost=1094, time=1.79599, max=0.616392, total=7.13571, pending=7)
[011]: Open (size=154, cost=1144, time=1.62499, max=0.616392, total=7.22295, pending=7)
[010]: Open (size=130, cost=1145, time=1.29225, max=0.616392, total=7.78738, pending=7)
[100]: Open (size=247, cost=1152, time=1.60136, max=0.616392, total=7.90256, pending=7)
[001]: Open (size=165, cost=1157, time=1.6188, max=0.616392, total=7.98175, pending=7)
[0010]: Open (size=198, cost=274, time=1.63334, max=0.616392, total=8.06904, pending=8)
******* COMPLETION *******
i(f(Y0,Z0)) -> f(i(Z0),i(Y0))
i(i(X1)) -> f(e,X1)
f(f(X1,i(X0)),X0) -> X1
f(X0,f(Y0,Z0)) -> f(f(X0,Y0),Z0)
i(e) -> e
f(X0,e) -> X0
f(i(X0),X0) -> e
f(f(X3,X1),i(X1)) -> X3
f(e,i(X0)) -> i(X0)
**************************
On branch: [0010]
With size, cost: 57, 133
Orientations: 192
Calls to AProVE (all, T, NT, ?): 105, 104, 1, 0
Time (all, branch, AProVE): 8.07116, 1.63334, 6.01127
Time/call in AProVE (Avg, Min, Max): 0.0572502, 0.616207, 0.0139151
Time/T-call in AProVE (Avg, Min, Max): 0.0537613, 0.616207, 0.616392
All conjectures solved.