[]: Open (size=31, cost=0, time=0, max=0, total=1.40667e-05, pending=1)
[0]: Open (size=31, cost=51, time=0.990161, max=0.804112, total=1.03222, pending=1)
[00]: Open (size=31, cost=51, time=1.1083, max=0.804112, total=1.19819, pending=2)
[1]: Open (size=31, cost=65, time=0.983497, max=0.804112, total=1.26753, pending=2)
[10]: Open (size=31, cost=65, time=1.02896, max=0.804112, total=1.37632, pending=3)
[01]: Open (size=31, cost=95, time=1.03723, max=0.804112, total=1.53606, pending=4)
[11]: Open (size=31, cost=109, time=1.04606, max=0.804112, total=1.66778, pending=4)
[111]: Open (size=48, cost=94, time=1.18007, max=0.804112, total=1.85988, pending=5)
[101]: Open (size=48, cost=114, time=1.14349, max=0.804112, total=1.96648, pending=5)
[111]: Open (size=70, cost=114, time=1.28543, max=0.804112, total=2.40795, pending=6)
[00]: Open (size=53, cost=133, time=1.17613, max=0.804112, total=2.80852, pending=7)
[001]: Open (size=91, cost=101, time=1.26119, max=0.804112, total=3.50359, pending=8)
******* COMPLETION *******
rev(at(X0,dot(X1,nil))) -> dot(X1,rev(X0))
rev(dot(X0,Y0)) -> at(rev(Y0),dot(X0,nil))
rev(rev(X0)) -> X0
at(nil,Y0) -> Y0
rev(nil) -> nil
at(dot(X0,Y0),Z0) -> dot(X0,at(Y0,Z0))
**************************
On branch: [001]
With size, cost: 41, 51
Orientations: 32
Calls to AProVE (all, T, NT, ?): 24, 24, 0, 0
Time (all, branch, AProVE): 3.50403, 1.26119, 3.48424
Time/call in AProVE (Avg, Min, Max): 0.145177, 0.803263, 0.0353029
Time/T-call in AProVE (Avg, Min, Max): 0.145177, 0.803263, 0.804112
All conjectures solved.