[]: Open (size=37, cost=0, time=0, max=0, total=1.28746e-05, pending=1)
[0]: Open (size=37, cost=37, time=0.737992, max=0.605282, total=0.775922, pending=1)
[1]: Open (size=37, cost=37, time=0.737669, max=0.605282, total=0.871686, pending=2)
[00]: Open (size=37, cost=37, time=0.790342, max=0.605282, total=0.966625, pending=3)
[000]: Open (size=37, cost=37, time=1.24022, max=0.605282, total=1.45849, pending=4)
[0000]: Open (size=37, cost=37, time=1.49736, max=0.605282, total=2.0733, pending=5)
******* COMPLETION *******
times(X0,s(Y0)) -> plus(times(X0,Y0),X0)
fac(s(X0)) -> times(s(X0),fac(X0))
plus(X0,s(Y0)) -> s(plus(X0,Y0))
times(X0,zero) -> zero
plus(X0,zero) -> X0
fac(zero) -> s(zero)
**************************
On branch: [0000]
With size, cost: 37, 37
Orientations: 14
Calls to AProVE (all, T, NT, ?): 12, 12, 0, 0
Time (all, branch, AProVE): 2.0747, 1.49736, 2.06909
Time/call in AProVE (Avg, Min, Max): 0.172425, 0.605068, 0.0374649
Time/T-call in AProVE (Avg, Min, Max): 0.172425, 0.605068, 0.605282
All conjectures solved.