%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : GRP617-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:11:23 AM UTC 2026
% Result : Unsatisfiable 36.28s 5.11s
% Output : Proof 38.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP617-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 10:12:11 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.28/5.11 Command-line arguments: --lhs-weight 1 --flip-ordering --normalise-queue-percent 10 --cp-renormalise-threshold 10 --complete-subsets --ground-joining-incomplete-limit 15 --flatten-every 2
% 36.28/5.11
% 36.28/5.11 % SZS status Unsatisfiable
% 36.28/5.11
% 37.29/5.18 % SZS output start Proof
% 37.29/5.18 Axiom 1 (u_in_G2): subgroup2_member(u) = true.
% 37.29/5.18 Axiom 2 (v_in_G1): subgroup1_member(v) = true.
% 37.29/5.18 Axiom 3 (right_identity): product(X, identity, X) = true.
% 37.29/5.18 Axiom 4 (left_identity): product(identity, X, X) = true.
% 37.29/5.19 Axiom 5 (right_inverse): product(X, inverse(X), identity) = true.
% 37.29/5.19 Axiom 6 (left_inverse): product(inverse(X), X, identity) = true.
% 37.29/5.19 Axiom 7 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 37.29/5.19 Axiom 8 (ifeq_axiom): ifeq2(X, X, Y, Z) = Y.
% 37.29/5.19 Axiom 9 (total_function1): product(X, Y, multiply(X, Y)) = true.
% 37.29/5.19 Axiom 10 (closure_of_inverse2): ifeq(subgroup2_member(X), true, subgroup2_member(inverse(X)), true) = true.
% 37.29/5.19 Axiom 11 (closure_of_inverse1): ifeq(subgroup1_member(X), true, subgroup1_member(inverse(X)), true) = true.
% 37.29/5.19 Axiom 12 (normality2): ifeq(subgroup2_member(X), true, subgroup2_member(multiply(Y, multiply(X, inverse(Y)))), true) = true.
% 37.29/5.19 Axiom 13 (trivial_intersection): ifeq2(subgroup2_member(X), true, ifeq2(subgroup1_member(X), true, X, identity), identity) = identity.
% 37.29/5.19 Axiom 14 (normality1): ifeq(subgroup1_member(X), true, subgroup1_member(multiply(Y, multiply(X, inverse(Y)))), true) = true.
% 37.29/5.19 Axiom 15 (total_function2): ifeq2(product(X, Y, Z), true, ifeq2(product(X, Y, W), true, W, Z), Z) = Z.
% 37.29/5.19 Axiom 16 (closure_of_product2): ifeq(subgroup2_member(X), true, ifeq(subgroup2_member(Y), true, ifeq(product(Y, X, Z), true, subgroup2_member(Z), true), true), true) = true.
% 37.29/5.19 Axiom 17 (closure_of_product1): ifeq(subgroup1_member(X), true, ifeq(subgroup1_member(Y), true, ifeq(product(Y, X, Z), true, subgroup1_member(Z), true), true), true) = true.
% 37.29/5.19 Axiom 18 (associativity1): ifeq(product(X, Y, Z), true, ifeq(product(W, Y, V), true, ifeq(product(U, W, X), true, product(U, V, Z), true), true), true) = true.
% 37.29/5.19 Axiom 19 (associativity2): ifeq(product(X, Y, Z), true, ifeq(product(W, Z, V), true, ifeq(product(W, X, U), true, product(U, Y, V), true), true), true) = true.
% 37.29/5.19
% 37.29/5.19 Lemma 20: ifeq2(product(X, Y, Z), true, multiply(X, Y), Z) = Z.
% 37.29/5.19 Proof:
% 37.29/5.19 ifeq2(product(X, Y, Z), true, multiply(X, Y), Z)
% 37.29/5.19 = { by axiom 8 (ifeq_axiom) R->L }
% 37.29/5.19 ifeq2(product(X, Y, Z), true, ifeq2(true, true, multiply(X, Y), Z), Z)
% 37.29/5.19 = { by axiom 9 (total_function1) R->L }
% 37.29/5.19 ifeq2(product(X, Y, Z), true, ifeq2(product(X, Y, multiply(X, Y)), true, multiply(X, Y), Z), Z)
% 37.29/5.19 = { by axiom 15 (total_function2) }
% 37.29/5.19 Z
% 37.29/5.19
% 37.29/5.19 Lemma 21: multiply(multiply(X, Y), inverse(Y)) = X.
% 37.29/5.19 Proof:
% 37.29/5.19 multiply(multiply(X, Y), inverse(Y))
% 37.29/5.19 = { by axiom 8 (ifeq_axiom) R->L }
% 37.29/5.19 ifeq2(true, true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by axiom 19 (associativity2) R->L }
% 37.29/5.19 ifeq2(ifeq(product(Y, inverse(Y), identity), true, ifeq(product(X, identity, X), true, ifeq(product(X, Y, multiply(X, Y)), true, product(multiply(X, Y), inverse(Y), X), true), true), true), true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by axiom 3 (right_identity) }
% 37.29/5.19 ifeq2(ifeq(product(Y, inverse(Y), identity), true, ifeq(true, true, ifeq(product(X, Y, multiply(X, Y)), true, product(multiply(X, Y), inverse(Y), X), true), true), true), true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.19 ifeq2(ifeq(product(Y, inverse(Y), identity), true, ifeq(product(X, Y, multiply(X, Y)), true, product(multiply(X, Y), inverse(Y), X), true), true), true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by axiom 5 (right_inverse) }
% 37.29/5.19 ifeq2(ifeq(true, true, ifeq(product(X, Y, multiply(X, Y)), true, product(multiply(X, Y), inverse(Y), X), true), true), true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.19 ifeq2(ifeq(product(X, Y, multiply(X, Y)), true, product(multiply(X, Y), inverse(Y), X), true), true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by axiom 9 (total_function1) }
% 37.29/5.19 ifeq2(ifeq(true, true, product(multiply(X, Y), inverse(Y), X), true), true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.19 ifeq2(product(multiply(X, Y), inverse(Y), X), true, multiply(multiply(X, Y), inverse(Y)), X)
% 37.29/5.19 = { by lemma 20 }
% 37.29/5.19 X
% 37.29/5.19
% 37.29/5.19 Lemma 22: multiply(X, inverse(multiply(Y, X))) = inverse(Y).
% 37.29/5.19 Proof:
% 37.29/5.19 multiply(X, inverse(multiply(Y, X)))
% 37.29/5.19 = { by lemma 20 R->L }
% 37.29/5.19 multiply(ifeq2(product(inverse(Y), multiply(Y, X), X), true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.19 multiply(ifeq2(ifeq(true, true, product(inverse(Y), multiply(Y, X), X), true), true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 9 (total_function1) R->L }
% 37.29/5.19 multiply(ifeq2(ifeq(product(Y, X, multiply(Y, X)), true, product(inverse(Y), multiply(Y, X), X), true), true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.19 multiply(ifeq2(ifeq(product(Y, X, multiply(Y, X)), true, ifeq(true, true, product(inverse(Y), multiply(Y, X), X), true), true), true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 6 (left_inverse) R->L }
% 37.29/5.19 multiply(ifeq2(ifeq(product(Y, X, multiply(Y, X)), true, ifeq(product(inverse(Y), Y, identity), true, product(inverse(Y), multiply(Y, X), X), true), true), true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.19 multiply(ifeq2(ifeq(true, true, ifeq(product(Y, X, multiply(Y, X)), true, ifeq(product(inverse(Y), Y, identity), true, product(inverse(Y), multiply(Y, X), X), true), true), true), true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 4 (left_identity) R->L }
% 37.29/5.19 multiply(ifeq2(ifeq(product(identity, X, X), true, ifeq(product(Y, X, multiply(Y, X)), true, ifeq(product(inverse(Y), Y, identity), true, product(inverse(Y), multiply(Y, X), X), true), true), true), true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 18 (associativity1) }
% 37.29/5.19 multiply(ifeq2(true, true, multiply(inverse(Y), multiply(Y, X)), X), inverse(multiply(Y, X)))
% 37.29/5.19 = { by axiom 8 (ifeq_axiom) }
% 37.29/5.19 multiply(multiply(inverse(Y), multiply(Y, X)), inverse(multiply(Y, X)))
% 37.29/5.19 = { by lemma 21 }
% 37.29/5.19 inverse(Y)
% 37.29/5.19
% 37.29/5.19 Lemma 23: multiply(inverse(X), inverse(Y)) = inverse(multiply(Y, X)).
% 37.29/5.19 Proof:
% 37.29/5.19 multiply(inverse(X), inverse(Y))
% 37.29/5.19 = { by lemma 21 R->L }
% 37.29/5.19 multiply(inverse(X), inverse(multiply(multiply(Y, X), inverse(X))))
% 37.29/5.19 = { by lemma 22 }
% 37.29/5.19 inverse(multiply(Y, X))
% 37.29/5.19
% 37.29/5.19 Lemma 24: multiply(multiply(X, Y), Z) = multiply(X, multiply(Y, Z)).
% 37.29/5.19 Proof:
% 37.29/5.19 multiply(multiply(X, Y), Z)
% 37.29/5.19 = { by lemma 20 R->L }
% 37.29/5.19 ifeq2(product(X, multiply(Y, Z), multiply(multiply(X, Y), Z)), true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.19 ifeq2(ifeq(true, true, product(X, multiply(Y, Z), multiply(multiply(X, Y), Z)), true), true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 9 (total_function1) R->L }
% 37.29/5.19 ifeq2(ifeq(product(Y, Z, multiply(Y, Z)), true, product(X, multiply(Y, Z), multiply(multiply(X, Y), Z)), true), true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.19 ifeq2(ifeq(product(Y, Z, multiply(Y, Z)), true, ifeq(true, true, product(X, multiply(Y, Z), multiply(multiply(X, Y), Z)), true), true), true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 9 (total_function1) R->L }
% 37.29/5.19 ifeq2(ifeq(product(Y, Z, multiply(Y, Z)), true, ifeq(product(X, Y, multiply(X, Y)), true, product(X, multiply(Y, Z), multiply(multiply(X, Y), Z)), true), true), true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.19 ifeq2(ifeq(true, true, ifeq(product(Y, Z, multiply(Y, Z)), true, ifeq(product(X, Y, multiply(X, Y)), true, product(X, multiply(Y, Z), multiply(multiply(X, Y), Z)), true), true), true), true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 9 (total_function1) R->L }
% 37.29/5.19 ifeq2(ifeq(product(multiply(X, Y), Z, multiply(multiply(X, Y), Z)), true, ifeq(product(Y, Z, multiply(Y, Z)), true, ifeq(product(X, Y, multiply(X, Y)), true, product(X, multiply(Y, Z), multiply(multiply(X, Y), Z)), true), true), true), true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 18 (associativity1) }
% 37.29/5.19 ifeq2(true, true, multiply(X, multiply(Y, Z)), multiply(multiply(X, Y), Z))
% 37.29/5.19 = { by axiom 8 (ifeq_axiom) }
% 37.29/5.19 multiply(X, multiply(Y, Z))
% 37.29/5.19
% 37.29/5.19 Lemma 25: ifeq2(product(identity, X, Y), true, Y, X) = X.
% 37.29/5.19 Proof:
% 37.29/5.19 ifeq2(product(identity, X, Y), true, Y, X)
% 37.29/5.19 = { by axiom 8 (ifeq_axiom) R->L }
% 37.29/5.19 ifeq2(true, true, ifeq2(product(identity, X, Y), true, Y, X), X)
% 37.29/5.19 = { by axiom 4 (left_identity) R->L }
% 37.29/5.19 ifeq2(product(identity, X, X), true, ifeq2(product(identity, X, Y), true, Y, X), X)
% 37.29/5.19 = { by axiom 15 (total_function2) }
% 37.29/5.19 X
% 37.29/5.19
% 37.29/5.19 Goal 1 (prove_vu_equals_uv): multiply(v, u) = multiply(u, v).
% 37.29/5.19 Proof:
% 37.29/5.19 multiply(v, u)
% 37.29/5.19 = { by lemma 21 R->L }
% 37.29/5.19 multiply(multiply(multiply(v, u), inverse(multiply(u, v))), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 8 (ifeq_axiom) R->L }
% 37.29/5.20 multiply(ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 8 (ifeq_axiom) R->L }
% 37.29/5.20 multiply(ifeq2(true, true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 10 (closure_of_inverse2) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(true, true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 12 (normality2) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(ifeq(subgroup2_member(inverse(u)), true, subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(ifeq(ifeq(true, true, subgroup2_member(inverse(u)), true), true, subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 1 (u_in_G2) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(ifeq(ifeq(subgroup2_member(u), true, subgroup2_member(inverse(u)), true), true, subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 10 (closure_of_inverse2) }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(ifeq(true, true, subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true, ifeq(true, true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 9 (total_function1) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true, ifeq(product(u, multiply(v, multiply(inverse(u), inverse(v))), multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true, ifeq(true, true, ifeq(product(u, multiply(v, multiply(inverse(u), inverse(v))), multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.20 = { by axiom 1 (u_in_G2) R->L }
% 37.29/5.20 multiply(ifeq2(ifeq(ifeq(subgroup2_member(multiply(v, multiply(inverse(u), inverse(v)))), true, ifeq(subgroup2_member(u), true, ifeq(product(u, multiply(v, multiply(inverse(u), inverse(v))), multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true, subgroup2_member(multiply(u, multiply(v, multiply(inverse(u), inverse(v))))), true), true), true), true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 16 (closure_of_product2) }
% 37.29/5.21 multiply(ifeq2(ifeq(true, true, subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(inverse(multiply(u, multiply(v, multiply(inverse(u), inverse(v)))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by lemma 23 }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(inverse(multiply(u, multiply(v, inverse(multiply(v, u)))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by lemma 24 R->L }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(inverse(multiply(multiply(u, v), inverse(multiply(v, u))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by lemma 22 R->L }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 8 (ifeq_axiom) R->L }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(true, true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 19 (associativity2) R->L }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(ifeq(product(inverse(multiply(v, u)), multiply(v, u), identity), true, ifeq(product(multiply(u, v), identity, multiply(u, v)), true, ifeq(product(multiply(u, v), inverse(multiply(v, u)), multiply(multiply(u, v), inverse(multiply(v, u)))), true, product(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u), multiply(u, v)), true), true), true), true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 3 (right_identity) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(ifeq(product(inverse(multiply(v, u)), multiply(v, u), identity), true, ifeq(true, true, ifeq(product(multiply(u, v), inverse(multiply(v, u)), multiply(multiply(u, v), inverse(multiply(v, u)))), true, product(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u), multiply(u, v)), true), true), true), true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(ifeq(product(inverse(multiply(v, u)), multiply(v, u), identity), true, ifeq(product(multiply(u, v), inverse(multiply(v, u)), multiply(multiply(u, v), inverse(multiply(v, u)))), true, product(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u), multiply(u, v)), true), true), true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 6 (left_inverse) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(ifeq(true, true, ifeq(product(multiply(u, v), inverse(multiply(v, u)), multiply(multiply(u, v), inverse(multiply(v, u)))), true, product(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u), multiply(u, v)), true), true), true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(ifeq(product(multiply(u, v), inverse(multiply(v, u)), multiply(multiply(u, v), inverse(multiply(v, u)))), true, product(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u), multiply(u, v)), true), true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 9 (total_function1) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(ifeq(true, true, product(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u), multiply(u, v)), true), true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(ifeq2(product(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u), multiply(u, v)), true, multiply(multiply(multiply(u, v), inverse(multiply(v, u))), multiply(v, u)), multiply(u, v))))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by lemma 20 }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(true, true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 17 (closure_of_product1) R->L }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(subgroup1_member(inverse(v)), true, ifeq(subgroup1_member(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v)), true, ifeq(product(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v), multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 9 (total_function1) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(subgroup1_member(inverse(v)), true, ifeq(subgroup1_member(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v)), true, ifeq(true, true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(subgroup1_member(inverse(v)), true, ifeq(subgroup1_member(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v)), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(true, true, subgroup1_member(inverse(v)), true), true, ifeq(subgroup1_member(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v)), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 2 (v_in_G1) R->L }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(subgroup1_member(v), true, subgroup1_member(inverse(v)), true), true, ifeq(subgroup1_member(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v)), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 11 (closure_of_inverse1) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(true, true, ifeq(subgroup1_member(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v)), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.21 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.21 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(subgroup1_member(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v)), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by lemma 23 R->L }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(true, true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 17 (closure_of_product1) R->L }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true, ifeq(subgroup1_member(v), true, ifeq(product(v, multiply(u, multiply(inverse(v), inverse(u))), multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 2 (v_in_G1) }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true, ifeq(true, true, ifeq(product(v, multiply(u, multiply(inverse(v), inverse(u))), multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true, ifeq(product(v, multiply(u, multiply(inverse(v), inverse(u))), multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 9 (total_function1) }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true, ifeq(true, true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(ifeq(true, true, subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 11 (closure_of_inverse1) R->L }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(ifeq(ifeq(subgroup1_member(v), true, subgroup1_member(inverse(v)), true), true, subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 2 (v_in_G1) }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, subgroup1_member(inverse(v)), true), true, subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.22 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(ifeq(subgroup1_member(inverse(v)), true, subgroup1_member(multiply(u, multiply(inverse(v), inverse(u)))), true), true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.22 = { by axiom 14 (normality1) }
% 37.29/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(ifeq(true, true, subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.23 = { by axiom 7 (ifeq_axiom) }
% 37.29/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.23 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, ifeq(true, true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.23 = { by axiom 9 (total_function1) R->L }
% 37.29/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, ifeq(product(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v, multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.23 = { by axiom 7 (ifeq_axiom) R->L }
% 37.29/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(true, true, ifeq(subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, ifeq(product(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v, multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 37.29/5.23 = { by axiom 2 (v_in_G1) R->L }
% 37.29/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(ifeq(subgroup1_member(v), true, ifeq(subgroup1_member(multiply(v, multiply(u, multiply(inverse(v), inverse(u))))), true, ifeq(product(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v, multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true, subgroup1_member(multiply(multiply(v, multiply(u, multiply(inverse(v), inverse(u)))), v)), true), true), true), true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 17 (closure_of_product1) }
% 38.04/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(ifeq(true, true, subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 7 (ifeq_axiom) }
% 38.04/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(subgroup1_member(multiply(multiply(multiply(v, multiply(u, inverse(multiply(u, v)))), v), inverse(v))), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by lemma 21 }
% 38.04/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(subgroup1_member(multiply(v, multiply(u, inverse(multiply(u, v))))), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by lemma 24 R->L }
% 38.04/5.23 multiply(ifeq2(subgroup2_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, ifeq2(subgroup1_member(multiply(multiply(v, u), inverse(multiply(u, v)))), true, multiply(multiply(v, u), inverse(multiply(u, v))), identity), identity), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 13 (trivial_intersection) }
% 38.04/5.23 multiply(identity, inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 8 (ifeq_axiom) R->L }
% 38.04/5.23 ifeq2(true, true, multiply(identity, inverse(inverse(multiply(u, v)))), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 9 (total_function1) R->L }
% 38.04/5.23 ifeq2(product(identity, inverse(inverse(multiply(u, v))), multiply(identity, inverse(inverse(multiply(u, v))))), true, multiply(identity, inverse(inverse(multiply(u, v)))), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by lemma 25 }
% 38.04/5.23 inverse(inverse(multiply(u, v)))
% 38.04/5.23 = { by lemma 25 R->L }
% 38.04/5.23 ifeq2(product(identity, inverse(inverse(multiply(u, v))), multiply(u, v)), true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 7 (ifeq_axiom) R->L }
% 38.04/5.23 ifeq2(ifeq(true, true, product(identity, inverse(inverse(multiply(u, v))), multiply(u, v)), true), true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 5 (right_inverse) R->L }
% 38.04/5.23 ifeq2(ifeq(product(multiply(u, v), inverse(multiply(u, v)), identity), true, product(identity, inverse(inverse(multiply(u, v))), multiply(u, v)), true), true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 7 (ifeq_axiom) R->L }
% 38.04/5.23 ifeq2(ifeq(true, true, ifeq(product(multiply(u, v), inverse(multiply(u, v)), identity), true, product(identity, inverse(inverse(multiply(u, v))), multiply(u, v)), true), true), true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 5 (right_inverse) R->L }
% 38.04/5.23 ifeq2(ifeq(product(inverse(multiply(u, v)), inverse(inverse(multiply(u, v))), identity), true, ifeq(product(multiply(u, v), inverse(multiply(u, v)), identity), true, product(identity, inverse(inverse(multiply(u, v))), multiply(u, v)), true), true), true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 7 (ifeq_axiom) R->L }
% 38.04/5.23 ifeq2(ifeq(product(inverse(multiply(u, v)), inverse(inverse(multiply(u, v))), identity), true, ifeq(true, true, ifeq(product(multiply(u, v), inverse(multiply(u, v)), identity), true, product(identity, inverse(inverse(multiply(u, v))), multiply(u, v)), true), true), true), true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 3 (right_identity) R->L }
% 38.04/5.23 ifeq2(ifeq(product(inverse(multiply(u, v)), inverse(inverse(multiply(u, v))), identity), true, ifeq(product(multiply(u, v), identity, multiply(u, v)), true, ifeq(product(multiply(u, v), inverse(multiply(u, v)), identity), true, product(identity, inverse(inverse(multiply(u, v))), multiply(u, v)), true), true), true), true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 19 (associativity2) }
% 38.04/5.23 ifeq2(true, true, multiply(u, v), inverse(inverse(multiply(u, v))))
% 38.04/5.23 = { by axiom 8 (ifeq_axiom) }
% 38.04/5.23 multiply(u, v)
% 38.04/5.23 % SZS output end Proof
% 38.04/5.23
% 38.04/5.23 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------