[]: Open (size=63, cost=0, time=0, max=0, total=1.69277e-05, pending=1)
[1]: Open (size=63, cost=63, time=0.975595, max=0.796186, total=1.00768, pending=1)
[10]: Open (size=63, cost=63, time=1.01289, max=0.796186, total=1.08258, pending=2)
[0]: Open (size=64, cost=67, time=0.970964, max=0.796186, total=1.16674, pending=3)
[00]: Open (size=61, cost=64, time=1.05339, max=0.796186, total=1.29088, pending=4)
[11]: Open (size=65, cost=74, time=1.01245, max=0.796186, total=1.44038, pending=5)
[110]: Open (size=60, cost=69, time=1.10833, max=0.796186, total=1.5808, pending=6)
[100]: Open (size=63, cost=83, time=1.0545, max=0.796186, total=1.72949, pending=7)
[1101]: Open (size=60, cost=83, time=1.17163, max=0.796186, total=1.9399, pending=8)
[000]: Open (size=61, cost=88, time=1.12102, max=0.796186, total=2.1786, pending=9)
[001]: Open (size=61, cost=96, time=1.1342, max=0.796186, total=2.27785, pending=10)
[1100]: Open (size=60, cost=97, time=1.19263, max=0.796186, total=2.3946, pending=11)
[11000]: Open (size=60, cost=69, time=1.3224, max=0.796186, total=2.73067, pending=12)
******* COMPLETION *******
rev(dot(X0,Y0)) -> at(rev(Y0),dot(X0,nil))
at(at(X0,Y0),Z0) -> at(X0,at(Y0,Z0))
at(dot(X0,Y0),Z0) -> dot(X0,at(Y0,Z0))
reviter(X0,Y0) -> at(rev(X0),Y0)
at(rev(X0),nil) -> rev(X0)
at(nil,Y0) -> Y0
rev(nil) -> nil
**************************
On branch: [11000]
With size, cost: 50, 59
Orientations: 34
Calls to AProVE (all, T, NT, ?): 29, 29, 0, 0
Time (all, branch, AProVE): 2.73548, 1.3224, 2.70909
Time/call in AProVE (Avg, Min, Max): 0.0934169, 0.795776, 0.029727
Time/T-call in AProVE (Avg, Min, Max): 0.0934169, 0.795776, 0.796186
All conjectures solved.