[]: Open (size=44, cost=0, time=0, max=0, total=1.00136e-05, pending=1)
[0]: Open (size=44, cost=164, time=0.929433, max=0.589942, total=0.971835, pending=1)
[00]: Open (size=63, cost=135, time=1.37454, max=0.589942, total=1.49168, pending=2)
[01]: Open (size=63, cost=135, time=1.36018, max=0.589942, total=1.61262, pending=2)
[1]: Open (size=44, cost=164, time=0.906125, max=0.589942, total=1.70547, pending=2)
[10]: Open (size=63, cost=135, time=1.25551, max=0.589942, total=2.16636, pending=3)
[11]: Open (size=63, cost=135, time=1.28628, max=0.589942, total=2.30955, pending=3)
[10]: Open (size=105, cost=184, time=1.39663, max=0.589942, total=2.48643, pending=3)
[11]: Open (size=105, cost=184, time=1.46106, max=0.589942, total=2.64432, pending=3)
[00]: Open (size=105, cost=195, time=1.49319, max=0.589942, total=2.8483, pending=3)
[01]: Open (size=105, cost=195, time=1.45087, max=0.589942, total=3.00429, pending=3)
[10]: Open (size=105, cost=263, time=1.55167, max=0.589942, total=3.1392, pending=3)
[11]: Open (size=105, cost=263, time=1.66221, max=0.589942, total=3.28183, pending=3)
[00]: Open (size=105, cost=274, time=1.64628, max=0.589942, total=3.42499, pending=3)
[01]: Open (size=105, cost=274, time=1.58297, max=0.589942, total=3.58763, pending=3)
[00]: Open (size=94, cost=318, time=1.8037, max=0.589942, total=3.70122, pending=3)
[01]: Open (size=94, cost=318, time=1.69146, max=0.589942, total=3.96879, pending=3)
[10]: Open (size=94, cost=318, time=1.68902, max=0.589942, total=4.25236, pending=3)
[11]: Open (size=94, cost=318, time=1.80017, max=0.589942, total=4.50787, pending=3)
[00]: Open (size=107, cost=454, time=2.05807, max=0.589942, total=4.65289, pending=3)
[01]: Open (size=107, cost=454, time=1.94906, max=0.589942, total=4.71188, pending=3)
[10]: Open (size=96, cost=480, time=1.91647, max=0.589942, total=4.79107, pending=3)
[11]: Open (size=96, cost=480, time=1.92577, max=0.589942, total=4.84631, pending=3)
[00]: Open (size=107, cost=656, time=2.09324, max=0.589942, total=4.90005, pending=3)
[01]: Open (size=107, cost=656, time=2.00474, max=0.589942, total=4.96059, pending=3)
[10]: Open (size=118, cost=667, time=1.9502, max=0.589942, total=5.01393, pending=3)
[11]: Open (size=118, cost=667, time=1.95647, max=0.589942, total=5.06591, pending=3)
[10]: Open (size=207, cost=761, time=1.98143, max=0.589942, total=5.11541, pending=3)
[11]: Open (size=207, cost=761, time=1.98465, max=0.589942, total=5.21708, pending=3)
[00]: Open (size=211, cost=829, time=2.13032, max=0.589942, total=5.35014, pending=3)
[01]: Open (size=211, cost=829, time=2.03545, max=0.589942, total=5.53768, pending=3)
[10]: Open (size=160, cost=1135, time=2.05377, max=0.589942, total=5.74715, pending=3)
[100]: Open (size=199, cost=300, time=2.11954, max=0.589942, total=5.90509, pending=4)
******* COMPLETION *******
i(f(X1,Y1)) -> f(i(Y1),i(X1))
f(f(X0,Y0),Z0) -> f(X0,f(Y0,Z0))
a(b(a(X0))) -> b(a(b(X0)))
f(i(X0),X0) -> e
a(a(X0)) -> X0
f(X0,e) -> X0
f(e,X0) -> X0
b(b(X0)) -> X0
i(e) -> e
f(X0,i(X0)) -> e
f(i(X0),f(X0,Z1)) -> Z1
i(i(X0)) -> X0
f(X0,f(i(X0),Z1)) -> Z1
**************************
On branch: [100]
With size, cost: 74, 175
Orientations: 112
Calls to AProVE (all, T, NT, ?): 60, 60, 0, 0
Time (all, branch, AProVE): 5.90699, 2.11954, 5.33772
Time/call in AProVE (Avg, Min, Max): 0.0889621, 0.589731, 0.0277622
Time/T-call in AProVE (Avg, Min, Max): 0.0889621, 0.589731, 0.589942
All conjectures solved.