%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : GRP053-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:09:10 AM UTC 2026
% Result : Unsatisfiable 9.32s 1.62s
% Output : Proof 11.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP053-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 09:17:16 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.32/1.62 Command-line arguments: --no-flatten-goal
% 9.32/1.62
% 9.32/1.62 % SZS status Unsatisfiable
% 9.32/1.62
% 10.88/1.89 % SZS output start Proof
% 10.88/1.89 Axiom 1 (single_axiom): inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(Z)))), inverse(multiply(inverse(X), X)))))) = Z.
% 10.88/1.89
% 10.88/1.89 Lemma 2: inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, Z))), inverse(multiply(inverse(X), X)))))) = multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W))))).
% 10.88/1.89 Proof:
% 10.88/1.89 inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, Z))), inverse(multiply(inverse(X), X))))))
% 10.88/1.89 = { by axiom 1 (single_axiom) R->L }
% 10.88/1.89 inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W))))))))), inverse(multiply(inverse(X), X))))))
% 10.88/1.89 = { by axiom 1 (single_axiom) }
% 10.88/1.89 multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W)))))
% 10.88/1.89
% 10.88/1.89 Lemma 3: multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(inverse(Z))))), inverse(multiply(inverse(X), X))))) = Z.
% 10.88/1.89 Proof:
% 10.88/1.89 multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(inverse(Z))))), inverse(multiply(inverse(X), X)))))
% 10.88/1.89 = { by lemma 2 R->L }
% 10.88/1.89 inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W))))))
% 10.88/1.89 = { by axiom 1 (single_axiom) }
% 10.88/1.89 Z
% 10.88/1.89
% 10.88/1.90 Lemma 4: multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W))))) = multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(Z)))), inverse(multiply(inverse(X), X))))).
% 10.88/1.90 Proof:
% 10.88/1.90 multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W)))))
% 10.88/1.90 = { by axiom 1 (single_axiom) R->L }
% 10.88/1.90 inverse(multiply(U, inverse(multiply(inverse(multiply(inverse(multiply(T, U)), multiply(T, inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W))))))))), inverse(multiply(inverse(U), U))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 inverse(multiply(U, inverse(multiply(inverse(multiply(inverse(multiply(T, U)), multiply(T, Z))), inverse(multiply(inverse(U), U))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) R->L }
% 10.88/1.90 inverse(multiply(U, inverse(multiply(inverse(multiply(inverse(multiply(T, U)), multiply(T, inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(Z)))), inverse(multiply(inverse(X), X))))))))), inverse(multiply(inverse(U), U))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(Z)))), inverse(multiply(inverse(X), X)))))
% 10.88/1.90
% 10.88/1.90 Lemma 5: multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), Z)), inverse(multiply(inverse(W), W))))) = multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), Z)), inverse(multiply(inverse(X), X))))).
% 10.88/1.90 Proof:
% 10.88/1.90 multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), Z)), inverse(multiply(inverse(W), W)))))
% 10.88/1.90 = { by lemma 3 R->L }
% 10.88/1.90 multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(V, Y)), multiply(V, inverse(inverse(Z))))), inverse(multiply(inverse(Y), Y))))))), inverse(multiply(inverse(W), W)))))
% 10.88/1.90 = { by lemma 4 }
% 10.88/1.90 multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(V, Y)), multiply(V, inverse(inverse(Z))))), inverse(multiply(inverse(Y), Y))))))), inverse(multiply(inverse(X), X)))))
% 10.88/1.90 = { by lemma 3 }
% 10.88/1.90 multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), Z)), inverse(multiply(inverse(X), X)))))
% 10.88/1.90
% 10.88/1.90 Lemma 6: inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), Z)), inverse(multiply(inverse(W), W)))))) = multiply(inverse(multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(Z))))), inverse(multiply(inverse(Y), Y))).
% 10.88/1.90 Proof:
% 10.88/1.90 inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), Z)), inverse(multiply(inverse(W), W))))))
% 10.88/1.90 = { by lemma 3 R->L }
% 10.88/1.90 inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(X, V)), multiply(X, inverse(inverse(Z))))), inverse(multiply(inverse(V), V))))))), inverse(multiply(inverse(W), W))))))
% 10.88/1.90 = { by lemma 5 }
% 10.88/1.90 inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(Z))))), inverse(multiply(inverse(Y), Y))))))), inverse(multiply(inverse(W), W))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 multiply(inverse(multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(Z))))), inverse(multiply(inverse(Y), Y)))
% 10.88/1.90
% 10.88/1.90 Lemma 7: multiply(X, inverse(inverse(multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(X, Y)), Z)), inverse(multiply(inverse(Y), Y)))))))) = Z.
% 10.88/1.90 Proof:
% 10.88/1.90 multiply(X, inverse(inverse(multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(X, Y)), Z)), inverse(multiply(inverse(Y), Y))))))))
% 10.88/1.90 = { by lemma 6 }
% 10.88/1.90 multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(W, X)), multiply(W, inverse(inverse(Z))))), inverse(multiply(inverse(X), X)))))
% 10.88/1.90 = { by lemma 4 R->L }
% 10.88/1.90 multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(U, V)), multiply(U, inverse(inverse(Z))))), inverse(multiply(inverse(V), V)))))
% 10.88/1.90 = { by lemma 3 }
% 10.88/1.90 Z
% 10.88/1.90
% 10.88/1.90 Lemma 8: inverse(multiply(inverse(multiply(inverse(multiply(X, inverse(multiply(Y, Z)))), multiply(X, inverse(W)))), inverse(multiply(inverse(inverse(multiply(Y, Z))), inverse(multiply(Y, Z)))))) = multiply(Y, inverse(inverse(multiply(Z, inverse(multiply(W, inverse(multiply(inverse(Z), Z)))))))).
% 10.88/1.90 Proof:
% 10.88/1.90 inverse(multiply(inverse(multiply(inverse(multiply(X, inverse(multiply(Y, Z)))), multiply(X, inverse(W)))), inverse(multiply(inverse(inverse(multiply(Y, Z))), inverse(multiply(Y, Z))))))
% 10.88/1.90 = { by lemma 7 R->L }
% 10.88/1.90 multiply(Y, inverse(inverse(multiply(Z, inverse(multiply(inverse(multiply(inverse(multiply(Y, Z)), inverse(multiply(inverse(multiply(inverse(multiply(X, inverse(multiply(Y, Z)))), multiply(X, inverse(W)))), inverse(multiply(inverse(inverse(multiply(Y, Z))), inverse(multiply(Y, Z)))))))), inverse(multiply(inverse(Z), Z))))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 multiply(Y, inverse(inverse(multiply(Z, inverse(multiply(W, inverse(multiply(inverse(Z), Z))))))))
% 10.88/1.90
% 10.88/1.90 Lemma 9: multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(multiply(Y, inverse(multiply(Z, inverse(multiply(inverse(Y), Y))))))))) = multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W))))).
% 10.88/1.90 Proof:
% 10.88/1.90 multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(multiply(Y, inverse(multiply(Z, inverse(multiply(inverse(Y), Y)))))))))
% 10.88/1.90 = { by lemma 8 R->L }
% 10.88/1.90 multiply(inverse(multiply(X, Y)), inverse(multiply(inverse(multiply(inverse(multiply(U, inverse(multiply(X, Y)))), multiply(U, inverse(Z)))), inverse(multiply(inverse(inverse(multiply(X, Y))), inverse(multiply(X, Y)))))))
% 10.88/1.90 = { by lemma 4 R->L }
% 10.88/1.90 multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(V, W)), multiply(V, inverse(Z)))), inverse(multiply(inverse(W), W)))))
% 10.88/1.90
% 10.88/1.90 Lemma 10: multiply(inverse(multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(multiply(Y, inverse(Z))))))), inverse(multiply(inverse(Y), Y))) = Z.
% 10.88/1.90 Proof:
% 10.88/1.90 multiply(inverse(multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(multiply(Y, inverse(Z))))))), inverse(multiply(inverse(Y), Y)))
% 10.88/1.90 = { by lemma 6 R->L }
% 10.88/1.90 inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), multiply(Y, inverse(Z)))), inverse(multiply(inverse(W), W))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 Z
% 10.88/1.90
% 10.88/1.90 Lemma 11: inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(Y, Z)), multiply(Y, inverse(inverse(multiply(Z, inverse(W))))))), X)), W)), inverse(multiply(inverse(X), X)))))) = multiply(inverse(Z), Z).
% 10.88/1.90 Proof:
% 10.88/1.90 inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(Y, Z)), multiply(Y, inverse(inverse(multiply(Z, inverse(W))))))), X)), W)), inverse(multiply(inverse(X), X))))))
% 10.88/1.90 = { by lemma 10 R->L }
% 10.88/1.90 inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(Y, Z)), multiply(Y, inverse(inverse(multiply(Z, inverse(W))))))), X)), multiply(inverse(multiply(inverse(multiply(Y, Z)), multiply(Y, inverse(inverse(multiply(Z, inverse(W))))))), inverse(multiply(inverse(Z), Z))))), inverse(multiply(inverse(X), X))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 multiply(inverse(Z), Z)
% 10.88/1.90
% 10.88/1.90 Lemma 12: inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X)))))))) = multiply(inverse(X), X).
% 10.88/1.90 Proof:
% 10.88/1.90 inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X))))))))
% 10.88/1.90 = { by lemma 10 R->L }
% 10.88/1.90 inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, inverse(Y))))))), inverse(multiply(inverse(X), X)))), Y)), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X))))))))
% 10.88/1.90 = { by lemma 11 }
% 10.88/1.90 multiply(inverse(X), X)
% 10.88/1.90
% 10.88/1.90 Lemma 13: inverse(multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(multiply(Y, inverse(multiply(Z, inverse(multiply(inverse(Y), Y)))))))))) = Z.
% 10.88/1.90 Proof:
% 10.88/1.90 inverse(multiply(inverse(multiply(X, Y)), multiply(X, inverse(inverse(multiply(Y, inverse(multiply(Z, inverse(multiply(inverse(Y), Y))))))))))
% 10.88/1.90 = { by lemma 8 R->L }
% 10.88/1.90 inverse(multiply(inverse(multiply(X, Y)), inverse(multiply(inverse(multiply(inverse(multiply(W, inverse(multiply(X, Y)))), multiply(W, inverse(Z)))), inverse(multiply(inverse(inverse(multiply(X, Y))), inverse(multiply(X, Y))))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 Z
% 10.88/1.90
% 10.88/1.90 Lemma 14: multiply(inverse(multiply(W, Y)), multiply(W, Z)) = multiply(inverse(multiply(X, Y)), multiply(X, Z)).
% 10.88/1.90 Proof:
% 10.88/1.90 multiply(inverse(multiply(W, Y)), multiply(W, Z))
% 10.88/1.90 = { by axiom 1 (single_axiom) R->L }
% 10.88/1.90 inverse(multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(U, V)), multiply(U, inverse(multiply(inverse(multiply(W, Y)), multiply(W, Z)))))), inverse(multiply(inverse(V), V))))))
% 10.88/1.90 = { by lemma 13 R->L }
% 10.88/1.90 inverse(multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(U, V)), multiply(U, inverse(multiply(inverse(multiply(T, Y)), multiply(T, inverse(inverse(multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(W, Y)), multiply(W, Z))), inverse(multiply(inverse(Y), Y))))))))))))), inverse(multiply(inverse(V), V))))))
% 10.88/1.90 = { by lemma 2 }
% 10.88/1.90 inverse(multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(U, V)), multiply(U, inverse(multiply(inverse(multiply(T, Y)), multiply(T, inverse(multiply(S, inverse(multiply(inverse(multiply(inverse(multiply(X2, S)), multiply(X2, inverse(Z)))), inverse(multiply(inverse(S), S)))))))))))), inverse(multiply(inverse(V), V))))))
% 10.88/1.90 = { by lemma 2 R->L }
% 10.88/1.90 inverse(multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(U, V)), multiply(U, inverse(multiply(inverse(multiply(T, Y)), multiply(T, inverse(inverse(multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(X, Y)), multiply(X, Z))), inverse(multiply(inverse(Y), Y))))))))))))), inverse(multiply(inverse(V), V))))))
% 10.88/1.90 = { by lemma 13 }
% 10.88/1.90 inverse(multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(U, V)), multiply(U, inverse(multiply(inverse(multiply(X, Y)), multiply(X, Z)))))), inverse(multiply(inverse(V), V))))))
% 10.88/1.90 = { by axiom 1 (single_axiom) }
% 10.88/1.90 multiply(inverse(multiply(X, Y)), multiply(X, Z))
% 10.88/1.90
% 10.88/1.90 Lemma 15: multiply(inverse(multiply(inverse(Z), Z)), Y) = multiply(inverse(multiply(inverse(X), X)), Y).
% 10.88/1.90 Proof:
% 10.88/1.90 multiply(inverse(multiply(inverse(Z), Z)), Y)
% 11.57/1.90 = { by lemma 7 R->L }
% 11.57/1.90 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.90 = { by lemma 3 R->L }
% 11.57/1.90 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(Y2, inverse(multiply(inverse(multiply(inverse(multiply(Z2, Y2)), multiply(Z2, inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))))))), inverse(multiply(inverse(Y2), Y2)))))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 9 R->L }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(T, S)), multiply(T, inverse(inverse(multiply(S, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))), inverse(multiply(inverse(S), S)))))))))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 10 R->L }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(T, S)), multiply(T, inverse(inverse(multiply(S, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2, inverse(multiply(inverse(W), W)))), multiply(X2, inverse(inverse(multiply(inverse(multiply(inverse(W), W)), inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))))))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))), inverse(multiply(inverse(S), S)))))))))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 12 }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(T, S)), multiply(T, inverse(inverse(multiply(S, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2, inverse(multiply(inverse(W), W)))), multiply(X2, inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))), inverse(multiply(inverse(S), S)))))))))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 12 R->L }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(T, S)), multiply(T, inverse(inverse(multiply(S, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2, inverse(multiply(inverse(W), W)))), multiply(X2, inverse(inverse(multiply(inverse(multiply(inverse(W), W)), inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))))))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))), inverse(multiply(inverse(S), S)))))))))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 10 }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(T, S)), multiply(T, inverse(inverse(multiply(S, inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))), inverse(multiply(inverse(S), S)))))))))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 9 }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(V, inverse(multiply(inverse(multiply(inverse(multiply(U, V)), multiply(U, inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))))))), inverse(multiply(inverse(V), V)))))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 3 }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(Z), Z)), Y))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 14 R->L }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))), multiply(inverse(multiply(inverse(X), X)), Y))), inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W))))))))))))
% 11.57/1.91 = { by lemma 7 }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), X)), Y)
% 11.57/1.91
% 11.57/1.91 Lemma 16: multiply(inverse(Y), Y) = multiply(inverse(X), X).
% 11.57/1.91 Proof:
% 11.57/1.91 multiply(inverse(Y), Y)
% 11.57/1.91 = { by lemma 3 R->L }
% 11.57/1.91 multiply(T, inverse(multiply(inverse(multiply(inverse(multiply(S, T)), multiply(S, inverse(inverse(multiply(inverse(Y), Y)))))), inverse(multiply(inverse(T), T)))))
% 11.57/1.91 = { by lemma 9 R->L }
% 11.57/1.91 multiply(inverse(multiply(V, U)), multiply(V, inverse(inverse(multiply(U, inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(U), U)))))))))
% 11.57/1.91 = { by lemma 15 }
% 11.57/1.91 multiply(inverse(multiply(V, U)), multiply(V, inverse(inverse(multiply(U, inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(U), U)))))))))
% 11.57/1.91 = { by lemma 9 }
% 11.57/1.91 multiply(Z, inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(multiply(inverse(X), X)))))), inverse(multiply(inverse(Z), Z)))))
% 11.57/1.91 = { by lemma 3 }
% 11.57/1.91 multiply(inverse(X), X)
% 11.57/1.91
% 11.57/1.91 Lemma 17: inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(Z), Z)))))) = X.
% 11.57/1.91 Proof:
% 11.57/1.91 inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(Z), Z))))))
% 11.57/1.91 = { by lemma 16 }
% 11.57/1.91 inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(inverse(X)), inverse(X)))))))
% 11.57/1.91 = { by lemma 16 }
% 11.57/1.91 inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(multiply(W, inverse(X))), multiply(W, inverse(X)))), inverse(multiply(inverse(inverse(X)), inverse(X)))))))
% 11.57/1.91 = { by axiom 1 (single_axiom) }
% 11.57/1.91 X
% 11.57/1.91
% 11.57/1.91 Lemma 18: inverse(multiply(inverse(X), inverse(multiply(inverse(Y), Y)))) = X.
% 11.57/1.91 Proof:
% 11.57/1.91 inverse(multiply(inverse(X), inverse(multiply(inverse(Y), Y))))
% 11.57/1.91 = { by lemma 16 }
% 11.57/1.91 inverse(multiply(inverse(X), inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(W), W))))), inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(W), W))))))))
% 11.57/1.91 = { by lemma 17 }
% 11.57/1.91 inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(W), W))))))
% 11.57/1.91 = { by lemma 17 }
% 11.57/1.91 X
% 11.57/1.91
% 11.57/1.91 Lemma 19: inverse(multiply(inverse(X), multiply(inverse(Y), Y))) = X.
% 11.57/1.91 Proof:
% 11.57/1.91 inverse(multiply(inverse(X), multiply(inverse(Y), Y)))
% 11.57/1.91 = { by lemma 18 R->L }
% 11.57/1.91 inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(Z), Z))))))
% 11.57/1.91 = { by lemma 17 }
% 11.57/1.91 X
% 11.57/1.91
% 11.57/1.91 Lemma 20: inverse(multiply(X, multiply(inverse(Y), Y))) = multiply(inverse(X), multiply(inverse(Z), Z)).
% 11.57/1.91 Proof:
% 11.57/1.91 inverse(multiply(X, multiply(inverse(Y), Y)))
% 11.57/1.91 = { by lemma 17 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(W), W)))))), multiply(inverse(Y), Y)))
% 11.57/1.91 = { by lemma 19 }
% 11.57/1.91 multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(W), W)))))
% 11.57/1.91 = { by lemma 18 }
% 11.57/1.91 multiply(inverse(X), multiply(inverse(Z), Z))
% 11.57/1.91
% 11.57/1.91 Lemma 21: inverse(multiply(inverse(X), X)) = multiply(inverse(Y), Y).
% 11.57/1.91 Proof:
% 11.57/1.91 inverse(multiply(inverse(X), X))
% 11.57/1.91 = { by lemma 16 }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(Y), Y)), multiply(inverse(Y), Y)))
% 11.57/1.91 = { by lemma 18 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(Z), Z))))))
% 11.57/1.91 = { by lemma 17 }
% 11.57/1.91 multiply(inverse(Y), Y)
% 11.57/1.91
% 11.57/1.91 Lemma 22: multiply(X, multiply(inverse(X), multiply(inverse(Y), Y))) = multiply(inverse(Z), Z).
% 11.57/1.91 Proof:
% 11.57/1.91 multiply(X, multiply(inverse(X), multiply(inverse(Y), Y)))
% 11.57/1.91 = { by lemma 19 R->L }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), multiply(inverse(Y), Y))), multiply(inverse(X), multiply(inverse(Y), Y)))
% 11.57/1.91 = { by lemma 16 R->L }
% 11.57/1.91 multiply(inverse(Z), Z)
% 11.57/1.91
% 11.57/1.91 Lemma 23: multiply(inverse(multiply(X, Y)), multiply(X, Z)) = multiply(multiply(inverse(W), W), multiply(inverse(Y), Z)).
% 11.57/1.91 Proof:
% 11.57/1.91 multiply(inverse(multiply(X, Y)), multiply(X, Z))
% 11.57/1.91 = { by lemma 14 }
% 11.57/1.91 multiply(inverse(multiply(inverse(Y), Y)), multiply(inverse(Y), Z))
% 11.57/1.91 = { by lemma 21 }
% 11.57/1.91 multiply(multiply(inverse(W), W), multiply(inverse(Y), Z))
% 11.57/1.91
% 11.57/1.91 Lemma 24: multiply(inverse(multiply(inverse(X), Y)), multiply(inverse(Z), Z)) = multiply(inverse(multiply(W, Y)), multiply(W, X)).
% 11.57/1.91 Proof:
% 11.57/1.91 multiply(inverse(multiply(inverse(X), Y)), multiply(inverse(Z), Z))
% 11.57/1.91 = { by lemma 16 }
% 11.57/1.91 multiply(inverse(multiply(inverse(X), Y)), multiply(inverse(X), X))
% 11.57/1.91 = { by lemma 14 R->L }
% 11.57/1.91 multiply(inverse(multiply(W, Y)), multiply(W, X))
% 11.57/1.91
% 11.57/1.91 Lemma 25: inverse(multiply(multiply(inverse(X), X), multiply(inverse(Y), Z))) = multiply(inverse(Z), Y).
% 11.57/1.91 Proof:
% 11.57/1.91 inverse(multiply(multiply(inverse(X), X), multiply(inverse(Y), Z)))
% 11.57/1.91 = { by lemma 23 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(W, Y)), multiply(W, Z)))
% 11.57/1.91 = { by lemma 24 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(Z), Y)), multiply(inverse(V), V)))
% 11.57/1.91 = { by lemma 19 }
% 11.57/1.91 multiply(inverse(Z), Y)
% 11.57/1.91
% 11.57/1.91 Lemma 26: inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(Y, multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, Y)))))), inverse(W)))), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X)))))))) = W.
% 11.57/1.91 Proof:
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(Y, multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, Y)))))), inverse(W)))), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X))))))))
% 11.57/1.91 = { by lemma 10 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(V, U)), multiply(V, inverse(inverse(multiply(U, inverse(Y))))))), inverse(multiply(inverse(U), U))), multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, Y)))))), inverse(W)))), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X))))))))
% 11.57/1.91 = { by lemma 6 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(inverse(multiply(T, inverse(multiply(inverse(multiply(inverse(multiply(U, T)), multiply(U, inverse(Y)))), inverse(multiply(inverse(T), T)))))), multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, Y)))))), inverse(W)))), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X))))))))
% 11.57/1.91 = { by lemma 2 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(inverse(inverse(multiply(S, inverse(multiply(inverse(multiply(inverse(multiply(X, S)), multiply(X, Y))), inverse(multiply(inverse(S), S))))))), multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, Y)))))), inverse(W)))), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X))))))))
% 11.57/1.91 = { by lemma 6 }
% 11.57/1.91 inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, Y)))))), inverse(multiply(inverse(X), X)))), multiply(inverse(multiply(inverse(multiply(Z, X)), multiply(Z, inverse(inverse(multiply(X, Y)))))), inverse(W)))), inverse(multiply(inverse(inverse(multiply(inverse(X), X))), inverse(multiply(inverse(X), X))))))))
% 11.57/1.91 = { by axiom 1 (single_axiom) }
% 11.57/1.91 W
% 11.57/1.91
% 11.57/1.91 Lemma 27: multiply(multiply(inverse(X), X), Y) = Y.
% 11.57/1.91 Proof:
% 11.57/1.91 multiply(multiply(inverse(X), X), Y)
% 11.57/1.91 = { by lemma 13 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(multiply(multiply(inverse(X), X), Y), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.91 = { by lemma 21 R->L }
% 11.57/1.91 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(multiply(inverse(multiply(inverse(V), V)), Y), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 21 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(multiply(inverse(inverse(multiply(inverse(U), U))), Y), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 21 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(multiply(inverse(inverse(inverse(multiply(inverse(T), T)))), Y), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 22 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(multiply(inverse(inverse(inverse(multiply(Y, multiply(inverse(Y), multiply(inverse(S), S)))))), Y), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 20 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(multiply(inverse(inverse(inverse(multiply(Y, inverse(multiply(Y, multiply(inverse(X2), X2))))))), Y), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 21 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(multiply(inverse(inverse(inverse(multiply(Y, inverse(multiply(Y, inverse(multiply(inverse(Y), Y)))))))), Y), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 25 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(multiply(inverse(Y2), Y2), multiply(inverse(Y), inverse(inverse(multiply(Y, inverse(multiply(Y, inverse(multiply(inverse(Y), Y)))))))))), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 23 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Z2, Y)), multiply(Z2, inverse(inverse(multiply(Y, inverse(multiply(Y, inverse(multiply(inverse(Y), Y)))))))))), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by axiom 1 (single_axiom) R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Z2, Y)), multiply(Z2, inverse(inverse(multiply(Y, inverse(multiply(Y, inverse(multiply(inverse(Y), Y)))))))))), inverse(multiply(W2, inverse(multiply(inverse(multiply(inverse(multiply(V2, W2)), multiply(V2, inverse(inverse(multiply(inverse(W), W)))))), inverse(multiply(inverse(W2), W2))))))))))))))
% 11.57/1.92 = { by lemma 3 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(U2, Y)), multiply(U2, inverse(inverse(multiply(inverse(multiply(inverse(multiply(Z2, Y)), multiply(Z2, inverse(inverse(multiply(Y, inverse(multiply(Y, inverse(multiply(inverse(Y), Y)))))))))), inverse(multiply(W2, inverse(multiply(inverse(multiply(inverse(multiply(V2, W2)), multiply(V2, inverse(inverse(multiply(inverse(W), W)))))), inverse(multiply(inverse(W2), W2)))))))))))), inverse(multiply(inverse(Y), Y))))))))))))
% 11.57/1.92 = { by lemma 6 R->L }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(Y, inverse(inverse(multiply(inverse(multiply(inverse(Y), Y)), inverse(multiply(inverse(multiply(inverse(multiply(Y, inverse(multiply(inverse(Y), Y)))), multiply(inverse(multiply(inverse(multiply(Z2, Y)), multiply(Z2, inverse(inverse(multiply(Y, inverse(multiply(Y, inverse(multiply(inverse(Y), Y)))))))))), inverse(multiply(W2, inverse(multiply(inverse(multiply(inverse(multiply(V2, W2)), multiply(V2, inverse(inverse(multiply(inverse(W), W)))))), inverse(multiply(inverse(W2), W2))))))))), inverse(multiply(inverse(inverse(multiply(inverse(Y), Y))), inverse(multiply(inverse(Y), Y)))))))))))))))))
% 11.57/1.92 = { by lemma 26 }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(Y, inverse(multiply(W2, inverse(multiply(inverse(multiply(inverse(multiply(V2, W2)), multiply(V2, inverse(inverse(multiply(inverse(W), W)))))), inverse(multiply(inverse(W2), W2))))))))))))))
% 11.57/1.92 = { by axiom 1 (single_axiom) }
% 11.57/1.92 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(Y, inverse(multiply(inverse(W), W))))))))))
% 11.57/1.92 = { by lemma 9 }
% 11.57/1.92 inverse(multiply(T2, inverse(multiply(inverse(multiply(inverse(multiply(S2, T2)), multiply(S2, inverse(Y)))), inverse(multiply(inverse(T2), T2))))))
% 11.57/1.92 = { by lemma 6 }
% 11.57/1.92 multiply(inverse(multiply(inverse(multiply(X3, S2)), multiply(X3, inverse(inverse(multiply(S2, inverse(Y))))))), inverse(multiply(inverse(S2), S2)))
% 11.57/1.92 = { by lemma 10 }
% 11.57/1.92 Y
% 11.57/1.92
% 11.57/1.92 Lemma 28: multiply(multiply(inverse(X), X), multiply(Y, Z)) = multiply(W, multiply(inverse(multiply(inverse(Y), W)), Z)).
% 11.57/1.92 Proof:
% 11.57/1.92 multiply(multiply(inverse(X), X), multiply(Y, Z))
% 11.57/1.92 = { by lemma 19 R->L }
% 11.57/1.92 multiply(multiply(inverse(X), X), inverse(multiply(inverse(multiply(Y, Z)), multiply(inverse(X), X))))
% 11.57/1.92 = { by lemma 25 R->L }
% 11.57/1.92 multiply(multiply(inverse(X), X), inverse(multiply(inverse(multiply(Y, Z)), inverse(multiply(multiply(inverse(V), V), multiply(inverse(X), X))))))
% 11.57/1.92 = { by lemma 23 R->L }
% 11.57/1.92 multiply(multiply(inverse(X), X), inverse(multiply(inverse(multiply(Y, Z)), inverse(multiply(inverse(multiply(inverse(X), X)), multiply(inverse(X), X))))))
% 11.57/1.92 = { by lemma 19 R->L }
% 11.57/1.92 multiply(multiply(inverse(X), X), inverse(multiply(inverse(multiply(inverse(multiply(inverse(Y), multiply(inverse(X), X))), Z)), inverse(multiply(inverse(multiply(inverse(X), X)), multiply(inverse(X), X))))))
% 11.57/1.92 = { by lemma 5 R->L }
% 11.57/1.92 multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(inverse(Y), W)), Z)), inverse(multiply(inverse(W), W)))))
% 11.57/1.92 = { by lemma 21 }
% 11.57/1.92 multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(inverse(Y), W)), Z)), multiply(inverse(U), U))))
% 11.57/1.92 = { by lemma 19 }
% 11.57/1.92 multiply(W, multiply(inverse(multiply(inverse(Y), W)), Z))
% 11.57/1.92
% 11.57/1.92 Lemma 29: multiply(X, multiply(inverse(X), Y)) = Y.
% 11.57/1.92 Proof:
% 11.57/1.92 multiply(X, multiply(inverse(X), Y))
% 11.57/1.92 = { by lemma 27 R->L }
% 11.57/1.92 multiply(X, multiply(inverse(multiply(multiply(inverse(Z), Z), X)), Y))
% 11.57/1.92 = { by lemma 21 R->L }
% 11.57/1.92 multiply(X, multiply(inverse(multiply(inverse(multiply(inverse(W), W)), X)), Y))
% 11.57/1.92 = { by lemma 28 R->L }
% 11.57/1.92 multiply(multiply(inverse(V), V), multiply(multiply(inverse(W), W), Y))
% 11.57/1.92 = { by lemma 27 }
% 11.57/1.92 multiply(multiply(inverse(V), V), Y)
% 11.57/1.92 = { by lemma 27 }
% 11.57/1.92 Y
% 11.57/1.92
% 11.57/1.92 Lemma 30: multiply(inverse(X), multiply(inverse(Y), Y)) = inverse(X).
% 11.57/1.92 Proof:
% 11.57/1.92 multiply(inverse(X), multiply(inverse(Y), Y))
% 11.57/1.92 = { by lemma 20 R->L }
% 11.57/1.92 inverse(multiply(X, multiply(inverse(X), X)))
% 11.57/1.92 = { by lemma 29 }
% 11.57/1.92 inverse(X)
% 11.57/1.92
% 11.57/1.92 Lemma 31: inverse(inverse(X)) = X.
% 11.57/1.92 Proof:
% 11.57/1.92 inverse(inverse(X))
% 11.57/1.92 = { by lemma 30 R->L }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(inverse(Y), Y)))
% 11.57/1.92 = { by lemma 19 }
% 11.57/1.92 X
% 11.57/1.92
% 11.57/1.92 Lemma 32: multiply(inverse(X), X) = multiply(Y, inverse(Y)).
% 11.57/1.92 Proof:
% 11.57/1.92 multiply(inverse(X), X)
% 11.57/1.92 = { by lemma 22 R->L }
% 11.57/1.92 multiply(Y, multiply(inverse(Y), multiply(inverse(Z), Z)))
% 11.57/1.92 = { by lemma 30 }
% 11.57/1.92 multiply(Y, inverse(Y))
% 11.57/1.92
% 11.57/1.92 Lemma 33: inverse(multiply(X, inverse(X))) = multiply(Y, inverse(Y)).
% 11.57/1.92 Proof:
% 11.57/1.92 inverse(multiply(X, inverse(X)))
% 11.57/1.92 = { by lemma 32 R->L }
% 11.57/1.92 inverse(multiply(inverse(Z), Z))
% 11.57/1.92 = { by lemma 21 }
% 11.57/1.92 multiply(inverse(W), W)
% 11.57/1.92 = { by lemma 32 }
% 11.57/1.92 multiply(Y, inverse(Y))
% 11.57/1.92
% 11.57/1.92 Lemma 34: inverse(multiply(inverse(X), multiply(Y, inverse(Y)))) = X.
% 11.57/1.92 Proof:
% 11.57/1.92 inverse(multiply(inverse(X), multiply(Y, inverse(Y))))
% 11.57/1.92 = { by lemma 32 R->L }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))), multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))), multiply(inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))), multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))))))
% 11.57/1.92 = { by lemma 21 }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(multiply(inverse(Z), Z), multiply(inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))), multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))))))
% 11.57/1.92 = { by lemma 20 R->L }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(multiply(inverse(Z), Z), inverse(multiply(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)), multiply(inverse(W), W))))))
% 11.57/1.92 = { by lemma 21 R->L }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(multiply(inverse(Z), Z), inverse(multiply(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))))))))
% 11.57/1.92 = { by lemma 21 R->L }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(multiply(inverse(Z), Z), inverse(multiply(multiply(inverse(inverse(multiply(inverse(V), V))), multiply(inverse(Z), Z)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))))))))
% 11.57/1.92 = { by lemma 25 R->L }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(multiply(inverse(U), U), multiply(inverse(multiply(inverse(Z), Z)), inverse(multiply(inverse(V), V))))), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))))))))
% 11.57/1.92 = { by lemma 23 R->L }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), inverse(multiply(inverse(V), V))))), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))))))))
% 11.57/1.92 = { by lemma 10 }
% 11.57/1.92 inverse(multiply(inverse(X), multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z))))))))
% 11.57/1.92 = { by axiom 1 (single_axiom) R->L }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(inverse(V), V), inverse(multiply(inverse(multiply(inverse(multiply(V, multiply(inverse(V), V))), multiply(V, inverse(multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))))))))), inverse(multiply(inverse(multiply(inverse(V), V)), multiply(inverse(V), V)))))))))
% 11.57/1.93 = { by lemma 29 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(inverse(V), V), inverse(multiply(inverse(multiply(inverse(V), multiply(V, inverse(multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))))))))), inverse(multiply(inverse(multiply(inverse(V), V)), multiply(inverse(V), V)))))))))
% 11.57/1.93 = { by lemma 32 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(inverse(V), V), inverse(multiply(inverse(multiply(inverse(V), multiply(V, inverse(multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))))))))), inverse(multiply(inverse(multiply(inverse(V), V)), multiply(X2, inverse(X2))))))))))
% 11.57/1.93 = { by lemma 32 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(inverse(V), V), inverse(multiply(inverse(multiply(inverse(V), multiply(V, inverse(multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))))))))), inverse(multiply(inverse(multiply(X2, inverse(X2))), multiply(X2, inverse(X2))))))))))
% 11.57/1.93 = { by lemma 32 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(Y2, inverse(Y2)), inverse(multiply(inverse(multiply(inverse(V), multiply(V, inverse(multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))))))))), inverse(multiply(inverse(multiply(X2, inverse(X2))), multiply(X2, inverse(X2))))))))))
% 11.57/1.93 = { by lemma 21 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(Y2, inverse(Y2)), inverse(multiply(inverse(multiply(inverse(V), multiply(V, inverse(multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))))))))), multiply(inverse(Z2), Z2)))))))
% 11.57/1.93 = { by lemma 19 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(Y2, inverse(Y2)), multiply(inverse(V), multiply(V, inverse(multiply(multiply(inverse(Z), Z), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(T, V)), multiply(T, inverse(inverse(multiply(V, inverse(S))))))), multiply(inverse(Z), Z))), S)), inverse(multiply(inverse(multiply(inverse(Z), Z)), multiply(inverse(Z), Z)))))))))))))
% 11.57/1.93 = { by lemma 11 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(Y2, inverse(Y2)), multiply(inverse(V), multiply(V, multiply(inverse(V), V)))))))
% 11.57/1.93 = { by lemma 29 }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(Y2, inverse(Y2)), multiply(inverse(V), V)))))
% 11.57/1.93 = { by lemma 21 R->L }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(multiply(Y2, inverse(Y2)), inverse(multiply(inverse(W2), W2))))))
% 11.57/1.93 = { by lemma 33 R->L }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(V2, inverse(V2))), inverse(multiply(inverse(W2), W2))))))
% 11.57/1.93 = { by lemma 32 R->L }
% 11.57/1.93 inverse(multiply(inverse(X), inverse(multiply(inverse(multiply(inverse(U2), U2)), inverse(multiply(inverse(W2), W2))))))
% 11.57/1.93 = { by lemma 17 }
% 11.57/1.93 X
% 11.57/1.93
% 11.57/1.93 Lemma 35: multiply(multiply(inverse(X), inverse(Y)), Y) = inverse(X).
% 11.57/1.93 Proof:
% 11.57/1.93 multiply(multiply(inverse(X), inverse(Y)), Y)
% 11.57/1.93 = { by lemma 34 R->L }
% 11.57/1.93 multiply(inverse(multiply(inverse(multiply(inverse(X), inverse(Y))), multiply(Z, inverse(Z)))), Y)
% 11.57/1.93 = { by lemma 25 R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(inverse(Y), multiply(inverse(multiply(inverse(X), inverse(Y))), multiply(Z, inverse(Z))))))
% 11.57/1.93 = { by lemma 32 R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(inverse(Y), multiply(inverse(multiply(inverse(X), inverse(Y))), multiply(inverse(V), V)))))
% 11.57/1.93 = { by lemma 20 R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(inverse(Y), inverse(multiply(multiply(inverse(X), inverse(Y)), multiply(inverse(U), U))))))
% 11.57/1.93 = { by lemma 21 R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(inverse(Y), inverse(multiply(multiply(inverse(X), inverse(Y)), inverse(multiply(inverse(inverse(Y)), inverse(Y))))))))
% 11.57/1.93 = { by lemma 19 R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(inverse(Y), inverse(multiply(inverse(multiply(inverse(multiply(inverse(X), inverse(Y))), multiply(inverse(X), X))), inverse(multiply(inverse(inverse(Y)), inverse(Y))))))))
% 11.57/1.93 = { by axiom 1 (single_axiom) R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), inverse(multiply(T, inverse(multiply(inverse(multiply(inverse(multiply(S, T)), multiply(S, inverse(multiply(inverse(Y), inverse(multiply(inverse(multiply(inverse(multiply(inverse(X), inverse(Y))), multiply(inverse(X), X))), inverse(multiply(inverse(inverse(Y)), inverse(Y)))))))))), inverse(multiply(inverse(T), T))))))))
% 11.57/1.93 = { by lemma 2 }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), inverse(multiply(T, inverse(multiply(inverse(multiply(inverse(multiply(S, T)), multiply(S, multiply(X2, inverse(multiply(inverse(multiply(inverse(multiply(Y2, X2)), multiply(Y2, inverse(X)))), inverse(multiply(inverse(X2), X2)))))))), inverse(multiply(inverse(T), T))))))))
% 11.57/1.93 = { by lemma 2 R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), inverse(multiply(T, inverse(multiply(inverse(multiply(inverse(multiply(S, T)), multiply(S, inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Z2, X)), multiply(Z2, X))), inverse(multiply(inverse(X), X))))))))), inverse(multiply(inverse(T), T))))))))
% 11.57/1.93 = { by axiom 1 (single_axiom) }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Z2, X)), multiply(Z2, X))), inverse(multiply(inverse(X), X)))))))
% 11.57/1.93 = { by lemma 15 R->L }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(X, inverse(multiply(inverse(multiply(inverse(X), X)), inverse(multiply(inverse(X), X)))))))
% 11.57/1.93 = { by lemma 18 }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(X, multiply(inverse(X), X))))
% 11.57/1.93 = { by lemma 29 }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), X))
% 11.57/1.93 = { by lemma 27 }
% 11.57/1.93 inverse(X)
% 11.57/1.93
% 11.57/1.93 Lemma 36: inverse(multiply(X, multiply(multiply(inverse(X), inverse(Y)), Z))) = multiply(inverse(Z), Y).
% 11.57/1.93 Proof:
% 11.57/1.93 inverse(multiply(X, multiply(multiply(inverse(X), inverse(Y)), Z)))
% 11.57/1.93 = { by lemma 31 R->L }
% 11.57/1.93 inverse(multiply(inverse(inverse(X)), multiply(multiply(inverse(X), inverse(Y)), Z)))
% 11.57/1.93 = { by lemma 35 R->L }
% 11.57/1.93 inverse(multiply(inverse(multiply(multiply(inverse(X), inverse(Y)), Y)), multiply(multiply(inverse(X), inverse(Y)), Z)))
% 11.57/1.93 = { by lemma 23 }
% 11.57/1.93 inverse(multiply(multiply(inverse(W), W), multiply(inverse(Y), Z)))
% 11.57/1.93 = { by lemma 25 }
% 11.57/1.93 multiply(inverse(Z), Y)
% 11.57/1.93
% 11.57/1.93 Lemma 37: multiply(inverse(multiply(X, Y)), multiply(X, Z)) = multiply(W, multiply(multiply(inverse(W), inverse(Y)), Z)).
% 11.57/1.93 Proof:
% 11.57/1.93 multiply(inverse(multiply(X, Y)), multiply(X, Z))
% 11.57/1.93 = { by lemma 14 }
% 11.57/1.93 multiply(inverse(multiply(multiply(inverse(W), inverse(Y)), Y)), multiply(multiply(inverse(W), inverse(Y)), Z))
% 11.57/1.93 = { by lemma 35 }
% 11.57/1.93 multiply(inverse(inverse(W)), multiply(multiply(inverse(W), inverse(Y)), Z))
% 11.57/1.93 = { by lemma 31 }
% 11.57/1.93 multiply(W, multiply(multiply(inverse(W), inverse(Y)), Z))
% 11.57/1.93
% 11.57/1.93 Lemma 38: inverse(multiply(X, multiply(Y, inverse(Y)))) = multiply(inverse(X), multiply(Z, inverse(Z))).
% 11.57/1.93 Proof:
% 11.57/1.93 inverse(multiply(X, multiply(Y, inverse(Y))))
% 11.57/1.93 = { by lemma 32 R->L }
% 11.57/1.93 inverse(multiply(X, multiply(inverse(W), W)))
% 11.57/1.93 = { by lemma 20 }
% 11.57/1.93 multiply(inverse(X), multiply(inverse(V), V))
% 11.57/1.93 = { by lemma 32 }
% 11.57/1.93 multiply(inverse(X), multiply(Z, inverse(Z)))
% 11.57/1.93
% 11.57/1.93 Lemma 39: multiply(inverse(multiply(X, Y)), X) = multiply(inverse(Y), multiply(Z, inverse(Z))).
% 11.57/1.93 Proof:
% 11.57/1.93 multiply(inverse(multiply(X, Y)), X)
% 11.57/1.93 = { by lemma 36 R->L }
% 11.57/1.93 inverse(multiply(W, multiply(multiply(inverse(W), inverse(X)), multiply(X, Y))))
% 11.57/1.93 = { by lemma 37 R->L }
% 11.57/1.93 inverse(multiply(inverse(multiply(V, X)), multiply(V, multiply(X, Y))))
% 11.57/1.93 = { by lemma 23 }
% 11.57/1.93 inverse(multiply(multiply(inverse(U), U), multiply(inverse(X), multiply(X, Y))))
% 11.57/1.93 = { by lemma 28 }
% 11.57/1.93 inverse(multiply(Y, multiply(inverse(multiply(inverse(inverse(X)), Y)), multiply(X, Y))))
% 11.57/1.93 = { by lemma 31 }
% 11.57/1.93 inverse(multiply(Y, multiply(inverse(multiply(X, Y)), multiply(X, Y))))
% 11.57/1.93 = { by lemma 32 }
% 11.57/1.93 inverse(multiply(Y, multiply(T, inverse(T))))
% 11.57/1.93 = { by lemma 38 }
% 11.57/1.93 multiply(inverse(Y), multiply(Z, inverse(Z)))
% 11.57/1.93
% 11.57/1.93 Lemma 40: inverse(multiply(X, multiply(inverse(multiply(Y, X)), Z))) = multiply(inverse(Z), Y).
% 11.57/1.93 Proof:
% 11.57/1.93 inverse(multiply(X, multiply(inverse(multiply(Y, X)), Z)))
% 11.57/1.93 = { by lemma 34 R->L }
% 11.57/1.93 inverse(multiply(inverse(multiply(inverse(X), multiply(W, inverse(W)))), multiply(inverse(multiply(Y, X)), Z)))
% 11.57/1.93 = { by lemma 39 R->L }
% 11.57/1.93 inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), Y)), multiply(inverse(multiply(Y, X)), Z)))
% 11.57/1.93 = { by lemma 37 }
% 11.57/1.93 inverse(multiply(V, multiply(multiply(inverse(V), inverse(Y)), Z)))
% 11.57/1.93 = { by lemma 36 }
% 11.57/1.93 multiply(inverse(Z), Y)
% 11.57/1.93
% 11.57/1.93 Lemma 41: multiply(inverse(multiply(X, inverse(multiply(Y, X)))), Z) = multiply(Y, Z).
% 11.57/1.93 Proof:
% 11.57/1.93 multiply(inverse(multiply(X, inverse(multiply(Y, X)))), Z)
% 11.57/1.93 = { by lemma 7 R->L }
% 11.57/1.93 multiply(Y, inverse(inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(Y, X)), multiply(inverse(multiply(X, inverse(multiply(Y, X)))), Z))), inverse(multiply(inverse(X), X))))))))
% 11.57/1.93 = { by lemma 40 }
% 11.57/1.93 multiply(Y, inverse(inverse(multiply(X, inverse(multiply(multiply(inverse(Z), X), inverse(multiply(inverse(X), X))))))))
% 11.57/1.93 = { by lemma 21 }
% 11.57/1.93 multiply(Y, inverse(inverse(multiply(X, inverse(multiply(multiply(inverse(Z), X), multiply(inverse(W), W)))))))
% 11.57/1.93 = { by lemma 20 }
% 11.57/1.93 multiply(Y, inverse(inverse(multiply(X, multiply(inverse(multiply(inverse(Z), X)), multiply(inverse(V), V))))))
% 11.57/1.93 = { by lemma 24 }
% 11.57/1.93 multiply(Y, inverse(inverse(multiply(X, multiply(inverse(multiply(U, X)), multiply(U, Z))))))
% 11.57/1.93 = { by lemma 40 }
% 11.57/1.93 multiply(Y, inverse(multiply(inverse(multiply(U, Z)), U)))
% 11.57/1.93 = { by lemma 39 }
% 11.57/1.93 multiply(Y, inverse(multiply(inverse(Z), multiply(T, inverse(T)))))
% 11.57/1.94 = { by lemma 34 }
% 11.57/1.94 multiply(Y, Z)
% 11.57/1.94
% 11.57/1.94 Lemma 42: inverse(multiply(X, inverse(multiply(Y, X)))) = Y.
% 11.57/1.94 Proof:
% 11.57/1.94 inverse(multiply(X, inverse(multiply(Y, X))))
% 11.57/1.94 = { by lemma 13 R->L }
% 11.57/1.94 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(X, inverse(multiply(Y, X)))), inverse(multiply(inverse(W), W))))))))))
% 11.57/1.94 = { by lemma 41 }
% 11.57/1.94 inverse(multiply(inverse(multiply(Z, W)), multiply(Z, inverse(inverse(multiply(W, inverse(multiply(Y, inverse(multiply(inverse(W), W))))))))))
% 11.57/1.94 = { by lemma 13 }
% 11.57/1.94 Y
% 11.57/1.94
% 11.57/1.94 Lemma 43: multiply(inverse(inverse(inverse(multiply(X, Y)))), X) = inverse(Y).
% 11.57/1.94 Proof:
% 11.57/1.94 multiply(inverse(inverse(inverse(multiply(X, Y)))), X)
% 11.57/1.94 = { by lemma 3 R->L }
% 11.57/1.94 multiply(inverse(inverse(inverse(multiply(X, multiply(Z, inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(Y))))), inverse(multiply(inverse(Z), Z))))))))), X)
% 11.57/1.94 = { by lemma 19 R->L }
% 11.57/1.94 multiply(inverse(inverse(inverse(multiply(X, inverse(multiply(inverse(multiply(Z, inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(Y))))), inverse(multiply(inverse(Z), Z)))))), multiply(inverse(V), V))))))), X)
% 11.57/1.94 = { by lemma 21 R->L }
% 11.57/1.94 multiply(inverse(inverse(inverse(multiply(X, inverse(multiply(inverse(multiply(Z, inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(Y))))), inverse(multiply(inverse(Z), Z)))))), inverse(multiply(inverse(X), X)))))))), X)
% 11.57/1.94 = { by lemma 31 R->L }
% 11.57/1.94 multiply(inverse(inverse(inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(inverse(Z)), inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(Y))))), inverse(multiply(inverse(Z), Z)))))), inverse(multiply(inverse(X), X)))))))), X)
% 11.57/1.94 = { by lemma 35 R->L }
% 11.57/1.94 multiply(inverse(inverse(inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(Z), inverse(X)), X)), inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(Y))))), inverse(multiply(inverse(Z), Z)))))), inverse(multiply(inverse(X), X)))))))), X)
% 11.57/1.94 = { by lemma 36 R->L }
% 11.57/1.94 inverse(multiply(Z, multiply(multiply(inverse(Z), inverse(X)), inverse(inverse(multiply(X, inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(Z), inverse(X)), X)), inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(Y))))), inverse(multiply(inverse(Z), Z)))))), inverse(multiply(inverse(X), X))))))))))
% 11.57/1.94 = { by lemma 7 }
% 11.57/1.94 inverse(multiply(Z, inverse(multiply(inverse(multiply(inverse(multiply(W, Z)), multiply(W, inverse(inverse(Y))))), inverse(multiply(inverse(Z), Z))))))
% 11.57/1.94 = { by lemma 6 }
% 11.57/1.94 multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(inverse(multiply(W, inverse(inverse(Y)))))))), inverse(multiply(inverse(W), W)))
% 11.57/1.94 = { by lemma 10 }
% 11.57/1.94 inverse(Y)
% 11.57/1.94
% 11.57/1.94 Lemma 44: multiply(multiply(X, Y), Z) = multiply(X, multiply(Y, Z)).
% 11.57/1.94 Proof:
% 11.57/1.94 multiply(multiply(X, Y), Z)
% 11.57/1.94 = { by lemma 31 R->L }
% 11.57/1.94 multiply(multiply(inverse(inverse(X)), Y), Z)
% 11.57/1.94 = { by lemma 42 R->L }
% 11.57/1.94 multiply(multiply(inverse(inverse(inverse(multiply(Y, inverse(multiply(X, Y)))))), Y), Z)
% 11.57/1.94 = { by lemma 43 }
% 11.57/1.94 multiply(inverse(inverse(multiply(X, Y))), Z)
% 11.57/1.94 = { by lemma 7 R->L }
% 11.57/1.94 multiply(X, inverse(inverse(multiply(Y, inverse(multiply(inverse(multiply(inverse(multiply(X, Y)), multiply(inverse(inverse(multiply(X, Y))), Z))), inverse(multiply(inverse(Y), Y))))))))
% 11.57/1.94 = { by lemma 29 }
% 11.57/1.94 multiply(X, inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))))
% 11.57/1.94 = { by lemma 7 R->L }
% 11.57/1.94 multiply(X, multiply(Y, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, W)), inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))))), inverse(multiply(inverse(W), W)))))))))
% 11.57/1.94 = { by lemma 31 R->L }
% 11.57/1.94 multiply(X, multiply(Y, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, inverse(inverse(W)))), inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))))), inverse(multiply(inverse(W), W)))))))))
% 11.57/1.94 = { by lemma 35 R->L }
% 11.57/1.94 multiply(X, multiply(Y, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(inverse(multiply(Y, inverse(multiply(multiply(inverse(W), inverse(Y)), Y)))), inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))))), inverse(multiply(inverse(W), W)))))))))
% 11.57/1.94 = { by lemma 42 }
% 11.57/1.94 multiply(X, multiply(Y, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(multiply(inverse(W), inverse(Y)), inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))))), inverse(multiply(inverse(W), W)))))))))
% 11.57/1.94 = { by lemma 21 }
% 11.57/1.94 multiply(X, multiply(Y, inverse(inverse(multiply(W, inverse(multiply(inverse(multiply(multiply(inverse(W), inverse(Y)), inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))))), multiply(inverse(V), V))))))))
% 11.57/1.94 = { by lemma 19 }
% 11.57/1.94 multiply(X, multiply(Y, inverse(inverse(multiply(W, multiply(multiply(inverse(W), inverse(Y)), inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y)))))))))))))
% 11.57/1.94 = { by lemma 36 }
% 11.57/1.94 multiply(X, multiply(Y, inverse(multiply(inverse(inverse(inverse(multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y)))))))), Y))))
% 11.57/1.94 = { by lemma 43 }
% 11.57/1.94 multiply(X, multiply(Y, inverse(inverse(inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))))
% 11.57/1.94 = { by lemma 31 }
% 11.57/1.94 multiply(X, multiply(Y, inverse(multiply(inverse(Z), inverse(multiply(inverse(Y), Y))))))
% 11.57/1.94 = { by lemma 21 }
% 11.57/1.94 multiply(X, multiply(Y, inverse(multiply(inverse(Z), multiply(inverse(U), U)))))
% 11.57/1.94 = { by lemma 19 }
% 11.57/1.94 multiply(X, multiply(Y, Z))
% 11.57/1.94
% 11.57/1.94 Lemma 45: multiply(multiply(X, inverse(X)), Y) = Y.
% 11.57/1.94 Proof:
% 11.57/1.94 multiply(multiply(X, inverse(X)), Y)
% 11.57/1.94 = { by lemma 32 R->L }
% 11.57/1.94 multiply(multiply(inverse(Z), Z), Y)
% 11.57/1.94 = { by lemma 27 }
% 11.57/1.94 Y
% 11.57/1.94
% 11.57/1.94 Goal 1 (prove_these_axioms): tuple(multiply(inverse(a1), a1), multiply(multiply(inverse(b2), b2), a2), multiply(multiply(a3, b3), c3)) = tuple(multiply(inverse(b1), b1), a2, multiply(a3, multiply(b3, c3))).
% 11.57/1.94 Proof:
% 11.57/1.94 tuple(multiply(inverse(a1), a1), multiply(multiply(inverse(b2), b2), a2), multiply(multiply(a3, b3), c3))
% 11.57/1.94 = { by lemma 44 }
% 11.57/1.94 tuple(multiply(inverse(a1), a1), multiply(inverse(b2), multiply(b2, a2)), multiply(multiply(a3, b3), c3))
% 11.57/1.94 = { by lemma 29 R->L }
% 11.57/1.94 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), multiply(b2, a2)), multiply(multiply(a3, b3), c3))
% 11.57/1.94 = { by lemma 19 R->L }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(b2, a2)), multiply(inverse(Y), Y)))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 21 R->L }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(b2, a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 26 R->L }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(W), W)), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(inverse(multiply(W, multiply(inverse(V), V))))))), inverse(b2)))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 20 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(W), W)), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(inverse(T), T)))))), inverse(b2)))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), inverse(multiply(inverse(W), W)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 21 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(W), W)), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(inverse(T), T)))))), inverse(b2)))), inverse(multiply(inverse(inverse(multiply(inverse(W), W))), multiply(inverse(S), S))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 21 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(W), W)), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(inverse(T), T)))))), inverse(b2)))), inverse(multiply(inverse(multiply(inverse(X2), X2)), multiply(inverse(S), S))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 21 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(Y2), Y2), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(inverse(T), T)))))), inverse(b2)))), inverse(multiply(inverse(multiply(inverse(X2), X2)), multiply(inverse(S), S))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 32 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(Y2), Y2), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(inverse(T), T)))))), inverse(b2)))), inverse(multiply(inverse(multiply(inverse(X2), X2)), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 32 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(Y2), Y2), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(inverse(T), T)))))), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 32 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(Y2), Y2), inverse(multiply(inverse(multiply(multiply(inverse(V), V), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(V2, inverse(V2))))))), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 32 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(Y2), Y2), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(V2, inverse(V2))))))), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 32 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(inverse(multiply(U, W)), multiply(U, inverse(multiply(inverse(W), multiply(V2, inverse(V2))))))), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 37 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(T2, multiply(multiply(inverse(T2), inverse(W)), inverse(multiply(inverse(W), multiply(V2, inverse(V2))))))), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 36 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(multiply(inverse(inverse(multiply(inverse(W), multiply(V2, inverse(V2))))), W), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 34 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(multiply(inverse(W), W), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 32 }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(multiply(S2, inverse(S2)), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 34 R->L }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), multiply(X3, inverse(X3)))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.95 = { by lemma 45 R->L }
% 11.57/1.95 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), multiply(X3, inverse(multiply(multiply(Y3, inverse(Y3)), X3))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 17 R->L }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), inverse(multiply(inverse(multiply(X3, inverse(multiply(multiply(Y3, inverse(Y3)), X3)))), inverse(multiply(inverse(multiply(inverse(Z3), Z3)), inverse(multiply(inverse(W3), W3)))))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 41 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), inverse(multiply(multiply(Y3, inverse(Y3)), inverse(multiply(inverse(multiply(inverse(Z3), Z3)), inverse(multiply(inverse(W3), W3)))))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 18 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), inverse(multiply(multiply(Y3, inverse(Y3)), multiply(inverse(Z3), Z3))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 20 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), multiply(inverse(multiply(Y3, inverse(Y3))), multiply(inverse(V3), V3)))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 32 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), multiply(inverse(multiply(Y3, inverse(Y3))), multiply(U3, inverse(U3))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 38 R->L }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(multiply(S2, inverse(S2)), inverse(b2))), inverse(multiply(multiply(Y3, inverse(Y3)), multiply(T3, inverse(T3)))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 33 R->L }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(multiply(Y3, inverse(Y3)), multiply(T3, inverse(T3)))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 33 R->L }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(T3, inverse(T3))), multiply(T3, inverse(T3)))))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 21 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), inverse(multiply(inverse(multiply(inverse(multiply(X, inverse(X))), inverse(b2))), multiply(inverse(S3), S3))))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 19 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2)))), inverse(multiply(inverse(multiply(W2, inverse(W2))), multiply(Z2, inverse(Z2)))))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 34 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2)))), multiply(W2, inverse(W2)))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 34 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(U2, inverse(U2)), multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 45 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2)))), a2)), inverse(multiply(inverse(Z), Z))))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 21 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), inverse(multiply(inverse(multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2)))), a2)), multiply(inverse(X4), X4)))), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 19 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), multiply(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2))), multiply(inverse(multiply(multiply(X, inverse(X)), multiply(inverse(multiply(X, inverse(X))), inverse(b2)))), a2)), multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 29 }
% 11.57/1.96 tuple(multiply(inverse(a1), a1), a2, multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 32 }
% 11.57/1.96 tuple(multiply(Y4, inverse(Y4)), a2, multiply(multiply(a3, b3), c3))
% 11.57/1.96 = { by lemma 44 }
% 11.57/1.96 tuple(multiply(Y4, inverse(Y4)), a2, multiply(a3, multiply(b3, c3)))
% 11.57/1.96 = { by lemma 32 R->L }
% 11.57/1.96 tuple(multiply(inverse(b1), b1), a2, multiply(a3, multiply(b3, c3)))
% 11.57/1.96 % SZS output end Proof
% 11.57/1.96
% 11.57/1.96 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------