%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : GRP082-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:13 AM UTC 2026
% Result : Unsatisfiable 6.24s 1.22s
% Output : Proof 9.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP082-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 27 09:16:24 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.24/1.22 Command-line arguments: --no-flatten-goal
% 6.24/1.22
% 6.24/1.22 % SZS status Unsatisfiable
% 6.24/1.22
% 9.22/1.62 % SZS output start Proof
% 9.22/1.62 Axiom 1 (multiply): multiply(X, Y) = inverse(double_divide(Y, X)).
% 9.22/1.62 Axiom 2 (single_axiom): double_divide(inverse(X), inverse(double_divide(inverse(double_divide(X, double_divide(Y, Z))), double_divide(W, double_divide(Y, W))))) = Z.
% 9.22/1.62
% 9.22/1.62 Lemma 3: double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), multiply(double_divide(Z, W), X))) = W.
% 9.22/1.62 Proof:
% 9.22/1.62 double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), multiply(double_divide(Z, W), X)))
% 9.22/1.62 = { by axiom 1 (multiply) }
% 9.22/1.62 double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), inverse(double_divide(X, double_divide(Z, W)))))
% 9.22/1.62 = { by axiom 1 (multiply) }
% 9.22/1.62 double_divide(inverse(X), inverse(double_divide(inverse(double_divide(X, double_divide(Z, W))), double_divide(Y, double_divide(Z, Y)))))
% 9.22/1.62 = { by axiom 2 (single_axiom) }
% 9.22/1.62 W
% 9.22/1.62
% 9.22/1.62 Lemma 4: multiply(multiply(double_divide(X, double_divide(Y, X)), multiply(double_divide(Y, Z), W)), inverse(W)) = inverse(Z).
% 9.22/1.62 Proof:
% 9.22/1.62 multiply(multiply(double_divide(X, double_divide(Y, X)), multiply(double_divide(Y, Z), W)), inverse(W))
% 9.22/1.62 = { by axiom 1 (multiply) }
% 9.22/1.62 inverse(double_divide(inverse(W), multiply(double_divide(X, double_divide(Y, X)), multiply(double_divide(Y, Z), W))))
% 9.22/1.62 = { by lemma 3 }
% 9.22/1.62 inverse(Z)
% 9.22/1.62
% 9.22/1.62 Lemma 5: multiply(double_divide(X, double_divide(Y, X)), multiply(double_divide(Y, Z), W)) = double_divide(inverse(V), multiply(double_divide(U, double_divide(inverse(W), U)), multiply(Z, V))).
% 9.22/1.62 Proof:
% 9.22/1.62 multiply(double_divide(X, double_divide(Y, X)), multiply(double_divide(Y, Z), W))
% 9.22/1.62 = { by lemma 3 R->L }
% 9.22/1.62 double_divide(inverse(V), multiply(double_divide(U, double_divide(inverse(W), U)), multiply(double_divide(inverse(W), multiply(double_divide(X, double_divide(Y, X)), multiply(double_divide(Y, Z), W))), V)))
% 9.22/1.62 = { by lemma 3 }
% 9.22/1.62 double_divide(inverse(V), multiply(double_divide(U, double_divide(inverse(W), U)), multiply(Z, V)))
% 9.22/1.62
% 9.22/1.62 Lemma 6: multiply(double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(W, X))), inverse(Z)) = inverse(W).
% 9.22/1.62 Proof:
% 9.22/1.62 multiply(double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(W, X))), inverse(Z))
% 9.22/1.62 = { by lemma 5 R->L }
% 9.22/1.62 multiply(multiply(double_divide(V, double_divide(U, V)), multiply(double_divide(U, W), Z)), inverse(Z))
% 9.22/1.62 = { by lemma 4 }
% 9.22/1.62 inverse(W)
% 9.22/1.62
% 9.22/1.62 Lemma 7: multiply(double_divide(X, double_divide(inverse(Y), X)), multiply(Z, W)) = double_divide(inverse(inverse(Y)), multiply(double_divide(V, double_divide(inverse(W), V)), inverse(Z))).
% 9.22/1.62 Proof:
% 9.22/1.62 multiply(double_divide(X, double_divide(inverse(Y), X)), multiply(Z, W))
% 9.22/1.62 = { by lemma 3 R->L }
% 9.22/1.63 double_divide(inverse(inverse(Y)), multiply(double_divide(V, double_divide(inverse(W), V)), multiply(double_divide(inverse(W), multiply(double_divide(X, double_divide(inverse(Y), X)), multiply(Z, W))), inverse(Y))))
% 9.22/1.63 = { by lemma 6 }
% 9.22/1.63 double_divide(inverse(inverse(Y)), multiply(double_divide(V, double_divide(inverse(W), V)), inverse(Z)))
% 9.22/1.63
% 9.22/1.63 Lemma 8: double_divide(multiply(X, Y), double_divide(inverse(Z), double_divide(inverse(multiply(X, Y)), multiply(double_divide(W, double_divide(inverse(Z), W)), inverse(V))))) = V.
% 9.22/1.63 Proof:
% 9.22/1.63 double_divide(multiply(X, Y), double_divide(inverse(Z), double_divide(inverse(multiply(X, Y)), multiply(double_divide(W, double_divide(inverse(Z), W)), inverse(V)))))
% 9.22/1.63 = { by axiom 1 (multiply) }
% 9.22/1.63 double_divide(multiply(X, Y), double_divide(inverse(Z), double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(W, double_divide(inverse(Z), W)), inverse(V)))))
% 9.22/1.63 = { by lemma 7 R->L }
% 9.22/1.63 double_divide(multiply(X, Y), double_divide(inverse(Z), multiply(double_divide(U, double_divide(inverse(double_divide(Y, X)), U)), multiply(V, Z))))
% 9.22/1.63 = { by lemma 5 R->L }
% 9.22/1.63 double_divide(multiply(X, Y), multiply(double_divide(T, double_divide(S, T)), multiply(double_divide(S, V), double_divide(Y, X))))
% 9.22/1.63 = { by axiom 1 (multiply) }
% 9.22/1.63 double_divide(inverse(double_divide(Y, X)), multiply(double_divide(T, double_divide(S, T)), multiply(double_divide(S, V), double_divide(Y, X))))
% 9.22/1.63 = { by lemma 3 }
% 9.22/1.63 V
% 9.22/1.63
% 9.22/1.63 Lemma 9: double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(X)), multiply(double_divide(Z, double_divide(inverse(Y), Z)), inverse(W))))) = W.
% 9.22/1.63 Proof:
% 9.22/1.63 double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(X)), multiply(double_divide(Z, double_divide(inverse(Y), Z)), inverse(W)))))
% 9.22/1.63 = { by lemma 4 R->L }
% 9.22/1.63 double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(multiply(multiply(double_divide(V, double_divide(U, V)), multiply(double_divide(U, X), T)), inverse(T))), multiply(double_divide(Z, double_divide(inverse(Y), Z)), inverse(W)))))
% 9.22/1.63 = { by lemma 4 R->L }
% 9.22/1.63 double_divide(multiply(multiply(double_divide(V, double_divide(U, V)), multiply(double_divide(U, X), T)), inverse(T)), double_divide(inverse(Y), double_divide(inverse(multiply(multiply(double_divide(V, double_divide(U, V)), multiply(double_divide(U, X), T)), inverse(T))), multiply(double_divide(Z, double_divide(inverse(Y), Z)), inverse(W)))))
% 9.22/1.63 = { by lemma 8 }
% 9.22/1.63 W
% 9.22/1.63
% 9.22/1.63 Lemma 10: double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(X)), multiply(double_divide(Z, double_divide(inverse(Y), Z)), multiply(W, V))))) = double_divide(V, W).
% 9.22/1.63 Proof:
% 9.22/1.63 double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(X)), multiply(double_divide(Z, double_divide(inverse(Y), Z)), multiply(W, V)))))
% 9.22/1.63 = { by axiom 1 (multiply) }
% 9.22/1.63 double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(X)), multiply(double_divide(Z, double_divide(inverse(Y), Z)), inverse(double_divide(V, W))))))
% 9.22/1.63 = { by lemma 9 }
% 9.22/1.63 double_divide(V, W)
% 9.22/1.63
% 9.22/1.63 Lemma 11: double_divide(inverse(X), double_divide(W, double_divide(inverse(Z), W))) = double_divide(inverse(X), double_divide(Y, double_divide(inverse(Z), Y))).
% 9.22/1.63 Proof:
% 9.22/1.63 double_divide(inverse(X), double_divide(W, double_divide(inverse(Z), W)))
% 9.22/1.63 = { by lemma 10 R->L }
% 9.22/1.63 double_divide(inverse(V), double_divide(inverse(U), double_divide(inverse(inverse(V)), multiply(double_divide(T, double_divide(inverse(U), T)), multiply(double_divide(W, double_divide(inverse(Z), W)), inverse(X))))))
% 9.22/1.63 = { by lemma 3 R->L }
% 9.22/1.63 double_divide(inverse(V), double_divide(inverse(U), double_divide(inverse(inverse(V)), multiply(double_divide(T, double_divide(inverse(U), T)), double_divide(inverse(S), multiply(double_divide(X2, double_divide(inverse(inverse(Y2)), X2)), multiply(double_divide(inverse(inverse(Y2)), multiply(double_divide(W, double_divide(inverse(Z), W)), inverse(X))), S)))))))
% 9.22/1.63 = { by lemma 6 R->L }
% 9.22/1.63 double_divide(inverse(V), double_divide(inverse(U), double_divide(inverse(inverse(V)), multiply(double_divide(T, double_divide(inverse(U), T)), double_divide(inverse(S), multiply(double_divide(X2, double_divide(inverse(inverse(Y2)), X2)), multiply(double_divide(inverse(inverse(Y2)), multiply(double_divide(W, double_divide(inverse(Z), W)), multiply(double_divide(inverse(Z), multiply(double_divide(Z2, double_divide(inverse(Y2), Z2)), multiply(X, Z))), inverse(Y2)))), S)))))))
% 9.22/1.63 = { by lemma 3 }
% 9.22/1.64 double_divide(inverse(V), double_divide(inverse(U), double_divide(inverse(inverse(V)), multiply(double_divide(T, double_divide(inverse(U), T)), double_divide(inverse(S), multiply(double_divide(X2, double_divide(inverse(inverse(Y2)), X2)), multiply(multiply(double_divide(Z2, double_divide(inverse(Y2), Z2)), multiply(X, Z)), S)))))))
% 9.22/1.64 = { by lemma 3 R->L }
% 9.22/1.64 double_divide(inverse(V), double_divide(inverse(U), double_divide(inverse(inverse(V)), multiply(double_divide(T, double_divide(inverse(U), T)), double_divide(inverse(S), multiply(double_divide(X2, double_divide(inverse(inverse(Y2)), X2)), multiply(double_divide(inverse(inverse(Y2)), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(double_divide(inverse(Z), multiply(double_divide(Z2, double_divide(inverse(Y2), Z2)), multiply(X, Z))), inverse(Y2)))), S)))))))
% 9.22/1.64 = { by lemma 6 }
% 9.22/1.64 double_divide(inverse(V), double_divide(inverse(U), double_divide(inverse(inverse(V)), multiply(double_divide(T, double_divide(inverse(U), T)), double_divide(inverse(S), multiply(double_divide(X2, double_divide(inverse(inverse(Y2)), X2)), multiply(double_divide(inverse(inverse(Y2)), multiply(double_divide(Y, double_divide(inverse(Z), Y)), inverse(X))), S)))))))
% 9.22/1.64 = { by lemma 3 }
% 9.22/1.64 double_divide(inverse(V), double_divide(inverse(U), double_divide(inverse(inverse(V)), multiply(double_divide(T, double_divide(inverse(U), T)), multiply(double_divide(Y, double_divide(inverse(Z), Y)), inverse(X))))))
% 9.22/1.64 = { by lemma 10 }
% 9.22/1.64 double_divide(inverse(X), double_divide(Y, double_divide(inverse(Z), Y)))
% 9.22/1.64
% 9.22/1.64 Lemma 12: double_divide(Z, double_divide(inverse(Y), Z)) = double_divide(X, double_divide(inverse(Y), X)).
% 9.22/1.64 Proof:
% 9.22/1.64 double_divide(Z, double_divide(inverse(Y), Z))
% 9.22/1.64 = { by lemma 3 R->L }
% 9.22/1.64 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(inverse(U), double_divide(Z, double_divide(inverse(Y), Z))), W)))
% 9.22/1.64 = { by lemma 11 }
% 9.22/1.64 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(inverse(U), double_divide(X, double_divide(inverse(Y), X))), W)))
% 9.22/1.64 = { by lemma 3 }
% 9.22/1.64 double_divide(X, double_divide(inverse(Y), X))
% 9.22/1.64
% 9.22/1.64 Lemma 13: multiply(double_divide(inverse(X), Z), Z) = multiply(double_divide(inverse(X), Y), Y).
% 9.22/1.64 Proof:
% 9.22/1.64 multiply(double_divide(inverse(X), Z), Z)
% 9.22/1.64 = { by axiom 1 (multiply) }
% 9.22/1.64 inverse(double_divide(Z, double_divide(inverse(X), Z)))
% 9.22/1.64 = { by lemma 4 R->L }
% 9.22/1.64 multiply(multiply(double_divide(W, double_divide(inverse(V), W)), multiply(double_divide(inverse(V), double_divide(Z, double_divide(inverse(X), Z))), U)), inverse(U))
% 9.22/1.64 = { by lemma 11 }
% 9.22/1.64 multiply(multiply(double_divide(W, double_divide(inverse(V), W)), multiply(double_divide(inverse(V), double_divide(Y, double_divide(inverse(X), Y))), U)), inverse(U))
% 9.22/1.64 = { by lemma 4 }
% 9.22/1.64 inverse(double_divide(Y, double_divide(inverse(X), Y)))
% 9.22/1.64 = { by axiom 1 (multiply) R->L }
% 9.22/1.64 multiply(double_divide(inverse(X), Y), Y)
% 9.22/1.64
% 9.22/1.64 Lemma 14: multiply(double_divide(X, double_divide(inverse(Y), X)), double_divide(inverse(Y), inverse(Z))) = multiply(double_divide(inverse(Z), W), W).
% 9.22/1.64 Proof:
% 9.22/1.64 multiply(double_divide(X, double_divide(inverse(Y), X)), double_divide(inverse(Y), inverse(Z)))
% 9.22/1.64 = { by lemma 12 }
% 9.22/1.64 multiply(double_divide(inverse(Z), double_divide(inverse(Y), inverse(Z))), double_divide(inverse(Y), inverse(Z)))
% 9.22/1.64 = { by lemma 13 R->L }
% 9.22/1.64 multiply(double_divide(inverse(Z), W), W)
% 9.22/1.64
% 9.22/1.64 Lemma 15: double_divide(multiply(inverse(X), inverse(Y)), multiply(double_divide(Z, double_divide(W, Z)), multiply(double_divide(inverse(X), V), V))) = double_divide(inverse(Y), W).
% 9.22/1.64 Proof:
% 9.22/1.64 double_divide(multiply(inverse(X), inverse(Y)), multiply(double_divide(Z, double_divide(W, Z)), multiply(double_divide(inverse(X), V), V)))
% 9.22/1.64 = { by axiom 1 (multiply) }
% 9.22/1.64 double_divide(inverse(double_divide(inverse(Y), inverse(X))), multiply(double_divide(Z, double_divide(W, Z)), multiply(double_divide(inverse(X), V), V)))
% 9.22/1.64 = { by lemma 14 R->L }
% 9.22/1.64 double_divide(inverse(double_divide(inverse(Y), inverse(X))), multiply(double_divide(Z, double_divide(W, Z)), multiply(double_divide(W, double_divide(inverse(Y), W)), double_divide(inverse(Y), inverse(X)))))
% 9.22/1.64 = { by lemma 3 }
% 9.22/1.64 double_divide(inverse(Y), W)
% 9.22/1.64
% 9.22/1.64 Lemma 16: double_divide(inverse(V), multiply(double_divide(U, double_divide(inverse(Z), U)), multiply(W, V))) = double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(W, X))).
% 9.22/1.64 Proof:
% 9.22/1.64 double_divide(inverse(V), multiply(double_divide(U, double_divide(inverse(Z), U)), multiply(W, V)))
% 9.22/1.64 = { by lemma 3 R->L }
% 9.22/1.64 double_divide(inverse(V), multiply(double_divide(U, double_divide(inverse(Z), U)), multiply(double_divide(inverse(Z), multiply(double_divide(T, double_divide(S, T)), multiply(double_divide(S, W), Z))), V)))
% 9.22/1.64 = { by lemma 3 }
% 9.22/1.64 multiply(double_divide(T, double_divide(S, T)), multiply(double_divide(S, W), Z))
% 9.22/1.64 = { by lemma 3 R->L }
% 9.22/1.64 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(double_divide(inverse(Z), multiply(double_divide(T, double_divide(S, T)), multiply(double_divide(S, W), Z))), X)))
% 9.22/1.64 = { by lemma 3 }
% 9.22/1.64 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(W, X)))
% 9.22/1.64
% 9.22/1.64 Lemma 17: double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(Z)), multiply(double_divide(W, double_divide(inverse(Y), W)), inverse(Z))))) = X.
% 9.22/1.64 Proof:
% 9.22/1.64 double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(Z)), multiply(double_divide(W, double_divide(inverse(Y), W)), inverse(Z)))))
% 9.22/1.64 = { by lemma 7 R->L }
% 9.22/1.64 double_divide(inverse(X), double_divide(inverse(Y), multiply(double_divide(V, double_divide(inverse(Z), V)), multiply(Z, Y))))
% 9.22/1.64 = { by lemma 16 }
% 9.22/1.64 double_divide(inverse(X), double_divide(inverse(inverse(U)), multiply(double_divide(T, double_divide(inverse(Z), T)), multiply(Z, inverse(U)))))
% 9.22/1.64 = { by axiom 1 (multiply) }
% 9.22/1.64 double_divide(inverse(X), double_divide(inverse(inverse(U)), multiply(double_divide(T, double_divide(inverse(Z), T)), inverse(double_divide(inverse(U), Z)))))
% 9.22/1.64 = { by lemma 7 R->L }
% 9.22/1.64 double_divide(inverse(X), multiply(double_divide(S, double_divide(inverse(U), S)), multiply(double_divide(inverse(U), Z), Z)))
% 9.22/1.64 = { by lemma 13 }
% 9.22/1.64 double_divide(inverse(X), multiply(double_divide(S, double_divide(inverse(U), S)), multiply(double_divide(inverse(U), X), X)))
% 9.22/1.64 = { by lemma 3 }
% 9.22/1.64 X
% 9.22/1.64
% 9.22/1.64 Lemma 18: double_divide(inverse(multiply(X, Y)), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(X, Y))) = double_divide(inverse(inverse(V)), multiply(double_divide(U, double_divide(inverse(W), U)), inverse(V))).
% 9.22/1.64 Proof:
% 9.22/1.64 double_divide(inverse(multiply(X, Y)), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(X, Y)))
% 9.22/1.65 = { by axiom 1 (multiply) }
% 9.22/1.65 double_divide(inverse(multiply(X, Y)), multiply(double_divide(Z, double_divide(inverse(W), Z)), inverse(double_divide(Y, X))))
% 9.22/1.65 = { by axiom 1 (multiply) }
% 9.22/1.65 double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(Z, double_divide(inverse(W), Z)), inverse(double_divide(Y, X))))
% 9.22/1.65 = { by lemma 4 R->L }
% 9.22/1.65 double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(multiply(double_divide(T, double_divide(inverse(S), T)), multiply(double_divide(inverse(S), double_divide(Y, X)), double_divide(Y, X))), inverse(double_divide(Y, X)))))
% 9.22/1.65 = { by lemma 13 R->L }
% 9.22/1.65 double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(multiply(double_divide(T, double_divide(inverse(S), T)), multiply(double_divide(inverse(S), V), V)), inverse(double_divide(Y, X)))))
% 9.22/1.65 = { by lemma 7 }
% 9.22/1.65 double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(double_divide(inverse(inverse(S)), multiply(double_divide(X2, double_divide(inverse(V), X2)), inverse(double_divide(inverse(S), V)))), inverse(double_divide(Y, X)))))
% 9.22/1.65 = { by axiom 1 (multiply) R->L }
% 9.22/1.65 double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(double_divide(inverse(inverse(S)), multiply(double_divide(X2, double_divide(inverse(V), X2)), multiply(V, inverse(S)))), inverse(double_divide(Y, X)))))
% 9.22/1.65 = { by lemma 16 R->L }
% 9.22/1.65 double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(double_divide(inverse(W), multiply(double_divide(Y2, double_divide(inverse(V), Y2)), multiply(V, W))), inverse(double_divide(Y, X)))))
% 9.22/1.65 = { by lemma 7 }
% 9.22/1.65 double_divide(inverse(inverse(double_divide(Y, X))), multiply(double_divide(Z, double_divide(inverse(W), Z)), multiply(double_divide(inverse(W), double_divide(inverse(inverse(V)), multiply(double_divide(U, double_divide(inverse(W), U)), inverse(V)))), inverse(double_divide(Y, X)))))
% 9.22/1.65 = { by lemma 3 }
% 9.22/1.65 double_divide(inverse(inverse(V)), multiply(double_divide(U, double_divide(inverse(W), U)), inverse(V)))
% 9.22/1.65
% 9.22/1.65 Lemma 19: double_divide(inverse(inverse(X)), multiply(double_divide(Y, double_divide(inverse(Z), Y)), inverse(X))) = multiply(double_divide(inverse(Z), W), W).
% 9.22/1.65 Proof:
% 9.22/1.65 double_divide(inverse(inverse(X)), multiply(double_divide(Y, double_divide(inverse(Z), Y)), inverse(X)))
% 9.22/1.65 = { by lemma 18 R->L }
% 9.22/1.65 double_divide(inverse(multiply(double_divide(inverse(Z), W), W)), multiply(double_divide(V, double_divide(inverse(Z), V)), multiply(double_divide(inverse(Z), W), W)))
% 9.22/1.65 = { by lemma 5 }
% 9.22/1.65 double_divide(inverse(multiply(double_divide(inverse(Z), W), W)), double_divide(inverse(U), multiply(double_divide(T, double_divide(inverse(W), T)), multiply(W, U))))
% 9.22/1.65 = { by lemma 7 }
% 9.22/1.65 double_divide(inverse(multiply(double_divide(inverse(Z), W), W)), double_divide(inverse(U), double_divide(inverse(inverse(W)), multiply(double_divide(S, double_divide(inverse(U), S)), inverse(W)))))
% 9.22/1.65 = { by lemma 17 }
% 9.22/1.65 multiply(double_divide(inverse(Z), W), W)
% 9.22/1.65
% 9.22/1.65 Lemma 20: multiply(double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y)), Z) = Z.
% 9.22/1.65 Proof:
% 9.22/1.65 multiply(double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y)), Z)
% 9.22/1.65 = { by lemma 3 R->L }
% 9.22/1.65 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(inverse(U), multiply(double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y)), Z)), W)))
% 9.22/1.65 = { by axiom 1 (multiply) }
% 9.22/1.65 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(inverse(U), inverse(double_divide(Z, double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y))))), W)))
% 9.22/1.65 = { by lemma 15 R->L }
% 9.22/1.65 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(multiply(inverse(T), inverse(U)), multiply(double_divide(double_divide(inverse(X), double_divide(inverse(inverse(S)), multiply(double_divide(X2, double_divide(inverse(X), X2)), inverse(S)))), double_divide(inverse(double_divide(Z, double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y)))), double_divide(inverse(X), double_divide(inverse(inverse(S)), multiply(double_divide(X2, double_divide(inverse(X), X2)), inverse(S)))))), multiply(double_divide(inverse(T), Y2), Y2))), W)))
% 9.22/1.66 = { by lemma 17 }
% 9.22/1.66 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(multiply(inverse(T), inverse(U)), multiply(double_divide(double_divide(inverse(X), double_divide(inverse(inverse(S)), multiply(double_divide(X2, double_divide(inverse(X), X2)), inverse(S)))), double_divide(Z, double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y)))), multiply(double_divide(inverse(T), Y2), Y2))), W)))
% 9.22/1.66 = { by lemma 19 }
% 9.22/1.66 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(multiply(inverse(T), inverse(U)), multiply(double_divide(double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y)), double_divide(Z, double_divide(inverse(X), multiply(double_divide(inverse(X), Y), Y)))), multiply(double_divide(inverse(T), Y2), Y2))), W)))
% 9.22/1.66 = { by lemma 15 }
% 9.22/1.66 double_divide(inverse(W), multiply(double_divide(V, double_divide(inverse(U), V)), multiply(double_divide(inverse(U), Z), W)))
% 9.22/1.66 = { by lemma 3 }
% 9.22/1.66 Z
% 9.22/1.66
% 9.22/1.66 Lemma 21: double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(multiply(double_divide(inverse(W), V), V), inverse(W)))) = multiply(double_divide(U, double_divide(X, U)), Z).
% 9.22/1.66 Proof:
% 9.22/1.66 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), multiply(multiply(double_divide(inverse(W), V), V), inverse(W))))
% 9.22/1.66 = { by axiom 1 (multiply) }
% 9.22/1.66 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), inverse(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)))))
% 9.22/1.66 = { by lemma 20 R->L }
% 9.22/1.66 double_divide(inverse(multiply(double_divide(inverse(T), multiply(double_divide(inverse(T), S), S)), X)), multiply(double_divide(Y, double_divide(inverse(Z), Y)), inverse(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)))))
% 9.22/1.66 = { by axiom 1 (multiply) }
% 9.22/1.66 double_divide(inverse(inverse(double_divide(X, double_divide(inverse(T), multiply(double_divide(inverse(T), S), S))))), multiply(double_divide(Y, double_divide(inverse(Z), Y)), inverse(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)))))
% 9.22/1.66 = { by lemma 7 R->L }
% 9.22/1.66 multiply(double_divide(U, double_divide(inverse(double_divide(X, double_divide(inverse(T), multiply(double_divide(inverse(T), S), S)))), U)), multiply(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)), Z))
% 9.22/1.66 = { by axiom 1 (multiply) R->L }
% 9.22/1.66 multiply(double_divide(U, double_divide(multiply(double_divide(inverse(T), multiply(double_divide(inverse(T), S), S)), X), U)), multiply(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)), Z))
% 9.22/1.66 = { by lemma 20 }
% 9.22/1.66 multiply(double_divide(U, double_divide(X, U)), multiply(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)), Z))
% 9.22/1.66 = { by lemma 20 }
% 9.22/1.66 multiply(double_divide(U, double_divide(X, U)), Z)
% 9.22/1.66
% 9.22/1.66 Lemma 22: double_divide(inverse(V), double_divide(inverse(Z), multiply(double_divide(U, double_divide(inverse(V), U)), inverse(W)))) = double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), multiply(W, X))).
% 9.22/1.66 Proof:
% 9.22/1.66 double_divide(inverse(V), double_divide(inverse(Z), multiply(double_divide(U, double_divide(inverse(V), U)), inverse(W))))
% 9.22/1.66 = { by lemma 20 R->L }
% 9.22/1.66 double_divide(inverse(V), double_divide(inverse(multiply(double_divide(inverse(T), multiply(double_divide(inverse(T), S), S)), Z)), multiply(double_divide(U, double_divide(inverse(V), U)), inverse(W))))
% 9.22/1.66 = { by axiom 1 (multiply) }
% 9.22/1.66 double_divide(inverse(V), double_divide(inverse(inverse(double_divide(Z, double_divide(inverse(T), multiply(double_divide(inverse(T), S), S))))), multiply(double_divide(U, double_divide(inverse(V), U)), inverse(W))))
% 9.22/1.66 = { by lemma 7 R->L }
% 9.22/1.66 double_divide(inverse(V), multiply(double_divide(X2, double_divide(inverse(double_divide(Z, double_divide(inverse(T), multiply(double_divide(inverse(T), S), S)))), X2)), multiply(W, V)))
% 9.22/1.66 = { by lemma 16 }
% 9.22/1.66 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(double_divide(Z, double_divide(inverse(T), multiply(double_divide(inverse(T), S), S)))), Y)), multiply(W, X)))
% 9.22/1.66 = { by axiom 1 (multiply) R->L }
% 9.22/1.66 double_divide(inverse(X), multiply(double_divide(Y, double_divide(multiply(double_divide(inverse(T), multiply(double_divide(inverse(T), S), S)), Z), Y)), multiply(W, X)))
% 9.22/1.66 = { by lemma 20 }
% 9.22/1.66 double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), multiply(W, X)))
% 9.22/1.66
% 9.22/1.66 Lemma 23: double_divide(inverse(X), double_divide(inverse(Y), multiply(double_divide(Z, double_divide(inverse(X), Z)), multiply(W, Y)))) = W.
% 9.22/1.66 Proof:
% 9.22/1.66 double_divide(inverse(X), double_divide(inverse(Y), multiply(double_divide(Z, double_divide(inverse(X), Z)), multiply(W, Y))))
% 9.22/1.66 = { by lemma 5 R->L }
% 9.22/1.66 double_divide(inverse(X), multiply(double_divide(V, double_divide(U, V)), multiply(double_divide(U, W), X)))
% 9.22/1.66 = { by lemma 3 }
% 9.22/1.66 W
% 9.22/1.66
% 9.22/1.66 Lemma 24: multiply(double_divide(X, double_divide(multiply(multiply(double_divide(inverse(Y), Z), Z), inverse(Y)), X)), W) = multiply(double_divide(inverse(W), V), V).
% 9.22/1.66 Proof:
% 9.22/1.66 multiply(double_divide(X, double_divide(multiply(multiply(double_divide(inverse(Y), Z), Z), inverse(Y)), X)), W)
% 9.22/1.66 = { by lemma 21 R->L }
% 9.22/1.66 double_divide(inverse(multiply(multiply(double_divide(inverse(Y), Z), Z), inverse(Y))), multiply(double_divide(U, double_divide(inverse(W), U)), multiply(multiply(double_divide(inverse(Y), Z), Z), inverse(Y))))
% 9.22/1.66 = { by lemma 18 }
% 9.22/1.66 double_divide(inverse(inverse(T)), multiply(double_divide(S, double_divide(inverse(W), S)), inverse(T)))
% 9.22/1.66 = { by lemma 19 }
% 9.22/1.66 multiply(double_divide(inverse(W), V), V)
% 9.22/1.66
% 9.22/1.66 Lemma 25: double_divide(X, double_divide(multiply(multiply(double_divide(inverse(Y), Z), Z), inverse(Y)), X)) = double_divide(inverse(W), W).
% 9.22/1.66 Proof:
% 9.22/1.66 double_divide(X, double_divide(multiply(multiply(double_divide(inverse(Y), Z), Z), inverse(Y)), X))
% 9.22/1.66 = { by lemma 23 R->L }
% 9.22/1.66 double_divide(inverse(V), double_divide(inverse(W), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(double_divide(X, double_divide(multiply(multiply(double_divide(inverse(Y), Z), Z), inverse(Y)), X)), W))))
% 9.22/1.66 = { by lemma 24 }
% 9.22/1.66 double_divide(inverse(V), double_divide(inverse(W), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(double_divide(inverse(W), W), W))))
% 9.22/1.66 = { by lemma 23 }
% 9.22/1.66 double_divide(inverse(W), W)
% 9.22/1.66
% 9.22/1.66 Lemma 26: double_divide(X, double_divide(inverse(Y), multiply(double_divide(Z, double_divide(X, Z)), Y))) = double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)).
% 9.22/1.66 Proof:
% 9.22/1.66 double_divide(X, double_divide(inverse(Y), multiply(double_divide(Z, double_divide(X, Z)), Y)))
% 9.22/1.67 = { by lemma 10 R->L }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Y), multiply(double_divide(Z, double_divide(X, Z)), Y)), X)))))
% 9.22/1.67 = { by lemma 20 R->L }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Y), multiply(double_divide(Z, double_divide(X, Z)), Y)), multiply(double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)), X))))))
% 9.22/1.67 = { by lemma 20 R->L }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Y), multiply(double_divide(Z, double_divide(multiply(double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)), X), Z)), Y)), multiply(double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)), X))))))
% 9.22/1.67 = { by lemma 20 R->L }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Y), multiply(double_divide(Z, double_divide(multiply(double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)), X), Z)), multiply(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)), Y))), multiply(double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)), X))))))
% 9.22/1.67 = { by axiom 1 (multiply) }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Y), multiply(double_divide(Z, double_divide(multiply(double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)), X), Z)), multiply(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)), Y))), inverse(double_divide(X, double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)))))))))
% 9.22/1.67 = { by axiom 1 (multiply) }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Y), multiply(double_divide(Z, double_divide(inverse(double_divide(X, double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)))), Z)), multiply(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)), Y))), inverse(double_divide(X, double_divide(inverse(X2), multiply(double_divide(inverse(X2), Y2), Y2)))))))))
% 9.22/1.67 = { by lemma 6 }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), inverse(double_divide(inverse(W), multiply(double_divide(inverse(W), V), V)))))))
% 9.22/1.67 = { by axiom 1 (multiply) R->L }
% 9.22/1.67 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(inverse(W), V), V), inverse(W))))))
% 9.22/1.67 = { by lemma 10 }
% 9.22/1.67 double_divide(inverse(W), multiply(double_divide(inverse(W), V), V))
% 9.22/1.67
% 9.22/1.67 Lemma 27: double_divide(inverse(W), multiply(double_divide(V, double_divide(Z, V)), W)) = double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), X)).
% 9.22/1.67 Proof:
% 9.22/1.67 double_divide(inverse(W), multiply(double_divide(V, double_divide(Z, V)), W))
% 9.22/1.67 = { by lemma 3 R->L }
% 9.22/1.67 double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), multiply(double_divide(Z, double_divide(inverse(W), multiply(double_divide(V, double_divide(Z, V)), W))), X)))
% 9.22/1.67 = { by lemma 26 }
% 9.22/1.67 double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), multiply(double_divide(inverse(U), multiply(double_divide(inverse(U), T), T)), X)))
% 9.22/1.67 = { by lemma 20 }
% 9.22/1.67 double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, Y)), X))
% 9.22/1.67
% 9.22/1.67 Lemma 28: double_divide(inverse(Z), multiply(double_divide(inverse(W), W), Z)) = double_divide(inverse(X), multiply(double_divide(inverse(Y), Y), X)).
% 9.22/1.67 Proof:
% 9.22/1.67 double_divide(inverse(Z), multiply(double_divide(inverse(W), W), Z))
% 9.22/1.67 = { by lemma 25 R->L }
% 9.22/1.67 double_divide(inverse(Z), multiply(double_divide(S, double_divide(multiply(multiply(double_divide(inverse(U), T), T), inverse(U)), S)), Z))
% 9.22/1.67 = { by lemma 27 }
% 9.22/1.67 double_divide(inverse(X), multiply(double_divide(V, double_divide(multiply(multiply(double_divide(inverse(U), T), T), inverse(U)), V)), X))
% 9.22/1.67 = { by lemma 25 }
% 9.22/1.67 double_divide(inverse(X), multiply(double_divide(inverse(Y), Y), X))
% 9.22/1.67
% 9.22/1.67 Lemma 29: double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), X)) = multiply(double_divide(inverse(W), W), Z).
% 9.22/1.67 Proof:
% 9.22/1.67 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Y)), X))
% 9.22/1.67 = { by lemma 21 R->L }
% 9.22/1.68 double_divide(inverse(X), double_divide(inverse(inverse(Z)), multiply(double_divide(V, double_divide(inverse(X), V)), multiply(multiply(double_divide(inverse(U), U), U), inverse(U)))))
% 9.22/1.68 = { by axiom 1 (multiply) }
% 9.22/1.68 double_divide(inverse(X), double_divide(inverse(inverse(Z)), multiply(double_divide(V, double_divide(inverse(X), V)), inverse(double_divide(inverse(U), multiply(double_divide(inverse(U), U), U))))))
% 9.22/1.68 = { by lemma 22 }
% 9.22/1.68 double_divide(inverse(T), multiply(double_divide(S, double_divide(inverse(Z), S)), multiply(double_divide(inverse(U), multiply(double_divide(inverse(U), U), U)), T)))
% 9.22/1.68 = { by lemma 28 }
% 9.22/1.68 double_divide(inverse(T), multiply(double_divide(S, double_divide(inverse(Z), S)), multiply(double_divide(inverse(Z), multiply(double_divide(inverse(W), W), Z)), T)))
% 9.22/1.68 = { by lemma 3 }
% 9.22/1.68 multiply(double_divide(inverse(W), W), Z)
% 9.22/1.68
% 9.22/1.68 Lemma 30: double_divide(inverse(X), multiply(double_divide(Y, double_divide(multiply(Z, W), Y)), X)) = multiply(double_divide(inverse(V), V), double_divide(W, Z)).
% 9.22/1.68 Proof:
% 9.22/1.68 double_divide(inverse(X), multiply(double_divide(Y, double_divide(multiply(Z, W), Y)), X))
% 9.22/1.68 = { by axiom 1 (multiply) }
% 9.22/1.68 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(double_divide(W, Z)), Y)), X))
% 9.22/1.68 = { by lemma 29 }
% 9.22/1.68 multiply(double_divide(inverse(V), V), double_divide(W, Z))
% 9.22/1.68
% 9.22/1.68 Lemma 31: multiply(double_divide(inverse(X), X), Y) = Y.
% 9.22/1.68 Proof:
% 9.22/1.68 multiply(double_divide(inverse(X), X), Y)
% 9.22/1.68 = { by lemma 29 R->L }
% 9.22/1.68 double_divide(inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), W), W))), multiply(double_divide(V, double_divide(inverse(Y), V)), double_divide(inverse(Z), multiply(double_divide(inverse(Z), W), W))))
% 9.22/1.68 = { by lemma 24 R->L }
% 9.22/1.68 double_divide(inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), W), W))), multiply(double_divide(V, double_divide(inverse(Y), V)), double_divide(inverse(Z), multiply(double_divide(U, double_divide(multiply(multiply(double_divide(inverse(Z), W), W), inverse(Z)), U)), Z))))
% 9.22/1.68 = { by lemma 30 }
% 9.22/1.68 double_divide(inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), W), W))), multiply(double_divide(V, double_divide(inverse(Y), V)), multiply(double_divide(inverse(Y), Y), double_divide(inverse(Z), multiply(double_divide(inverse(Z), W), W)))))
% 9.22/1.68 = { by lemma 3 }
% 9.22/1.68 Y
% 9.22/1.68
% 9.22/1.68 Lemma 32: double_divide(inverse(X), double_divide(inverse(Y), multiply(double_divide(inverse(Y), Z), Z))) = X.
% 9.22/1.68 Proof:
% 9.22/1.68 double_divide(inverse(X), double_divide(inverse(Y), multiply(double_divide(inverse(Y), Z), Z)))
% 9.22/1.68 = { by lemma 19 R->L }
% 9.22/1.68 double_divide(inverse(X), double_divide(inverse(Y), double_divide(inverse(inverse(X)), multiply(double_divide(W, double_divide(inverse(Y), W)), inverse(X)))))
% 9.22/1.68 = { by lemma 9 }
% 9.22/1.68 X
% 9.22/1.68
% 9.22/1.68 Lemma 33: double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Z)), X)) = multiply(double_divide(inverse(W), W), Y).
% 9.22/1.68 Proof:
% 9.22/1.68 double_divide(inverse(X), multiply(double_divide(Y, double_divide(inverse(Z), Z)), X))
% 9.22/1.68 = { by lemma 32 R->L }
% 9.22/1.68 double_divide(inverse(X), multiply(double_divide(inverse(double_divide(Y, double_divide(inverse(Z), Z))), double_divide(inverse(V), multiply(double_divide(inverse(V), V), V))), X))
% 9.22/1.68 = { by axiom 1 (multiply) R->L }
% 9.22/1.68 double_divide(inverse(X), multiply(double_divide(multiply(double_divide(inverse(Z), Z), Y), double_divide(inverse(V), multiply(double_divide(inverse(V), V), V))), X))
% 9.22/1.68 = { by lemma 28 }
% 9.22/1.68 double_divide(inverse(X), multiply(double_divide(multiply(double_divide(inverse(Z), Z), Y), double_divide(inverse(Y), multiply(double_divide(inverse(Z), Z), Y))), X))
% 9.22/1.68 = { by lemma 27 R->L }
% 9.22/1.68 double_divide(inverse(U), multiply(double_divide(T, double_divide(inverse(Y), T)), U))
% 9.22/1.68 = { by lemma 29 }
% 9.22/1.68 multiply(double_divide(inverse(W), W), Y)
% 9.22/1.68
% 9.22/1.68 Lemma 34: double_divide(inverse(X), double_divide(inverse(Y), Y)) = X.
% 9.22/1.68 Proof:
% 9.22/1.68 double_divide(inverse(X), double_divide(inverse(Y), Y))
% 9.22/1.68 = { by lemma 31 R->L }
% 9.22/1.68 double_divide(inverse(X), double_divide(inverse(Y), multiply(double_divide(inverse(Y), Y), Y)))
% 9.22/1.68 = { by lemma 32 }
% 9.22/1.68 X
% 9.22/1.68
% 9.22/1.68 Lemma 35: multiply(X, double_divide(inverse(Y), multiply(double_divide(inverse(Y), Z), Z))) = multiply(double_divide(inverse(X), W), W).
% 9.22/1.68 Proof:
% 9.22/1.68 multiply(X, double_divide(inverse(Y), multiply(double_divide(inverse(Y), Z), Z)))
% 9.22/1.68 = { by lemma 32 R->L }
% 9.22/1.68 multiply(double_divide(inverse(X), double_divide(inverse(Y), multiply(double_divide(inverse(Y), Z), Z))), double_divide(inverse(Y), multiply(double_divide(inverse(Y), Z), Z)))
% 9.22/1.68 = { by lemma 13 R->L }
% 9.22/1.68 multiply(double_divide(inverse(X), W), W)
% 9.22/1.68
% 9.22/1.68 Lemma 36: multiply(X, inverse(X)) = double_divide(inverse(Y), Y).
% 9.22/1.68 Proof:
% 9.22/1.68 multiply(X, inverse(X))
% 9.22/1.68 = { by axiom 1 (multiply) }
% 9.22/1.68 inverse(double_divide(inverse(X), X))
% 9.22/1.68 = { by lemma 31 R->L }
% 9.22/1.68 multiply(double_divide(inverse(Z), Z), inverse(double_divide(inverse(X), X)))
% 9.22/1.68 = { by lemma 33 R->L }
% 9.22/1.68 double_divide(inverse(Y), multiply(double_divide(inverse(double_divide(inverse(X), X)), double_divide(inverse(X), X)), Y))
% 9.22/1.68 = { by lemma 31 }
% 9.22/1.68 double_divide(inverse(Y), Y)
% 9.22/1.68
% 9.22/1.68 Lemma 37: inverse(inverse(X)) = X.
% 9.22/1.68 Proof:
% 9.22/1.68 inverse(inverse(X))
% 9.22/1.68 = { by lemma 31 R->L }
% 9.22/1.68 inverse(multiply(double_divide(inverse(Y), Y), inverse(X)))
% 9.22/1.68 = { by lemma 33 R->L }
% 9.22/1.68 inverse(double_divide(inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z))), multiply(double_divide(inverse(X), double_divide(inverse(W), W)), double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z)))))
% 9.22/1.68 = { by axiom 1 (multiply) R->L }
% 9.22/1.68 multiply(multiply(double_divide(inverse(X), double_divide(inverse(W), W)), double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z))), inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z))))
% 9.22/1.68 = { by lemma 34 }
% 9.22/1.68 multiply(multiply(X, double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z))), inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z))))
% 9.22/1.68 = { by lemma 35 }
% 9.22/1.68 multiply(multiply(double_divide(inverse(X), X), X), inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z))))
% 9.22/1.68 = { by lemma 31 }
% 9.22/1.68 multiply(X, inverse(double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z))))
% 9.22/1.68 = { by lemma 31 }
% 9.22/1.68 multiply(X, inverse(double_divide(inverse(Z), Z)))
% 9.22/1.68 = { by axiom 1 (multiply) R->L }
% 9.22/1.68 multiply(X, multiply(Z, inverse(Z)))
% 9.22/1.68 = { by lemma 36 }
% 9.22/1.68 multiply(X, double_divide(inverse(V), V))
% 9.22/1.68 = { by lemma 31 R->L }
% 9.22/1.69 multiply(X, double_divide(inverse(V), multiply(double_divide(inverse(V), V), V)))
% 9.22/1.69 = { by lemma 35 }
% 9.22/1.69 multiply(double_divide(inverse(X), X), X)
% 9.22/1.69 = { by lemma 31 }
% 9.22/1.69 X
% 9.22/1.69
% 9.22/1.69 Lemma 38: double_divide(inverse(X), X) = double_divide(Y, inverse(Y)).
% 9.22/1.69 Proof:
% 9.22/1.69 double_divide(inverse(X), X)
% 9.22/1.69 = { by lemma 31 R->L }
% 9.22/1.69 double_divide(inverse(X), multiply(double_divide(inverse(X), X), X))
% 9.22/1.69 = { by lemma 26 R->L }
% 9.22/1.69 double_divide(inverse(inverse(Y)), double_divide(inverse(Z), multiply(double_divide(W, double_divide(inverse(inverse(Y)), W)), Z)))
% 9.22/1.69 = { by lemma 37 }
% 9.22/1.69 double_divide(Y, double_divide(inverse(Z), multiply(double_divide(W, double_divide(inverse(inverse(Y)), W)), Z)))
% 9.22/1.69 = { by lemma 29 }
% 9.22/1.69 double_divide(Y, multiply(double_divide(inverse(V), V), inverse(Y)))
% 9.22/1.69 = { by lemma 31 }
% 9.22/1.69 double_divide(Y, inverse(Y))
% 9.22/1.69
% 9.22/1.69 Lemma 39: multiply(double_divide(X, inverse(X)), Y) = Y.
% 9.22/1.69 Proof:
% 9.22/1.69 multiply(double_divide(X, inverse(X)), Y)
% 9.22/1.69 = { by lemma 38 R->L }
% 9.22/1.69 multiply(double_divide(inverse(Z), Z), Y)
% 9.22/1.69 = { by lemma 31 }
% 9.22/1.69 Y
% 9.22/1.69
% 9.22/1.69 Lemma 40: double_divide(double_divide(X, inverse(X)), Y) = inverse(Y).
% 9.22/1.69 Proof:
% 9.22/1.69 double_divide(double_divide(X, inverse(X)), Y)
% 9.22/1.69 = { by lemma 38 R->L }
% 9.22/1.69 double_divide(double_divide(inverse(Z), Z), Y)
% 9.22/1.69 = { by lemma 36 R->L }
% 9.22/1.69 double_divide(multiply(W, inverse(W)), Y)
% 9.22/1.69 = { by lemma 31 R->L }
% 9.22/1.69 double_divide(multiply(W, inverse(W)), multiply(double_divide(inverse(Y), Y), Y))
% 9.22/1.69 = { by axiom 1 (multiply) }
% 9.22/1.69 double_divide(inverse(double_divide(inverse(W), W)), multiply(double_divide(inverse(Y), Y), Y))
% 9.22/1.69 = { by lemma 13 }
% 9.22/1.69 double_divide(inverse(double_divide(inverse(W), W)), multiply(double_divide(inverse(Y), double_divide(inverse(W), W)), double_divide(inverse(W), W)))
% 9.22/1.69 = { by lemma 33 }
% 9.22/1.69 multiply(double_divide(inverse(V), V), inverse(Y))
% 9.22/1.69 = { by lemma 31 }
% 9.22/1.69 inverse(Y)
% 9.22/1.69
% 9.22/1.69 Lemma 41: multiply(double_divide(X, Y), multiply(Y, X)) = double_divide(Z, inverse(Z)).
% 9.22/1.69 Proof:
% 9.22/1.69 multiply(double_divide(X, Y), multiply(Y, X))
% 9.22/1.69 = { by lemma 31 R->L }
% 9.22/1.69 multiply(multiply(double_divide(inverse(W), W), double_divide(X, Y)), multiply(Y, X))
% 9.22/1.69 = { by axiom 1 (multiply) }
% 9.22/1.69 multiply(multiply(double_divide(inverse(W), W), double_divide(X, Y)), inverse(double_divide(X, Y)))
% 9.22/1.69 = { by lemma 31 }
% 9.22/1.69 multiply(double_divide(X, Y), inverse(double_divide(X, Y)))
% 9.22/1.69 = { by lemma 36 }
% 9.22/1.69 double_divide(inverse(V), V)
% 9.22/1.69 = { by lemma 38 }
% 9.22/1.69 double_divide(Z, inverse(Z))
% 9.22/1.69
% 9.22/1.69 Lemma 42: double_divide(inverse(X), double_divide(Y, inverse(Y))) = X.
% 9.22/1.69 Proof:
% 9.22/1.69 double_divide(inverse(X), double_divide(Y, inverse(Y)))
% 9.22/1.69 = { by lemma 38 R->L }
% 9.22/1.69 double_divide(inverse(X), double_divide(inverse(Z), Z))
% 9.22/1.69 = { by lemma 31 R->L }
% 9.22/1.69 double_divide(inverse(X), double_divide(inverse(Z), multiply(double_divide(inverse(Z), Z), Z)))
% 9.22/1.69 = { by lemma 32 }
% 9.22/1.69 X
% 9.22/1.69
% 9.22/1.69 Lemma 43: double_divide(X, double_divide(Y, inverse(Y))) = inverse(X).
% 9.22/1.69 Proof:
% 9.22/1.69 double_divide(X, double_divide(Y, inverse(Y)))
% 9.22/1.69 = { by lemma 38 R->L }
% 9.22/1.69 double_divide(X, double_divide(inverse(X), X))
% 9.22/1.69 = { by lemma 12 }
% 9.22/1.69 double_divide(double_divide(Z, inverse(Z)), double_divide(inverse(X), double_divide(Z, inverse(Z))))
% 9.22/1.69 = { by lemma 42 }
% 9.22/1.69 double_divide(double_divide(Z, inverse(Z)), X)
% 9.22/1.69 = { by lemma 40 }
% 9.22/1.69 inverse(X)
% 9.22/1.69
% 9.22/1.69 Lemma 44: double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), X))) = Y.
% 9.22/1.69 Proof:
% 9.22/1.69 double_divide(inverse(X), multiply(double_divide(Y, double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), X)))
% 9.22/1.69 = { by lemma 10 R->L }
% 9.22/1.69 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y, double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), X)), inverse(X))))))
% 9.22/1.69 = { by lemma 12 }
% 9.22/1.69 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y, double_divide(multiply(double_divide(X2, double_divide(Y2, X2)), multiply(double_divide(Y2, Y), W)), double_divide(inverse(W), multiply(double_divide(X2, double_divide(Y2, X2)), multiply(double_divide(Y2, Y), W))))), multiply(double_divide(V, double_divide(inverse(W), V)), X)), inverse(X))))))
% 9.22/1.69 = { by lemma 3 }
% 9.22/1.69 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y, double_divide(multiply(double_divide(X2, double_divide(Y2, X2)), multiply(double_divide(Y2, Y), W)), Y)), multiply(double_divide(V, double_divide(inverse(W), V)), X)), inverse(X))))))
% 9.22/1.69 = { by lemma 5 }
% 9.22/1.69 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y, double_divide(double_divide(inverse(Z2), multiply(double_divide(W2, double_divide(inverse(W), W2)), multiply(Y, Z2))), Y)), multiply(double_divide(V, double_divide(inverse(W), V)), X)), inverse(X))))))
% 9.22/1.69 = { by lemma 7 }
% 9.22/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y, double_divide(double_divide(inverse(Z2), double_divide(inverse(inverse(W)), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))), Y)), multiply(double_divide(V, double_divide(inverse(W), V)), X)), inverse(X))))))
% 9.22/1.70 = { by lemma 12 }
% 9.22/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y, double_divide(double_divide(inverse(Z2), double_divide(inverse(inverse(W)), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))), Y)), multiply(double_divide(double_divide(inverse(Z2), double_divide(inverse(inverse(W)), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))), double_divide(inverse(W), double_divide(inverse(Z2), double_divide(inverse(inverse(W)), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))))), X)), inverse(X))))))
% 9.22/1.70 = { by lemma 4 }
% 9.22/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), inverse(double_divide(inverse(W), double_divide(inverse(Z2), double_divide(inverse(inverse(W)), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y))))))))))
% 9.22/1.70 = { by axiom 1 (multiply) R->L }
% 9.22/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Z2), double_divide(inverse(inverse(W)), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))), inverse(W))))))
% 9.22/1.70 = { by lemma 4 R->L }
% 9.22/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Z2), double_divide(inverse(inverse(W)), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))), multiply(multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)), inverse(S2)))))))
% 9.22/1.70 = { by lemma 4 R->L }
% 9.22/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Z2), double_divide(inverse(multiply(multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)), inverse(S2))), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))), multiply(multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)), inverse(S2)))))))
% 9.93/1.70 = { by axiom 1 (multiply) }
% 9.93/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Z2), double_divide(inverse(inverse(double_divide(inverse(S2), multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2))))), multiply(double_divide(V2, double_divide(inverse(Z2), V2)), inverse(Y)))), multiply(multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)), inverse(S2)))))))
% 9.93/1.70 = { by lemma 7 R->L }
% 9.93/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(double_divide(inverse(Z2), multiply(double_divide(X3, double_divide(inverse(double_divide(inverse(S2), multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)))), X3)), multiply(Y, Z2))), multiply(multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)), inverse(S2)))))))
% 9.93/1.70 = { by lemma 5 R->L }
% 9.93/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y3, double_divide(Z3, Y3)), multiply(double_divide(Z3, Y), double_divide(inverse(S2), multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2))))), multiply(multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)), inverse(S2)))))))
% 9.93/1.70 = { by axiom 1 (multiply) }
% 9.93/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), multiply(multiply(double_divide(Y3, double_divide(Z3, Y3)), multiply(double_divide(Z3, Y), double_divide(inverse(S2), multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2))))), inverse(double_divide(inverse(S2), multiply(double_divide(U2, double_divide(T2, U2)), multiply(double_divide(T2, W), S2)))))))))
% 9.93/1.70 = { by lemma 4 }
% 9.93/1.70 double_divide(inverse(U), double_divide(inverse(T), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(T), S)), inverse(Y)))))
% 9.93/1.70 = { by lemma 9 }
% 9.93/1.70 Y
% 9.93/1.70
% 9.93/1.70 Lemma 45: multiply(double_divide(double_divide(X, double_divide(inverse(Y), X)), double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), U)) = double_divide(inverse(Y), inverse(U)).
% 9.93/1.70 Proof:
% 9.93/1.70 multiply(double_divide(double_divide(X, double_divide(inverse(Y), X)), double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), U))
% 9.93/1.70 = { by lemma 44 R->L }
% 9.93/1.70 double_divide(inverse(Y), multiply(double_divide(multiply(double_divide(double_divide(X, double_divide(inverse(Y), X)), double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), U)), double_divide(X, double_divide(inverse(Y), X))), multiply(double_divide(T, double_divide(inverse(Y), T)), Y)))
% 9.93/1.70 = { by lemma 44 R->L }
% 9.93/1.70 double_divide(inverse(Y), multiply(double_divide(multiply(double_divide(double_divide(X, double_divide(inverse(Y), X)), double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), U)), double_divide(inverse(U), multiply(double_divide(double_divide(X, double_divide(inverse(Y), X)), double_divide(Z, double_divide(inverse(W), Z))), multiply(double_divide(V, double_divide(inverse(W), V)), U)))), multiply(double_divide(T, double_divide(inverse(Y), T)), Y)))
% 9.93/1.71 = { by lemma 7 }
% 9.93/1.71 double_divide(inverse(Y), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(Y), S)), inverse(double_divide(T, double_divide(inverse(Y), T))))))
% 9.93/1.71 = { by axiom 1 (multiply) R->L }
% 9.93/1.71 double_divide(inverse(Y), double_divide(inverse(inverse(U)), multiply(double_divide(S, double_divide(inverse(Y), S)), multiply(double_divide(inverse(Y), T), T))))
% 9.93/1.71 = { by lemma 7 }
% 9.93/1.71 double_divide(inverse(Y), double_divide(inverse(inverse(U)), double_divide(inverse(inverse(Y)), multiply(double_divide(X2, double_divide(inverse(T), X2)), inverse(double_divide(inverse(Y), T))))))
% 9.93/1.71 = { by axiom 1 (multiply) R->L }
% 9.93/1.71 double_divide(inverse(Y), double_divide(inverse(inverse(U)), double_divide(inverse(inverse(Y)), multiply(double_divide(X2, double_divide(inverse(T), X2)), multiply(T, inverse(Y))))))
% 9.93/1.71 = { by lemma 7 }
% 9.93/1.71 double_divide(inverse(Y), double_divide(inverse(inverse(U)), double_divide(inverse(inverse(Y)), double_divide(inverse(inverse(T)), multiply(double_divide(Y2, double_divide(inverse(inverse(Y)), Y2)), inverse(T))))))
% 9.93/1.71 = { by lemma 17 }
% 9.93/1.71 double_divide(inverse(Y), inverse(U))
% 9.93/1.71
% 9.93/1.71 Lemma 46: multiply(double_divide(X, Y), Y) = inverse(X).
% 9.93/1.71 Proof:
% 9.93/1.71 multiply(double_divide(X, Y), Y)
% 9.93/1.71 = { by lemma 37 R->L }
% 9.93/1.71 multiply(double_divide(inverse(inverse(X)), Y), Y)
% 9.93/1.71 = { by lemma 8 R->L }
% 9.93/1.71 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), inverse(multiply(double_divide(inverse(inverse(X)), Y), Y))))))
% 9.93/1.71 = { by lemma 39 R->L }
% 9.93/1.71 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(double_divide(T, inverse(T)), inverse(multiply(double_divide(inverse(inverse(X)), Y), Y)))))))
% 9.93/1.71 = { by lemma 41 R->L }
% 9.93/1.71 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(multiply(double_divide(Y, double_divide(inverse(inverse(X)), Y)), multiply(double_divide(inverse(inverse(X)), Y), Y)), inverse(multiply(double_divide(inverse(inverse(X)), Y), Y)))))))
% 9.93/1.71 = { by lemma 20 R->L }
% 9.93/1.71 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(multiply(double_divide(Y, double_divide(inverse(inverse(X)), Y)), multiply(double_divide(inverse(S), multiply(double_divide(inverse(S), X2), X2)), multiply(double_divide(inverse(inverse(X)), Y), Y))), inverse(multiply(double_divide(inverse(inverse(X)), Y), Y)))))))
% 9.93/1.71 = { by lemma 26 R->L }
% 9.93/1.71 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(multiply(double_divide(Y, double_divide(inverse(inverse(X)), Y)), multiply(double_divide(inverse(inverse(X)), double_divide(inverse(Y2), multiply(double_divide(Z2, double_divide(inverse(inverse(X)), Z2)), Y2))), multiply(double_divide(inverse(inverse(X)), Y), Y))), inverse(multiply(double_divide(inverse(inverse(X)), Y), Y)))))))
% 9.93/1.71 = { by lemma 4 }
% 9.93/1.71 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), inverse(double_divide(inverse(Y2), multiply(double_divide(Z2, double_divide(inverse(inverse(X)), Z2)), Y2)))))))
% 9.93/1.71 = { by lemma 4 R->L }
% 9.93/1.72 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(multiply(double_divide(multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)), double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))), multiply(double_divide(inverse(inverse(X)), double_divide(inverse(Y2), multiply(double_divide(Z2, double_divide(inverse(inverse(X)), Z2)), Y2))), multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))))), inverse(multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))))))))
% 9.93/1.72 = { by lemma 26 }
% 9.93/1.72 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(multiply(double_divide(multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)), double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))), multiply(double_divide(inverse(V2), multiply(double_divide(inverse(V2), U2), U2)), multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))))), inverse(multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))))))))
% 9.93/1.72 = { by lemma 20 }
% 9.93/1.72 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(multiply(double_divide(multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)), double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))), multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))), inverse(multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))))))))
% 9.93/1.72 = { by lemma 41 }
% 9.93/1.72 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), multiply(double_divide(T2, inverse(T2)), inverse(multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))))))))
% 9.93/1.72 = { by lemma 39 }
% 9.93/1.72 double_divide(multiply(Z, W), double_divide(inverse(V), double_divide(inverse(multiply(Z, W)), multiply(double_divide(U, double_divide(inverse(V), U)), inverse(multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))))))))
% 9.93/1.72 = { by lemma 8 }
% 9.93/1.72 multiply(double_divide(inverse(inverse(X)), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X))), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))
% 9.93/1.72 = { by lemma 19 }
% 9.93/1.72 multiply(multiply(double_divide(inverse(W2), W2), W2), multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))
% 9.93/1.72 = { by lemma 31 }
% 9.93/1.72 multiply(W2, multiply(double_divide(W2, double_divide(inverse(W2), W2)), inverse(X)))
% 9.93/1.72 = { by lemma 38 }
% 9.93/1.72 multiply(W2, multiply(double_divide(W2, double_divide(S2, inverse(S2))), inverse(X)))
% 9.93/1.72 = { by lemma 43 }
% 9.93/1.72 multiply(W2, multiply(inverse(W2), inverse(X)))
% 9.93/1.72 = { by lemma 31 R->L }
% 9.93/1.72 multiply(multiply(double_divide(inverse(W2), W2), W2), multiply(inverse(W2), inverse(X)))
% 9.93/1.72 = { by axiom 1 (multiply) }
% 9.93/1.72 multiply(multiply(double_divide(inverse(W2), W2), W2), inverse(double_divide(inverse(X), inverse(W2))))
% 9.93/1.72 = { by lemma 45 R->L }
% 9.93/1.72 multiply(multiply(double_divide(inverse(W2), W2), W2), inverse(multiply(double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3))), multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2))))
% 9.93/1.72 = { by lemma 14 R->L }
% 9.93/1.72 multiply(multiply(double_divide(V3, double_divide(inverse(X), V3)), double_divide(inverse(X), inverse(W2))), inverse(multiply(double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3))), multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2))))
% 9.93/1.72 = { by lemma 45 R->L }
% 9.93/1.72 multiply(multiply(double_divide(V3, double_divide(inverse(X), V3)), multiply(double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3))), multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2))), inverse(multiply(double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3))), multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2))))
% 9.93/1.72 = { by axiom 1 (multiply) }
% 9.93/1.72 multiply(multiply(double_divide(V3, double_divide(inverse(X), V3)), multiply(double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3))), multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2))), inverse(inverse(double_divide(multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2), double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3)))))))
% 9.93/1.72 = { by axiom 1 (multiply) }
% 9.93/1.72 multiply(multiply(double_divide(V3, double_divide(inverse(X), V3)), inverse(double_divide(multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2), double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3)))))), inverse(inverse(double_divide(multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2), double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3)))))))
% 9.93/1.72 = { by axiom 1 (multiply) }
% 9.93/1.72 inverse(double_divide(inverse(inverse(double_divide(multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2), double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3)))))), multiply(double_divide(V3, double_divide(inverse(X), V3)), inverse(double_divide(multiply(double_divide(W3, double_divide(inverse(Z3), W3)), W2), double_divide(double_divide(X3, double_divide(inverse(X), X3)), double_divide(Y3, double_divide(inverse(Z3), Y3))))))))
% 9.93/1.72 = { by lemma 19 }
% 9.93/1.72 inverse(multiply(double_divide(inverse(X), X), X))
% 9.93/1.72 = { by lemma 31 }
% 9.93/1.72 inverse(X)
% 9.93/1.72
% 9.93/1.73 Lemma 47: double_divide(X, double_divide(Y, X)) = Y.
% 9.93/1.73 Proof:
% 9.93/1.73 double_divide(X, double_divide(Y, X))
% 9.93/1.73 = { by lemma 10 R->L }
% 9.93/1.73 double_divide(inverse(Z), double_divide(inverse(W), double_divide(inverse(inverse(Z)), multiply(double_divide(V, double_divide(inverse(W), V)), multiply(double_divide(Y, X), X)))))
% 9.93/1.73 = { by lemma 46 }
% 9.93/1.73 double_divide(inverse(Z), double_divide(inverse(W), double_divide(inverse(inverse(Z)), multiply(double_divide(V, double_divide(inverse(W), V)), inverse(Y)))))
% 9.93/1.73 = { by lemma 20 R->L }
% 9.93/1.73 double_divide(inverse(Z), double_divide(inverse(W), double_divide(inverse(multiply(double_divide(inverse(U), multiply(double_divide(inverse(U), T), T)), inverse(Z))), multiply(double_divide(V, double_divide(inverse(W), V)), inverse(Y)))))
% 9.93/1.73 = { by lemma 20 R->L }
% 9.93/1.73 double_divide(multiply(double_divide(inverse(U), multiply(double_divide(inverse(U), T), T)), inverse(Z)), double_divide(inverse(W), double_divide(inverse(multiply(double_divide(inverse(U), multiply(double_divide(inverse(U), T), T)), inverse(Z))), multiply(double_divide(V, double_divide(inverse(W), V)), inverse(Y)))))
% 9.93/1.73 = { by lemma 8 }
% 9.93/1.73 Y
% 9.93/1.73
% 9.93/1.73 Lemma 48: multiply(X, Y) = double_divide(inverse(X), inverse(Y)).
% 9.93/1.73 Proof:
% 9.93/1.73 multiply(X, Y)
% 9.93/1.73 = { by lemma 39 R->L }
% 9.93/1.73 multiply(double_divide(Z, inverse(Z)), multiply(X, Y))
% 9.93/1.73 = { by lemma 40 R->L }
% 9.93/1.73 multiply(double_divide(Z, double_divide(double_divide(W, inverse(W)), Z)), multiply(X, Y))
% 9.93/1.73 = { by lemma 47 R->L }
% 9.93/1.73 multiply(double_divide(Z, double_divide(double_divide(W, inverse(W)), Z)), multiply(double_divide(double_divide(W, inverse(W)), double_divide(X, double_divide(W, inverse(W)))), Y))
% 9.93/1.73 = { by lemma 43 }
% 9.93/1.73 multiply(double_divide(Z, double_divide(double_divide(W, inverse(W)), Z)), multiply(double_divide(double_divide(W, inverse(W)), inverse(X)), Y))
% 9.93/1.73 = { by lemma 5 }
% 9.93/1.73 double_divide(inverse(V), multiply(double_divide(U, double_divide(inverse(Y), U)), multiply(inverse(X), V)))
% 9.93/1.73 = { by lemma 22 R->L }
% 9.93/1.73 double_divide(inverse(X), double_divide(inverse(inverse(Y)), multiply(double_divide(X, double_divide(inverse(X), X)), inverse(inverse(X)))))
% 9.93/1.73 = { by lemma 38 }
% 9.93/1.73 double_divide(inverse(X), double_divide(inverse(inverse(Y)), multiply(double_divide(X, double_divide(T, inverse(T))), inverse(inverse(X)))))
% 9.93/1.73 = { by lemma 43 }
% 9.93/1.73 double_divide(inverse(X), double_divide(inverse(inverse(Y)), multiply(inverse(X), inverse(inverse(X)))))
% 9.93/1.73 = { by lemma 36 }
% 9.93/1.73 double_divide(inverse(X), double_divide(inverse(inverse(Y)), double_divide(inverse(S), S)))
% 9.93/1.73 = { by lemma 38 }
% 9.93/1.73 double_divide(inverse(X), double_divide(inverse(inverse(Y)), double_divide(X2, inverse(X2))))
% 9.93/1.73 = { by lemma 42 }
% 9.93/1.73 double_divide(inverse(X), inverse(Y))
% 9.93/1.73
% 9.93/1.73 Lemma 49: multiply(inverse(X), X) = double_divide(Y, inverse(Y)).
% 9.93/1.73 Proof:
% 9.93/1.73 multiply(inverse(X), X)
% 9.93/1.73 = { by lemma 31 R->L }
% 9.93/1.73 multiply(multiply(double_divide(inverse(Z), Z), inverse(X)), X)
% 9.93/1.73 = { by lemma 37 R->L }
% 9.93/1.73 multiply(multiply(double_divide(inverse(Z), Z), inverse(X)), inverse(inverse(X)))
% 9.93/1.73 = { by lemma 31 }
% 9.93/1.73 multiply(inverse(X), inverse(inverse(X)))
% 9.93/1.73 = { by lemma 36 }
% 9.93/1.73 double_divide(inverse(W), W)
% 9.93/1.73 = { by lemma 38 }
% 9.93/1.73 double_divide(Y, inverse(Y))
% 9.93/1.73
% 9.93/1.73 Lemma 50: inverse(multiply(X, Y)) = double_divide(Y, X).
% 9.93/1.73 Proof:
% 9.93/1.73 inverse(multiply(X, Y))
% 9.93/1.73 = { by lemma 31 R->L }
% 9.93/1.73 multiply(double_divide(inverse(Z), Z), inverse(multiply(X, Y)))
% 9.93/1.73 = { by lemma 29 R->L }
% 9.93/1.73 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), inverse(V))), W))
% 9.93/1.73 = { by lemma 3 R->L }
% 9.93/1.73 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(V, inverse(V)), U))))), W))
% 9.93/1.74 = { by lemma 49 R->L }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(multiply(inverse(V), V), U))))), W))
% 9.93/1.74 = { by lemma 43 R->L }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(multiply(double_divide(V, double_divide(S, inverse(S))), V), U))))), W))
% 9.93/1.74 = { by lemma 38 R->L }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(multiply(double_divide(V, double_divide(inverse(V), V)), V), U))))), W))
% 9.93/1.74 = { by lemma 31 R->L }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(multiply(double_divide(V, double_divide(inverse(V), V)), multiply(double_divide(inverse(X2), X2), V)), U))))), W))
% 9.93/1.74 = { by lemma 7 }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(inverse(inverse(V)), multiply(double_divide(V, double_divide(inverse(V), V)), inverse(double_divide(inverse(X2), X2)))), U))))), W))
% 9.93/1.74 = { by lemma 37 }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(V, multiply(double_divide(V, double_divide(inverse(V), V)), inverse(double_divide(inverse(X2), X2)))), U))))), W))
% 9.93/1.74 = { by lemma 38 }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(V, multiply(double_divide(V, double_divide(inverse(V), V)), inverse(double_divide(Y2, inverse(Y2))))), U))))), W))
% 9.93/1.74 = { by lemma 38 }
% 9.93/1.74 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(V, multiply(double_divide(V, double_divide(Z2, inverse(Z2))), inverse(double_divide(Y2, inverse(Y2))))), U))))), W))
% 9.93/1.75 = { by lemma 43 }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(V, multiply(inverse(V), inverse(double_divide(Y2, inverse(Y2))))), U))))), W))
% 9.93/1.75 = { by axiom 1 (multiply) R->L }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(V, multiply(inverse(V), multiply(inverse(Y2), Y2))), U))))), W))
% 9.93/1.75 = { by lemma 49 }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), double_divide(inverse(U), multiply(double_divide(T, double_divide(V, T)), multiply(double_divide(V, multiply(inverse(V), double_divide(W2, inverse(W2)))), U))))), W))
% 9.93/1.75 = { by lemma 3 }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), multiply(inverse(V), double_divide(W2, inverse(W2))))), W))
% 9.93/1.75 = { by lemma 49 R->L }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), multiply(inverse(V), multiply(inverse(V2), V2)))), W))
% 9.93/1.75 = { by axiom 1 (multiply) }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), multiply(inverse(V), inverse(double_divide(V2, inverse(V2)))))), W))
% 9.93/1.75 = { by lemma 43 R->L }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), multiply(double_divide(V, double_divide(U2, inverse(U2))), inverse(double_divide(V2, inverse(V2)))))), W))
% 9.93/1.75 = { by lemma 38 R->L }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(V), double_divide(inverse(inverse(multiply(X, Y))), multiply(double_divide(V, double_divide(inverse(V), V)), inverse(double_divide(V2, inverse(V2)))))), W))
% 9.93/1.75 = { by lemma 22 }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(V2, inverse(V2)), T2))), W))
% 9.93/1.75 = { by lemma 38 R->L }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(inverse(double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3))), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3))), T2))), W))
% 9.93/1.75 = { by lemma 31 R->L }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(inverse(double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3))), multiply(double_divide(inverse(double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3))), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3))), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3)))), T2))), W))
% 9.93/1.75 = { by lemma 24 R->L }
% 9.93/1.75 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(inverse(double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3))), multiply(double_divide(Y3, double_divide(multiply(multiply(double_divide(inverse(Z3), W3), W3), inverse(Z3)), Y3)), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3)))), T2))), W))
% 9.93/1.75 = { by axiom 1 (multiply) R->L }
% 9.93/1.76 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(multiply(double_divide(inverse(X3), X3), inverse(multiply(X, Y))), multiply(double_divide(Y3, double_divide(multiply(multiply(double_divide(inverse(Z3), W3), W3), inverse(Z3)), Y3)), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3)))), T2))), W))
% 9.93/1.76 = { by lemma 25 }
% 9.93/1.76 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(multiply(double_divide(inverse(X3), X3), inverse(multiply(X, Y))), multiply(double_divide(inverse(V3), V3), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3)))), T2))), W))
% 9.93/1.76 = { by lemma 31 }
% 9.93/1.76 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(inverse(multiply(X, Y)), multiply(double_divide(inverse(V3), V3), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3)))), T2))), W))
% 9.93/1.76 = { by lemma 31 }
% 9.93/1.76 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(inverse(multiply(X, Y)), double_divide(inverse(multiply(X, Y)), double_divide(inverse(X3), X3))), T2))), W))
% 9.93/1.76 = { by lemma 38 }
% 9.93/1.76 double_divide(inverse(W), multiply(double_divide(inverse(T2), multiply(double_divide(S2, double_divide(inverse(multiply(X, Y)), S2)), multiply(double_divide(inverse(multiply(X, Y)), double_divide(inverse(multiply(X, Y)), double_divide(multiply(X, Y), inverse(multiply(X, Y))))), T2))), W))
% 9.93/1.76 = { by lemma 3 }
% 9.93/1.76 double_divide(inverse(W), multiply(double_divide(inverse(multiply(X, Y)), double_divide(multiply(X, Y), inverse(multiply(X, Y)))), W))
% 9.93/1.76 = { by lemma 30 }
% 9.93/1.76 multiply(double_divide(inverse(U3), U3), double_divide(Y, X))
% 9.93/1.76 = { by lemma 31 }
% 9.93/1.76 double_divide(Y, X)
% 9.93/1.76
% 9.93/1.76 Lemma 51: multiply(inverse(X), inverse(Y)) = double_divide(X, Y).
% 9.93/1.76 Proof:
% 9.93/1.76 multiply(inverse(X), inverse(Y))
% 9.93/1.76 = { by lemma 43 R->L }
% 9.93/1.76 multiply(double_divide(X, double_divide(Z, inverse(Z))), inverse(Y))
% 9.93/1.76 = { by lemma 38 R->L }
% 9.93/1.76 multiply(double_divide(X, double_divide(inverse(X), X)), inverse(Y))
% 9.93/1.76 = { by lemma 46 R->L }
% 9.93/1.76 multiply(double_divide(X, double_divide(inverse(X), X)), multiply(double_divide(Y, W), W))
% 9.93/1.76 = { by lemma 7 }
% 9.93/1.76 double_divide(inverse(inverse(X)), multiply(double_divide(W, double_divide(inverse(W), W)), inverse(double_divide(Y, W))))
% 9.93/1.76 = { by lemma 37 }
% 9.93/1.76 double_divide(X, multiply(double_divide(W, double_divide(inverse(W), W)), inverse(double_divide(Y, W))))
% 9.93/1.76 = { by lemma 38 }
% 9.93/1.76 double_divide(X, multiply(double_divide(W, double_divide(V, inverse(V))), inverse(double_divide(Y, W))))
% 9.93/1.76 = { by lemma 43 }
% 9.93/1.76 double_divide(X, multiply(inverse(W), inverse(double_divide(Y, W))))
% 9.93/1.76 = { by axiom 1 (multiply) R->L }
% 9.93/1.76 double_divide(X, multiply(inverse(W), multiply(W, Y)))
% 9.93/1.76 = { by lemma 31 R->L }
% 9.93/1.76 double_divide(X, multiply(multiply(double_divide(inverse(U), U), inverse(W)), multiply(W, Y)))
% 9.93/1.76 = { by lemma 34 R->L }
% 9.93/1.76 double_divide(X, multiply(multiply(double_divide(inverse(U), U), inverse(W)), multiply(double_divide(inverse(W), double_divide(inverse(T), T)), Y)))
% 9.93/1.76 = { by lemma 33 R->L }
% 9.93/1.76 double_divide(X, multiply(double_divide(inverse(Y), multiply(double_divide(inverse(W), double_divide(inverse(T), T)), Y)), multiply(double_divide(inverse(W), double_divide(inverse(T), T)), Y)))
% 9.93/1.76 = { by lemma 13 R->L }
% 9.93/1.76 double_divide(X, multiply(double_divide(inverse(Y), Y), Y))
% 9.93/1.76 = { by lemma 31 }
% 9.93/1.76 double_divide(X, Y)
% 9.93/1.76
% 9.93/1.76 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))).
% 9.93/1.76 Proof:
% 9.93/1.76 tuple(multiply(inverse(a1), a1), multiply(multiply(inverse(b2), b2), a2), multiply(multiply(a3, b3), c3))
% 9.93/1.76 = { by lemma 49 }
% 9.93/1.76 tuple(double_divide(X, inverse(X)), multiply(multiply(inverse(b2), b2), a2), multiply(multiply(a3, b3), c3))
% 9.93/1.76 = { by lemma 49 }
% 9.93/1.76 tuple(double_divide(X, inverse(X)), multiply(double_divide(Y, inverse(Y)), a2), multiply(multiply(a3, b3), c3))
% 9.93/1.77 = { by lemma 39 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, multiply(multiply(a3, b3), c3))
% 9.93/1.77 = { by lemma 48 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(multiply(a3, b3)), inverse(c3)))
% 9.93/1.77 = { by lemma 50 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(b3, a3), inverse(c3)))
% 9.93/1.77 = { by lemma 47 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(b3, a3), double_divide(Z, double_divide(inverse(c3), Z))))
% 9.93/1.77 = { by lemma 42 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(inverse(double_divide(b3, a3)), double_divide(W, inverse(W))), double_divide(Z, double_divide(inverse(c3), Z))))
% 9.93/1.77 = { by lemma 49 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(inverse(double_divide(b3, a3)), multiply(inverse(V), V)), double_divide(Z, double_divide(inverse(c3), Z))))
% 9.93/1.77 = { by axiom 1 (multiply) }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(inverse(double_divide(b3, a3)), inverse(double_divide(V, inverse(V)))), double_divide(Z, double_divide(inverse(c3), Z))))
% 9.93/1.77 = { by lemma 48 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(b3, a3), double_divide(V, inverse(V))), double_divide(Z, double_divide(inverse(c3), Z))))
% 9.93/1.77 = { by lemma 50 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, inverse(multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(V, inverse(V))))))
% 9.93/1.77 = { by lemma 40 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(double_divide(U, T), inverse(double_divide(U, T))), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(V, inverse(V))))))
% 9.93/1.77 = { by lemma 51 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(multiply(inverse(U), inverse(T)), inverse(double_divide(U, T))), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(V, inverse(V))))))
% 9.93/1.77 = { by axiom 1 (multiply) }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(double_divide(inverse(double_divide(inverse(T), inverse(U))), inverse(double_divide(U, T))), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(V, inverse(V))))))
% 9.93/1.77 = { by lemma 48 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(inverse(T), inverse(U)), double_divide(U, T)), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(V, inverse(V))))))
% 9.93/1.77 = { by lemma 38 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(inverse(T), inverse(U)), double_divide(U, T)), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(inverse(T), T)))))
% 9.93/1.77 = { by lemma 15 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(inverse(T), inverse(U)), double_divide(U, T)), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(multiply(inverse(U), inverse(T)), multiply(double_divide(inverse(T), double_divide(T, inverse(T))), multiply(double_divide(inverse(U), U), U)))))))
% 9.93/1.77 = { by lemma 42 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(inverse(T), inverse(U)), double_divide(U, T)), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(multiply(inverse(U), inverse(T)), multiply(T, multiply(double_divide(inverse(U), U), U)))))))
% 9.93/1.77 = { by lemma 51 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(inverse(T), inverse(U)), double_divide(U, T)), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(double_divide(U, T), multiply(T, multiply(double_divide(inverse(U), U), U)))))))
% 9.93/1.77 = { by lemma 48 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(inverse(T), inverse(U)), double_divide(U, T)), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(double_divide(U, T), double_divide(inverse(T), inverse(multiply(double_divide(inverse(U), U), U))))))))
% 9.93/1.77 = { by lemma 31 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(multiply(double_divide(inverse(T), inverse(U)), double_divide(U, T)), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(double_divide(U, T), double_divide(inverse(T), inverse(U)))))))
% 9.93/1.77 = { by axiom 1 (multiply) }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(double_divide(double_divide(U, T), double_divide(inverse(T), inverse(U)))), multiply(double_divide(Z, double_divide(inverse(c3), Z)), multiply(double_divide(b3, a3), double_divide(double_divide(U, T), double_divide(inverse(T), inverse(U)))))))
% 9.93/1.77 = { by lemma 16 R->L }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), multiply(double_divide(S, double_divide(inverse(c3), S)), multiply(double_divide(b3, a3), a3))))
% 9.93/1.77 = { by lemma 7 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), double_divide(inverse(inverse(c3)), multiply(double_divide(a3, double_divide(inverse(a3), a3)), inverse(double_divide(b3, a3))))))
% 9.93/1.77 = { by lemma 37 }
% 9.93/1.77 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), double_divide(c3, multiply(double_divide(a3, double_divide(inverse(a3), a3)), inverse(double_divide(b3, a3))))))
% 9.93/1.78 = { by lemma 48 }
% 9.93/1.78 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), double_divide(c3, double_divide(inverse(double_divide(a3, double_divide(inverse(a3), a3))), inverse(inverse(double_divide(b3, a3)))))))
% 9.93/1.78 = { by axiom 1 (multiply) R->L }
% 9.93/1.78 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), double_divide(c3, double_divide(multiply(double_divide(inverse(a3), a3), a3), inverse(inverse(double_divide(b3, a3)))))))
% 9.93/1.78 = { by lemma 31 }
% 9.93/1.78 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), double_divide(c3, double_divide(a3, inverse(inverse(double_divide(b3, a3)))))))
% 9.93/1.78 = { by lemma 37 }
% 9.93/1.78 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), double_divide(c3, double_divide(a3, double_divide(b3, a3)))))
% 9.93/1.78 = { by lemma 47 }
% 9.93/1.78 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), double_divide(c3, b3)))
% 9.93/1.78 = { by lemma 50 R->L }
% 9.93/1.78 tuple(double_divide(X, inverse(X)), a2, double_divide(inverse(a3), inverse(multiply(b3, c3))))
% 9.93/1.78 = { by lemma 48 R->L }
% 9.93/1.78 tuple(double_divide(X, inverse(X)), a2, multiply(a3, multiply(b3, c3)))
% 9.93/1.78 = { by lemma 49 R->L }
% 9.93/1.78 tuple(multiply(inverse(b1), b1), a2, multiply(a3, multiply(b3, c3)))
% 9.93/1.78 % SZS output end Proof
% 9.93/1.78
% 9.93/1.78 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------