[]: Open (size=20, cost=0, time=0, max=0, total=1.21593e-05, pending=1)
[0]: Open (size=20, cost=60, time=0.717434, max=0.6587, total=1.08837, pending=1)
[01]: Open (size=50, cost=50, time=0.749018, max=0.6587, total=1.16663, pending=2)
[011]: Open (size=50, cost=50, time=0.790734, max=0.6587, total=1.2534, pending=3)
******* COMPLETION *******
or(and(X1,X0),X0) -> and(or(X1,X0),X0)
or(X0,and(Z1,X0)) -> and(or(X0,Z1),X0)
or(and(X0,Y0),and(Z0,Y0)) -> and(or(X0,Z0),Y0)
and(X0,X0) -> X0
or(X0,X0) -> X0
**************************
On branch: [011]
With size, cost: 40, 40
Orientations: 10
Calls to AProVE (all, T, NT, ?): 8, 8, 0, 0
Time (all, branch, AProVE): 1.25386, 0.790734, 1.24997
Time/call in AProVE (Avg, Min, Max): 0.156246, 0.658505, 0.0231071
Time/T-call in AProVE (Avg, Min, Max): 0.156246, 0.658505, 0.6587
All conjectures solved.