%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GRP039-4 : 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:55 AM UTC 2025
% Result : Unsatisfiable 15.15s 15.31s
% Output : Proof 15.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : GRP039-4 : TPTP v9.0.0. Released v1.0.0.
% 0.10/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:31:26 EDT 2025
% 0.11/0.32 % CPUTime :
% 15.15/15.31 % SZS status Unsatisfiable
% 15.15/15.31 % SZS output start Proof
% 15.15/15.31 tff(product_type, type, (
% 15.15/15.31 product: ( $i * $i * $i ) > $o)).
% 15.15/15.31 tff(inverse_type, type, (
% 15.15/15.31 inverse: $i > $i)).
% 15.15/15.31 tff(c_type, type, (
% 15.15/15.31 c: $i)).
% 15.15/15.31 tff(identity_type, type, (
% 15.15/15.31 identity: $i)).
% 15.15/15.31 tff(element_in_O2_type, type, (
% 15.15/15.31 element_in_O2: ( $i * $i ) > $i)).
% 15.15/15.31 tff(a_type, type, (
% 15.15/15.31 a: $i)).
% 15.15/15.31 tff(d_type, type, (
% 15.15/15.31 d: $i)).
% 15.15/15.31 tff(multiply_type, type, (
% 15.15/15.31 multiply: ( $i * $i ) > $i)).
% 15.15/15.31 tff(subgroup_member_type, type, (
% 15.15/15.31 subgroup_member: $i > $o)).
% 15.15/15.31 tff(b_type, type, (
% 15.15/15.31 b: $i)).
% 15.15/15.31 tff(1,assumption,(subgroup_member(c)), introduced(assumption)).
% 15.15/15.31 tff(2,plain,
% 15.15/15.31 ((~subgroup_member(d)) <=> (~subgroup_member(d))),
% 15.15/15.31 inference(rewrite,[status(thm)],[])).
% 15.15/15.31 tff(3,axiom,(~subgroup_member(d)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_d_is_in_subgroup')).
% 15.15/15.31 tff(4,plain,
% 15.15/15.31 (~subgroup_member(d)),
% 15.15/15.31 inference(modus_ponens,[status(thm)],[3, 2])).
% 15.15/15.31 tff(5,plain,
% 15.15/15.31 (product(a, c, d) <=> product(a, c, d)),
% 15.15/15.31 inference(rewrite,[status(thm)],[])).
% 15.15/15.31 tff(6,axiom,(product(a, c, d)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a_times_c_is_d')).
% 15.15/15.31 tff(7,plain,
% 15.15/15.31 (product(a, c, d)),
% 15.15/15.31 inference(modus_ponens,[status(thm)],[6, 5])).
% 15.15/15.31 tff(8,plain,
% 15.15/15.31 (^[B: $i, A: $i, C: $i] : refl((subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A))) <=> (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A))))),
% 15.15/15.31 inference(bind,[status(th)],[])).
% 15.15/15.31 tff(9,plain,
% 15.15/15.31 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A))) <=> ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 15.15/15.31 inference(quant_intro,[status(thm)],[8])).
% 15.15/15.31 tff(10,plain,
% 15.15/15.31 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A))) <=> ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 15.15/15.31 inference(rewrite,[status(thm)],[])).
% 15.15/15.31 tff(11,plain,
% 15.15/15.31 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, B, C))) <=> ((~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))), (((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, B, C))) | subgroup_member(C)) <=> (((~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A))) | subgroup_member(C)))), rewrite((((~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A))) | subgroup_member(C)) <=> (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))), (((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, B, C))) | subgroup_member(C)) <=> (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))))),
% 15.15/15.31 inference(bind,[status(th)],[])).
% 15.15/15.31 tff(12,plain,
% 15.15/15.31 (![B: $i, A: $i, C: $i] : ((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, B, C))) | subgroup_member(C)) <=> ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 15.15/15.31 inference(quant_intro,[status(thm)],[11])).
% 15.15/15.31 tff(13,axiom,(![B: $i, A: $i, C: $i] : ((((~subgroup_member(A)) | (~subgroup_member(B))) | (~product(A, B, C))) | subgroup_member(C))), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-1.ax','closure_of_product')).
% 15.15/15.31 tff(14,plain,
% 15.15/15.31 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 15.15/15.31 inference(modus_ponens,[status(thm)],[13, 12])).
% 15.15/15.31 tff(15,plain,
% 15.15/15.31 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 15.15/15.31 inference(modus_ponens,[status(thm)],[14, 10])).
% 15.15/15.31 tff(16,plain,(
% 15.15/15.31 ![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 15.15/15.31 inference(skolemize,[status(sab)],[15])).
% 15.15/15.31 tff(17,plain,
% 15.15/15.31 (![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[16, 9])).
% 15.15/15.32 tff(18,plain,
% 15.15/15.32 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(d) | (~product(a, c, d)) | (~subgroup_member(c)) | (~subgroup_member(a)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(d) | (~product(a, c, d)) | (~subgroup_member(c)) | (~subgroup_member(a)))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(19,plain,
% 15.15/15.32 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(d) | (~product(a, c, d)) | (~subgroup_member(c)) | (~subgroup_member(a)))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(20,plain,
% 15.15/15.32 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(d) | (~product(a, c, d)) | (~subgroup_member(c)) | (~subgroup_member(a))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[19, 18])).
% 15.15/15.32 tff(21,plain,
% 15.15/15.32 ((~subgroup_member(c)) | (~subgroup_member(a))),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[20, 17, 7, 4])).
% 15.15/15.32 tff(22,plain,
% 15.15/15.32 (~subgroup_member(a)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[21, 1])).
% 15.15/15.32 tff(23,plain,
% 15.15/15.32 (^[B: $i, A: $i] : refl((subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B)) <=> (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B)))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(24,plain,
% 15.15/15.32 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B)) <=> ![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[23])).
% 15.15/15.32 tff(25,plain,
% 15.15/15.32 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B)) <=> ![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(26,plain,
% 15.15/15.32 (^[B: $i, A: $i] : trans(monotonicity(rewrite((product(A, element_in_O2(A, B), B) | subgroup_member(B)) <=> (subgroup_member(B) | product(A, element_in_O2(A, B), B))), (((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A)) <=> ((subgroup_member(B) | product(A, element_in_O2(A, B), B)) | subgroup_member(A)))), rewrite(((subgroup_member(B) | product(A, element_in_O2(A, B), B)) | subgroup_member(A)) <=> (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))), (((product(A, element_in_O2(A, B), B) | subgroup_member(B)) | subgroup_member(A)) <=> (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(27,plain,
% 15.15/15.32 (![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) | subgroup_member(B) | product(A, element_in_O2(A, B), B))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[26])).
% 15.15/15.32 tff(28,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')).
% 15.15/15.32 tff(29,plain,
% 15.15/15.32 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[28, 27])).
% 15.15/15.32 tff(30,plain,
% 15.15/15.32 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[29, 25])).
% 15.15/15.32 tff(31,plain,(
% 15.15/15.32 ![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))),
% 15.15/15.32 inference(skolemize,[status(sab)],[30])).
% 15.15/15.32 tff(32,plain,
% 15.15/15.32 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[31, 24])).
% 15.15/15.32 tff(33,plain,
% 15.15/15.32 (((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))) | (subgroup_member(d) | subgroup_member(a) | product(d, element_in_O2(d, a), a))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))) | subgroup_member(d) | subgroup_member(a) | product(d, element_in_O2(d, a), a))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(34,plain,
% 15.15/15.32 ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))) | (subgroup_member(d) | subgroup_member(a) | product(d, element_in_O2(d, a), a))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(35,plain,
% 15.15/15.32 ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(B) | product(A, element_in_O2(A, B), B))) | subgroup_member(d) | subgroup_member(a) | product(d, element_in_O2(d, a), a)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[34, 33])).
% 15.15/15.32 tff(36,plain,
% 15.15/15.32 (subgroup_member(a) | product(d, element_in_O2(d, a), a)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[35, 32, 4])).
% 15.15/15.32 tff(37,plain,
% 15.15/15.32 (product(d, element_in_O2(d, a), a)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[36, 22])).
% 15.15/15.32 tff(38,plain,
% 15.15/15.32 (^[X: $i] : refl(product(identity, X, X) <=> product(identity, X, X))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(39,plain,
% 15.15/15.32 (![X: $i] : product(identity, X, X) <=> ![X: $i] : product(identity, X, X)),
% 15.15/15.32 inference(quant_intro,[status(thm)],[38])).
% 15.15/15.32 tff(40,plain,
% 15.15/15.32 (![X: $i] : product(identity, X, X) <=> ![X: $i] : product(identity, X, X)),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(41,axiom,(![X: $i] : product(identity, X, X)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','left_identity')).
% 15.15/15.32 tff(42,plain,
% 15.15/15.32 (![X: $i] : product(identity, X, X)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[41, 40])).
% 15.15/15.32 tff(43,plain,(
% 15.15/15.32 ![X: $i] : product(identity, X, X)),
% 15.15/15.32 inference(skolemize,[status(sab)],[42])).
% 15.15/15.32 tff(44,plain,
% 15.15/15.32 (![X: $i] : product(identity, X, X)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[43, 39])).
% 15.15/15.32 tff(45,plain,
% 15.15/15.32 ((~![X: $i] : product(identity, X, X)) | product(identity, d, d)),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(46,plain,
% 15.15/15.32 (product(identity, d, d)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[45, 44])).
% 15.15/15.32 tff(47,plain,
% 15.15/15.32 (^[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))))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(48,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[47])).
% 15.15/15.32 tff(49,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(50,plain,
% 15.15/15.32 (^[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)))))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(51,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[50])).
% 15.15/15.32 tff(52,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')).
% 15.15/15.32 tff(53,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[52, 51])).
% 15.15/15.32 tff(54,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[53, 49])).
% 15.15/15.32 tff(55,plain,(
% 15.15/15.32 ![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)))),
% 15.15/15.32 inference(skolemize,[status(sab)],[54])).
% 15.15/15.32 tff(56,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[55, 48])).
% 15.15/15.32 tff(57,plain,
% 15.15/15.32 (((~![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(d, element_in_O2(d, a), a)) | (~product(identity, d, d)) | product(identity, a, 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(d, element_in_O2(d, a), a)) | (~product(identity, d, d)) | product(identity, a, a))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(58,plain,
% 15.15/15.32 ((product(identity, a, a) | (~product(d, element_in_O2(d, a), a)) | (~product(d, element_in_O2(d, a), a)) | (~product(identity, d, d))) <=> ((~product(d, element_in_O2(d, a), a)) | (~product(identity, d, d)) | product(identity, a, a))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(59,plain,
% 15.15/15.32 (((~![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, a, a) | (~product(d, element_in_O2(d, a), a)) | (~product(d, element_in_O2(d, a), a)) | (~product(identity, 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(d, element_in_O2(d, a), a)) | (~product(identity, d, d)) | product(identity, a, a)))),
% 15.15/15.32 inference(monotonicity,[status(thm)],[58])).
% 15.15/15.32 tff(60,plain,
% 15.15/15.32 (((~![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, a, a) | (~product(d, element_in_O2(d, a), a)) | (~product(d, element_in_O2(d, a), a)) | (~product(identity, 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(d, element_in_O2(d, a), a)) | (~product(identity, d, d)) | product(identity, a, a))),
% 15.15/15.32 inference(transitivity,[status(thm)],[59, 57])).
% 15.15/15.32 tff(61,plain,
% 15.15/15.32 ((~![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, a, a) | (~product(d, element_in_O2(d, a), a)) | (~product(d, element_in_O2(d, a), a)) | (~product(identity, d, d)))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(62,plain,
% 15.15/15.32 ((~![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(d, element_in_O2(d, a), a)) | (~product(identity, d, d)) | product(identity, a, a)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[61, 60])).
% 15.15/15.32 tff(63,plain,
% 15.15/15.32 ((~product(d, element_in_O2(d, a), a)) | product(identity, a, a)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[62, 56, 46])).
% 15.15/15.32 tff(64,plain,
% 15.15/15.32 (product(identity, a, a)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[63, 37])).
% 15.15/15.32 tff(65,plain,
% 15.15/15.32 (^[X: $i] : refl(product(inverse(X), X, identity) <=> product(inverse(X), X, identity))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(66,plain,
% 15.15/15.32 (![X: $i] : product(inverse(X), X, identity) <=> ![X: $i] : product(inverse(X), X, identity)),
% 15.15/15.32 inference(quant_intro,[status(thm)],[65])).
% 15.15/15.32 tff(67,plain,
% 15.15/15.32 (![X: $i] : product(inverse(X), X, identity) <=> ![X: $i] : product(inverse(X), X, identity)),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(68,axiom,(![X: $i] : product(inverse(X), X, identity)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','left_inverse')).
% 15.15/15.32 tff(69,plain,
% 15.15/15.32 (![X: $i] : product(inverse(X), X, identity)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[68, 67])).
% 15.15/15.32 tff(70,plain,(
% 15.15/15.32 ![X: $i] : product(inverse(X), X, identity)),
% 15.15/15.32 inference(skolemize,[status(sab)],[69])).
% 15.15/15.32 tff(71,plain,
% 15.15/15.32 (![X: $i] : product(inverse(X), X, identity)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[70, 66])).
% 15.15/15.32 tff(72,plain,
% 15.15/15.32 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(inverse(a)), inverse(a), identity)),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(73,plain,
% 15.15/15.32 (product(inverse(inverse(a)), inverse(a), identity)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[72, 71])).
% 15.15/15.32 tff(74,plain,
% 15.15/15.32 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(a), a, identity)),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(75,plain,
% 15.15/15.32 (product(inverse(a), a, identity)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[74, 71])).
% 15.15/15.32 tff(76,plain,
% 15.15/15.32 (((~![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(identity, a, a)) | (~product(inverse(inverse(a)), inverse(a), identity)) | product(inverse(inverse(a)), identity, a))) <=> ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(inverse(a), a, identity)) | (~product(identity, a, a)) | (~product(inverse(inverse(a)), inverse(a), identity)) | product(inverse(inverse(a)), identity, a))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(77,plain,
% 15.15/15.32 ((product(inverse(inverse(a)), identity, a) | (~product(identity, a, a)) | (~product(inverse(a), a, identity)) | (~product(inverse(inverse(a)), inverse(a), identity))) <=> ((~product(inverse(a), a, identity)) | (~product(identity, a, a)) | (~product(inverse(inverse(a)), inverse(a), identity)) | product(inverse(inverse(a)), identity, a))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(78,plain,
% 15.15/15.32 (((~![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(inverse(a)), identity, a) | (~product(identity, a, a)) | (~product(inverse(a), a, identity)) | (~product(inverse(inverse(a)), inverse(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(identity, a, a)) | (~product(inverse(inverse(a)), inverse(a), identity)) | product(inverse(inverse(a)), identity, a)))),
% 15.15/15.32 inference(monotonicity,[status(thm)],[77])).
% 15.15/15.32 tff(79,plain,
% 15.15/15.32 (((~![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(inverse(a)), identity, a) | (~product(identity, a, a)) | (~product(inverse(a), a, identity)) | (~product(inverse(inverse(a)), inverse(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(identity, a, a)) | (~product(inverse(inverse(a)), inverse(a), identity)) | product(inverse(inverse(a)), identity, a))),
% 15.15/15.32 inference(transitivity,[status(thm)],[78, 76])).
% 15.15/15.32 tff(80,plain,
% 15.15/15.32 ((~![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(inverse(a)), identity, a) | (~product(identity, a, a)) | (~product(inverse(a), a, identity)) | (~product(inverse(inverse(a)), inverse(a), identity)))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(81,plain,
% 15.15/15.32 ((~![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(identity, a, a)) | (~product(inverse(inverse(a)), inverse(a), identity)) | product(inverse(inverse(a)), identity, a)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[80, 79])).
% 15.15/15.32 tff(82,plain,
% 15.15/15.32 ((~product(identity, a, a)) | product(inverse(inverse(a)), identity, a)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[81, 56, 75, 73])).
% 15.15/15.32 tff(83,plain,
% 15.15/15.32 (product(inverse(inverse(a)), identity, a)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[82, 64])).
% 15.15/15.32 tff(84,plain,
% 15.15/15.32 (^[Y: $i, X: $i] : refl(product(X, Y, multiply(X, Y)) <=> product(X, Y, multiply(X, Y)))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(85,plain,
% 15.15/15.32 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y)) <=> ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[84])).
% 15.15/15.32 tff(86,plain,
% 15.15/15.32 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y)) <=> ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(87,axiom,(![Y: $i, X: $i] : product(X, Y, multiply(X, Y))), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','total_function1')).
% 15.15/15.32 tff(88,plain,
% 15.15/15.32 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[87, 86])).
% 15.15/15.32 tff(89,plain,(
% 15.15/15.32 ![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 15.15/15.32 inference(skolemize,[status(sab)],[88])).
% 15.15/15.32 tff(90,plain,
% 15.15/15.32 (![Y: $i, X: $i] : product(X, Y, multiply(X, Y))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[89, 85])).
% 15.15/15.32 tff(91,plain,
% 15.15/15.32 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(identity, inverse(b), multiply(identity, inverse(b)))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(92,plain,
% 15.15/15.32 (product(identity, inverse(b), multiply(identity, inverse(b)))),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[91, 90])).
% 15.15/15.32 tff(93,plain,
% 15.15/15.32 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(b), inverse(b))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(94,plain,
% 15.15/15.32 (product(identity, inverse(b), inverse(b))),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[93, 44])).
% 15.15/15.32 tff(95,plain,
% 15.15/15.32 (^[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))))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(96,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[95])).
% 15.15/15.32 tff(97,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(98,plain,
% 15.15/15.32 (^[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))))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(99,plain,
% 15.15/15.32 (![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)))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[98])).
% 15.15/15.32 tff(100,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')).
% 15.15/15.32 tff(101,plain,
% 15.15/15.32 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[100, 99])).
% 15.15/15.32 tff(102,plain,
% 15.15/15.32 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[101, 97])).
% 15.15/15.32 tff(103,plain,(
% 15.15/15.32 ![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 15.15/15.32 inference(skolemize,[status(sab)],[102])).
% 15.15/15.32 tff(104,plain,
% 15.15/15.32 (![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[103, 96])).
% 15.15/15.32 tff(105,plain,
% 15.15/15.32 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(b) = multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~product(identity, inverse(b), inverse(b))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (inverse(b) = multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~product(identity, inverse(b), inverse(b))))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(106,plain,
% 15.15/15.32 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((inverse(b) = multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~product(identity, inverse(b), inverse(b))))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(107,plain,
% 15.15/15.32 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (inverse(b) = multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~product(identity, inverse(b), inverse(b)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[106, 105])).
% 15.15/15.32 tff(108,plain,
% 15.15/15.32 (inverse(b) = multiply(identity, inverse(b))),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[107, 104, 94, 92])).
% 15.15/15.32 tff(109,plain,
% 15.15/15.32 (multiply(identity, inverse(b)) = inverse(b)),
% 15.15/15.32 inference(symmetry,[status(thm)],[108])).
% 15.15/15.32 tff(110,plain,
% 15.15/15.32 (product(multiply(identity, inverse(b)), b, identity) <=> product(inverse(b), b, identity)),
% 15.15/15.32 inference(monotonicity,[status(thm)],[109])).
% 15.15/15.32 tff(111,plain,
% 15.15/15.32 (product(inverse(b), b, identity) <=> product(multiply(identity, inverse(b)), b, identity)),
% 15.15/15.32 inference(symmetry,[status(thm)],[110])).
% 15.15/15.32 tff(112,plain,
% 15.15/15.32 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(b), b, identity)),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(113,plain,
% 15.15/15.32 (product(inverse(b), b, identity)),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[112, 71])).
% 15.15/15.32 tff(114,plain,
% 15.15/15.32 (product(multiply(identity, inverse(b)), b, identity)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[113, 111])).
% 15.15/15.32 tff(115,plain,
% 15.15/15.32 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(a), inverse(a))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(116,plain,
% 15.15/15.32 (product(identity, inverse(a), inverse(a))),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[115, 44])).
% 15.15/15.32 tff(117,plain,
% 15.15/15.32 (product(b, inverse(a), c) <=> product(b, inverse(a), c)),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(118,axiom,(product(b, inverse(a), c)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','b_times_a_inverse_is_c')).
% 15.15/15.32 tff(119,plain,
% 15.15/15.32 (product(b, inverse(a), c)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[118, 117])).
% 15.15/15.32 tff(120,plain,
% 15.15/15.32 (((~![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(identity, inverse(a), inverse(a))) | (~product(multiply(identity, inverse(b)), b, identity)) | product(multiply(identity, 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(identity, inverse(a), inverse(a))) | (~product(multiply(identity, inverse(b)), b, identity)) | product(multiply(identity, inverse(b)), c, inverse(a)))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(121,plain,
% 15.15/15.32 ((product(multiply(identity, inverse(b)), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(multiply(identity, inverse(b)), b, identity))) <=> ((~product(b, inverse(a), c)) | (~product(identity, inverse(a), inverse(a))) | (~product(multiply(identity, inverse(b)), b, identity)) | product(multiply(identity, inverse(b)), c, inverse(a)))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(122,plain,
% 15.15/15.32 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(identity, inverse(b)), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(multiply(identity, 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(identity, inverse(a), inverse(a))) | (~product(multiply(identity, inverse(b)), b, identity)) | product(multiply(identity, inverse(b)), c, inverse(a))))),
% 15.15/15.32 inference(monotonicity,[status(thm)],[121])).
% 15.15/15.32 tff(123,plain,
% 15.15/15.32 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(identity, inverse(b)), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(multiply(identity, 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(identity, inverse(a), inverse(a))) | (~product(multiply(identity, inverse(b)), b, identity)) | product(multiply(identity, inverse(b)), c, inverse(a)))),
% 15.15/15.32 inference(transitivity,[status(thm)],[122, 120])).
% 15.15/15.32 tff(124,plain,
% 15.15/15.32 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(multiply(identity, inverse(b)), c, inverse(a)) | (~product(identity, inverse(a), inverse(a))) | (~product(b, inverse(a), c)) | (~product(multiply(identity, inverse(b)), b, identity)))),
% 15.15/15.32 inference(quant_inst,[status(thm)],[])).
% 15.15/15.32 tff(125,plain,
% 15.15/15.32 ((~![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(identity, inverse(a), inverse(a))) | (~product(multiply(identity, inverse(b)), b, identity)) | product(multiply(identity, inverse(b)), c, inverse(a))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[124, 123])).
% 15.15/15.32 tff(126,plain,
% 15.15/15.32 ((~product(multiply(identity, inverse(b)), b, identity)) | product(multiply(identity, inverse(b)), c, inverse(a))),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[125, 56, 119, 116])).
% 15.15/15.32 tff(127,plain,
% 15.15/15.32 (product(multiply(identity, inverse(b)), c, inverse(a))),
% 15.15/15.32 inference(unit_resolution,[status(thm)],[126, 114])).
% 15.15/15.32 tff(128,plain,
% 15.15/15.32 (subgroup_member(b) <=> subgroup_member(b)),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(129,axiom,(subgroup_member(b)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','b_is_in_subgroup')).
% 15.15/15.32 tff(130,plain,
% 15.15/15.32 (subgroup_member(b)),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[129, 128])).
% 15.15/15.32 tff(131,plain,
% 15.15/15.32 (^[X: $i] : refl(((~subgroup_member(X)) | subgroup_member(inverse(X))) <=> ((~subgroup_member(X)) | subgroup_member(inverse(X))))),
% 15.15/15.32 inference(bind,[status(th)],[])).
% 15.15/15.32 tff(132,plain,
% 15.15/15.32 (![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X))) <=> ![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))),
% 15.15/15.32 inference(quant_intro,[status(thm)],[131])).
% 15.15/15.32 tff(133,plain,
% 15.15/15.32 (![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X))) <=> ![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))),
% 15.15/15.32 inference(rewrite,[status(thm)],[])).
% 15.15/15.32 tff(134,axiom,(![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-1.ax','closure_of_inverse')).
% 15.15/15.32 tff(135,plain,
% 15.15/15.32 (![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))),
% 15.15/15.32 inference(modus_ponens,[status(thm)],[134, 133])).
% 15.15/15.33 tff(136,plain,(
% 15.15/15.33 ![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))),
% 15.15/15.33 inference(skolemize,[status(sab)],[135])).
% 15.15/15.33 tff(137,plain,
% 15.15/15.33 (![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[136, 132])).
% 15.15/15.33 tff(138,plain,
% 15.15/15.33 (((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(b)) | subgroup_member(inverse(b)))) <=> ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(b)) | subgroup_member(inverse(b)))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(139,plain,
% 15.15/15.33 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(b)) | subgroup_member(inverse(b)))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(140,plain,
% 15.15/15.33 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(b)) | subgroup_member(inverse(b))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[139, 138])).
% 15.15/15.33 tff(141,plain,
% 15.15/15.33 (subgroup_member(inverse(b))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[140, 137, 130])).
% 15.15/15.33 tff(142,plain,
% 15.15/15.33 (subgroup_member(identity) <=> subgroup_member(identity)),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(143,axiom,(subgroup_member(identity)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','identity_is_in_subgroup')).
% 15.15/15.33 tff(144,plain,
% 15.15/15.33 (subgroup_member(identity)),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[143, 142])).
% 15.15/15.33 tff(145,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | ((~subgroup_member(identity)) | (~subgroup_member(inverse(b))) | subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(identity)) | (~subgroup_member(inverse(b))) | subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(146,plain,
% 15.15/15.33 ((subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~subgroup_member(inverse(b))) | (~subgroup_member(identity))) <=> ((~subgroup_member(identity)) | (~subgroup_member(inverse(b))) | subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(147,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~subgroup_member(inverse(b))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | ((~subgroup_member(identity)) | (~subgroup_member(inverse(b))) | subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b))))))),
% 15.15/15.33 inference(monotonicity,[status(thm)],[146])).
% 15.15/15.33 tff(148,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~subgroup_member(inverse(b))) | (~subgroup_member(identity)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(identity)) | (~subgroup_member(inverse(b))) | subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))))),
% 15.15/15.33 inference(transitivity,[status(thm)],[147, 145])).
% 15.15/15.33 tff(149,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b)))) | (~subgroup_member(inverse(b))) | (~subgroup_member(identity)))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(150,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(identity)) | (~subgroup_member(inverse(b))) | subgroup_member(multiply(identity, inverse(b))) | (~product(identity, inverse(b), multiply(identity, inverse(b))))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[149, 148])).
% 15.15/15.33 tff(151,plain,
% 15.15/15.33 (subgroup_member(multiply(identity, inverse(b)))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[150, 17, 144, 141, 92])).
% 15.15/15.33 tff(152,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~subgroup_member(c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(multiply(identity, inverse(b)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(multiply(identity, inverse(b)))))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(153,plain,
% 15.15/15.33 ((subgroup_member(inverse(a)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(c)) | (~subgroup_member(multiply(identity, inverse(b))))) <=> (subgroup_member(inverse(a)) | (~subgroup_member(c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(multiply(identity, inverse(b)))))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(154,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(c)) | (~subgroup_member(multiply(identity, inverse(b)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~subgroup_member(c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(multiply(identity, inverse(b))))))),
% 15.15/15.33 inference(monotonicity,[status(thm)],[153])).
% 15.15/15.33 tff(155,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(c)) | (~subgroup_member(multiply(identity, inverse(b)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(multiply(identity, inverse(b)))))),
% 15.15/15.33 inference(transitivity,[status(thm)],[154, 152])).
% 15.15/15.33 tff(156,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(a)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(c)) | (~subgroup_member(multiply(identity, inverse(b)))))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(157,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(inverse(a)) | (~subgroup_member(c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~subgroup_member(multiply(identity, inverse(b))))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[156, 155])).
% 15.15/15.33 tff(158,plain,
% 15.15/15.33 (subgroup_member(inverse(a)) | (~subgroup_member(c))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[157, 17, 151, 127])).
% 15.15/15.33 tff(159,plain,
% 15.15/15.33 (subgroup_member(inverse(a))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[158, 1])).
% 15.15/15.33 tff(160,plain,
% 15.15/15.33 (((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(inverse(a))) | subgroup_member(inverse(inverse(a))))) <=> ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(inverse(a))) | subgroup_member(inverse(inverse(a))))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(161,plain,
% 15.15/15.33 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(inverse(a))) | subgroup_member(inverse(inverse(a))))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(162,plain,
% 15.15/15.33 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(inverse(a))) | subgroup_member(inverse(inverse(a)))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[161, 160])).
% 15.15/15.33 tff(163,plain,
% 15.15/15.33 ((~subgroup_member(inverse(a))) | subgroup_member(inverse(inverse(a)))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[162, 137])).
% 15.15/15.33 tff(164,plain,
% 15.15/15.33 (subgroup_member(inverse(inverse(a)))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[163, 159])).
% 15.15/15.33 tff(165,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~subgroup_member(identity)) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(inverse(inverse(a)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(a) | (~subgroup_member(identity)) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(inverse(inverse(a)))))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(166,plain,
% 15.15/15.33 ((subgroup_member(a) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(a))))) <=> (subgroup_member(a) | (~subgroup_member(identity)) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(inverse(inverse(a)))))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(167,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(a)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~subgroup_member(identity)) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(inverse(inverse(a))))))),
% 15.15/15.33 inference(monotonicity,[status(thm)],[166])).
% 15.15/15.33 tff(168,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(a)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(a) | (~subgroup_member(identity)) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(inverse(inverse(a)))))),
% 15.15/15.33 inference(transitivity,[status(thm)],[167, 165])).
% 15.15/15.33 tff(169,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(a) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(a)))))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(170,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(a) | (~subgroup_member(identity)) | (~product(inverse(inverse(a)), identity, a)) | (~subgroup_member(inverse(inverse(a))))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[169, 168])).
% 15.15/15.33 tff(171,plain,
% 15.15/15.33 ($false),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[170, 17, 144, 22, 164, 83])).
% 15.15/15.33 tff(172,plain,(~subgroup_member(c)), inference(lemma,lemma(discharge,[]))).
% 15.15/15.33 tff(173,plain,
% 15.15/15.33 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(c) | (~product(b, inverse(a), c)) | (~subgroup_member(inverse(a))) | (~subgroup_member(b)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(c) | (~product(b, inverse(a), c)) | (~subgroup_member(inverse(a))) | (~subgroup_member(b)))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(174,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(c) | (~product(b, inverse(a), c)) | (~subgroup_member(inverse(a))) | (~subgroup_member(b)))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(175,plain,
% 15.15/15.33 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(c) | (~product(b, inverse(a), c)) | (~subgroup_member(inverse(a))) | (~subgroup_member(b))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[174, 173])).
% 15.15/15.33 tff(176,plain,
% 15.15/15.33 (subgroup_member(c) | (~subgroup_member(inverse(a)))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[175, 17, 130, 119])).
% 15.15/15.33 tff(177,plain,
% 15.15/15.33 (~subgroup_member(inverse(a))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[176, 172])).
% 15.15/15.33 tff(178,plain,
% 15.15/15.33 (((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(a)) | subgroup_member(inverse(a)))) <=> ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(a)) | subgroup_member(inverse(a)))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(179,plain,
% 15.15/15.33 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(a)) | subgroup_member(inverse(a)))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(180,plain,
% 15.15/15.33 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(a)) | subgroup_member(inverse(a))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[179, 178])).
% 15.15/15.33 tff(181,plain,
% 15.15/15.33 ((~subgroup_member(a)) | subgroup_member(inverse(a))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[180, 137])).
% 15.15/15.33 tff(182,plain,
% 15.15/15.33 (~subgroup_member(a)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[181, 177])).
% 15.15/15.33 tff(183,plain,
% 15.15/15.33 (product(d, element_in_O2(d, a), a)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[36, 182])).
% 15.15/15.33 tff(184,plain,
% 15.15/15.33 ((~![Y: $i, X: $i] : product(X, Y, multiply(X, Y))) | product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(185,plain,
% 15.15/15.33 (product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[184, 90])).
% 15.15/15.33 tff(186,plain,
% 15.15/15.33 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(a, c, d)) | (~product(d, element_in_O2(d, a), a)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | product(d, multiply(element_in_O2(d, a), c), 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(a, c, d)) | (~product(d, element_in_O2(d, a), a)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | product(d, multiply(element_in_O2(d, a), c), d))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(187,plain,
% 15.15/15.33 ((product(d, multiply(element_in_O2(d, a), c), d) | (~product(a, c, d)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | (~product(d, element_in_O2(d, a), a))) <=> ((~product(a, c, d)) | (~product(d, element_in_O2(d, a), a)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | product(d, multiply(element_in_O2(d, a), c), d))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(188,plain,
% 15.15/15.33 (((~![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(d, multiply(element_in_O2(d, a), c), d) | (~product(a, c, d)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | (~product(d, element_in_O2(d, a), 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(a, c, d)) | (~product(d, element_in_O2(d, a), a)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | product(d, multiply(element_in_O2(d, a), c), d)))),
% 15.15/15.33 inference(monotonicity,[status(thm)],[187])).
% 15.15/15.33 tff(189,plain,
% 15.15/15.33 (((~![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(d, multiply(element_in_O2(d, a), c), d) | (~product(a, c, d)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | (~product(d, element_in_O2(d, a), 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(a, c, d)) | (~product(d, element_in_O2(d, a), a)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | product(d, multiply(element_in_O2(d, a), c), d))),
% 15.15/15.33 inference(transitivity,[status(thm)],[188, 186])).
% 15.15/15.33 tff(190,plain,
% 15.15/15.33 ((~![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(d, multiply(element_in_O2(d, a), c), d) | (~product(a, c, d)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | (~product(d, element_in_O2(d, a), a)))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(191,plain,
% 15.15/15.33 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, c, d)) | (~product(d, element_in_O2(d, a), a)) | (~product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))) | product(d, multiply(element_in_O2(d, a), c), d)),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[190, 189])).
% 15.15/15.33 tff(192,plain,
% 15.15/15.33 ((~product(d, element_in_O2(d, a), a)) | product(d, multiply(element_in_O2(d, a), c), d)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[191, 56, 7, 185])).
% 15.15/15.33 tff(193,plain,
% 15.15/15.33 (product(d, multiply(element_in_O2(d, a), c), d)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[192, 183])).
% 15.15/15.33 tff(194,plain,
% 15.15/15.33 (^[X: $i] : refl(product(X, inverse(X), identity) <=> product(X, inverse(X), identity))),
% 15.15/15.33 inference(bind,[status(th)],[])).
% 15.15/15.33 tff(195,plain,
% 15.15/15.33 (![X: $i] : product(X, inverse(X), identity) <=> ![X: $i] : product(X, inverse(X), identity)),
% 15.15/15.33 inference(quant_intro,[status(thm)],[194])).
% 15.15/15.33 tff(196,plain,
% 15.15/15.33 (![X: $i] : product(X, inverse(X), identity) <=> ![X: $i] : product(X, inverse(X), identity)),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(197,axiom,(![X: $i] : product(X, inverse(X), identity)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','right_inverse')).
% 15.15/15.33 tff(198,plain,
% 15.15/15.33 (![X: $i] : product(X, inverse(X), identity)),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[197, 196])).
% 15.15/15.33 tff(199,plain,(
% 15.15/15.33 ![X: $i] : product(X, inverse(X), identity)),
% 15.15/15.33 inference(skolemize,[status(sab)],[198])).
% 15.15/15.33 tff(200,plain,
% 15.15/15.33 (![X: $i] : product(X, inverse(X), identity)),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[199, 195])).
% 15.15/15.33 tff(201,plain,
% 15.15/15.33 ((~![X: $i] : product(X, inverse(X), identity)) | product(c, inverse(c), identity)),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(202,plain,
% 15.15/15.33 (product(c, inverse(c), identity)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[201, 200])).
% 15.15/15.33 tff(203,plain,
% 15.15/15.33 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(c), c, identity)),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(204,plain,
% 15.15/15.33 (product(inverse(c), c, identity)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[203, 71])).
% 15.15/15.33 tff(205,plain,
% 15.15/15.33 (^[X: $i] : refl(product(X, identity, X) <=> product(X, identity, X))),
% 15.15/15.33 inference(bind,[status(th)],[])).
% 15.15/15.33 tff(206,plain,
% 15.15/15.33 (![X: $i] : product(X, identity, X) <=> ![X: $i] : product(X, identity, X)),
% 15.15/15.33 inference(quant_intro,[status(thm)],[205])).
% 15.15/15.33 tff(207,plain,
% 15.15/15.33 (![X: $i] : product(X, identity, X) <=> ![X: $i] : product(X, identity, X)),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(208,axiom,(![X: $i] : product(X, identity, X)), file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax','right_identity')).
% 15.15/15.33 tff(209,plain,
% 15.15/15.33 (![X: $i] : product(X, identity, X)),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[208, 207])).
% 15.15/15.33 tff(210,plain,(
% 15.15/15.33 ![X: $i] : product(X, identity, X)),
% 15.15/15.33 inference(skolemize,[status(sab)],[209])).
% 15.15/15.33 tff(211,plain,
% 15.15/15.33 (![X: $i] : product(X, identity, X)),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[210, 206])).
% 15.15/15.33 tff(212,plain,
% 15.15/15.33 ((~![X: $i] : product(X, identity, X)) | product(c, identity, c)),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(213,plain,
% 15.15/15.33 (product(c, identity, c)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[212, 211])).
% 15.15/15.33 tff(214,plain,
% 15.15/15.33 (^[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))))),
% 15.15/15.33 inference(bind,[status(th)],[])).
% 15.15/15.33 tff(215,plain,
% 15.15/15.33 (![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)))),
% 15.15/15.33 inference(quant_intro,[status(thm)],[214])).
% 15.15/15.33 tff(216,plain,
% 15.15/15.33 (![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)))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(217,plain,
% 15.15/15.33 (^[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)))))),
% 15.15/15.33 inference(bind,[status(th)],[])).
% 15.15/15.33 tff(218,plain,
% 15.15/15.33 (![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)))),
% 15.15/15.33 inference(quant_intro,[status(thm)],[217])).
% 15.15/15.33 tff(219,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')).
% 15.15/15.33 tff(220,plain,
% 15.15/15.33 (![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)))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[219, 218])).
% 15.15/15.33 tff(221,plain,
% 15.15/15.33 (![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)))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[220, 216])).
% 15.15/15.33 tff(222,plain,(
% 15.15/15.33 ![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)))),
% 15.15/15.33 inference(skolemize,[status(sab)],[221])).
% 15.15/15.33 tff(223,plain,
% 15.15/15.33 (![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)))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[222, 215])).
% 15.15/15.33 tff(224,plain,
% 15.15/15.33 (((~![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, identity, c)) | product(identity, c, c) | (~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity)))) <=> ((~![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, identity, c)) | product(identity, c, c) | (~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity)))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(225,plain,
% 15.15/15.33 ((product(identity, c, c) | (~product(inverse(c), c, identity)) | (~product(c, inverse(c), identity)) | (~product(c, identity, c))) <=> ((~product(c, identity, c)) | product(identity, c, c) | (~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity)))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(226,plain,
% 15.15/15.33 (((~![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, identity, c)) | product(identity, c, c) | (~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity))))),
% 15.15/15.33 inference(monotonicity,[status(thm)],[225])).
% 15.15/15.33 tff(227,plain,
% 15.15/15.33 (((~![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, identity, c)) | product(identity, c, c) | (~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity)))),
% 15.15/15.33 inference(transitivity,[status(thm)],[226, 224])).
% 15.15/15.33 tff(228,plain,
% 15.15/15.33 ((~![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)))),
% 15.15/15.33 inference(quant_inst,[status(thm)],[])).
% 15.15/15.33 tff(229,plain,
% 15.15/15.33 ((~![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, identity, c)) | product(identity, c, c) | (~product(c, inverse(c), identity)) | (~product(inverse(c), c, identity))),
% 15.15/15.33 inference(modus_ponens,[status(thm)],[228, 227])).
% 15.15/15.33 tff(230,plain,
% 15.15/15.33 (product(identity, c, c)),
% 15.15/15.33 inference(unit_resolution,[status(thm)],[229, 223, 213, 204, 202])).
% 15.15/15.33 tff(231,plain,
% 15.15/15.33 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(a, c, d)) | (~product(inverse(a), a, identity)) | (~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(a, c, d)) | (~product(inverse(a), a, identity)) | (~product(identity, c, c)) | product(inverse(a), d, c))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(232,plain,
% 15.15/15.33 ((product(inverse(a), d, c) | (~product(identity, c, c)) | (~product(a, c, d)) | (~product(inverse(a), a, identity))) <=> ((~product(a, c, d)) | (~product(inverse(a), a, identity)) | (~product(identity, c, c)) | product(inverse(a), d, c))),
% 15.15/15.33 inference(rewrite,[status(thm)],[])).
% 15.15/15.33 tff(233,plain,
% 15.15/15.33 (((~![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(a, c, d)) | (~product(inverse(a), a, identity)) | (~product(identity, c, c)) | product(inverse(a), d, c)))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[232])).
% 15.15/15.34 tff(234,plain,
% 15.15/15.34 (((~![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(a, c, d)) | (~product(inverse(a), a, identity)) | (~product(identity, c, c)) | product(inverse(a), d, c))),
% 15.15/15.34 inference(transitivity,[status(thm)],[233, 231])).
% 15.15/15.34 tff(235,plain,
% 15.15/15.34 ((~![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)))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(236,plain,
% 15.15/15.34 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, c, d)) | (~product(inverse(a), a, identity)) | (~product(identity, c, c)) | product(inverse(a), d, c)),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[235, 234])).
% 15.15/15.34 tff(237,plain,
% 15.15/15.34 (product(inverse(a), d, c)),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[236, 56, 7, 75, 230])).
% 15.15/15.34 tff(238,plain,
% 15.15/15.34 (((~![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(a), d, c)) | product(c, multiply(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, 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(inverse(a), d, c)) | product(c, multiply(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(239,plain,
% 15.15/15.34 ((product(c, multiply(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d)) | (~product(inverse(a), d, c)) | (~product(inverse(a), d, c))) <=> ((~product(inverse(a), d, c)) | product(c, multiply(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(240,plain,
% 15.15/15.34 (((~![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(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d)) | (~product(inverse(a), d, c)) | (~product(inverse(a), d, 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(inverse(a), d, c)) | product(c, multiply(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d))))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[239])).
% 15.15/15.34 tff(241,plain,
% 15.15/15.34 (((~![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(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d)) | (~product(inverse(a), d, c)) | (~product(inverse(a), d, 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(inverse(a), d, c)) | product(c, multiply(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d)))),
% 15.15/15.34 inference(transitivity,[status(thm)],[240, 238])).
% 15.15/15.34 tff(242,plain,
% 15.15/15.34 ((~![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(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d)) | (~product(inverse(a), d, c)) | (~product(inverse(a), d, c)))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(243,plain,
% 15.15/15.34 ((~![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(a), d, c)) | product(c, multiply(element_in_O2(d, a), c), c) | (~product(d, multiply(element_in_O2(d, a), c), d))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[242, 241])).
% 15.15/15.34 tff(244,plain,
% 15.15/15.34 (product(c, multiply(element_in_O2(d, a), c), c)),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[243, 223, 237, 193])).
% 15.15/15.34 tff(245,plain,
% 15.15/15.34 (((~![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(b)), c, inverse(a))) | (~product(c, multiply(element_in_O2(d, a), c), c)) | product(inverse(a), multiply(element_in_O2(d, a), c), inverse(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(multiply(identity, inverse(b)), c, inverse(a))) | (~product(c, multiply(element_in_O2(d, a), c), c)) | product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(246,plain,
% 15.15/15.34 ((product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a)) | (~product(c, multiply(element_in_O2(d, a), c), c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~product(multiply(identity, inverse(b)), c, inverse(a)))) <=> ((~product(multiply(identity, inverse(b)), c, inverse(a))) | (~product(c, multiply(element_in_O2(d, a), c), c)) | product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(247,plain,
% 15.15/15.34 (((~![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(a), multiply(element_in_O2(d, a), c), inverse(a)) | (~product(c, multiply(element_in_O2(d, a), c), c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~product(multiply(identity, inverse(b)), c, inverse(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(multiply(identity, inverse(b)), c, inverse(a))) | (~product(c, multiply(element_in_O2(d, a), c), c)) | product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[246])).
% 15.15/15.34 tff(248,plain,
% 15.15/15.34 (((~![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(a), multiply(element_in_O2(d, a), c), inverse(a)) | (~product(c, multiply(element_in_O2(d, a), c), c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~product(multiply(identity, inverse(b)), c, inverse(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(multiply(identity, inverse(b)), c, inverse(a))) | (~product(c, multiply(element_in_O2(d, a), c), c)) | product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a)))),
% 15.15/15.34 inference(transitivity,[status(thm)],[247, 245])).
% 15.15/15.34 tff(249,plain,
% 15.15/15.34 ((~![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(a), multiply(element_in_O2(d, a), c), inverse(a)) | (~product(c, multiply(element_in_O2(d, a), c), c)) | (~product(multiply(identity, inverse(b)), c, inverse(a))) | (~product(multiply(identity, inverse(b)), c, inverse(a))))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(250,plain,
% 15.15/15.34 ((~![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(b)), c, inverse(a))) | (~product(c, multiply(element_in_O2(d, a), c), c)) | product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[249, 248])).
% 15.15/15.34 tff(251,plain,
% 15.15/15.34 (product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[250, 223, 127, 244])).
% 15.15/15.34 tff(252,plain,
% 15.15/15.34 ((~![X: $i] : product(identity, X, X)) | product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(253,plain,
% 15.15/15.34 (product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[252, 44])).
% 15.15/15.34 tff(254,plain,
% 15.15/15.34 ((~![X: $i] : product(X, inverse(X), identity)) | product(a, inverse(a), identity)),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(255,plain,
% 15.15/15.34 (product(a, inverse(a), identity)),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[254, 200])).
% 15.15/15.34 tff(256,plain,
% 15.15/15.34 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | ((~product(a, inverse(a), identity)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(inverse(a), multiply(element_in_O2(d, a), 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(a, inverse(a), identity)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(257,plain,
% 15.15/15.34 ((product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))) | (~product(a, inverse(a), identity))) <=> ((~product(a, inverse(a), identity)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(258,plain,
% 15.15/15.34 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))) | (~product(a, inverse(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(a, inverse(a), identity)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a)))))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[257])).
% 15.15/15.34 tff(259,plain,
% 15.15/15.34 (((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))) | (~product(a, inverse(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(a, inverse(a), identity)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))))),
% 15.15/15.34 inference(transitivity,[status(thm)],[258, 256])).
% 15.15/15.34 tff(260,plain,
% 15.15/15.34 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a))) | (~product(a, inverse(a), identity)))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(261,plain,
% 15.15/15.34 ((~![W: $i, V: $i, Z: $i, Y: $i, U: $i, X: $i] : (product(X, V, W) | (~product(U, Z, W)) | (~product(Y, Z, V)) | (~product(X, Y, U)))) | (~product(a, inverse(a), identity)) | (~product(identity, multiply(element_in_O2(d, a), c), multiply(element_in_O2(d, a), c))) | product(a, inverse(a), multiply(element_in_O2(d, a), c)) | (~product(inverse(a), multiply(element_in_O2(d, a), c), inverse(a)))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[260, 259])).
% 15.15/15.34 tff(262,plain,
% 15.15/15.34 (product(a, inverse(a), multiply(element_in_O2(d, a), c))),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[261, 56, 255, 253, 251])).
% 15.15/15.34 tff(263,plain,
% 15.15/15.34 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((~product(a, inverse(a), identity)) | (multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(a, inverse(a), identity)) | (multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c))))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(264,plain,
% 15.15/15.34 (((multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), identity)) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c)))) <=> ((~product(a, inverse(a), identity)) | (multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c))))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(265,plain,
% 15.15/15.34 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), identity)) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((~product(a, inverse(a), identity)) | (multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c)))))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[264])).
% 15.15/15.34 tff(266,plain,
% 15.15/15.34 (((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), identity)) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c))))) <=> ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(a, inverse(a), identity)) | (multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c))))),
% 15.15/15.34 inference(transitivity,[status(thm)],[265, 263])).
% 15.15/15.34 tff(267,plain,
% 15.15/15.34 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | ((multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), identity)) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c))))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(268,plain,
% 15.15/15.34 ((~![W: $i, Z: $i, Y: $i, X: $i] : ((Z = W) | (~product(X, Y, W)) | (~product(X, Y, Z)))) | (~product(a, inverse(a), identity)) | (multiply(element_in_O2(d, a), c) = identity) | (~product(a, inverse(a), multiply(element_in_O2(d, a), c)))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[267, 266])).
% 15.15/15.34 tff(269,plain,
% 15.15/15.34 (multiply(element_in_O2(d, a), c) = identity),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[268, 104, 255, 262])).
% 15.15/15.34 tff(270,plain,
% 15.15/15.34 (identity = multiply(element_in_O2(d, a), c)),
% 15.15/15.34 inference(symmetry,[status(thm)],[269])).
% 15.15/15.34 tff(271,plain,
% 15.15/15.34 (product(element_in_O2(d, a), c, identity) <=> product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[270])).
% 15.15/15.34 tff(272,plain,
% 15.15/15.34 (product(element_in_O2(d, a), c, multiply(element_in_O2(d, a), c)) <=> product(element_in_O2(d, a), c, identity)),
% 15.15/15.34 inference(symmetry,[status(thm)],[271])).
% 15.15/15.34 tff(273,plain,
% 15.15/15.34 (product(element_in_O2(d, a), c, identity)),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[185, 272])).
% 15.15/15.34 tff(274,plain,
% 15.15/15.34 ((~![X: $i] : product(identity, X, X)) | product(identity, inverse(c), inverse(c))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(275,plain,
% 15.15/15.34 (product(identity, inverse(c), inverse(c))),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[274, 44])).
% 15.15/15.34 tff(276,plain,
% 15.15/15.34 (((~![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(c, inverse(c), identity)) | (~product(identity, inverse(c), inverse(c))) | (~product(element_in_O2(d, a), c, identity)) | product(element_in_O2(d, a), identity, inverse(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(c, inverse(c), identity)) | (~product(identity, inverse(c), inverse(c))) | (~product(element_in_O2(d, a), c, identity)) | product(element_in_O2(d, a), identity, inverse(c)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(277,plain,
% 15.15/15.34 ((product(element_in_O2(d, a), identity, inverse(c)) | (~product(identity, inverse(c), inverse(c))) | (~product(c, inverse(c), identity)) | (~product(element_in_O2(d, a), c, identity))) <=> ((~product(c, inverse(c), identity)) | (~product(identity, inverse(c), inverse(c))) | (~product(element_in_O2(d, a), c, identity)) | product(element_in_O2(d, a), identity, inverse(c)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(278,plain,
% 15.15/15.34 (((~![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(element_in_O2(d, a), identity, inverse(c)) | (~product(identity, inverse(c), inverse(c))) | (~product(c, inverse(c), identity)) | (~product(element_in_O2(d, a), c, 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(c, inverse(c), identity)) | (~product(identity, inverse(c), inverse(c))) | (~product(element_in_O2(d, a), c, identity)) | product(element_in_O2(d, a), identity, inverse(c))))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[277])).
% 15.15/15.34 tff(279,plain,
% 15.15/15.34 (((~![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(element_in_O2(d, a), identity, inverse(c)) | (~product(identity, inverse(c), inverse(c))) | (~product(c, inverse(c), identity)) | (~product(element_in_O2(d, a), c, 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(c, inverse(c), identity)) | (~product(identity, inverse(c), inverse(c))) | (~product(element_in_O2(d, a), c, identity)) | product(element_in_O2(d, a), identity, inverse(c)))),
% 15.15/15.34 inference(transitivity,[status(thm)],[278, 276])).
% 15.15/15.34 tff(280,plain,
% 15.15/15.34 ((~![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(element_in_O2(d, a), identity, inverse(c)) | (~product(identity, inverse(c), inverse(c))) | (~product(c, inverse(c), identity)) | (~product(element_in_O2(d, a), c, identity)))),
% 15.15/15.34 inference(quant_inst,[status(thm)],[])).
% 15.15/15.34 tff(281,plain,
% 15.15/15.34 ((~![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(c, inverse(c), identity)) | (~product(identity, inverse(c), inverse(c))) | (~product(element_in_O2(d, a), c, identity)) | product(element_in_O2(d, a), identity, inverse(c))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[280, 279])).
% 15.15/15.34 tff(282,plain,
% 15.15/15.34 (product(element_in_O2(d, a), identity, inverse(c))),
% 15.15/15.34 inference(unit_resolution,[status(thm)],[281, 56, 202, 275, 273])).
% 15.15/15.34 tff(283,plain,
% 15.15/15.34 (^[B: $i, A: $i] : refl((subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) <=> (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B)))),
% 15.15/15.34 inference(bind,[status(th)],[])).
% 15.15/15.34 tff(284,plain,
% 15.15/15.34 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) <=> ![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))),
% 15.15/15.34 inference(quant_intro,[status(thm)],[283])).
% 15.15/15.34 tff(285,plain,
% 15.15/15.34 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) <=> ![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(286,plain,
% 15.15/15.34 (^[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(A) | 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(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))))),
% 15.15/15.34 inference(bind,[status(th)],[])).
% 15.15/15.34 tff(287,plain,
% 15.15/15.34 (![B: $i, A: $i] : ((subgroup_member(element_in_O2(A, B)) | subgroup_member(B)) | subgroup_member(A)) <=> ![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))),
% 15.15/15.34 inference(quant_intro,[status(thm)],[286])).
% 15.15/15.34 tff(288,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')).
% 15.15/15.34 tff(289,plain,
% 15.15/15.34 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[288, 287])).
% 15.15/15.34 tff(290,plain,
% 15.15/15.34 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[289, 285])).
% 15.15/15.34 tff(291,plain,(
% 15.15/15.34 ![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))),
% 15.15/15.34 inference(skolemize,[status(sab)],[290])).
% 15.15/15.34 tff(292,plain,
% 15.15/15.34 (![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))),
% 15.15/15.34 inference(modus_ponens,[status(thm)],[291, 284])).
% 15.15/15.34 tff(293,plain,
% 15.15/15.34 (((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | (subgroup_member(d) | subgroup_member(a) | subgroup_member(element_in_O2(d, a)))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | subgroup_member(d) | subgroup_member(a) | subgroup_member(element_in_O2(d, a)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(294,plain,
% 15.15/15.34 ((subgroup_member(d) | subgroup_member(element_in_O2(d, a)) | subgroup_member(a)) <=> (subgroup_member(d) | subgroup_member(a) | subgroup_member(element_in_O2(d, a)))),
% 15.15/15.34 inference(rewrite,[status(thm)],[])).
% 15.15/15.34 tff(295,plain,
% 15.15/15.34 (((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | (subgroup_member(d) | subgroup_member(element_in_O2(d, a)) | subgroup_member(a))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | (subgroup_member(d) | subgroup_member(a) | subgroup_member(element_in_O2(d, a))))),
% 15.15/15.34 inference(monotonicity,[status(thm)],[294])).
% 15.15/15.34 tff(296,plain,
% 15.15/15.34 (((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | (subgroup_member(d) | subgroup_member(element_in_O2(d, a)) | subgroup_member(a))) <=> ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | subgroup_member(d) | subgroup_member(a) | subgroup_member(element_in_O2(d, a)))),
% 15.15/15.35 inference(transitivity,[status(thm)],[295, 293])).
% 15.15/15.35 tff(297,plain,
% 15.15/15.35 ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | (subgroup_member(d) | subgroup_member(element_in_O2(d, a)) | subgroup_member(a))),
% 15.15/15.35 inference(quant_inst,[status(thm)],[])).
% 15.15/15.35 tff(298,plain,
% 15.15/15.35 ((~![B: $i, A: $i] : (subgroup_member(A) | subgroup_member(element_in_O2(A, B)) | subgroup_member(B))) | subgroup_member(d) | subgroup_member(a) | subgroup_member(element_in_O2(d, a))),
% 15.15/15.35 inference(modus_ponens,[status(thm)],[297, 296])).
% 15.15/15.35 tff(299,plain,
% 15.15/15.35 (subgroup_member(a) | subgroup_member(element_in_O2(d, a))),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[298, 292, 4])).
% 15.15/15.35 tff(300,plain,
% 15.15/15.35 (subgroup_member(element_in_O2(d, a))),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[299, 182])).
% 15.15/15.35 tff(301,plain,
% 15.15/15.35 ((~![X: $i] : product(inverse(X), X, identity)) | product(inverse(inverse(c)), inverse(c), identity)),
% 15.15/15.35 inference(quant_inst,[status(thm)],[])).
% 15.15/15.35 tff(302,plain,
% 15.15/15.35 (product(inverse(inverse(c)), inverse(c), identity)),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[301, 71])).
% 15.15/15.35 tff(303,plain,
% 15.15/15.35 (((~![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(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity)) | (~product(identity, c, c)) | product(inverse(inverse(c)), identity, 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(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity)) | (~product(identity, c, c)) | product(inverse(inverse(c)), identity, c))),
% 15.15/15.35 inference(rewrite,[status(thm)],[])).
% 15.15/15.35 tff(304,plain,
% 15.15/15.35 ((product(inverse(inverse(c)), identity, c) | (~product(identity, c, c)) | (~product(inverse(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity))) <=> ((~product(inverse(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity)) | (~product(identity, c, c)) | product(inverse(inverse(c)), identity, c))),
% 15.15/15.35 inference(rewrite,[status(thm)],[])).
% 15.15/15.35 tff(305,plain,
% 15.15/15.35 (((~![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(inverse(c)), identity, c) | (~product(identity, c, c)) | (~product(inverse(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), 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(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity)) | (~product(identity, c, c)) | product(inverse(inverse(c)), identity, c)))),
% 15.15/15.35 inference(monotonicity,[status(thm)],[304])).
% 15.15/15.35 tff(306,plain,
% 15.15/15.35 (((~![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(inverse(c)), identity, c) | (~product(identity, c, c)) | (~product(inverse(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), 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(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity)) | (~product(identity, c, c)) | product(inverse(inverse(c)), identity, c))),
% 15.15/15.35 inference(transitivity,[status(thm)],[305, 303])).
% 15.15/15.35 tff(307,plain,
% 15.15/15.35 ((~![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(inverse(c)), identity, c) | (~product(identity, c, c)) | (~product(inverse(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity)))),
% 15.15/15.35 inference(quant_inst,[status(thm)],[])).
% 15.15/15.35 tff(308,plain,
% 15.15/15.35 ((~![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(c), c, identity)) | (~product(inverse(inverse(c)), inverse(c), identity)) | (~product(identity, c, c)) | product(inverse(inverse(c)), identity, c)),
% 15.15/15.35 inference(modus_ponens,[status(thm)],[307, 306])).
% 15.15/15.35 tff(309,plain,
% 15.15/15.35 (product(inverse(inverse(c)), identity, c)),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[308, 56, 204, 302, 230])).
% 15.15/15.35 tff(310,plain,
% 15.15/15.35 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(c) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))) | (~product(inverse(inverse(c)), identity, c)))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(c) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))) | (~product(inverse(inverse(c)), identity, c)))),
% 15.15/15.35 inference(rewrite,[status(thm)],[])).
% 15.15/15.35 tff(311,plain,
% 15.15/15.35 ((subgroup_member(c) | (~product(inverse(inverse(c)), identity, c)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c))))) <=> (subgroup_member(c) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))) | (~product(inverse(inverse(c)), identity, c)))),
% 15.15/15.35 inference(rewrite,[status(thm)],[])).
% 15.15/15.35 tff(312,plain,
% 15.15/15.35 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(c) | (~product(inverse(inverse(c)), identity, c)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(c) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))) | (~product(inverse(inverse(c)), identity, c))))),
% 15.15/15.35 inference(monotonicity,[status(thm)],[311])).
% 15.15/15.35 tff(313,plain,
% 15.15/15.35 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(c) | (~product(inverse(inverse(c)), identity, c)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(c) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))) | (~product(inverse(inverse(c)), identity, c)))),
% 15.15/15.35 inference(transitivity,[status(thm)],[312, 310])).
% 15.15/15.35 tff(314,plain,
% 15.15/15.35 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(c) | (~product(inverse(inverse(c)), identity, c)) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))))),
% 15.15/15.35 inference(quant_inst,[status(thm)],[])).
% 15.15/15.35 tff(315,plain,
% 15.15/15.35 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | subgroup_member(c) | (~subgroup_member(identity)) | (~subgroup_member(inverse(inverse(c)))) | (~product(inverse(inverse(c)), identity, c))),
% 15.15/15.35 inference(modus_ponens,[status(thm)],[314, 313])).
% 15.15/15.35 tff(316,plain,
% 15.15/15.35 (subgroup_member(c) | (~subgroup_member(inverse(inverse(c))))),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[315, 17, 144, 309])).
% 15.15/15.35 tff(317,plain,
% 15.15/15.35 (~subgroup_member(inverse(inverse(c)))),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[316, 172])).
% 15.15/15.35 tff(318,plain,
% 15.15/15.35 (((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(inverse(c))) | subgroup_member(inverse(inverse(c))))) <=> ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(inverse(c))) | subgroup_member(inverse(inverse(c))))),
% 15.15/15.35 inference(rewrite,[status(thm)],[])).
% 15.15/15.35 tff(319,plain,
% 15.15/15.35 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | ((~subgroup_member(inverse(c))) | subgroup_member(inverse(inverse(c))))),
% 15.15/15.35 inference(quant_inst,[status(thm)],[])).
% 15.15/15.35 tff(320,plain,
% 15.15/15.35 ((~![X: $i] : ((~subgroup_member(X)) | subgroup_member(inverse(X)))) | (~subgroup_member(inverse(c))) | subgroup_member(inverse(inverse(c)))),
% 15.15/15.35 inference(modus_ponens,[status(thm)],[319, 318])).
% 15.15/15.35 tff(321,plain,
% 15.15/15.35 ((~subgroup_member(inverse(c))) | subgroup_member(inverse(inverse(c)))),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[320, 137])).
% 15.15/15.35 tff(322,plain,
% 15.15/15.35 (~subgroup_member(inverse(c))),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[321, 317])).
% 15.15/15.35 tff(323,plain,
% 15.15/15.35 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | ((~subgroup_member(identity)) | subgroup_member(inverse(c)) | (~subgroup_member(element_in_O2(d, a))) | (~product(element_in_O2(d, a), identity, inverse(c))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(identity)) | subgroup_member(inverse(c)) | (~subgroup_member(element_in_O2(d, a))) | (~product(element_in_O2(d, a), identity, inverse(c))))),
% 15.15/15.35 inference(rewrite,[status(thm)],[])).
% 15.15/15.35 tff(324,plain,
% 15.15/15.35 ((subgroup_member(inverse(c)) | (~product(element_in_O2(d, a), identity, inverse(c))) | (~subgroup_member(identity)) | (~subgroup_member(element_in_O2(d, a)))) <=> ((~subgroup_member(identity)) | subgroup_member(inverse(c)) | (~subgroup_member(element_in_O2(d, a))) | (~product(element_in_O2(d, a), identity, inverse(c))))),
% 15.15/15.35 inference(rewrite,[status(thm)],[])).
% 15.15/15.35 tff(325,plain,
% 15.15/15.35 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(c)) | (~product(element_in_O2(d, a), identity, inverse(c))) | (~subgroup_member(identity)) | (~subgroup_member(element_in_O2(d, a))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | ((~subgroup_member(identity)) | subgroup_member(inverse(c)) | (~subgroup_member(element_in_O2(d, a))) | (~product(element_in_O2(d, a), identity, inverse(c)))))),
% 15.15/15.35 inference(monotonicity,[status(thm)],[324])).
% 15.15/15.35 tff(326,plain,
% 15.15/15.35 (((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(c)) | (~product(element_in_O2(d, a), identity, inverse(c))) | (~subgroup_member(identity)) | (~subgroup_member(element_in_O2(d, a))))) <=> ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(identity)) | subgroup_member(inverse(c)) | (~subgroup_member(element_in_O2(d, a))) | (~product(element_in_O2(d, a), identity, inverse(c))))),
% 15.15/15.35 inference(transitivity,[status(thm)],[325, 323])).
% 15.15/15.35 tff(327,plain,
% 15.15/15.35 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (subgroup_member(inverse(c)) | (~product(element_in_O2(d, a), identity, inverse(c))) | (~subgroup_member(identity)) | (~subgroup_member(element_in_O2(d, a))))),
% 15.15/15.35 inference(quant_inst,[status(thm)],[])).
% 15.15/15.35 tff(328,plain,
% 15.15/15.35 ((~![B: $i, A: $i, C: $i] : (subgroup_member(C) | (~product(A, B, C)) | (~subgroup_member(B)) | (~subgroup_member(A)))) | (~subgroup_member(identity)) | subgroup_member(inverse(c)) | (~subgroup_member(element_in_O2(d, a))) | (~product(element_in_O2(d, a), identity, inverse(c)))),
% 15.15/15.35 inference(modus_ponens,[status(thm)],[327, 326])).
% 15.15/15.35 tff(329,plain,
% 15.15/15.35 ($false),
% 15.15/15.35 inference(unit_resolution,[status(thm)],[328, 17, 144, 322, 300, 282])).
% 15.15/15.35 % SZS output end Proof
% 15.15/15.36 % E exiting
%------------------------------------------------------------------------------