%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GRP040-3 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.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:56 AM UTC 2025
% Result : Unsatisfiable 14.11s 14.28s
% Output : Proof 14.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GRP040-3 : TPTP v9.0.0. Released v1.0.0.
% 0.03/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n010.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 19 15:32:41 EDT 2025
% 0.11/0.32 % CPUTime :
% 14.11/14.28 % SZS status Unsatisfiable
% 14.11/14.28 % SZS output start Proof
% 14.11/14.28 tff(product_type, type, (
% 14.11/14.28 product: ( $i * $i * $i ) > $o)).
% 14.11/14.28 tff(inverse_type, type, (
% 14.11/14.28 inverse: $i > $i)).
% 14.11/14.28 tff(d_type, type, (
% 14.11/14.28 d: $i)).
% 14.11/14.28 tff(element_in_O2_type, type, (
% 14.11/14.28 element_in_O2: ( $i * $i ) > $i)).
% 14.11/14.28 tff(multiply_type, type, (
% 14.11/14.28 multiply: ( $i * $i ) > $i)).
% 14.11/14.28 tff(c_type, type, (
% 14.11/14.28 c: $i)).
% 14.11/14.28 tff(identity_type, type, (
% 14.11/14.28 identity: $i)).
% 14.11/14.28 tff(subgroup_member_type, type, (
% 14.11/14.28 subgroup_member: $i > $o)).
% 14.11/14.28 tff(a_type, type, (
% 14.11/14.28 a: $i)).
% 14.11/14.28 tff(b_type, type, (
% 14.11/14.28 b: $i)).
% 14.11/14.28 tff(1,plain,
% 14.11/14.28 (^[X: $i] : refl(product(X, inverse(X), identity) <=> product(X, inverse(X), identity))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(2,plain,
% 14.11/14.28 (![X: $i] : product(X, inverse(X), identity) <=> ![X: $i] : product(X, inverse(X), identity)),
% 14.11/14.28 inference(quant_intro,[status(thm)],[1])).
% 14.11/14.28 tff(3,plain,
% 14.11/14.28 (![X: $i] : product(X, inverse(X), identity) <=> ![X: $i] : product(X, inverse(X), identity)),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(4,axiom,(![X: $i] : product(X, inverse(X), identity)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','right_inverse')).
% 14.11/14.28 tff(5,plain,
% 14.11/14.28 (![X: $i] : product(X, inverse(X), identity)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[4, 3])).
% 14.11/14.28 tff(6,plain,(
% 14.11/14.28 ![X: $i] : product(X, inverse(X), identity)),
% 14.11/14.28 inference(skolemize,[status(sab)],[5])).
% 14.11/14.28 tff(7,plain,
% 14.11/14.28 (![X: $i] : product(X, inverse(X), identity)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[6, 2])).
% 14.11/14.28 tff(8,plain,
% 14.11/14.28 ((~![X: $i] : product(X, inverse(X), identity)) | product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(9,plain,
% 14.11/14.28 (product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[8, 7])).
% 14.11/14.28 tff(10,plain,
% 14.11/14.28 (![A: $i] : (inverse(inverse(A)) = A) <=> ![A: $i] : (inverse(inverse(A)) = A)),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(11,plain,
% 14.11/14.28 (![A: $i] : (inverse(inverse(A)) = A) <=> ![A: $i] : (inverse(inverse(A)) = A)),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(12,axiom,(![A: $i] : (inverse(inverse(A)) = A)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_inverse_is_self_cancelling')).
% 14.11/14.28 tff(13,plain,
% 14.11/14.28 (![A: $i] : (inverse(inverse(A)) = A)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[12, 11])).
% 14.11/14.28 tff(14,plain,(
% 14.11/14.28 ![A: $i] : (inverse(inverse(A)) = A)),
% 14.11/14.28 inference(skolemize,[status(sab)],[13])).
% 14.11/14.28 tff(15,plain,
% 14.11/14.28 (![A: $i] : (inverse(inverse(A)) = A)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[14, 10])).
% 14.11/14.28 tff(16,plain,
% 14.11/14.28 ((~![A: $i] : (inverse(inverse(A)) = A)) | (inverse(inverse(c)) = c)),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(17,plain,
% 14.11/14.28 (inverse(inverse(c)) = c),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[16, 15])).
% 14.11/14.28 tff(18,plain,
% 14.11/14.28 (^[Y: $i, X: $i] : refl(product(X, Y, multiply(X, Y)) <=> product(X, Y, multiply(X, Y)))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(19,plain,
% 14.11/14.28 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y)) <=> ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 14.11/14.28 inference(quant_intro,[status(thm)],[18])).
% 14.11/14.28 tff(20,plain,
% 14.11/14.28 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y)) <=> ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(21,axiom,(![Y: $i, X: $i] : product(X, Y, multiply(X, Y))), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','total_function1')).
% 14.11/14.28 tff(22,plain,
% 14.11/14.28 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[21, 20])).
% 14.11/14.28 tff(23,plain,(
% 14.11/14.28 ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 14.11/14.28 inference(skolemize,[status(sab)],[22])).
% 14.11/14.28 tff(24,plain,
% 14.11/14.28 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[23, 19])).
% 14.11/14.28 tff(25,plain,
% 14.11/14.28 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(identity, inverse(c), multiply(identity, inverse(c)))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(26,plain,
% 14.11/14.28 (product(identity, inverse(c), multiply(identity, inverse(c)))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[25, 24])).
% 14.11/14.28 tff(27,plain,
% 14.11/14.28 (^[X: $i] : refl(product(identity, X, X) <=> product(identity, X, X))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(28,plain,
% 14.11/14.28 (![X: $i] : product(identity, X, X) <=> ![X: $i] : product(identity, X, X)),
% 14.11/14.28 inference(quant_intro,[status(thm)],[27])).
% 14.11/14.28 tff(29,plain,
% 14.11/14.28 (![X: $i] : product(identity, X, X) <=> ![X: $i] : product(identity, X, X)),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(30,axiom,(![X: $i] : product(identity, X, X)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','left_identity')).
% 14.11/14.28 tff(31,plain,
% 14.11/14.28 (![X: $i] : product(identity, X, X)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[30, 29])).
% 14.11/14.28 tff(32,plain,(
% 14.11/14.28 ![X: $i] : product(identity, X, X)),
% 14.11/14.28 inference(skolemize,[status(sab)],[31])).
% 14.11/14.28 tff(33,plain,
% 14.11/14.28 (![X: $i] : product(identity, X, X)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[32, 28])).
% 14.11/14.28 tff(34,plain,
% 14.11/14.28 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(c), inverse(c))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(35,plain,
% 14.11/14.28 (product(identity, inverse(c), inverse(c))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[34, 33])).
% 14.11/14.28 tff(36,plain,
% 14.11/14.28 (^[W: $i, Z: $i, Y: $i, X: $i] : refl(((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z))) <=> ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z))))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(37,plain,
% 14.11/14.28 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z))) <=> ![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 14.11/14.28 inference(quant_intro,[status(thm)],[36])).
% 14.11/14.28 tff(38,plain,
% 14.11/14.28 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z))) <=> ![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(39,plain,
% 14.11/14.28 (^[W: $i, Z: $i, Y: $i, X: $i] : rewrite((((~product(X, Y, Z)) | (~product(X, Y, W))) | (Z = W)) <=> ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z))))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(40,plain,
% 14.11/14.28 (![W: $i, Z: $i, Y: $i, X: $i] : (((~product(X, Y, Z)) | (~product(X, Y, W))) | (Z = W)) <=> ![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 14.11/14.28 inference(quant_intro,[status(thm)],[39])).
% 14.11/14.28 tff(41,axiom,(![W: $i, Z: $i, Y: $i, X: $i] : (((~product(X, Y, Z)) | (~product(X, Y, W))) | (Z = W))), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','total_function2')).
% 14.11/14.28 tff(42,plain,
% 14.11/14.28 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[41, 40])).
% 14.11/14.28 tff(43,plain,
% 14.11/14.28 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[42, 38])).
% 14.11/14.28 tff(44,plain,(
% 14.11/14.28 ![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 14.11/14.28 inference(skolemize,[status(sab)],[43])).
% 14.11/14.28 tff(45,plain,
% 14.11/14.28 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[44, 37])).
% 14.11/14.28 tff(46,plain,
% 14.11/14.28 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(c) = multiply(identity, inverse(c))) | (~product(identity, inverse(c), multiply(identity, inverse(c)))) | (~product(identity, inverse(c), inverse(c))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (inverse(c) = multiply(identity, inverse(c))) | (~product(identity, inverse(c), multiply(identity, inverse(c)))) | (~product(identity, inverse(c), inverse(c))))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(47,plain,
% 14.11/14.28 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(c) = multiply(identity, inverse(c))) | (~product(identity, inverse(c), multiply(identity, inverse(c)))) | (~product(identity, inverse(c), inverse(c))))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(48,plain,
% 14.11/14.28 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (inverse(c) = multiply(identity, inverse(c))) | (~product(identity, inverse(c), multiply(identity, inverse(c)))) | (~product(identity, inverse(c), inverse(c)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[47, 46])).
% 14.11/14.28 tff(49,plain,
% 14.11/14.28 (inverse(c) = multiply(identity, inverse(c))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[48, 45, 35, 26])).
% 14.11/14.28 tff(50,plain,
% 14.11/14.28 (multiply(identity, inverse(c)) = inverse(c)),
% 14.11/14.28 inference(symmetry,[status(thm)],[49])).
% 14.11/14.28 tff(51,plain,
% 14.11/14.28 (inverse(multiply(identity, inverse(c))) = inverse(inverse(c))),
% 14.11/14.28 inference(monotonicity,[status(thm)],[50])).
% 14.11/14.28 tff(52,plain,
% 14.11/14.28 (inverse(multiply(identity, inverse(c))) = c),
% 14.11/14.28 inference(transitivity,[status(thm)],[51, 17])).
% 14.11/14.28 tff(53,plain,
% 14.11/14.28 (product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a)) <=> product(inverse(b), c, inverse(a))),
% 14.11/14.28 inference(monotonicity,[status(thm)],[52])).
% 14.11/14.28 tff(54,plain,
% 14.11/14.28 (product(inverse(b), c, inverse(a)) <=> product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))),
% 14.11/14.28 inference(symmetry,[status(thm)],[53])).
% 14.11/14.28 tff(55,plain,
% 14.11/14.28 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(a), inverse(a))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(56,plain,
% 14.11/14.28 (product(identity, inverse(a), inverse(a))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[55, 33])).
% 14.11/14.28 tff(57,plain,
% 14.11/14.28 (^[X: $i] : refl(product(inverse(X), X, identity) <=> product(inverse(X), X, identity))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(58,plain,
% 14.11/14.28 (![X: $i] : product(inverse(X), X, identity) <=> ![X: $i] : product(inverse(X), X, identity)),
% 14.11/14.28 inference(quant_intro,[status(thm)],[57])).
% 14.11/14.28 tff(59,plain,
% 14.11/14.28 (![X: $i] : product(inverse(X), X, identity) <=> ![X: $i] : product(inverse(X), X, identity)),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(60,axiom,(![X: $i] : product(inverse(X), X, identity)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','left_inverse')).
% 14.11/14.28 tff(61,plain,
% 14.11/14.28 (![X: $i] : product(inverse(X), X, identity)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[60, 59])).
% 14.11/14.28 tff(62,plain,(
% 14.11/14.28 ![X: $i] : product(inverse(X), X, identity)),
% 14.11/14.28 inference(skolemize,[status(sab)],[61])).
% 14.11/14.28 tff(63,plain,
% 14.11/14.28 (![X: $i] : product(inverse(X), X, identity)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[62, 58])).
% 14.11/14.28 tff(64,plain,
% 14.11/14.28 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(b), b, identity)),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(65,plain,
% 14.11/14.28 (product(inverse(b), b, identity)),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[64, 63])).
% 14.11/14.28 tff(66,plain,
% 14.11/14.28 (product(b, inverse(a), c) <=> product(b, inverse(a), c)),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(67,axiom,(product(b, inverse(a), c)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','b_times_a_inverse_is_c')).
% 14.11/14.28 tff(68,plain,
% 14.11/14.28 (product(b, inverse(a), c)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[67, 66])).
% 14.11/14.28 tff(69,plain,
% 14.11/14.28 (^[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))))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(70,plain,
% 14.11/14.28 (![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)))),
% 14.11/14.28 inference(quant_intro,[status(thm)],[69])).
% 14.11/14.28 tff(71,plain,
% 14.11/14.28 (![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)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(72,plain,
% 14.11/14.28 (^[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)))))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(73,plain,
% 14.11/14.28 (![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)))),
% 14.11/14.28 inference(quant_intro,[status(thm)],[72])).
% 14.11/14.28 tff(74,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/sandbox2/benchmark/Axioms/GRP003-0.ax','associativity1')).
% 14.11/14.28 tff(75,plain,
% 14.11/14.28 (![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)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[74, 73])).
% 14.11/14.28 tff(76,plain,
% 14.11/14.28 (![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)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[75, 71])).
% 14.11/14.28 tff(77,plain,(
% 14.11/14.28 ![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)))),
% 14.11/14.28 inference(skolemize,[status(sab)],[76])).
% 14.11/14.28 tff(78,plain,
% 14.11/14.28 (![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)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[77, 70])).
% 14.11/14.28 tff(79,plain,
% 14.11/14.28 (((~![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(b, inverse(a), c)) | (~product(inverse(b), b, identity)) | (~product(identity, inverse(a), inverse(a))) | product(inverse(b), c, 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(b, inverse(a), c)) | (~product(inverse(b), b, identity)) | (~product(identity, inverse(a), inverse(a))) | product(inverse(b), c, inverse(a)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(80,plain,
% 14.11/14.28 ((product(inverse(b), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(inverse(b), b, identity))) <=> ((~product(b, inverse(a), c)) | (~product(inverse(b), b, identity)) | (~product(identity, inverse(a), inverse(a))) | product(inverse(b), c, inverse(a)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(81,plain,
% 14.11/14.28 (((~![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(b), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(inverse(b), b, 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(b, inverse(a), c)) | (~product(inverse(b), b, identity)) | (~product(identity, inverse(a), inverse(a))) | product(inverse(b), c, inverse(a))))),
% 14.11/14.28 inference(monotonicity,[status(thm)],[80])).
% 14.11/14.28 tff(82,plain,
% 14.11/14.28 (((~![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(b), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(inverse(b), b, 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(b, inverse(a), c)) | (~product(inverse(b), b, identity)) | (~product(identity, inverse(a), inverse(a))) | product(inverse(b), c, inverse(a)))),
% 14.11/14.28 inference(transitivity,[status(thm)],[81, 79])).
% 14.11/14.28 tff(83,plain,
% 14.11/14.28 ((~![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(b), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(inverse(b), b, identity)))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(84,plain,
% 14.11/14.28 ((~![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(b, inverse(a), c)) | (~product(inverse(b), b, identity)) | (~product(identity, inverse(a), inverse(a))) | product(inverse(b), c, inverse(a))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[83, 82])).
% 14.11/14.28 tff(85,plain,
% 14.11/14.28 (product(inverse(b), c, inverse(a))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[84, 78, 68, 65, 56])).
% 14.11/14.28 tff(86,plain,
% 14.11/14.28 (product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[85, 54])).
% 14.11/14.28 tff(87,plain,
% 14.11/14.28 ((~![A: $i] : (inverse(inverse(A)) = A)) | (inverse(inverse(a)) = a)),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(88,plain,
% 14.11/14.28 (inverse(inverse(a)) = a),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[87, 15])).
% 14.11/14.28 tff(89,plain,
% 14.11/14.28 (product(identity, inverse(inverse(a)), a) <=> product(identity, a, a)),
% 14.11/14.28 inference(monotonicity,[status(thm)],[88])).
% 14.11/14.28 tff(90,plain,
% 14.11/14.28 (product(identity, a, a) <=> product(identity, inverse(inverse(a)), a)),
% 14.11/14.28 inference(symmetry,[status(thm)],[89])).
% 14.11/14.28 tff(91,plain,
% 14.11/14.28 ((~![X: $i] : product(identity, X, X)) | product(identity, a, a)),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(92,plain,
% 14.11/14.28 (product(identity, a, a)),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[91, 33])).
% 14.11/14.28 tff(93,plain,
% 14.11/14.28 (product(identity, inverse(inverse(a)), a)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[92, 90])).
% 14.11/14.28 tff(94,assumption,(~product(b, inverse(b), identity)), introduced(assumption)).
% 14.11/14.28 tff(95,plain,
% 14.11/14.28 ((~![X: $i] : product(X, inverse(X), identity)) | product(b, inverse(b), identity)),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(96,plain,
% 14.11/14.28 ($false),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[95, 7, 94])).
% 14.11/14.28 tff(97,plain,(product(b, inverse(b), identity)), inference(lemma,lemma(discharge,[]))).
% 14.11/14.28 tff(98,assumption,(product(b, inverse(b), identity)), introduced(assumption)).
% 14.11/14.28 tff(99,assumption,(~subgroup_member(identity)), introduced(assumption)).
% 14.11/14.28 tff(100,plain,
% 14.11/14.28 (subgroup_member(b) <=> subgroup_member(b)),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(101,axiom,(subgroup_member(b)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','b_is_in_subgroup')).
% 14.11/14.28 tff(102,plain,
% 14.11/14.28 (subgroup_member(b)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[101, 100])).
% 14.11/14.28 tff(103,plain,
% 14.11/14.28 (^[B: $i, A: $i, C: $i] : refl((subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A))) <=> (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A))))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(104,plain,
% 14.11/14.28 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A))) <=> ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 14.11/14.28 inference(quant_intro,[status(thm)],[103])).
% 14.11/14.28 tff(105,plain,
% 14.11/14.28 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A))) <=> ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(106,plain,
% 14.11/14.28 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, inverse(B), C))) <=> ((~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))), (((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, inverse(B), C))) | subgroup_member(C)) <=> (((~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A))) | subgroup_member(C)))), rewrite((((~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A))) | subgroup_member(C)) <=> (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))), (((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, inverse(B), C))) | subgroup_member(C)) <=> (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))))),
% 14.11/14.28 inference(bind,[status(th)],[])).
% 14.11/14.28 tff(107,plain,
% 14.11/14.28 (![B: $i, A: $i, C: $i] : ((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, inverse(B), C))) | subgroup_member(C)) <=> ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 14.11/14.28 inference(quant_intro,[status(thm)],[106])).
% 14.11/14.28 tff(108,axiom,(![B: $i, A: $i, C: $i] : ((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, inverse(B), C))) | subgroup_member(C))), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-2.ax','closure_of_product_and_inverse')).
% 14.11/14.28 tff(109,plain,
% 14.11/14.28 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[108, 107])).
% 14.11/14.28 tff(110,plain,
% 14.11/14.28 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[109, 105])).
% 14.11/14.28 tff(111,plain,(
% 14.11/14.28 ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 14.11/14.28 inference(skolemize,[status(sab)],[110])).
% 14.11/14.28 tff(112,plain,
% 14.11/14.28 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[111, 104])).
% 14.11/14.28 tff(113,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(identity) | (~subgroup_member(b)) | (~product(b, inverse(b), identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(identity) | (~subgroup_member(b)) | (~product(b, inverse(b), identity)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(114,plain,
% 14.11/14.28 ((subgroup_member(identity) | (~product(b, inverse(b), identity)) | (~subgroup_member(b)) | (~subgroup_member(b))) <=> (subgroup_member(identity) | (~subgroup_member(b)) | (~product(b, inverse(b), identity)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(115,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(identity) | (~product(b, inverse(b), identity)) | (~subgroup_member(b)) | (~subgroup_member(b)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(identity) | (~subgroup_member(b)) | (~product(b, inverse(b), identity))))),
% 14.11/14.28 inference(monotonicity,[status(thm)],[114])).
% 14.11/14.28 tff(116,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(identity) | (~product(b, inverse(b), identity)) | (~subgroup_member(b)) | (~subgroup_member(b)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(identity) | (~subgroup_member(b)) | (~product(b, inverse(b), identity)))),
% 14.11/14.28 inference(transitivity,[status(thm)],[115, 113])).
% 14.11/14.28 tff(117,plain,
% 14.11/14.28 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(identity) | (~product(b, inverse(b), identity)) | (~subgroup_member(b)) | (~subgroup_member(b)))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(118,plain,
% 14.11/14.28 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(identity) | (~subgroup_member(b)) | (~product(b, inverse(b), identity))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[117, 116])).
% 14.11/14.28 tff(119,plain,
% 14.11/14.28 ($false),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[118, 112, 102, 99, 98])).
% 14.11/14.28 tff(120,plain,((~product(b, inverse(b), identity)) | subgroup_member(identity)), inference(lemma,lemma(discharge,[]))).
% 14.11/14.28 tff(121,plain,
% 14.11/14.28 (subgroup_member(identity)),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[120, 97])).
% 14.11/14.28 tff(122,plain,
% 14.11/14.28 ((~subgroup_member(a)) <=> (~subgroup_member(a))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(123,axiom,(~subgroup_member(a)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a_in_subgroup')).
% 14.11/14.28 tff(124,plain,
% 14.11/14.28 (~subgroup_member(a)),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[123, 122])).
% 14.11/14.28 tff(125,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(a)), a)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(a) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(a)), a)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(126,plain,
% 14.11/14.28 ((subgroup_member(a) | (~product(identity, inverse(inverse(a)), a)) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity))) <=> (subgroup_member(a) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(a)), a)))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(127,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~product(identity, inverse(inverse(a)), a)) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(a)), a))))),
% 14.11/14.28 inference(monotonicity,[status(thm)],[126])).
% 14.11/14.28 tff(128,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~product(identity, inverse(inverse(a)), a)) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(a) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(a)), a)))),
% 14.11/14.28 inference(transitivity,[status(thm)],[127, 125])).
% 14.11/14.28 tff(129,plain,
% 14.11/14.28 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~product(identity, inverse(inverse(a)), a)) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(130,plain,
% 14.11/14.28 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(a) | (~subgroup_member(inverse(a))) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(a)), a))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[129, 128])).
% 14.11/14.28 tff(131,plain,
% 14.11/14.28 ((~subgroup_member(inverse(a))) | (~product(identity, inverse(inverse(a)), a))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[130, 112, 124, 121])).
% 14.11/14.28 tff(132,plain,
% 14.11/14.28 (~subgroup_member(inverse(a))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[131, 93])).
% 14.11/14.28 tff(133,plain,
% 14.11/14.28 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(b), inverse(b))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(134,plain,
% 14.11/14.28 (product(identity, inverse(b), inverse(b))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[133, 33])).
% 14.11/14.28 tff(135,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | ((~subgroup_member(b)) | subgroup_member(inverse(b)) | (~subgroup_member(identity)) | (~product(identity, inverse(b), inverse(b))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(b)) | subgroup_member(inverse(b)) | (~subgroup_member(identity)) | (~product(identity, inverse(b), inverse(b))))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(136,plain,
% 14.11/14.28 ((subgroup_member(inverse(b)) | (~product(identity, inverse(b), inverse(b))) | (~subgroup_member(b)) | (~subgroup_member(identity))) <=> ((~subgroup_member(b)) | subgroup_member(inverse(b)) | (~subgroup_member(identity)) | (~product(identity, inverse(b), inverse(b))))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.28 tff(137,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(b)) | (~product(identity, inverse(b), inverse(b))) | (~subgroup_member(b)) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | ((~subgroup_member(b)) | subgroup_member(inverse(b)) | (~subgroup_member(identity)) | (~product(identity, inverse(b), inverse(b)))))),
% 14.11/14.28 inference(monotonicity,[status(thm)],[136])).
% 14.11/14.28 tff(138,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(b)) | (~product(identity, inverse(b), inverse(b))) | (~subgroup_member(b)) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(b)) | subgroup_member(inverse(b)) | (~subgroup_member(identity)) | (~product(identity, inverse(b), inverse(b))))),
% 14.11/14.28 inference(transitivity,[status(thm)],[137, 135])).
% 14.11/14.28 tff(139,plain,
% 14.11/14.28 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(b)) | (~product(identity, inverse(b), inverse(b))) | (~subgroup_member(b)) | (~subgroup_member(identity)))),
% 14.11/14.28 inference(quant_inst,[status(thm)],[])).
% 14.11/14.28 tff(140,plain,
% 14.11/14.28 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(b)) | subgroup_member(inverse(b)) | (~subgroup_member(identity)) | (~product(identity, inverse(b), inverse(b)))),
% 14.11/14.28 inference(modus_ponens,[status(thm)],[139, 138])).
% 14.11/14.28 tff(141,plain,
% 14.11/14.28 (subgroup_member(inverse(b))),
% 14.11/14.28 inference(unit_resolution,[status(thm)],[140, 112, 102, 121, 134])).
% 14.11/14.28 tff(142,plain,
% 14.11/14.28 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~subgroup_member(inverse(b))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(inverse(b))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))))),
% 14.11/14.28 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(143,plain,
% 14.11/14.29 ((subgroup_member(inverse(a)) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~subgroup_member(inverse(b)))) <=> (subgroup_member(inverse(a)) | (~subgroup_member(inverse(b))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(144,plain,
% 14.11/14.29 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~subgroup_member(inverse(b))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~subgroup_member(inverse(b))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a)))))),
% 14.11/14.29 inference(monotonicity,[status(thm)],[143])).
% 14.11/14.29 tff(145,plain,
% 14.11/14.29 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~subgroup_member(inverse(b))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(inverse(b))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))))),
% 14.11/14.29 inference(transitivity,[status(thm)],[144, 142])).
% 14.11/14.29 tff(146,plain,
% 14.11/14.29 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~subgroup_member(inverse(b))))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(147,plain,
% 14.11/14.29 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(inverse(b))) | (~subgroup_member(multiply(identity, inverse(c)))) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a)))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[146, 145])).
% 14.11/14.29 tff(148,plain,
% 14.11/14.29 (subgroup_member(inverse(a)) | (~subgroup_member(multiply(identity, inverse(c)))) | (~product(inverse(b), inverse(multiply(identity, inverse(c))), inverse(a)))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[147, 112, 141])).
% 14.11/14.29 tff(149,plain,
% 14.11/14.29 (~subgroup_member(multiply(identity, inverse(c)))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[148, 132, 86])).
% 14.11/14.29 tff(150,plain,
% 14.11/14.29 ((~![A: $i] : (inverse(inverse(A)) = A)) | (inverse(inverse(d)) = d)),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(151,plain,
% 14.11/14.29 (inverse(inverse(d)) = d),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[150, 15])).
% 14.11/14.29 tff(152,plain,
% 14.11/14.29 (product(identity, inverse(inverse(d)), d) <=> product(identity, d, d)),
% 14.11/14.29 inference(monotonicity,[status(thm)],[151])).
% 14.11/14.29 tff(153,plain,
% 14.11/14.29 (product(identity, d, d) <=> product(identity, inverse(inverse(d)), d)),
% 14.11/14.29 inference(symmetry,[status(thm)],[152])).
% 14.11/14.29 tff(154,plain,
% 14.11/14.29 ((~![X: $i] : product(identity, X, X)) | product(identity, d, d)),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(155,plain,
% 14.11/14.29 (product(identity, d, d)),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[154, 33])).
% 14.11/14.29 tff(156,plain,
% 14.11/14.29 (product(identity, inverse(inverse(d)), d)),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[155, 153])).
% 14.11/14.29 tff(157,plain,
% 14.11/14.29 ((~subgroup_member(d)) <=> (~subgroup_member(d))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(158,axiom,(~subgroup_member(d)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','d_in_subgroup')).
% 14.11/14.29 tff(159,plain,
% 14.11/14.29 (~subgroup_member(d)),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[158, 157])).
% 14.11/14.29 tff(160,plain,
% 14.11/14.29 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(d) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(d) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(161,plain,
% 14.11/14.29 ((subgroup_member(d) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))) | (~subgroup_member(identity))) <=> (subgroup_member(d) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(162,plain,
% 14.11/14.29 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(d) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(d) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d)))))),
% 14.11/14.29 inference(monotonicity,[status(thm)],[161])).
% 14.11/14.29 tff(163,plain,
% 14.11/14.29 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(d) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(d) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))))),
% 14.11/14.29 inference(transitivity,[status(thm)],[162, 160])).
% 14.11/14.29 tff(164,plain,
% 14.11/14.29 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(d) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d))) | (~subgroup_member(identity)))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(165,plain,
% 14.11/14.29 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(d) | (~subgroup_member(identity)) | (~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d)))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[164, 163])).
% 14.11/14.29 tff(166,plain,
% 14.11/14.29 ((~product(identity, inverse(inverse(d)), d)) | (~subgroup_member(inverse(d)))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[165, 112, 159, 121])).
% 14.11/14.29 tff(167,plain,
% 14.11/14.29 (~subgroup_member(inverse(d))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[166, 156])).
% 14.11/14.29 tff(168,plain,
% 14.11/14.29 (^[B: $i, A: $i] : refl((subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B)) <=> (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B)))),
% 14.11/14.29 inference(bind,[status(th)],[])).
% 14.11/14.29 tff(169,plain,
% 14.11/14.29 (![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B)) <=> ![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))),
% 14.11/14.29 inference(quant_intro,[status(thm)],[168])).
% 14.11/14.29 tff(170,plain,
% 14.11/14.29 (![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B)) <=> ![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(171,plain,
% 14.11/14.29 (^[B: $i, A: $i] : trans(monotonicity(rewrite((product(A, element_in_O2(A, B), B) | subgroup_member(B)) <=> (product(A, element_in_O2(A, B), B) | subgroup_member(B))), (((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A)) <=> ((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A)))), rewrite(((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A)) <=> (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))), (((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A)) <=> (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))))),
% 14.11/14.29 inference(bind,[status(th)],[])).
% 14.11/14.29 tff(172,plain,
% 14.11/14.29 (![B: $i, A: $i] : ((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A)) <=> ![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))),
% 14.11/14.29 inference(quant_intro,[status(thm)],[171])).
% 14.11/14.29 tff(173,axiom,(![B: $i, A: $i] : ((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','property_of_O2')).
% 14.11/14.29 tff(174,plain,
% 14.11/14.29 (![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[173, 172])).
% 14.11/14.29 tff(175,plain,
% 14.11/14.29 (![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[174, 170])).
% 14.11/14.29 tff(176,plain,(
% 14.11/14.29 ![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))),
% 14.11/14.29 inference(skolemize,[status(sab)],[175])).
% 14.11/14.29 tff(177,plain,
% 14.11/14.29 (![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[176, 169])).
% 14.11/14.29 tff(178,plain,
% 14.11/14.29 (((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(inverse(d)))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(inverse(d)))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(179,plain,
% 14.11/14.29 ((subgroup_member(inverse(d)) | product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c)))) <=> (product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(inverse(d)))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(180,plain,
% 14.11/14.29 (((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(inverse(d)) | product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(inverse(d))))),
% 14.11/14.29 inference(monotonicity,[status(thm)],[179])).
% 14.11/14.29 tff(181,plain,
% 14.11/14.29 (((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(inverse(d)) | product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(inverse(d)))),
% 14.11/14.29 inference(transitivity,[status(thm)],[180, 178])).
% 14.11/14.29 tff(182,plain,
% 14.11/14.29 ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(inverse(d)) | product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(183,plain,
% 14.11/14.29 ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(inverse(d))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[182, 181])).
% 14.11/14.29 tff(184,plain,
% 14.11/14.29 (product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(inverse(d))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[183, 177])).
% 14.11/14.29 tff(185,plain,
% 14.11/14.29 (product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c))) | subgroup_member(multiply(identity, inverse(c)))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[184, 167])).
% 14.11/14.29 tff(186,plain,
% 14.11/14.29 (product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[185, 149])).
% 14.11/14.29 tff(187,plain,
% 14.11/14.29 (d = inverse(inverse(d))),
% 14.11/14.29 inference(symmetry,[status(thm)],[151])).
% 14.11/14.29 tff(188,plain,
% 14.11/14.29 (product(inverse(d), d, identity) <=> product(inverse(d), inverse(inverse(d)), identity)),
% 14.11/14.29 inference(monotonicity,[status(thm)],[187])).
% 14.11/14.29 tff(189,plain,
% 14.11/14.29 (product(inverse(d), inverse(inverse(d)), identity) <=> product(inverse(d), d, identity)),
% 14.11/14.29 inference(symmetry,[status(thm)],[188])).
% 14.11/14.29 tff(190,plain,
% 14.11/14.29 ((~![X: $i] : product(X, inverse(X), identity)) | product(inverse(d), inverse(inverse(d)), identity)),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(191,plain,
% 14.11/14.29 (product(inverse(d), inverse(inverse(d)), identity)),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[190, 7])).
% 14.11/14.29 tff(192,plain,
% 14.11/14.29 (product(inverse(d), d, identity)),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[191, 189])).
% 14.11/14.29 tff(193,plain,
% 14.11/14.29 (product(d, inverse(d), identity) <=> product(inverse(inverse(d)), inverse(d), identity)),
% 14.11/14.29 inference(monotonicity,[status(thm)],[187])).
% 14.11/14.29 tff(194,plain,
% 14.11/14.29 (product(inverse(inverse(d)), inverse(d), identity) <=> product(d, inverse(d), identity)),
% 14.11/14.29 inference(symmetry,[status(thm)],[193])).
% 14.11/14.29 tff(195,plain,
% 14.11/14.29 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(inverse(d)), inverse(d), identity)),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(196,plain,
% 14.11/14.29 (product(inverse(inverse(d)), inverse(d), identity)),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[195, 63])).
% 14.11/14.29 tff(197,plain,
% 14.11/14.29 (product(d, inverse(d), identity)),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[196, 194])).
% 14.11/14.29 tff(198,plain,
% 14.11/14.29 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(d), inverse(d))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(199,plain,
% 14.11/14.29 (product(identity, inverse(d), inverse(d))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[198, 33])).
% 14.11/14.29 tff(200,plain,
% 14.11/14.29 (((~![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(d), identity, inverse(d)) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity)) | (~product(identity, inverse(d), inverse(d))))) <=> ((~![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(d), identity, inverse(d)) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity)) | (~product(identity, inverse(d), inverse(d))))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(201,plain,
% 14.11/14.29 ((product(inverse(d), identity, inverse(d)) | (~product(identity, inverse(d), inverse(d))) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity))) <=> (product(inverse(d), identity, inverse(d)) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity)) | (~product(identity, inverse(d), inverse(d))))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(202,plain,
% 14.11/14.29 (((~![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(d), identity, inverse(d)) | (~product(identity, inverse(d), inverse(d))) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, 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(inverse(d), identity, inverse(d)) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity)) | (~product(identity, inverse(d), inverse(d)))))),
% 14.11/14.29 inference(monotonicity,[status(thm)],[201])).
% 14.11/14.29 tff(203,plain,
% 14.11/14.29 (((~![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(d), identity, inverse(d)) | (~product(identity, inverse(d), inverse(d))) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, 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(inverse(d), identity, inverse(d)) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity)) | (~product(identity, inverse(d), inverse(d))))),
% 14.11/14.29 inference(transitivity,[status(thm)],[202, 200])).
% 14.11/14.29 tff(204,plain,
% 14.11/14.29 ((~![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(d), identity, inverse(d)) | (~product(identity, inverse(d), inverse(d))) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity)))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(205,plain,
% 14.11/14.29 ((~![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(d), identity, inverse(d)) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity)) | (~product(identity, inverse(d), inverse(d)))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[204, 203])).
% 14.11/14.29 tff(206,plain,
% 14.11/14.29 (product(inverse(d), identity, inverse(d)) | (~product(d, inverse(d), identity)) | (~product(inverse(d), d, identity))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[205, 78, 199])).
% 14.11/14.29 tff(207,plain,
% 14.11/14.29 (product(inverse(d), identity, inverse(d))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[206, 197, 192])).
% 14.11/14.29 tff(208,plain,
% 14.11/14.29 (^[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))))),
% 14.11/14.29 inference(bind,[status(th)],[])).
% 14.11/14.29 tff(209,plain,
% 14.11/14.29 (![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)))),
% 14.11/14.29 inference(quant_intro,[status(thm)],[208])).
% 14.11/14.29 tff(210,plain,
% 14.11/14.29 (![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)))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(211,plain,
% 14.11/14.29 (^[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)))))),
% 14.11/14.29 inference(bind,[status(th)],[])).
% 14.11/14.29 tff(212,plain,
% 14.11/14.29 (![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)))),
% 14.11/14.29 inference(quant_intro,[status(thm)],[211])).
% 14.11/14.29 tff(213,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/sandbox2/benchmark/Axioms/GRP003-0.ax','associativity2')).
% 14.11/14.29 tff(214,plain,
% 14.11/14.29 (![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)))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[213, 212])).
% 14.11/14.29 tff(215,plain,
% 14.11/14.29 (![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)))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[214, 210])).
% 14.11/14.29 tff(216,plain,(
% 14.11/14.29 ![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)))),
% 14.11/14.29 inference(skolemize,[status(sab)],[215])).
% 14.11/14.29 tff(217,plain,
% 14.11/14.29 (![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)))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[216, 209])).
% 14.11/14.29 tff(218,plain,
% 14.11/14.29 (((~![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(d), identity, inverse(d))) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)))) <=> ((~![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(d), identity, inverse(d))) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(219,plain,
% 14.11/14.29 ((product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | (~product(inverse(d), identity, inverse(d)))) <=> ((~product(inverse(d), identity, inverse(d))) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(220,plain,
% 14.11/14.29 (((~![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(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | (~product(inverse(d), identity, inverse(d))))) <=> ((~![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(d), identity, inverse(d))) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))))),
% 14.11/14.29 inference(monotonicity,[status(thm)],[219])).
% 14.11/14.29 tff(221,plain,
% 14.11/14.29 (((~![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(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | (~product(inverse(d), identity, inverse(d))))) <=> ((~![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(d), identity, inverse(d))) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)))),
% 14.11/14.29 inference(transitivity,[status(thm)],[220, 218])).
% 14.11/14.29 tff(222,plain,
% 14.11/14.29 ((~![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(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | (~product(inverse(d), identity, inverse(d))))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(223,plain,
% 14.11/14.29 ((~![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(d), identity, inverse(d))) | (~product(element_in_O2(inverse(d), multiply(identity, inverse(c))), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), identity)) | (~product(inverse(d), element_in_O2(inverse(d), multiply(identity, inverse(c))), multiply(identity, inverse(c)))) | product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[222, 221])).
% 14.11/14.29 tff(224,plain,
% 14.11/14.29 (product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[223, 217, 207, 186, 9])).
% 14.11/14.29 tff(225,plain,
% 14.11/14.29 ((~![A: $i] : (inverse(inverse(A)) = A)) | (inverse(inverse(element_in_O2(d, d))) = element_in_O2(d, d))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(226,plain,
% 14.11/14.29 (inverse(inverse(element_in_O2(d, d))) = element_in_O2(d, d)),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[225, 15])).
% 14.11/14.29 tff(227,plain,
% 14.11/14.29 (element_in_O2(d, d) = inverse(inverse(element_in_O2(d, d)))),
% 14.11/14.29 inference(symmetry,[status(thm)],[226])).
% 14.11/14.29 tff(228,plain,
% 14.11/14.29 (product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity) <=> product(inverse(inverse(element_in_O2(d, d))), inverse(element_in_O2(d, d)), identity)),
% 14.11/14.29 inference(monotonicity,[status(thm)],[227])).
% 14.11/14.29 tff(229,plain,
% 14.11/14.29 (product(inverse(inverse(element_in_O2(d, d))), inverse(element_in_O2(d, d)), identity) <=> product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)),
% 14.11/14.29 inference(symmetry,[status(thm)],[228])).
% 14.11/14.29 tff(230,plain,
% 14.11/14.29 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(inverse(element_in_O2(d, d))), inverse(element_in_O2(d, d)), identity)),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(231,plain,
% 14.11/14.29 (product(inverse(inverse(element_in_O2(d, d))), inverse(element_in_O2(d, d)), identity)),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[230, 63])).
% 14.11/14.29 tff(232,plain,
% 14.11/14.29 (product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[231, 229])).
% 14.11/14.29 tff(233,plain,
% 14.11/14.29 (((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(d) | product(d, element_in_O2(d, d), d))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | subgroup_member(d) | product(d, element_in_O2(d, d), d))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(234,plain,
% 14.11/14.29 ((subgroup_member(d) | product(d, element_in_O2(d, d), d) | subgroup_member(d)) <=> (subgroup_member(d) | product(d, element_in_O2(d, d), d))),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(235,plain,
% 14.11/14.29 (((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(d) | product(d, element_in_O2(d, d), d) | subgroup_member(d))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(d) | product(d, element_in_O2(d, d), d)))),
% 14.11/14.29 inference(monotonicity,[status(thm)],[234])).
% 14.11/14.29 tff(236,plain,
% 14.11/14.29 (((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(d) | product(d, element_in_O2(d, d), d) | subgroup_member(d))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | subgroup_member(d) | product(d, element_in_O2(d, d), d))),
% 14.11/14.29 inference(transitivity,[status(thm)],[235, 233])).
% 14.11/14.29 tff(237,plain,
% 14.11/14.29 ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | (subgroup_member(d) | product(d, element_in_O2(d, d), d) | subgroup_member(d))),
% 14.11/14.29 inference(quant_inst,[status(thm)],[])).
% 14.11/14.29 tff(238,plain,
% 14.11/14.29 ((~![B: $i, A: $i] : (subgroup_member(A) | product(A, element_in_O2(A, B), B) | subgroup_member(B))) | subgroup_member(d) | product(d, element_in_O2(d, d), d)),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[237, 236])).
% 14.11/14.29 tff(239,plain,
% 14.11/14.29 (product(d, element_in_O2(d, d), d)),
% 14.11/14.29 inference(unit_resolution,[status(thm)],[238, 177, 159])).
% 14.11/14.29 tff(240,assumption,(~product(c, identity, c)), introduced(assumption)).
% 14.11/14.29 tff(241,plain,
% 14.11/14.29 (^[X: $i] : refl(product(X, identity, X) <=> product(X, identity, X))),
% 14.11/14.29 inference(bind,[status(th)],[])).
% 14.11/14.29 tff(242,plain,
% 14.11/14.29 (![X: $i] : product(X, identity, X) <=> ![X: $i] : product(X, identity, X)),
% 14.11/14.29 inference(quant_intro,[status(thm)],[241])).
% 14.11/14.29 tff(243,plain,
% 14.11/14.29 (![X: $i] : product(X, identity, X) <=> ![X: $i] : product(X, identity, X)),
% 14.11/14.29 inference(rewrite,[status(thm)],[])).
% 14.11/14.29 tff(244,axiom,(![X: $i] : product(X, identity, X)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','right_identity')).
% 14.11/14.29 tff(245,plain,
% 14.11/14.29 (![X: $i] : product(X, identity, X)),
% 14.11/14.29 inference(modus_ponens,[status(thm)],[244, 243])).
% 14.11/14.29 tff(246,plain,(
% 14.11/14.29 ![X: $i] : product(X, identity, X)),
% 14.11/14.30 inference(skolemize,[status(sab)],[245])).
% 14.11/14.30 tff(247,plain,
% 14.11/14.30 (![X: $i] : product(X, identity, X)),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[246, 242])).
% 14.11/14.30 tff(248,plain,
% 14.11/14.30 ((~![X: $i] : product(X, identity, X)) | product(c, identity, c)),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(249,plain,
% 14.11/14.30 ($false),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[248, 247, 240])).
% 14.11/14.30 tff(250,plain,(product(c, identity, c)), inference(lemma,lemma(discharge,[]))).
% 14.11/14.30 tff(251,plain,
% 14.11/14.30 (product(a, c, d) <=> product(a, c, d)),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(252,axiom,(product(a, c, d)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a_times_c_is_d')).
% 14.11/14.30 tff(253,plain,
% 14.11/14.30 (product(a, c, d)),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[252, 251])).
% 14.11/14.30 tff(254,plain,
% 14.11/14.30 (((~![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, c, d)) | product(d, identity, d) | (~product(c, identity, c)))) <=> ((~![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, c, d)) | product(d, identity, d) | (~product(c, identity, c)))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(255,plain,
% 14.11/14.30 ((product(d, identity, d) | (~product(c, identity, c)) | (~product(a, c, d)) | (~product(a, c, d))) <=> ((~product(a, c, d)) | product(d, identity, d) | (~product(c, identity, c)))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(256,plain,
% 14.11/14.30 (((~![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(d, identity, d) | (~product(c, identity, c)) | (~product(a, c, d)) | (~product(a, c, d)))) <=> ((~![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, c, d)) | product(d, identity, d) | (~product(c, identity, c))))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[255])).
% 14.11/14.30 tff(257,plain,
% 14.11/14.30 (((~![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(d, identity, d) | (~product(c, identity, c)) | (~product(a, c, d)) | (~product(a, c, d)))) <=> ((~![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, c, d)) | product(d, identity, d) | (~product(c, identity, c)))),
% 14.11/14.30 inference(transitivity,[status(thm)],[256, 254])).
% 14.11/14.30 tff(258,plain,
% 14.11/14.30 ((~![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(d, identity, d) | (~product(c, identity, c)) | (~product(a, c, d)) | (~product(a, c, d)))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(259,plain,
% 14.11/14.30 ((~![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, c, d)) | product(d, identity, d) | (~product(c, identity, c))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[258, 257])).
% 14.11/14.30 tff(260,plain,
% 14.11/14.30 (product(d, identity, d)),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[259, 217, 253, 250])).
% 14.11/14.30 tff(261,plain,
% 14.11/14.30 (((~![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(d, element_in_O2(d, d), d)) | (~product(d, identity, d)) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | product(d, inverse(element_in_O2(d, d)), d))) <=> ((~![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(d, element_in_O2(d, d), d)) | (~product(d, identity, d)) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | product(d, inverse(element_in_O2(d, d)), d))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(262,plain,
% 14.11/14.30 ((product(d, inverse(element_in_O2(d, d)), d) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | (~product(d, element_in_O2(d, d), d)) | (~product(d, identity, d))) <=> ((~product(d, element_in_O2(d, d), d)) | (~product(d, identity, d)) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | product(d, inverse(element_in_O2(d, d)), d))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(263,plain,
% 14.11/14.30 (((~![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(d, inverse(element_in_O2(d, d)), d) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | (~product(d, element_in_O2(d, d), d)) | (~product(d, identity, d)))) <=> ((~![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(d, element_in_O2(d, d), d)) | (~product(d, identity, d)) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | product(d, inverse(element_in_O2(d, d)), d)))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[262])).
% 14.11/14.30 tff(264,plain,
% 14.11/14.30 (((~![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(d, inverse(element_in_O2(d, d)), d) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | (~product(d, element_in_O2(d, d), d)) | (~product(d, identity, d)))) <=> ((~![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(d, element_in_O2(d, d), d)) | (~product(d, identity, d)) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | product(d, inverse(element_in_O2(d, d)), d))),
% 14.11/14.30 inference(transitivity,[status(thm)],[263, 261])).
% 14.11/14.30 tff(265,plain,
% 14.11/14.30 ((~![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(d, inverse(element_in_O2(d, d)), d) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | (~product(d, element_in_O2(d, d), d)) | (~product(d, identity, d)))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(266,plain,
% 14.11/14.30 ((~![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(d, element_in_O2(d, d), d)) | (~product(d, identity, d)) | (~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | product(d, inverse(element_in_O2(d, d)), d)),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[265, 264])).
% 14.11/14.30 tff(267,plain,
% 14.11/14.30 ((~product(element_in_O2(d, d), inverse(element_in_O2(d, d)), identity)) | product(d, inverse(element_in_O2(d, d)), d)),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[266, 217, 260, 239])).
% 14.11/14.30 tff(268,plain,
% 14.11/14.30 (product(d, inverse(element_in_O2(d, d)), d)),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[267, 232])).
% 14.11/14.30 tff(269,plain,
% 14.11/14.30 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(element_in_O2(d, d)), inverse(element_in_O2(d, d)))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(270,plain,
% 14.11/14.30 (product(identity, inverse(element_in_O2(d, d)), inverse(element_in_O2(d, d)))),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[269, 33])).
% 14.11/14.30 tff(271,plain,
% 14.11/14.30 (((~![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(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(inverse(d), d, identity)) | (~product(d, inverse(element_in_O2(d, d)), d)) | product(inverse(d), d, inverse(element_in_O2(d, d))))) <=> ((~![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(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(inverse(d), d, identity)) | (~product(d, inverse(element_in_O2(d, d)), d)) | product(inverse(d), d, inverse(element_in_O2(d, d))))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(272,plain,
% 14.11/14.30 ((product(inverse(d), d, inverse(element_in_O2(d, d))) | (~product(identity, inverse(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(d, inverse(element_in_O2(d, d)), d)) | (~product(inverse(d), d, identity))) <=> ((~product(identity, inverse(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(inverse(d), d, identity)) | (~product(d, inverse(element_in_O2(d, d)), d)) | product(inverse(d), d, inverse(element_in_O2(d, d))))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(273,plain,
% 14.11/14.30 (((~![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(d), d, inverse(element_in_O2(d, d))) | (~product(identity, inverse(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(d, inverse(element_in_O2(d, d)), d)) | (~product(inverse(d), d, 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(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(inverse(d), d, identity)) | (~product(d, inverse(element_in_O2(d, d)), d)) | product(inverse(d), d, inverse(element_in_O2(d, d)))))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[272])).
% 14.11/14.30 tff(274,plain,
% 14.11/14.30 (((~![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(d), d, inverse(element_in_O2(d, d))) | (~product(identity, inverse(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(d, inverse(element_in_O2(d, d)), d)) | (~product(inverse(d), d, 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(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(inverse(d), d, identity)) | (~product(d, inverse(element_in_O2(d, d)), d)) | product(inverse(d), d, inverse(element_in_O2(d, d))))),
% 14.11/14.30 inference(transitivity,[status(thm)],[273, 271])).
% 14.11/14.30 tff(275,plain,
% 14.11/14.30 ((~![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(d), d, inverse(element_in_O2(d, d))) | (~product(identity, inverse(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(d, inverse(element_in_O2(d, d)), d)) | (~product(inverse(d), d, identity)))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(276,plain,
% 14.11/14.30 ((~![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(element_in_O2(d, d)), inverse(element_in_O2(d, d)))) | (~product(inverse(d), d, identity)) | (~product(d, inverse(element_in_O2(d, d)), d)) | product(inverse(d), d, inverse(element_in_O2(d, d)))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[275, 274])).
% 14.11/14.30 tff(277,plain,
% 14.11/14.30 (product(inverse(d), d, inverse(element_in_O2(d, d)))),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[276, 78, 270, 192, 268])).
% 14.11/14.30 tff(278,plain,
% 14.11/14.30 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))) | (inverse(element_in_O2(d, d)) = identity))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))) | (inverse(element_in_O2(d, d)) = identity))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(279,plain,
% 14.11/14.30 (((inverse(element_in_O2(d, d)) = identity) | (~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d))))) <=> ((~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))) | (inverse(element_in_O2(d, d)) = identity))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(280,plain,
% 14.11/14.30 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(element_in_O2(d, d)) = identity) | (~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))) | (inverse(element_in_O2(d, d)) = identity)))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[279])).
% 14.11/14.30 tff(281,plain,
% 14.11/14.30 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(element_in_O2(d, d)) = identity) | (~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))) | (inverse(element_in_O2(d, d)) = identity))),
% 14.11/14.30 inference(transitivity,[status(thm)],[280, 278])).
% 14.11/14.30 tff(282,plain,
% 14.11/14.30 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(element_in_O2(d, d)) = identity) | (~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(283,plain,
% 14.11/14.30 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(inverse(d), d, identity)) | (~product(inverse(d), d, inverse(element_in_O2(d, d)))) | (inverse(element_in_O2(d, d)) = identity)),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[282, 281])).
% 14.11/14.30 tff(284,plain,
% 14.11/14.30 (inverse(element_in_O2(d, d)) = identity),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[283, 45, 192, 277])).
% 14.11/14.30 tff(285,plain,
% 14.11/14.30 (inverse(inverse(element_in_O2(d, d))) = inverse(identity)),
% 14.11/14.30 inference(monotonicity,[status(thm)],[284])).
% 14.11/14.30 tff(286,plain,
% 14.11/14.30 (inverse(identity) = inverse(inverse(element_in_O2(d, d)))),
% 14.11/14.30 inference(symmetry,[status(thm)],[285])).
% 14.11/14.30 tff(287,plain,
% 14.11/14.30 ((~![A: $i] : (inverse(inverse(A)) = A)) | (inverse(inverse(identity)) = identity)),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(288,plain,
% 14.11/14.30 (inverse(inverse(identity)) = identity),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[287, 15])).
% 14.11/14.30 tff(289,plain,
% 14.11/14.30 (identity = inverse(inverse(identity))),
% 14.11/14.30 inference(symmetry,[status(thm)],[288])).
% 14.11/14.30 tff(290,plain,
% 14.11/14.30 (product(inverse(identity), identity, identity) <=> product(inverse(identity), inverse(inverse(identity)), identity)),
% 14.11/14.30 inference(monotonicity,[status(thm)],[289])).
% 14.11/14.30 tff(291,plain,
% 14.11/14.30 (product(inverse(identity), inverse(inverse(identity)), identity) <=> product(inverse(identity), identity, identity)),
% 14.11/14.30 inference(symmetry,[status(thm)],[290])).
% 14.11/14.30 tff(292,plain,
% 14.11/14.30 ((~![X: $i] : product(X, inverse(X), identity)) | product(inverse(identity), inverse(inverse(identity)), identity)),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(293,plain,
% 14.11/14.30 (product(inverse(identity), inverse(inverse(identity)), identity)),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[292, 7])).
% 14.11/14.30 tff(294,plain,
% 14.11/14.30 (product(inverse(identity), identity, identity)),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[293, 291])).
% 14.11/14.30 tff(295,plain,
% 14.11/14.30 ((~![X: $i] : product(X, identity, X)) | product(inverse(identity), identity, inverse(identity))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(296,plain,
% 14.11/14.30 (product(inverse(identity), identity, inverse(identity))),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[295, 247])).
% 14.11/14.30 tff(297,plain,
% 14.11/14.30 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((~product(inverse(identity), identity, identity)) | (inverse(identity) = identity) | (~product(inverse(identity), identity, inverse(identity))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(inverse(identity), identity, identity)) | (inverse(identity) = identity) | (~product(inverse(identity), identity, inverse(identity))))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(298,plain,
% 14.11/14.30 (((inverse(identity) = identity) | (~product(inverse(identity), identity, identity)) | (~product(inverse(identity), identity, inverse(identity)))) <=> ((~product(inverse(identity), identity, identity)) | (inverse(identity) = identity) | (~product(inverse(identity), identity, inverse(identity))))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(299,plain,
% 14.11/14.30 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(identity) = identity) | (~product(inverse(identity), identity, identity)) | (~product(inverse(identity), identity, inverse(identity))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((~product(inverse(identity), identity, identity)) | (inverse(identity) = identity) | (~product(inverse(identity), identity, inverse(identity)))))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[298])).
% 14.11/14.30 tff(300,plain,
% 14.11/14.30 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(identity) = identity) | (~product(inverse(identity), identity, identity)) | (~product(inverse(identity), identity, inverse(identity))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(inverse(identity), identity, identity)) | (inverse(identity) = identity) | (~product(inverse(identity), identity, inverse(identity))))),
% 14.11/14.30 inference(transitivity,[status(thm)],[299, 297])).
% 14.11/14.30 tff(301,plain,
% 14.11/14.30 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(identity) = identity) | (~product(inverse(identity), identity, identity)) | (~product(inverse(identity), identity, inverse(identity))))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(302,plain,
% 14.11/14.30 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(inverse(identity), identity, identity)) | (inverse(identity) = identity) | (~product(inverse(identity), identity, inverse(identity)))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[301, 300])).
% 14.11/14.30 tff(303,plain,
% 14.11/14.30 ((~product(inverse(identity), identity, identity)) | (inverse(identity) = identity)),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[302, 45, 296])).
% 14.11/14.30 tff(304,plain,
% 14.11/14.30 (inverse(identity) = identity),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[303, 294])).
% 14.11/14.30 tff(305,plain,
% 14.11/14.30 (identity = inverse(identity)),
% 14.11/14.30 inference(symmetry,[status(thm)],[304])).
% 14.11/14.30 tff(306,plain,
% 14.11/14.30 (identity = element_in_O2(d, d)),
% 14.11/14.30 inference(transitivity,[status(thm)],[305, 286, 226])).
% 14.11/14.30 tff(307,plain,
% 14.11/14.30 (product(identity, a, multiply(element_in_O2(d, d), a)) <=> product(element_in_O2(d, d), a, multiply(element_in_O2(d, d), a))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[306])).
% 14.11/14.30 tff(308,plain,
% 14.11/14.30 (product(element_in_O2(d, d), a, multiply(element_in_O2(d, d), a)) <=> product(identity, a, multiply(element_in_O2(d, d), a))),
% 14.11/14.30 inference(symmetry,[status(thm)],[307])).
% 14.11/14.30 tff(309,plain,
% 14.11/14.30 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(element_in_O2(d, d), a, multiply(element_in_O2(d, d), a))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(310,plain,
% 14.11/14.30 (product(element_in_O2(d, d), a, multiply(element_in_O2(d, d), a))),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[309, 24])).
% 14.11/14.30 tff(311,plain,
% 14.11/14.30 (product(identity, a, multiply(element_in_O2(d, d), a))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[310, 308])).
% 14.11/14.30 tff(312,plain,
% 14.11/14.30 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((a = multiply(element_in_O2(d, d), a)) | (~product(identity, a, multiply(element_in_O2(d, d), a))) | (~product(identity, a, a)))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (a = multiply(element_in_O2(d, d), a)) | (~product(identity, a, multiply(element_in_O2(d, d), a))) | (~product(identity, a, a)))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(313,plain,
% 14.11/14.30 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((a = multiply(element_in_O2(d, d), a)) | (~product(identity, a, multiply(element_in_O2(d, d), a))) | (~product(identity, a, a)))),
% 14.11/14.30 inference(quant_inst,[status(thm)],[])).
% 14.11/14.30 tff(314,plain,
% 14.11/14.30 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (a = multiply(element_in_O2(d, d), a)) | (~product(identity, a, multiply(element_in_O2(d, d), a))) | (~product(identity, a, a))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[313, 312])).
% 14.11/14.30 tff(315,plain,
% 14.11/14.30 ((a = multiply(element_in_O2(d, d), a)) | (~product(identity, a, multiply(element_in_O2(d, d), a)))),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[314, 45, 92])).
% 14.11/14.30 tff(316,plain,
% 14.11/14.30 (a = multiply(element_in_O2(d, d), a)),
% 14.11/14.30 inference(unit_resolution,[status(thm)],[315, 311])).
% 14.11/14.30 tff(317,plain,
% 14.11/14.30 (inverse(a) = inverse(multiply(element_in_O2(d, d), a))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[316])).
% 14.11/14.30 tff(318,plain,
% 14.11/14.30 (inverse(multiply(element_in_O2(d, d), a)) = inverse(a)),
% 14.11/14.30 inference(symmetry,[status(thm)],[317])).
% 14.11/14.30 tff(319,plain,
% 14.11/14.30 (product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) <=> product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[318])).
% 14.11/14.30 tff(320,plain,
% 14.11/14.30 (product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a)) <=> product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a)))),
% 14.11/14.30 inference(symmetry,[status(thm)],[319])).
% 14.11/14.30 tff(321,plain,
% 14.11/14.30 ((~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) <=> (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[320])).
% 14.11/14.30 tff(322,plain,
% 14.11/14.30 (^[B: $i, A: $i] : refl((subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B)) <=> (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B)))),
% 14.11/14.30 inference(bind,[status(th)],[])).
% 14.11/14.30 tff(323,plain,
% 14.11/14.30 (![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B)) <=> ![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))),
% 14.11/14.30 inference(quant_intro,[status(thm)],[322])).
% 14.11/14.30 tff(324,plain,
% 14.11/14.30 (![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B)) <=> ![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(325,plain,
% 14.11/14.30 (^[B: $i, A: $i] : trans(monotonicity(rewrite((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) <=> (subgroup_member(element_in_O2(A, B)) | subgroup_member(B))), (((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) | subgroup_member(A)) <=> ((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) | subgroup_member(A)))), rewrite(((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) | subgroup_member(A)) <=> (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))), (((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) | subgroup_member(A)) <=> (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))))),
% 14.11/14.30 inference(bind,[status(th)],[])).
% 14.11/14.30 tff(326,plain,
% 14.11/14.30 (![B: $i, A: $i] : ((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) | subgroup_member(A)) <=> ![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))),
% 14.11/14.30 inference(quant_intro,[status(thm)],[325])).
% 14.11/14.30 tff(327,axiom,(![B: $i, A: $i] : ((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) | subgroup_member(A))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','an_element_in_O2')).
% 14.11/14.30 tff(328,plain,
% 14.11/14.30 (![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[327, 326])).
% 14.11/14.30 tff(329,plain,
% 14.11/14.30 (![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[328, 324])).
% 14.11/14.30 tff(330,plain,(
% 14.11/14.30 ![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))),
% 14.11/14.30 inference(skolemize,[status(sab)],[329])).
% 14.11/14.30 tff(331,plain,
% 14.11/14.30 (![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))),
% 14.11/14.30 inference(modus_ponens,[status(thm)],[330, 323])).
% 14.11/14.30 tff(332,plain,
% 14.11/14.30 (((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | (subgroup_member(multiply(identity, inverse(c))) | subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)))) <=> ((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(333,plain,
% 14.11/14.30 ((subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)) | subgroup_member(multiply(identity, inverse(c)))) <=> (subgroup_member(multiply(identity, inverse(c))) | subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)))),
% 14.11/14.30 inference(rewrite,[status(thm)],[])).
% 14.11/14.30 tff(334,plain,
% 14.11/14.30 (((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | (subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)) | subgroup_member(multiply(identity, inverse(c))))) <=> ((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | (subgroup_member(multiply(identity, inverse(c))) | subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d))))),
% 14.11/14.30 inference(monotonicity,[status(thm)],[333])).
% 14.11/14.30 tff(335,plain,
% 14.11/14.30 (((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | (subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)) | subgroup_member(multiply(identity, inverse(c))))) <=> ((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)))),
% 14.11/14.31 inference(transitivity,[status(thm)],[334, 332])).
% 14.11/14.31 tff(336,plain,
% 14.11/14.31 ((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | (subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d)) | subgroup_member(multiply(identity, inverse(c))))),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(337,plain,
% 14.11/14.31 ((~![B: $i, A: $i] : (subgroup_member(element_in_O2(A, B)) | subgroup_member(A) | subgroup_member(B))) | subgroup_member(multiply(identity, inverse(c))) | subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))) | subgroup_member(inverse(d))),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[336, 335])).
% 14.11/14.31 tff(338,plain,
% 14.11/14.31 (subgroup_member(multiply(identity, inverse(c))) | subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[337, 331, 167])).
% 14.11/14.31 tff(339,plain,
% 14.11/14.31 (subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[338, 149])).
% 14.11/14.31 tff(340,plain,
% 14.11/14.31 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~subgroup_member(identity)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(identity)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(341,plain,
% 14.11/14.31 ((subgroup_member(inverse(a)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))) | (~subgroup_member(identity))) <=> (subgroup_member(inverse(a)) | (~subgroup_member(identity)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(342,plain,
% 14.11/14.31 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~subgroup_member(identity)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))))))),
% 14.11/14.31 inference(monotonicity,[status(thm)],[341])).
% 14.11/14.31 tff(343,plain,
% 14.11/14.31 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(identity)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))))),
% 14.11/14.31 inference(transitivity,[status(thm)],[342, 340])).
% 14.11/14.31 tff(344,plain,
% 14.11/14.31 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c))))) | (~subgroup_member(identity)))),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(345,plain,
% 14.11/14.31 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, inverse(B), C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(identity)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))))),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[344, 343])).
% 14.11/14.31 tff(346,plain,
% 14.11/14.31 (subgroup_member(inverse(a)) | (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))) | (~subgroup_member(element_in_O2(inverse(d), multiply(identity, inverse(c)))))),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[345, 112, 121])).
% 14.11/14.31 tff(347,plain,
% 14.11/14.31 (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(a))),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[346, 339, 132])).
% 14.11/14.31 tff(348,plain,
% 14.11/14.31 (~product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a)))),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[347, 321])).
% 14.11/14.31 tff(349,plain,
% 14.11/14.31 (product(inverse(multiply(element_in_O2(d, d), a)), d, c) <=> product(inverse(a), d, c)),
% 14.11/14.31 inference(monotonicity,[status(thm)],[318])).
% 14.11/14.31 tff(350,plain,
% 14.11/14.31 (product(inverse(a), d, c) <=> product(inverse(multiply(element_in_O2(d, d), a)), d, c)),
% 14.11/14.31 inference(symmetry,[status(thm)],[349])).
% 14.11/14.31 tff(351,plain,
% 14.11/14.31 (c = inverse(inverse(c))),
% 14.11/14.31 inference(symmetry,[status(thm)],[17])).
% 14.11/14.31 tff(352,plain,
% 14.11/14.31 (product(c, inverse(c), identity) <=> product(inverse(inverse(c)), inverse(c), identity)),
% 14.11/14.31 inference(monotonicity,[status(thm)],[351])).
% 14.11/14.31 tff(353,plain,
% 14.11/14.31 (product(inverse(inverse(c)), inverse(c), identity) <=> product(c, inverse(c), identity)),
% 14.11/14.31 inference(symmetry,[status(thm)],[352])).
% 14.11/14.31 tff(354,plain,
% 14.11/14.31 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(inverse(c)), inverse(c), identity)),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(355,plain,
% 14.11/14.31 (product(inverse(inverse(c)), inverse(c), identity)),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[354, 63])).
% 14.11/14.31 tff(356,plain,
% 14.11/14.31 (product(c, inverse(c), identity)),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[355, 353])).
% 14.11/14.31 tff(357,plain,
% 14.11/14.31 (product(inverse(c), c, identity) <=> product(inverse(c), inverse(inverse(c)), identity)),
% 14.11/14.31 inference(monotonicity,[status(thm)],[351])).
% 14.11/14.31 tff(358,plain,
% 14.11/14.31 (product(inverse(c), inverse(inverse(c)), identity) <=> product(inverse(c), c, identity)),
% 14.11/14.31 inference(symmetry,[status(thm)],[357])).
% 14.11/14.31 tff(359,plain,
% 14.11/14.31 ((~![X: $i] : product(X, inverse(X), identity)) | product(inverse(c), inverse(inverse(c)), identity)),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(360,plain,
% 14.11/14.31 (product(inverse(c), inverse(inverse(c)), identity)),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[359, 7])).
% 14.11/14.31 tff(361,plain,
% 14.11/14.31 (product(inverse(c), c, identity)),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[360, 358])).
% 14.11/14.31 tff(362,plain,
% 14.11/14.31 (((~![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(c, inverse(c), identity)) | (~product(inverse(c), c, identity)) | (~product(c, identity, c)) | product(identity, c, c))) <=> ((~![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(c, inverse(c), identity)) | (~product(inverse(c), c, identity)) | (~product(c, identity, c)) | product(identity, c, c))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(363,plain,
% 14.11/14.31 ((product(identity, c, c) | (~product(inverse(c), c, identity)) | (~product(c, inverse(c), identity)) | (~product(c, identity, c))) <=> ((~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity)) | (~product(c, identity, c)) | product(identity, c, c))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(364,plain,
% 14.11/14.31 (((~![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, c, c) | (~product(inverse(c), c, identity)) | (~product(c, inverse(c), identity)) | (~product(c, identity, c)))) <=> ((~![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(c, inverse(c), identity)) | (~product(inverse(c), c, identity)) | (~product(c, identity, c)) | product(identity, c, c)))),
% 14.11/14.31 inference(monotonicity,[status(thm)],[363])).
% 14.11/14.31 tff(365,plain,
% 14.11/14.31 (((~![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, c, c) | (~product(inverse(c), c, identity)) | (~product(c, inverse(c), identity)) | (~product(c, identity, c)))) <=> ((~![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(c, inverse(c), identity)) | (~product(inverse(c), c, identity)) | (~product(c, identity, c)) | product(identity, c, c))),
% 14.11/14.31 inference(transitivity,[status(thm)],[364, 362])).
% 14.11/14.31 tff(366,plain,
% 14.11/14.31 ((~![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, c, c) | (~product(inverse(c), c, identity)) | (~product(c, inverse(c), identity)) | (~product(c, identity, c)))),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(367,plain,
% 14.11/14.31 ((~![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(c, inverse(c), identity)) | (~product(inverse(c), c, identity)) | (~product(c, identity, c)) | product(identity, c, c)),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[366, 365])).
% 14.11/14.31 tff(368,plain,
% 14.11/14.31 ((~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity)) | product(identity, c, c)),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[367, 217, 250])).
% 14.11/14.31 tff(369,plain,
% 14.11/14.31 (product(identity, c, c)),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[368, 361, 356])).
% 14.11/14.31 tff(370,plain,
% 14.11/14.31 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(a), a, identity)),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(371,plain,
% 14.11/14.31 (product(inverse(a), a, identity)),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[370, 63])).
% 14.11/14.31 tff(372,plain,
% 14.11/14.31 (((~![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(a, c, d)) | (~product(identity, c, c)) | product(inverse(a), d, c))) <=> ((~![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(a, c, d)) | (~product(identity, c, c)) | product(inverse(a), d, c))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(373,plain,
% 14.11/14.31 ((product(inverse(a), d, c) | (~product(identity, c, c)) | (~product(a, c, d)) | (~product(inverse(a), a, identity))) <=> ((~product(inverse(a), a, identity)) | (~product(a, c, d)) | (~product(identity, c, c)) | product(inverse(a), d, c))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(374,plain,
% 14.11/14.31 (((~![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), d, c) | (~product(identity, c, c)) | (~product(a, c, d)) | (~product(inverse(a), a, 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(inverse(a), a, identity)) | (~product(a, c, d)) | (~product(identity, c, c)) | product(inverse(a), d, c)))),
% 14.11/14.31 inference(monotonicity,[status(thm)],[373])).
% 14.11/14.31 tff(375,plain,
% 14.11/14.31 (((~![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), d, c) | (~product(identity, c, c)) | (~product(a, c, d)) | (~product(inverse(a), a, 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(inverse(a), a, identity)) | (~product(a, c, d)) | (~product(identity, c, c)) | product(inverse(a), d, c))),
% 14.11/14.31 inference(transitivity,[status(thm)],[374, 372])).
% 14.11/14.31 tff(376,plain,
% 14.11/14.31 ((~![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), d, c) | (~product(identity, c, c)) | (~product(a, c, d)) | (~product(inverse(a), a, identity)))),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(377,plain,
% 14.11/14.31 ((~![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(a, c, d)) | (~product(identity, c, c)) | product(inverse(a), d, c)),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[376, 375])).
% 14.11/14.31 tff(378,plain,
% 14.11/14.31 (product(inverse(a), d, c)),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[377, 78, 253, 371, 369])).
% 14.11/14.31 tff(379,plain,
% 14.11/14.31 (product(inverse(multiply(element_in_O2(d, d), a)), d, c)),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[378, 350])).
% 14.11/14.31 tff(380,plain,
% 14.11/14.31 (product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a))) <=> product(inverse(a), identity, inverse(a))),
% 14.11/14.31 inference(monotonicity,[status(thm)],[318, 318])).
% 14.11/14.31 tff(381,plain,
% 14.11/14.31 (product(inverse(a), identity, inverse(a)) <=> product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))),
% 14.11/14.31 inference(symmetry,[status(thm)],[380])).
% 14.11/14.31 tff(382,assumption,(~product(inverse(a), identity, inverse(a))), introduced(assumption)).
% 14.11/14.31 tff(383,plain,
% 14.11/14.31 ((~![X: $i] : product(X, identity, X)) | product(inverse(a), identity, inverse(a))),
% 14.11/14.31 inference(quant_inst,[status(thm)],[])).
% 14.11/14.31 tff(384,plain,
% 14.11/14.31 ($false),
% 14.11/14.31 inference(unit_resolution,[status(thm)],[383, 247, 382])).
% 14.11/14.31 tff(385,plain,(product(inverse(a), identity, inverse(a))), inference(lemma,lemma(discharge,[]))).
% 14.11/14.31 tff(386,plain,
% 14.11/14.31 (product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))),
% 14.11/14.31 inference(modus_ponens,[status(thm)],[385, 381])).
% 14.11/14.31 tff(387,plain,
% 14.11/14.31 (((~![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(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | product(c, inverse(d), inverse(multiply(element_in_O2(d, d), 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(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(388,plain,
% 14.11/14.31 ((product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))) | (~product(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a))))) <=> ((~product(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))))),
% 14.11/14.31 inference(rewrite,[status(thm)],[])).
% 14.11/14.31 tff(389,plain,
% 14.11/14.31 (((~![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(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))) | (~product(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), 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(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))))),
% 14.11/14.31 inference(monotonicity,[status(thm)],[388])).
% 14.11/14.31 tff(390,plain,
% 14.11/14.31 (((~![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(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))) | (~product(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), 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(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))))),
% 14.17/14.31 inference(transitivity,[status(thm)],[389, 387])).
% 14.17/14.31 tff(391,plain,
% 14.17/14.31 ((~![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(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))) | (~product(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))))),
% 14.17/14.31 inference(quant_inst,[status(thm)],[])).
% 14.17/14.31 tff(392,plain,
% 14.17/14.31 ((~![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(d, inverse(d), identity)) | (~product(inverse(multiply(element_in_O2(d, d), a)), identity, inverse(multiply(element_in_O2(d, d), a)))) | (~product(inverse(multiply(element_in_O2(d, d), a)), d, c)) | product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))),
% 14.17/14.31 inference(modus_ponens,[status(thm)],[391, 390])).
% 14.17/14.31 tff(393,plain,
% 14.17/14.31 (product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))),
% 14.17/14.31 inference(unit_resolution,[status(thm)],[392, 217, 197, 386, 379])).
% 14.17/14.31 tff(394,plain,
% 14.17/14.31 (product(c, multiply(identity, inverse(c)), identity) <=> product(inverse(inverse(c)), inverse(c), identity)),
% 14.17/14.31 inference(monotonicity,[status(thm)],[351, 50])).
% 14.17/14.31 tff(395,plain,
% 14.17/14.31 (product(inverse(inverse(c)), inverse(c), identity) <=> product(c, multiply(identity, inverse(c)), identity)),
% 14.17/14.31 inference(symmetry,[status(thm)],[394])).
% 14.17/14.31 tff(396,plain,
% 14.17/14.31 (product(c, multiply(identity, inverse(c)), identity)),
% 14.17/14.31 inference(modus_ponens,[status(thm)],[355, 395])).
% 14.17/14.31 tff(397,plain,
% 14.17/14.31 (((~![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(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))) | product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))))) <=> ((~![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(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))) | product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))))),
% 14.17/14.31 inference(rewrite,[status(thm)],[])).
% 14.17/14.31 tff(398,plain,
% 14.17/14.31 ((product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))) | (~product(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a))))) <=> ((~product(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))) | product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))))),
% 14.17/14.31 inference(rewrite,[status(thm)],[])).
% 14.17/14.31 tff(399,plain,
% 14.17/14.31 (((~![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(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))) | (~product(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), 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(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))) | product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)))))),
% 14.17/14.32 inference(monotonicity,[status(thm)],[398])).
% 14.17/14.32 tff(400,plain,
% 14.17/14.32 (((~![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(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))) | (~product(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), 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(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))) | product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))))),
% 14.17/14.32 inference(transitivity,[status(thm)],[399, 397])).
% 14.17/14.32 tff(401,plain,
% 14.17/14.32 ((~![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(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d))) | (~product(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))))),
% 14.17/14.32 inference(quant_inst,[status(thm)],[])).
% 14.17/14.32 tff(402,plain,
% 14.17/14.32 ((~![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(c, multiply(identity, inverse(c)), identity)) | (~product(c, inverse(d), inverse(multiply(element_in_O2(d, d), a)))) | product(identity, inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(multiply(element_in_O2(d, d), a))) | (~product(multiply(identity, inverse(c)), inverse(element_in_O2(inverse(d), multiply(identity, inverse(c)))), inverse(d)))),
% 14.17/14.32 inference(modus_ponens,[status(thm)],[401, 400])).
% 14.17/14.32 tff(403,plain,
% 14.17/14.32 ($false),
% 14.17/14.32 inference(unit_resolution,[status(thm)],[402, 217, 396, 393, 348, 224])).
% 14.17/14.32 % SZS output end Proof
% 14.17/14.32 % E exiting
%------------------------------------------------------------------------------