[]: Open (size=76, cost=0, time=0, max=0, total=2.59876e-05, pending=1)
[0]: Open (size=76, cost=76, time=0.684969, max=0.684969, total=0.702614, pending=1)
[1]: Open (size=76, cost=76, time=0.0173218, max=0.0173218, total=0.734133, pending=1)
[0]: Open (size=76, cost=76, time=0.716297, max=0.684969, total=0.760063, pending=1)
[1]: Open (size=76, cost=76, time=0.0430617, max=0.0257399, total=0.851275, pending=2)
[01]: Open (size=78, cost=76, time=0.759917, max=0.684969, total=0.960689, pending=3)
[00]: Open (size=76, cost=76, time=0.763362, max=0.684969, total=1.01761, pending=3)
[000]: Open (size=76, cost=76, time=2.03078, max=0.684969, total=2.36892, pending=4)
[0000]: Open (size=76, cost=76, time=2.45041, max=0.684969, total=3.26333, pending=5)
******* COMPLETION *******
subset(plus(u,X0),v) -> if(has(v,X0),subset(u,v),ff)
has(plus(u,X0),Y0) -> if(eq(X0,Y0),tt,has(u,Y0))
eq(s(X0),s(Y0)) -> eq(X0,Y0)
if(X0,tt,ff) -> X0
if(ff,X0,Y0) -> Y0
eq(zero,s(X0)) -> ff
if(X0,Y0,Y0) -> Y0
eq(s(X0),zero) -> ff
if(tt,X0,Y0) -> X0
has(emptY,X0) -> ff
subset(emptY,v) -> tt
eq(zero,zero) -> tt
**************************
On branch: [0000]
With size, cost: 76, 76
Orientations: 30
Calls to AProVE (all, T, NT, ?): 20, 20, 0, 0
Time (all, branch, AProVE): 3.27076, 2.45041, 3.25194
Time/call in AProVE (Avg, Min, Max): 0.162597, 0.684623, 0.0172851
Time/T-call in AProVE (Avg, Min, Max): 0.162597, 0.684623, 0.684969
All conjectures solved.