[]: Open (size=19, cost=0, time=0, max=0, total=1.40667e-05, pending=1)
[0]: Open (size=19, cost=33, time=0.833922, max=0.71058, total=0.858141, pending=1)
[1]: Open (size=19, cost=89, time=0.823326, max=0.71058, total=0.904875, pending=1)
[0]: Open (size=50, cost=96, time=0.879797, max=0.71058, total=0.9894, pending=1)
[1]: Open (size=78, cost=163, time=0.905602, max=0.71058, total=1.27687, pending=1)
[0]: Open (size=65, cost=332, time=1.16237, max=0.71058, total=1.51581, pending=1)
[1]: Open (size=133, cost=649, time=1.12149, max=0.71058, total=2.036, pending=1)
[0]: Open (size=191, cost=724, time=1.63203, max=0.71058, total=2.1129, pending=1)
[1]: Open (size=94, cost=1019, time=1.17262, max=0.71058, total=2.20464, pending=1)
[0]: Open (size=144, cost=1098, time=1.6806, max=0.71058, total=2.37187, pending=1)
[00]: Open (size=183, cost=263, time=1.83776, max=0.71058, total=2.6864, pending=2)
******* COMPLETION *******
inverse(multiply(X0,Y0)) -> multiply(inverse(Y0),inverse(X0))
multiply(X2,inverse(X2)) -> identity
inverse(inverse(X2)) -> X2
multiply(X0,identity) -> X0
multiply(multiply(X0,Y0),Z0) -> multiply(X0,multiply(Y0,Z0))
multiply(inverse(X0),X0) -> identity
multiply(identity,X0) -> X0
multiply(inverse(X0),multiply(X0,Z1)) -> Z1
inverse(identity) -> identity
multiply(X2,multiply(inverse(X2),Z1)) -> Z1
**************************
On branch: [00]
With size, cost: 58, 138
Orientations: 56
Calls to AProVE (all, T, NT, ?): 30, 30, 0, 0
Time (all, branch, AProVE): 2.68838, 1.83776, 2.36721
Time/call in AProVE (Avg, Min, Max): 0.0789071, 0.710245, 0.023057
Time/T-call in AProVE (Avg, Min, Max): 0.0789071, 0.710245, 0.71058
All conjectures solved.