[]: Open (size=19, cost=0, time=0, max=0, total=1.19209e-05, pending=1)
[0]: Open (size=19, cost=65, time=0.728371, max=0.607426, total=0.754755, pending=1)
[1]: Open (size=19, cost=81, time=0.720525, max=0.607426, total=0.902889, pending=1)
[0]: Open (size=63, cost=126, time=0.873468, max=0.607426, total=0.992103, pending=1)
[1]: Open (size=73, cost=183, time=0.807595, max=0.607426, total=1.10132, pending=1)
[0]: Open (size=57, cost=237, time=0.977646, max=0.607426, total=1.13244, pending=1)
[00]: Open (size=130, cost=174, time=1.01497, max=0.607426, total=1.23907, pending=2)
[1]: Open (size=71, cost=246, time=0.836693, max=0.607426, total=1.37402, pending=2)
[10]: Open (size=91, cost=242, time=0.876667, max=0.607426, total=1.47785, pending=3)
[01]: Open (size=130, cost=259, time=1.04335, max=0.607426, total=1.51113, pending=3)
[11]: Open (size=91, cost=267, time=0.897468, max=0.607426, total=1.5991, pending=3)
[00]: Open (size=130, cost=281, time=1.14746, max=0.607426, total=1.63686, pending=3)
[001]: Open (size=107, cost=187, time=1.36305, max=0.607426, total=1.94649, pending=4)
[11]: Open (size=85, cost=328, time=0.931667, max=0.607426, total=2.0506, pending=4)
[001]: Open (size=76, cost=355, time=1.44702, max=0.607426, total=2.10526, pending=4)
[000]: Open (size=107, cost=381, time=1.40379, max=0.607426, total=2.23103, pending=4)
[10]: Open (size=66, cost=386, time=0.904965, max=0.607426, total=2.35253, pending=4)
[101]: Open (size=79, cost=389, time=1.01932, max=0.607426, total=2.56354, pending=5)
[001]: Open (size=140, cost=471, time=1.52795, max=0.607426, total=2.83256, pending=5)
[01]: Open (size=89, cost=487, time=1.12139, max=0.607426, total=2.90048, pending=5)
[100]: Open (size=79, cost=536, time=1.01159, max=0.607426, total=2.95188, pending=5)
[01]: Open (size=102, cost=547, time=1.15779, max=0.607426, total=2.99111, pending=5)
[011]: Open (size=102, cost=368, time=1.26263, max=0.607426, total=3.2314, pending=6)
[010]: Open (size=102, cost=493, time=1.2725, max=0.607426, total=3.64682, pending=6)
[001]: Open (size=94, cost=578, time=1.57645, max=0.607426, total=3.79891, pending=6)
[010]: Open (size=145, cost=579, time=1.38858, max=0.607426, total=3.85456, pending=6)
[100]: Open (size=72, cost=579, time=1.03957, max=0.607426, total=3.91886, pending=6)
[11]: Open (size=85, cost=601, time=0.976383, max=0.607426, total=3.98899, pending=6)
[111]: Open (size=90, cost=408, time=1.11931, max=0.607426, total=4.19512, pending=7)
[011]: Open (size=106, cost=644, time=1.62354, max=0.607426, total=4.47575, pending=7)
[101]: Open (size=85, cost=664, time=1.2549, max=0.607426, total=4.79972, pending=7)
[001]: Open (size=176, cost=684, time=1.60534, max=0.607426, total=4.8586, pending=7)
[011]: Open (size=107, cost=687, time=1.88193, max=0.607426, total=4.93, pending=7)
[101]: Open (size=95, cost=687, time=1.2834, max=0.607426, total=4.99807, pending=7)
[000]: Open (size=107, cost=694, time=1.49129, max=0.607426, total=5.04266, pending=7)
[011]: Open (size=115, cost=705, time=1.90782, max=0.607426, total=5.11718, pending=7)
[000]: Open (size=107, cost=707, time=1.5172, max=0.607426, total=5.19278, pending=7)
[101]: Open (size=282, cost=724, time=1.30435, max=0.607426, total=5.25328, pending=7)
[001]: Open (size=154, cost=728, time=1.64838, max=0.607426, total=5.29921, pending=7)
[110]: Open (size=90, cost=729, time=1.08598, max=0.607426, total=5.37177, pending=7)
[100]: Open (size=85, cost=739, time=1.08683, max=0.607426, total=5.48214, pending=7)
[000]: Open (size=117, cost=746, time=1.54121, max=0.607426, total=5.59596, pending=7)
[111]: Open (size=104, cost=758, time=1.34229, max=0.607426, total=5.66834, pending=7)
[101]: Open (size=212, cost=759, time=1.32346, max=0.607426, total=5.78589, pending=7)
[100]: Open (size=212, cost=759, time=1.1502, max=0.607426, total=5.84106, pending=7)
[011]: Open (size=136, cost=823, time=1.93169, max=0.607426, total=5.89785, pending=7)
[110]: Open (size=129, cost=854, time=1.14609, max=0.607426, total=6.00659, pending=7)
[010]: Open (size=124, cost=863, time=1.42108, max=0.607426, total=6.10976, pending=7)
[000]: Open (size=247, cost=869, time=1.57195, max=0.607426, total=6.4993, pending=7)
[111]: Open (size=244, cost=869, time=1.39308, max=0.607426, total=6.59681, pending=7)
[001]: Open (size=143, cost=969, time=1.6798, max=0.607426, total=6.71493, pending=7)
[010]: Open (size=212, cost=1094, time=1.63836, max=0.607426, total=6.78122, pending=7)
[011]: Open (size=212, cost=1094, time=1.95619, max=0.607426, total=6.87104, pending=7)
[110]: Open (size=108, cost=1123, time=1.19774, max=0.607426, total=6.96614, pending=7)
[111]: Open (size=154, cost=1144, time=1.46262, max=0.607426, total=7.08458, pending=7)
[000]: Open (size=247, cost=1152, time=1.62315, max=0.607426, total=7.7285, pending=7)
[101]: Open (size=165, cost=1157, time=1.34711, max=0.607426, total=7.80836, pending=7)
[1010]: Open (size=198, cost=274, time=1.36381, max=0.607426, total=7.89839, pending=8)
******* COMPLETION *******
i(f(X0,Y0)) -> f(i(Y0),i(X0))
i(i(X1)) -> f(X1,e)
f(X0,f(i(X0),Z1)) -> Z1
f(f(X0,Y0),Z0) -> f(X0,f(Y0,Z0))
i(e) -> e
f(e,X0) -> X0
f(X0,i(X0)) -> e
f(i(X1),f(X1,Z3)) -> Z3
f(i(X0),e) -> i(X0)
**************************
On branch: [1010]
With size, cost: 57, 133
Orientations: 192
Calls to AProVE (all, T, NT, ?): 105, 104, 1, 0
Time (all, branch, AProVE): 7.90024, 1.36381, 5.77709
Time/call in AProVE (Avg, Min, Max): 0.0550199, 0.607227, 0.0159919
Time/T-call in AProVE (Avg, Min, Max): 0.0507757, 0.607227, 0.607426
All conjectures solved.