%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GRP031-2 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:06:54 AM UTC 2025
% Result : Unsatisfiable 24.44s 24.64s
% Output : Proof 24.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP031-2 : TPTP v9.0.0. Released v1.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 19 15:28:47 EDT 2025
% 0.13/0.34 % CPUTime :
% 24.44/24.64 % SZS status Unsatisfiable
% 24.44/24.64 % SZS output start Proof
% 24.44/24.64 tff(product_type, type, (
% 24.44/24.64 product: ( $i * $i * $i ) > $o)).
% 24.44/24.64 tff(multiply_type, type, (
% 24.44/24.64 multiply: ( $i * $i ) > $i)).
% 24.44/24.64 tff(inverse_type, type, (
% 24.44/24.64 inverse: $i > $i)).
% 24.44/24.64 tff(elem_0_type, type, (
% 24.44/24.64 elem_0: $i)).
% 24.44/24.64 tff(a_type, type, (
% 24.44/24.64 a: $i)).
% 24.44/24.64 tff(identity_type, type, (
% 24.44/24.64 identity: $i)).
% 24.44/24.64 tff(1,plain,
% 24.44/24.64 (^[Y: $i, X: $i] : refl(product(X, Y, multiply(X, Y)) <=> product(X, Y, multiply(X, Y)))),
% 24.44/24.64 inference(bind,[status(th)],[])).
% 24.44/24.64 tff(2,plain,
% 24.44/24.64 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y)) <=> ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 24.44/24.64 inference(quant_intro,[status(thm)],[1])).
% 24.44/24.64 tff(3,plain,
% 24.44/24.64 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y)) <=> ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(4,axiom,(![Y: $i, X: $i] : product(X, Y, multiply(X, Y))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','total_function1')).
% 24.44/24.64 tff(5,plain,
% 24.44/24.64 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[4, 3])).
% 24.44/24.64 tff(6,plain,(
% 24.44/24.64 ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 24.44/24.64 inference(skolemize,[status(sab)],[5])).
% 24.44/24.64 tff(7,plain,
% 24.44/24.64 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[6, 2])).
% 24.44/24.64 tff(8,plain,
% 24.44/24.64 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))),
% 24.44/24.64 inference(quant_inst,[status(thm)],[])).
% 24.44/24.64 tff(9,plain,
% 24.44/24.64 (product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))),
% 24.44/24.64 inference(unit_resolution,[status(thm)],[8, 7])).
% 24.44/24.64 tff(10,plain,
% 24.44/24.64 (^[A: $i] : refl(product(A, inverse(A), identity) <=> product(A, inverse(A), identity))),
% 24.44/24.64 inference(bind,[status(th)],[])).
% 24.44/24.64 tff(11,plain,
% 24.44/24.64 (![A: $i] : product(A, inverse(A), identity) <=> ![A: $i] : product(A, inverse(A), identity)),
% 24.44/24.64 inference(quant_intro,[status(thm)],[10])).
% 24.44/24.64 tff(12,plain,
% 24.44/24.64 (![A: $i] : product(A, inverse(A), identity) <=> ![A: $i] : product(A, inverse(A), identity)),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(13,axiom,(![A: $i] : product(A, inverse(A), identity)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','right_inverse')).
% 24.44/24.64 tff(14,plain,
% 24.44/24.64 (![A: $i] : product(A, inverse(A), identity)),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[13, 12])).
% 24.44/24.64 tff(15,plain,(
% 24.44/24.64 ![A: $i] : product(A, inverse(A), identity)),
% 24.44/24.64 inference(skolemize,[status(sab)],[14])).
% 24.44/24.64 tff(16,plain,
% 24.44/24.64 (![A: $i] : product(A, inverse(A), identity)),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[15, 11])).
% 24.44/24.64 tff(17,plain,
% 24.44/24.64 ((~![A: $i] : product(A, inverse(A), identity)) | product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)),
% 24.44/24.64 inference(quant_inst,[status(thm)],[])).
% 24.44/24.64 tff(18,plain,
% 24.44/24.64 (product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)),
% 24.44/24.64 inference(unit_resolution,[status(thm)],[17, 16])).
% 24.44/24.64 tff(19,plain,
% 24.44/24.64 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))),
% 24.44/24.64 inference(quant_inst,[status(thm)],[])).
% 24.44/24.64 tff(20,plain,
% 24.44/24.64 (product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))),
% 24.44/24.64 inference(unit_resolution,[status(thm)],[19, 7])).
% 24.44/24.64 tff(21,plain,
% 24.44/24.64 (^[W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : refl((product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U))) <=> (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U))))),
% 24.44/24.64 inference(bind,[status(th)],[])).
% 24.44/24.64 tff(22,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U))) <=> ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))),
% 24.44/24.64 inference(quant_intro,[status(thm)],[21])).
% 24.44/24.64 tff(23,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U))) <=> ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(24,plain,
% 24.44/24.64 (^[W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : trans(monotonicity(rewrite((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(U, Z, W))) <=> ((~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))), (((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(U, Z, W))) | product(X, V, W)) <=> (((~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U))) | product(X, V, W)))), rewrite((((~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U))) | product(X, V, W)) <=> (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))), (((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(U, Z, W))) | product(X, V, W)) <=> (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))))),
% 24.44/24.64 inference(bind,[status(th)],[])).
% 24.44/24.64 tff(25,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : ((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(U, Z, W))) | product(X, V, W)) <=> ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))),
% 24.44/24.64 inference(quant_intro,[status(thm)],[24])).
% 24.44/24.64 tff(26,axiom,(![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : ((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(U, Z, W))) | product(X, V, W))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','associativity1')).
% 24.44/24.64 tff(27,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[26, 25])).
% 24.44/24.64 tff(28,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[27, 23])).
% 24.44/24.64 tff(29,plain,(
% 24.44/24.64 ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))),
% 24.44/24.64 inference(skolemize,[status(sab)],[28])).
% 24.44/24.64 tff(30,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[29, 22])).
% 24.44/24.64 tff(31,plain,
% 24.44/24.64 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(32,plain,
% 24.44/24.64 ((product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | (~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0))))) <=> ((~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(33,plain,
% 24.44/24.64 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | (~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))),
% 24.44/24.64 inference(monotonicity,[status(thm)],[32])).
% 24.44/24.64 tff(34,plain,
% 24.44/24.64 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | (~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))),
% 24.44/24.64 inference(transitivity,[status(thm)],[33, 31])).
% 24.44/24.64 tff(35,plain,
% 24.44/24.64 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | (~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))))),
% 24.44/24.64 inference(quant_inst,[status(thm)],[])).
% 24.44/24.64 tff(36,plain,
% 24.44/24.64 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, multiply(elem!0, elem!0), multiply(a, multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(multiply(elem!0, elem!0), inverse(multiply(elem!0, elem!0)), identity)) | product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[35, 34])).
% 24.44/24.64 tff(37,plain,
% 24.44/24.64 (product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))),
% 24.44/24.64 inference(unit_resolution,[status(thm)],[36, 30, 20, 18, 9])).
% 24.44/24.64 tff(38,plain,
% 24.44/24.64 ((~![A: $i] : product(A, inverse(A), identity)) | product(inverse(a), inverse(inverse(a)), identity)),
% 24.44/24.64 inference(quant_inst,[status(thm)],[])).
% 24.44/24.64 tff(39,plain,
% 24.44/24.64 (product(inverse(a), inverse(inverse(a)), identity)),
% 24.44/24.64 inference(unit_resolution,[status(thm)],[38, 16])).
% 24.44/24.64 tff(40,plain,
% 24.44/24.64 ((~![A: $i] : product(A, inverse(A), identity)) | product(a, inverse(a), identity)),
% 24.44/24.64 inference(quant_inst,[status(thm)],[])).
% 24.44/24.64 tff(41,plain,
% 24.44/24.64 (product(a, inverse(a), identity)),
% 24.44/24.64 inference(unit_resolution,[status(thm)],[40, 16])).
% 24.44/24.64 tff(42,plain,
% 24.44/24.64 (^[W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : refl((product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W))) <=> (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W))))),
% 24.44/24.64 inference(bind,[status(th)],[])).
% 24.44/24.64 tff(43,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W))) <=> ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))),
% 24.44/24.64 inference(quant_intro,[status(thm)],[42])).
% 24.44/24.64 tff(44,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W))) <=> ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(45,plain,
% 24.44/24.64 (^[W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : trans(monotonicity(rewrite((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(X, V, W))) <=> ((~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))), (((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(X, V, W))) | product(U, Z, W)) <=> (((~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W))) | product(U, Z, W)))), rewrite((((~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W))) | product(U, Z, W)) <=> (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))), (((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(X, V, W))) | product(U, Z, W)) <=> (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))))),
% 24.44/24.64 inference(bind,[status(th)],[])).
% 24.44/24.64 tff(46,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : ((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(X, V, W))) | product(U, Z, W)) <=> ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))),
% 24.44/24.64 inference(quant_intro,[status(thm)],[45])).
% 24.44/24.64 tff(47,axiom,(![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : ((((~product(X, Y, U)) | (~product(Y, Z, V))) | (~product(X, V, W))) | product(U, Z, W))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','associativity2')).
% 24.44/24.64 tff(48,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[47, 46])).
% 24.44/24.64 tff(49,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[48, 44])).
% 24.44/24.64 tff(50,plain,(
% 24.44/24.64 ![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))),
% 24.44/24.64 inference(skolemize,[status(sab)],[49])).
% 24.44/24.64 tff(51,plain,
% 24.44/24.64 (![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))),
% 24.44/24.64 inference(modus_ponens,[status(thm)],[50, 43])).
% 24.44/24.64 tff(52,plain,
% 24.44/24.64 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(a, inverse(a), identity)) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, inverse(a), identity)) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(53,plain,
% 24.44/24.64 ((product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, inverse(a), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))) <=> ((~product(a, inverse(a), identity)) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))),
% 24.44/24.64 inference(rewrite,[status(thm)],[])).
% 24.44/24.64 tff(54,plain,
% 24.44/24.64 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, inverse(a), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(a, inverse(a), identity)) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))),
% 24.44/24.64 inference(monotonicity,[status(thm)],[53])).
% 24.44/24.64 tff(55,plain,
% 24.44/24.64 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, inverse(a), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, inverse(a), identity)) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))),
% 24.44/24.64 inference(transitivity,[status(thm)],[54, 52])).
% 24.44/24.64 tff(56,plain,
% 24.44/24.64 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, inverse(a), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(57,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, inverse(a), identity)) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))),
% 24.48/24.65 inference(modus_ponens,[status(thm)],[56, 55])).
% 24.48/24.65 tff(58,plain,
% 24.48/24.65 (product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[57, 51, 41, 39, 37])).
% 24.48/24.65 tff(59,plain,
% 24.48/24.65 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(a, inverse(elem!0), multiply(a, inverse(elem!0)))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(60,plain,
% 24.48/24.65 (product(a, inverse(elem!0), multiply(a, inverse(elem!0)))),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[59, 7])).
% 24.48/24.65 tff(61,plain,
% 24.48/24.65 (^[A: $i] : refl(product(A, identity, A) <=> product(A, identity, A))),
% 24.48/24.65 inference(bind,[status(th)],[])).
% 24.48/24.65 tff(62,plain,
% 24.48/24.65 (![A: $i] : product(A, identity, A) <=> ![A: $i] : product(A, identity, A)),
% 24.48/24.65 inference(quant_intro,[status(thm)],[61])).
% 24.48/24.65 tff(63,plain,
% 24.48/24.65 (![A: $i] : product(A, identity, A) <=> ![A: $i] : product(A, identity, A)),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(64,axiom,(![A: $i] : product(A, identity, A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','right_identity')).
% 24.48/24.65 tff(65,plain,
% 24.48/24.65 (![A: $i] : product(A, identity, A)),
% 24.48/24.65 inference(modus_ponens,[status(thm)],[64, 63])).
% 24.48/24.65 tff(66,plain,(
% 24.48/24.65 ![A: $i] : product(A, identity, A)),
% 24.48/24.65 inference(skolemize,[status(sab)],[65])).
% 24.48/24.65 tff(67,plain,
% 24.48/24.65 (![A: $i] : product(A, identity, A)),
% 24.48/24.65 inference(modus_ponens,[status(thm)],[66, 62])).
% 24.48/24.65 tff(68,plain,
% 24.48/24.65 ((~![A: $i] : product(A, identity, A)) | product(a, identity, a)),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(69,plain,
% 24.48/24.65 (product(a, identity, a)),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[68, 67])).
% 24.48/24.65 tff(70,plain,
% 24.48/24.65 ((~![A: $i] : product(A, inverse(A), identity)) | product(inverse(elem!0), inverse(inverse(elem!0)), identity)),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(71,plain,
% 24.48/24.65 (product(inverse(elem!0), inverse(inverse(elem!0)), identity)),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[70, 16])).
% 24.48/24.65 tff(72,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, identity, a)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, identity, a)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(73,plain,
% 24.48/24.65 ((product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(a, identity, a))) <=> ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, identity, a)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(74,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(a, identity, a)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, identity, a)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)))),
% 24.48/24.65 inference(monotonicity,[status(thm)],[73])).
% 24.48/24.65 tff(75,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(a, identity, a)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, identity, a)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a))),
% 24.48/24.65 inference(transitivity,[status(thm)],[74, 72])).
% 24.48/24.65 tff(76,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(a, identity, a)))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(77,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(a, identity, a)) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)),
% 24.48/24.65 inference(modus_ponens,[status(thm)],[76, 75])).
% 24.48/24.65 tff(78,plain,
% 24.48/24.65 (product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[77, 51, 71, 69, 60])).
% 24.48/24.65 tff(79,assumption,(~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))), introduced(assumption)).
% 24.48/24.65 tff(80,plain,
% 24.48/24.65 ((~![A: $i] : product(A, identity, A)) | product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(81,plain,
% 24.48/24.65 ($false),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[80, 67, 79])).
% 24.48/24.65 tff(82,plain,(product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))), inference(lemma,lemma(discharge,[]))).
% 24.48/24.65 tff(83,plain,
% 24.48/24.65 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(84,plain,
% 24.48/24.65 (product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[83, 7])).
% 24.48/24.65 tff(85,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(86,plain,
% 24.48/24.65 ((product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))) <=> (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(87,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.65 inference(monotonicity,[status(thm)],[86])).
% 24.48/24.65 tff(88,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))))),
% 24.48/24.65 inference(transitivity,[status(thm)],[87, 85])).
% 24.48/24.65 tff(89,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(90,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0)))),
% 24.48/24.65 inference(modus_ponens,[status(thm)],[89, 88])).
% 24.48/24.65 tff(91,plain,
% 24.48/24.65 (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[90, 51, 84, 82])).
% 24.48/24.65 tff(92,plain,
% 24.48/24.65 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(93,plain,
% 24.48/24.65 (product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[92, 7])).
% 24.48/24.65 tff(94,plain,
% 24.48/24.65 ((~![A: $i] : product(A, identity, A)) | product(inverse(elem!0), identity, inverse(elem!0))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(95,plain,
% 24.48/24.65 (product(inverse(elem!0), identity, inverse(elem!0))),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[94, 67])).
% 24.48/24.65 tff(96,plain,
% 24.48/24.65 ((~![A: $i] : product(A, inverse(A), identity)) | product(elem!0, inverse(elem!0), identity)),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(97,plain,
% 24.48/24.65 (product(elem!0, inverse(elem!0), identity)),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[96, 16])).
% 24.48/24.65 tff(98,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(99,plain,
% 24.48/24.65 ((product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)) | (~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), identity, inverse(elem!0)))) <=> ((~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(100,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)) | (~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), identity, inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.65 inference(monotonicity,[status(thm)],[99])).
% 24.48/24.65 tff(101,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)) | (~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), identity, inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))),
% 24.48/24.65 inference(transitivity,[status(thm)],[100, 98])).
% 24.48/24.65 tff(102,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)) | (~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), identity, inverse(elem!0))))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(103,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(elem!0, inverse(elem!0), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(elem!0), elem!0, multiply(inverse(elem!0), elem!0))) | product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))),
% 24.48/24.65 inference(modus_ponens,[status(thm)],[102, 101])).
% 24.48/24.65 tff(104,plain,
% 24.48/24.65 (product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[103, 51, 97, 95, 93])).
% 24.48/24.65 tff(105,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(106,plain,
% 24.48/24.65 ((product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))) <=> ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(107,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))))),
% 24.48/24.65 inference(monotonicity,[status(thm)],[106])).
% 24.48/24.65 tff(108,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.65 inference(transitivity,[status(thm)],[107, 105])).
% 24.48/24.65 tff(109,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.65 inference(quant_inst,[status(thm)],[])).
% 24.48/24.65 tff(110,plain,
% 24.48/24.65 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(multiply(inverse(elem!0), elem!0), identity, identity) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))),
% 24.48/24.65 inference(modus_ponens,[status(thm)],[109, 108])).
% 24.48/24.65 tff(111,plain,
% 24.48/24.65 (product(multiply(inverse(elem!0), elem!0), identity, identity)),
% 24.48/24.65 inference(unit_resolution,[status(thm)],[110, 30, 71, 104])).
% 24.48/24.65 tff(112,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(113,plain,
% 24.48/24.65 ((product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))) <=> ((~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.65 inference(rewrite,[status(thm)],[])).
% 24.48/24.65 tff(114,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.65 inference(monotonicity,[status(thm)],[113])).
% 24.48/24.65 tff(115,plain,
% 24.48/24.65 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.66 inference(transitivity,[status(thm)],[114, 112])).
% 24.48/24.66 tff(116,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(117,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, identity)) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.66 inference(modus_ponens,[status(thm)],[116, 115])).
% 24.48/24.66 tff(118,plain,
% 24.48/24.66 (product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[117, 30, 84, 111, 91])).
% 24.48/24.66 tff(119,assumption,(~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))), introduced(assumption)).
% 24.48/24.66 tff(120,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(121,plain,
% 24.48/24.66 ((product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0)))) <=> ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(122,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))))),
% 24.48/24.66 inference(monotonicity,[status(thm)],[121])).
% 24.48/24.66 tff(123,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.66 inference(transitivity,[status(thm)],[122, 120])).
% 24.48/24.66 tff(124,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))))),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(125,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))),
% 24.48/24.66 inference(modus_ponens,[status(thm)],[124, 123])).
% 24.48/24.66 tff(126,plain,
% 24.48/24.66 ($false),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[125, 51, 71, 104, 119, 82])).
% 24.48/24.66 tff(127,plain,(product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))), inference(lemma,lemma(discharge,[]))).
% 24.48/24.66 tff(128,plain,
% 24.48/24.66 ((~![A: $i] : product(A, identity, A)) | product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(129,plain,
% 24.48/24.66 (product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[128, 67])).
% 24.48/24.66 tff(130,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(131,plain,
% 24.48/24.66 ((product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0)))) <=> ((~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(132,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.66 inference(monotonicity,[status(thm)],[131])).
% 24.48/24.66 tff(133,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.66 inference(transitivity,[status(thm)],[132, 130])).
% 24.48/24.66 tff(134,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(135,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(inverse(elem!0), elem!0))) | (~product(inverse(inverse(elem!0)), identity, inverse(inverse(elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), identity, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.66 inference(modus_ponens,[status(thm)],[134, 133])).
% 24.48/24.66 tff(136,plain,
% 24.48/24.66 (product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[135, 30, 129, 127, 118])).
% 24.48/24.66 tff(137,plain,
% 24.48/24.66 ((~![A: $i] : product(A, inverse(A), identity)) | product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(138,plain,
% 24.48/24.66 (product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[137, 16])).
% 24.48/24.66 tff(139,plain,
% 24.48/24.66 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(140,plain,
% 24.48/24.66 (product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[139, 7])).
% 24.48/24.66 tff(141,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(a, identity, a)) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, identity, a)) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(142,plain,
% 24.48/24.66 ((product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(a, identity, a))) <=> ((~product(a, identity, a)) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(143,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(a, identity, a)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(a, identity, a)) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)))),
% 24.48/24.66 inference(monotonicity,[status(thm)],[142])).
% 24.48/24.66 tff(144,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(a, identity, a)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, identity, a)) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a))),
% 24.48/24.66 inference(transitivity,[status(thm)],[143, 141])).
% 24.48/24.66 tff(145,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(a, identity, a)))),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(146,plain,
% 24.48/24.66 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, identity, a)) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)),
% 24.48/24.66 inference(modus_ponens,[status(thm)],[145, 144])).
% 24.48/24.66 tff(147,plain,
% 24.48/24.66 (product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[146, 51, 69, 140, 138])).
% 24.48/24.66 tff(148,plain,
% 24.48/24.66 (^[A: $i] : refl((~product(A, a, identity)) <=> (~product(A, a, identity)))),
% 24.48/24.66 inference(bind,[status(th)],[])).
% 24.48/24.66 tff(149,plain,
% 24.48/24.66 (![A: $i] : (~product(A, a, identity)) <=> ![A: $i] : (~product(A, a, identity))),
% 24.48/24.66 inference(quant_intro,[status(thm)],[148])).
% 24.48/24.66 tff(150,plain,
% 24.48/24.66 (![A: $i] : (~product(A, a, identity)) <=> ![A: $i] : (~product(A, a, identity))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(151,axiom,(![A: $i] : (~product(A, a, identity))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','prove_a_has_a_left_inverse')).
% 24.48/24.66 tff(152,plain,
% 24.48/24.66 (![A: $i] : (~product(A, a, identity))),
% 24.48/24.66 inference(modus_ponens,[status(thm)],[151, 150])).
% 24.48/24.66 tff(153,plain,(
% 24.48/24.66 ![A: $i] : (~product(A, a, identity))),
% 24.48/24.66 inference(skolemize,[status(sab)],[152])).
% 24.48/24.66 tff(154,plain,
% 24.48/24.66 (![A: $i] : (~product(A, a, identity))),
% 24.48/24.66 inference(modus_ponens,[status(thm)],[153, 149])).
% 24.48/24.66 tff(155,plain,
% 24.48/24.66 ((~![A: $i] : (~product(A, a, identity))) | (~product(inverse(a), a, identity))),
% 24.48/24.66 inference(quant_inst,[status(thm)],[])).
% 24.48/24.66 tff(156,plain,
% 24.48/24.66 (~product(inverse(a), a, identity)),
% 24.48/24.66 inference(unit_resolution,[status(thm)],[155, 154])).
% 24.48/24.66 tff(157,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(158,plain,
% 24.48/24.66 ((product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))))) <=> (product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)))),
% 24.48/24.66 inference(rewrite,[status(thm)],[])).
% 24.48/24.66 tff(159,plain,
% 24.48/24.66 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a))))),
% 24.48/24.67 inference(monotonicity,[status(thm)],[158])).
% 24.48/24.67 tff(160,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)))),
% 24.48/24.67 inference(transitivity,[status(thm)],[159, 157])).
% 24.48/24.67 tff(161,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))),
% 24.48/24.67 inference(quant_inst,[status(thm)],[])).
% 24.48/24.67 tff(162,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | product(inverse(a), a, identity) | (~product(multiply(inverse(elem!0), multiply(elem!0, elem!0)), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), identity)) | (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), inverse(multiply(inverse(elem!0), multiply(elem!0, elem!0))), a))),
% 24.48/24.67 inference(modus_ponens,[status(thm)],[161, 160])).
% 24.48/24.67 tff(163,plain,
% 24.48/24.67 (~product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0)))),
% 24.48/24.67 inference(unit_resolution,[status(thm)],[162, 30, 156, 138, 147])).
% 24.48/24.67 tff(164,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.67 inference(rewrite,[status(thm)],[])).
% 24.48/24.67 tff(165,plain,
% 24.48/24.67 ((product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))) <=> (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.67 inference(rewrite,[status(thm)],[])).
% 24.48/24.67 tff(166,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))))),
% 24.48/24.67 inference(monotonicity,[status(thm)],[165])).
% 24.48/24.67 tff(167,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.67 inference(transitivity,[status(thm)],[166, 164])).
% 24.48/24.67 tff(168,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.67 inference(quant_inst,[status(thm)],[])).
% 24.48/24.67 tff(169,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)) | (~product(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(inverse(elem!0), elem!0), inverse(elem!0), inverse(elem!0)))),
% 24.48/24.67 inference(modus_ponens,[status(thm)],[168, 167])).
% 24.48/24.67 tff(170,plain,
% 24.48/24.67 (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))),
% 24.48/24.67 inference(unit_resolution,[status(thm)],[169, 51, 104, 84])).
% 24.48/24.67 tff(171,plain,
% 24.48/24.67 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))),
% 24.48/24.67 inference(quant_inst,[status(thm)],[])).
% 24.48/24.67 tff(172,plain,
% 24.48/24.67 (product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))),
% 24.48/24.67 inference(unit_resolution,[status(thm)],[171, 7])).
% 24.48/24.67 tff(173,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))))),
% 24.48/24.67 inference(rewrite,[status(thm)],[])).
% 24.48/24.67 tff(174,plain,
% 24.48/24.67 ((product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0)))) <=> ((~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))))),
% 24.48/24.67 inference(rewrite,[status(thm)],[])).
% 24.48/24.67 tff(175,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))),
% 24.48/24.67 inference(monotonicity,[status(thm)],[174])).
% 24.48/24.67 tff(176,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))))),
% 24.48/24.67 inference(transitivity,[status(thm)],[175, 173])).
% 24.48/24.67 tff(177,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))))),
% 24.48/24.67 inference(quant_inst,[status(thm)],[])).
% 24.48/24.67 tff(178,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(elem!0), multiply(elem!0, elem!0), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), inverse(elem!0), inverse(elem!0))) | product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))),
% 24.48/24.67 inference(modus_ponens,[status(thm)],[177, 176])).
% 24.48/24.67 tff(179,plain,
% 24.48/24.67 (product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))),
% 24.48/24.67 inference(unit_resolution,[status(thm)],[178, 30, 172, 170])).
% 24.48/24.67 tff(180,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))),
% 24.48/24.67 inference(rewrite,[status(thm)],[])).
% 24.48/24.67 tff(181,plain,
% 24.48/24.67 ((product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))) <=> ((~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))),
% 24.48/24.67 inference(rewrite,[status(thm)],[])).
% 24.48/24.67 tff(182,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))))))),
% 24.48/24.67 inference(monotonicity,[status(thm)],[181])).
% 24.48/24.67 tff(183,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))))),
% 24.48/24.67 inference(transitivity,[status(thm)],[182, 180])).
% 24.48/24.67 tff(184,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)))) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.67 inference(quant_inst,[status(thm)],[])).
% 24.48/24.67 tff(185,plain,
% 24.48/24.67 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))))) | (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | product(inverse(a), multiply(a, multiply(inverse(elem!0), multiply(elem!0, elem!0))), multiply(inverse(elem!0), multiply(elem!0, elem!0))) | (~product(multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0)), multiply(inverse(elem!0), multiply(elem!0, elem!0))))),
% 24.48/24.67 inference(modus_ponens,[status(thm)],[184, 183])).
% 24.48/24.67 tff(186,plain,
% 24.48/24.67 (~product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))),
% 24.48/24.67 inference(unit_resolution,[status(thm)],[185, 30, 140, 179, 163])).
% 24.48/24.67 tff(187,plain,
% 24.48/24.67 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(188,plain,
% 24.48/24.68 ((product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)))) <=> (product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(189,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))))),
% 24.48/24.68 inference(monotonicity,[status(thm)],[188])).
% 24.48/24.68 tff(190,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))))),
% 24.48/24.68 inference(transitivity,[status(thm)],[189, 187])).
% 24.48/24.68 tff(191,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0)))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))))),
% 24.48/24.68 inference(quant_inst,[status(thm)],[])).
% 24.48/24.68 tff(192,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | product(inverse(a), a, multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))) | (~product(multiply(a, inverse(elem!0)), inverse(inverse(elem!0)), a)) | (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), multiply(multiply(inverse(elem!0), elem!0), multiply(inverse(elem!0), elem!0))))),
% 24.48/24.68 inference(modus_ponens,[status(thm)],[191, 190])).
% 24.48/24.68 tff(193,plain,
% 24.48/24.68 (~product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0))),
% 24.48/24.68 inference(unit_resolution,[status(thm)],[192, 30, 186, 136, 78])).
% 24.48/24.68 tff(194,plain,
% 24.48/24.68 ((~![A: $i] : product(A, inverse(A), identity)) | product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)),
% 24.48/24.68 inference(quant_inst,[status(thm)],[])).
% 24.48/24.68 tff(195,plain,
% 24.48/24.68 (product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)),
% 24.48/24.68 inference(unit_resolution,[status(thm)],[194, 16])).
% 24.48/24.68 tff(196,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(197,plain,
% 24.48/24.68 ((product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0)))) <=> ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(198,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))))),
% 24.48/24.68 inference(monotonicity,[status(thm)],[197])).
% 24.48/24.68 tff(199,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)))),
% 24.48/24.68 inference(transitivity,[status(thm)],[198, 196])).
% 24.48/24.68 tff(200,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0)) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))))),
% 24.48/24.68 inference(quant_inst,[status(thm)],[])).
% 24.48/24.68 tff(201,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(inverse(elem!0), inverse(inverse(elem!0)), identity)) | (~product(inverse(elem!0), identity, inverse(elem!0))) | (~product(inverse(inverse(elem!0)), inverse(inverse(inverse(elem!0))), identity)) | product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))),
% 24.48/24.68 inference(modus_ponens,[status(thm)],[200, 199])).
% 24.48/24.68 tff(202,plain,
% 24.48/24.68 (product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))),
% 24.48/24.68 inference(unit_resolution,[status(thm)],[201, 51, 71, 95, 195])).
% 24.48/24.68 tff(203,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(204,plain,
% 24.48/24.68 ((product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0))))) <=> ((~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(205,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | ((~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))))),
% 24.48/24.68 inference(monotonicity,[status(thm)],[204])).
% 24.48/24.68 tff(206,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))))),
% 24.48/24.68 inference(transitivity,[status(thm)],[205, 203])).
% 24.48/24.68 tff(207,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))))),
% 24.48/24.68 inference(quant_inst,[status(thm)],[])).
% 24.48/24.68 tff(208,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(U, Z, W) | (~product(Y, Z, V)) | (~product(X, Y, U)) | (~product(X, V, W)))) | (~product(a, inverse(elem!0), multiply(a, inverse(elem!0)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(a, identity, multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))),
% 24.48/24.68 inference(modus_ponens,[status(thm)],[207, 206])).
% 24.48/24.68 tff(209,plain,
% 24.48/24.68 (product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))),
% 24.48/24.68 inference(unit_resolution,[status(thm)],[208, 51, 60, 37, 202])).
% 24.48/24.68 tff(210,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(211,plain,
% 24.48/24.68 ((product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity))) <=> ((~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(212,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))))))),
% 24.48/24.68 inference(monotonicity,[status(thm)],[211])).
% 24.48/24.68 tff(213,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))))),
% 24.48/24.68 inference(transitivity,[status(thm)],[212, 210])).
% 24.48/24.68 tff(214,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0)))) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)))),
% 24.48/24.68 inference(quant_inst,[status(thm)],[])).
% 24.48/24.68 tff(215,plain,
% 24.48/24.68 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(identity, inverse(inverse(inverse(elem!0))), inverse(elem!0))) | product(inverse(a), multiply(a, inverse(elem!0)), inverse(elem!0)) | (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)) | (~product(multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), inverse(inverse(inverse(elem!0))), multiply(a, inverse(elem!0))))),
% 24.48/24.68 inference(modus_ponens,[status(thm)],[214, 213])).
% 24.48/24.68 tff(216,plain,
% 24.48/24.68 (~product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity)),
% 24.48/24.68 inference(unit_resolution,[status(thm)],[215, 30, 202, 209, 193])).
% 24.48/24.68 tff(217,plain,
% 24.48/24.68 ((~![A: $i] : product(A, identity, A)) | product(inverse(a), identity, inverse(a))),
% 24.48/24.68 inference(quant_inst,[status(thm)],[])).
% 24.48/24.68 tff(218,plain,
% 24.48/24.68 (product(inverse(a), identity, inverse(a))),
% 24.48/24.68 inference(unit_resolution,[status(thm)],[217, 67])).
% 24.48/24.68 tff(219,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(a), identity, inverse(a))) | product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(a), identity, inverse(a))) | product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(220,plain,
% 24.48/24.68 ((product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(inverse(a), identity, inverse(a)))) <=> ((~product(inverse(a), identity, inverse(a))) | product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))),
% 24.48/24.68 inference(rewrite,[status(thm)],[])).
% 24.48/24.68 tff(221,plain,
% 24.48/24.68 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(inverse(a), identity, inverse(a))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(inverse(a), identity, inverse(a))) | product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))))),
% 24.48/24.69 inference(monotonicity,[status(thm)],[220])).
% 24.48/24.69 tff(222,plain,
% 24.48/24.69 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(inverse(a), identity, inverse(a))))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(a), identity, inverse(a))) | product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))))),
% 24.48/24.69 inference(transitivity,[status(thm)],[221, 219])).
% 24.48/24.69 tff(223,plain,
% 24.48/24.69 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))))) | (~product(inverse(a), identity, inverse(a))))),
% 24.48/24.69 inference(quant_inst,[status(thm)],[])).
% 24.48/24.69 tff(224,plain,
% 24.48/24.69 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(a), identity, inverse(a))) | product(inverse(a), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0))), identity) | (~product(inverse(a), inverse(inverse(a)), identity)) | (~product(identity, inverse(inverse(a)), multiply(multiply(a, multiply(elem!0, elem!0)), inverse(multiply(elem!0, elem!0)))))),
% 24.48/24.69 inference(modus_ponens,[status(thm)],[223, 222])).
% 24.48/24.69 tff(225,plain,
% 24.48/24.69 ($false),
% 24.48/24.69 inference(unit_resolution,[status(thm)],[224, 30, 39, 218, 216, 58])).
% 24.48/24.69 % SZS output end Proof
% 24.48/24.70 % E exiting
%------------------------------------------------------------------------------