[]: Open (size=40, cost=0, time=0, max=0, total=9.05991e-06, pending=1)
[0]: Open (size=40, cost=40, time=0.846824, max=0.846824, total=0.87947, pending=1)
[1]: Open (size=40, cost=40, time=0.032454, max=0.032454, total=0.959481, pending=1)
[0]: Open (size=40, cost=40, time=0.926658, max=0.846824, total=0.979421, pending=1)
[00]: Open (size=40, cost=40, time=0.997103, max=0.846824, total=1.08091, pending=2)
[001]: Open (size=40, cost=40, time=1.08248, max=0.846824, total=1.23263, pending=3)
[0011]: Open (size=40, cost=40, time=1.12794, max=0.846824, total=1.33535, pending=4)
******* COMPLETION *******
plus(X0,plus(Y0,Z0)) -> plus(plus(X0,Y0),Z0)
times(X0,times(Y0,Z0)) -> times(times(X0,Y0),Z0)
exp(plus(X0,Y0)) -> times(exp(X0),exp(Y0))
times(X0,one) -> X0
plus(X0,zero) -> X0
exp(zero) -> one
**************************
On branch: [0011]
With size, cost: 40, 40
Orientations: 14
Calls to AProVE (all, T, NT, ?): 11, 11, 0, 0
Time (all, branch, AProVE): 1.33864, 1.12794, 1.33021
Time/call in AProVE (Avg, Min, Max): 0.120928, 0.846648, 0.0197132
Time/T-call in AProVE (Avg, Min, Max): 0.120928, 0.846648, 0.846824
All conjectures solved.