[]: Open (size=28, cost=0, time=0, max=0, total=7.86781e-06, pending=1)
[0]: Open (size=28, cost=116, time=0.792377, max=0.617144, total=0.820369, pending=1)
[1]: Open (size=28, cost=116, time=0.791133, max=0.617144, total=0.930802, pending=1)
[0]: Open (size=89, cost=139, time=0.89901, max=0.617144, total=1.08215, pending=1)
[1]: Open (size=89, cost=207, time=0.936755, max=0.617144, total=1.14911, pending=1)
[0]: Open (size=89, cost=218, time=0.963631, max=0.617144, total=1.21232, pending=1)
[1]: Open (size=78, cost=262, time=0.995786, max=0.617144, total=1.26549, pending=1)
[0]: Open (size=78, cost=262, time=1.01275, max=0.617144, total=1.35366, pending=1)
[1]: Open (size=69, cost=413, time=1.07382, max=0.617144, total=1.51574, pending=1)
[0]: Open (size=91, cost=600, time=1.15077, max=0.617144, total=1.57503, pending=1)
[1]: Open (size=102, cost=611, time=1.11546, max=0.617144, total=1.65104, pending=1)
[0]: Open (size=195, cost=773, time=1.20727, max=0.617144, total=1.81325, pending=1)
[1]: Open (size=144, cost=1079, time=1.23538, max=0.617144, total=1.94731, pending=1)
[10]: Open (size=183, cost=244, time=1.32905, max=0.617144, total=2.13004, pending=2)
******* COMPLETION *******
inverse(multiply(Y1,Z1)) -> multiply(inverse(Z1),inverse(Y1))
multiply(X0,multiply(Y0,Z0)) -> multiply(multiply(X0,Y0),Z0)
multiply(X0,inverse(X0)) -> identity
inverse(identity) -> identity
multiply(identity,X0) -> X0
multiply(X0,identity) -> X0
multiply(inverse(X0),X0) -> identity
multiply(multiply(X1,X0),inverse(X0)) -> X1
inverse(inverse(X0)) -> X0
multiply(multiply(X1,inverse(X0)),X0) -> X1
**************************
On branch: [10]
With size, cost: 58, 119
Orientations: 52
Calls to AProVE (all, T, NT, ?): 28, 28, 0, 0
Time (all, branch, AProVE): 2.1319, 1.32905, 1.91479
Time/call in AProVE (Avg, Min, Max): 0.0683852, 0.616946, 0.0210612
Time/T-call in AProVE (Avg, Min, Max): 0.0683852, 0.616946, 0.617144
All conjectures solved.