[]: Open (size=68, cost=0, time=0, max=0, total=1.5974e-05, pending=1)
[0]: Open (size=68, cost=68, time=0.762163, max=0.762163, total=0.785814, pending=1)
[1]: Open (size=68, cost=68, time=0.0233481, max=0.0233481, total=0.913306, pending=1)
[0]: Open (size=68, cost=68, time=0.889459, max=0.762163, total=0.932935, pending=1)
[1]: Open (size=68, cost=68, time=0.0427873, max=0.0233481, total=0.970143, pending=1)
[0]: Open (size=68, cost=68, time=0.926162, max=0.762163, total=0.999543, pending=1)
[00]: Open (size=68, cost=68, time=1.12179, max=0.762163, total=1.24243, pending=2)
[000]: Open (size=68, cost=68, time=1.17967, max=0.762163, total=1.36226, pending=3)
[0000]: Open (size=68, cost=68, time=1.23072, max=0.762163, total=1.48482, pending=4)
[1]: Open (size=69, cost=69, time=0.0719693, max=0.029182, total=1.79443, pending=5)
[10]: Open (size=69, cost=69, time=0.311575, max=0.118213, total=2.06198, pending=6)
[100]: Open (size=69, cost=69, time=0.420036, max=0.118213, total=2.25371, pending=7)
[1000]: Open (size=69, cost=69, time=0.471066, max=0.118213, total=2.35386, pending=8)
[00000]: Open (size=68, cost=84, time=1.41047, max=0.762163, total=2.49055, pending=9)
******* COMPLETION *******
and(true,true) -> true
null(nil) -> true
dot(nil,Y0) -> Y0
eq(X0,X0) -> true
null(end(X0,Y0)) -> false
f(X0,nil) -> end(nil,X0)
eq(nil,end(Y0,Z0)) -> false
eq(end(X0,Y0),nil) -> false
dot(end(X0,Y0),Z0) -> dot(X0,f(Y0,Z0))
f(X0,end(Y0,Z0)) -> end(f(X0,Y0),Z0)
eq(end(X0,Y0),end(u,v)) -> and(eq(Y0,v),eq(X0,u))
**************************
On branch: [00000]
With size, cost: 72, 72
Orientations: 40
Calls to AProVE (all, T, NT, ?): 29, 29, 0, 0
Time (all, branch, AProVE): 2.65307, 1.5597, 2.62186
Time/call in AProVE (Avg, Min, Max): 0.0904089, 0.761831, 0.019392
Time/T-call in AProVE (Avg, Min, Max): 0.0904089, 0.761831, 0.762163
All conjectures solved.