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