%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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 : Tue May 5 07:08:14 PM UTC 2026
% Result : Theorem 7.74s 7.97s
% Output : Proof 7.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.16/0.33 % Computer : n013.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 09:54:27 EDT 2026
% 0.16/0.33 % CPUTime :
% 7.74/7.97 % SZS status Theorem
% 7.74/7.97 % SZS output start Proof
% 7.74/7.97 tff(y_type, type, (
% 7.74/7.97 y: ( $i * $i ) > $i)).
% 7.74/7.97 tff(n_type, type, (
% 7.74/7.97 n: $i > $i)).
% 7.74/7.97 tff(z_type, type, (
% 7.74/7.97 z: $i)).
% 7.74/7.97 tff(proj1N_type, type, (
% 7.74/7.97 proj1N: $i > $i)).
% 7.74/7.97 tff(d_type, type, (
% 7.74/7.97 d: $i > $i)).
% 7.74/7.97 tff(addNat_type, type, (
% 7.74/7.97 addNat: ( $i * $i ) > $i)).
% 7.74/7.97 tff(s_type, type, (
% 7.74/7.97 s: $i > $i)).
% 7.74/7.97 tff(opt_type, type, (
% 7.74/7.97 opt: $i > $i)).
% 7.74/7.97 tff(x_type, type, (
% 7.74/7.97 x: ( $i * $i ) > $i)).
% 7.74/7.97 tff(fail2_type, type, (
% 7.74/7.97 fail2: ( $i * $i ) > $i)).
% 7.74/7.97 tff(fail1_type, type, (
% 7.74/7.97 fail1: ( $i * $i ) > $i)).
% 7.74/7.97 tff(fail_type, type, (
% 7.74/7.97 fail: ( $i * $i ) > $i)).
% 7.74/7.97 tff(x2_type, type, (
% 7.74/7.97 x2: $i)).
% 7.74/7.97 tff(1,plain,
% 7.74/7.97 (^[Y: $i] : refl((d(n(Y)) = n(z)) <=> (d(n(Y)) = n(z)))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(2,plain,
% 7.74/7.97 (![Y: $i] : (d(n(Y)) = n(z)) <=> ![Y: $i] : (d(n(Y)) = n(z))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[1])).
% 7.74/7.97 tff(3,plain,
% 7.74/7.97 (![Y: $i] : (d(n(Y)) = n(z)) <=> ![Y: $i] : (d(n(Y)) = n(z))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(4,axiom,(![Y: $i] : (d(n(Y)) = n(z))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_039')).
% 7.74/7.97 tff(5,plain,
% 7.74/7.97 (![Y: $i] : (d(n(Y)) = n(z))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[4, 3])).
% 7.74/7.97 tff(6,plain,(
% 7.74/7.97 ![Y: $i] : (d(n(Y)) = n(z))),
% 7.74/7.97 inference(skolemize,[status(sab)],[5])).
% 7.74/7.97 tff(7,plain,
% 7.74/7.97 (![Y: $i] : (d(n(Y)) = n(z))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[6, 2])).
% 7.74/7.97 tff(8,plain,
% 7.74/7.97 ((~![Y: $i] : (d(n(Y)) = n(z))) | (d(n(addNat(s(z), s(z)))) = n(z))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(9,plain,
% 7.74/7.97 (d(n(addNat(s(z), s(z)))) = n(z)),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[8, 7])).
% 7.74/7.97 tff(10,plain,
% 7.74/7.97 (n(z) = d(n(addNat(s(z), s(z))))),
% 7.74/7.97 inference(symmetry,[status(thm)],[9])).
% 7.74/7.97 tff(11,plain,
% 7.74/7.97 (y(n(z), n(z)) = y(d(n(addNat(s(z), s(z)))), n(z))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[10])).
% 7.74/7.97 tff(12,plain,
% 7.74/7.97 (y(d(n(addNat(s(z), s(z)))), n(z)) = y(n(z), n(z))),
% 7.74/7.97 inference(symmetry,[status(thm)],[11])).
% 7.74/7.97 tff(13,plain,
% 7.74/7.97 ((~![Y: $i] : (d(n(Y)) = n(z))) | (d(n(s(z))) = n(z))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(14,plain,
% 7.74/7.97 (d(n(s(z))) = n(z)),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[13, 7])).
% 7.74/7.97 tff(15,plain,
% 7.74/7.97 (n(z) = d(n(s(z)))),
% 7.74/7.97 inference(symmetry,[status(thm)],[14])).
% 7.74/7.97 tff(16,plain,
% 7.74/7.97 (x(n(z), n(z)) = x(d(n(s(z))), d(n(s(z))))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[15, 15])).
% 7.74/7.97 tff(17,plain,
% 7.74/7.97 (x(d(n(s(z))), d(n(s(z)))) = x(n(z), n(z))),
% 7.74/7.97 inference(symmetry,[status(thm)],[16])).
% 7.74/7.97 tff(18,plain,
% 7.74/7.97 (opt(x(d(n(s(z))), d(n(s(z))))) = opt(x(n(z), n(z)))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[17])).
% 7.74/7.97 tff(19,plain,
% 7.74/7.97 (opt(x(n(z), n(z))) = opt(x(d(n(s(z))), d(n(s(z)))))),
% 7.74/7.97 inference(symmetry,[status(thm)],[18])).
% 7.74/7.97 tff(20,plain,
% 7.74/7.97 (^[E: $i] : refl((opt(x(n(z), E)) = E) <=> (opt(x(n(z), E)) = E))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(21,plain,
% 7.74/7.97 (![E: $i] : (opt(x(n(z), E)) = E) <=> ![E: $i] : (opt(x(n(z), E)) = E)),
% 7.74/7.97 inference(quant_intro,[status(thm)],[20])).
% 7.74/7.97 tff(22,plain,
% 7.74/7.97 (![E: $i] : (opt(x(n(z), E)) = E) <=> ![E: $i] : (opt(x(n(z), E)) = E)),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(23,axiom,(![E: $i] : (opt(x(n(z), E)) = E)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_050')).
% 7.74/7.97 tff(24,plain,
% 7.74/7.97 (![E: $i] : (opt(x(n(z), E)) = E)),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[23, 22])).
% 7.74/7.97 tff(25,plain,(
% 7.74/7.97 ![E: $i] : (opt(x(n(z), E)) = E)),
% 7.74/7.97 inference(skolemize,[status(sab)],[24])).
% 7.74/7.97 tff(26,plain,
% 7.74/7.97 (![E: $i] : (opt(x(n(z), E)) = E)),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[25, 21])).
% 7.74/7.97 tff(27,plain,
% 7.74/7.97 ((~![E: $i] : (opt(x(n(z), E)) = E)) | (opt(x(n(z), n(z))) = n(z))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(28,plain,
% 7.74/7.97 (opt(x(n(z), n(z))) = n(z)),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[27, 26])).
% 7.74/7.97 tff(29,plain,
% 7.74/7.97 (n(z) = opt(x(n(z), n(z)))),
% 7.74/7.97 inference(symmetry,[status(thm)],[28])).
% 7.74/7.97 tff(30,plain,
% 7.74/7.97 (n(z) = opt(x(d(n(s(z))), d(n(s(z)))))),
% 7.74/7.97 inference(transitivity,[status(thm)],[29, 19])).
% 7.74/7.97 tff(31,plain,
% 7.74/7.97 (^[Y: $i, Z: $i] : refl((addNat(s(Z), Y) = s(addNat(Z, Y))) <=> (addNat(s(Z), Y) = s(addNat(Z, Y))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(32,plain,
% 7.74/7.97 (![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y))) <=> ![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y)))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[31])).
% 7.74/7.97 tff(33,plain,
% 7.74/7.97 (![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y))) <=> ![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y)))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(34,axiom,(![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_043')).
% 7.74/7.97 tff(35,plain,
% 7.74/7.97 (![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[34, 33])).
% 7.74/7.97 tff(36,plain,(
% 7.74/7.97 ![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y)))),
% 7.74/7.97 inference(skolemize,[status(sab)],[35])).
% 7.74/7.97 tff(37,plain,
% 7.74/7.97 (![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[36, 32])).
% 7.74/7.97 tff(38,plain,
% 7.74/7.97 ((~![Y: $i, Z: $i] : (addNat(s(Z), Y) = s(addNat(Z, Y)))) | (addNat(s(z), s(z)) = s(addNat(z, s(z))))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(39,plain,
% 7.74/7.97 (addNat(s(z), s(z)) = s(addNat(z, s(z)))),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[38, 37])).
% 7.74/7.97 tff(40,plain,
% 7.74/7.97 (s(addNat(z, s(z))) = addNat(s(z), s(z))),
% 7.74/7.97 inference(symmetry,[status(thm)],[39])).
% 7.74/7.97 tff(41,plain,
% 7.74/7.97 (^[Y: $i] : refl((addNat(z, Y) = Y) <=> (addNat(z, Y) = Y))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(42,plain,
% 7.74/7.97 (![Y: $i] : (addNat(z, Y) = Y) <=> ![Y: $i] : (addNat(z, Y) = Y)),
% 7.74/7.97 inference(quant_intro,[status(thm)],[41])).
% 7.74/7.97 tff(43,plain,
% 7.74/7.97 (![Y: $i] : (addNat(z, Y) = Y) <=> ![Y: $i] : (addNat(z, Y) = Y)),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(44,axiom,(![Y: $i] : (addNat(z, Y) = Y)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_044')).
% 7.74/7.97 tff(45,plain,
% 7.74/7.97 (![Y: $i] : (addNat(z, Y) = Y)),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[44, 43])).
% 7.74/7.97 tff(46,plain,(
% 7.74/7.97 ![Y: $i] : (addNat(z, Y) = Y)),
% 7.74/7.97 inference(skolemize,[status(sab)],[45])).
% 7.74/7.97 tff(47,plain,
% 7.74/7.97 (![Y: $i] : (addNat(z, Y) = Y)),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[46, 42])).
% 7.74/7.97 tff(48,plain,
% 7.74/7.97 ((~![Y: $i] : (addNat(z, Y) = Y)) | (addNat(z, s(z)) = s(z))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(49,plain,
% 7.74/7.97 (addNat(z, s(z)) = s(z)),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[48, 47])).
% 7.74/7.97 tff(50,plain,
% 7.74/7.97 (s(z) = addNat(z, s(z))),
% 7.74/7.97 inference(symmetry,[status(thm)],[49])).
% 7.74/7.97 tff(51,plain,
% 7.74/7.97 (s(s(z)) = s(addNat(z, s(z)))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[50])).
% 7.74/7.97 tff(52,plain,
% 7.74/7.97 (s(s(z)) = addNat(s(z), s(z))),
% 7.74/7.97 inference(transitivity,[status(thm)],[51, 40])).
% 7.74/7.97 tff(53,plain,
% 7.74/7.97 (n(s(s(z))) = n(addNat(s(z), s(z)))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[52])).
% 7.74/7.97 tff(54,plain,
% 7.74/7.97 (n(addNat(s(z), s(z))) = n(s(s(z)))),
% 7.74/7.97 inference(symmetry,[status(thm)],[53])).
% 7.74/7.97 tff(55,plain,
% 7.74/7.97 (y(n(addNat(s(z), s(z))), n(z)) = y(n(s(s(z))), opt(x(d(n(s(z))), d(n(s(z))))))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[54, 30])).
% 7.74/7.97 tff(56,plain,
% 7.74/7.97 (y(n(s(s(z))), opt(x(d(n(s(z))), d(n(s(z)))))) = y(n(addNat(s(z), s(z))), n(z))),
% 7.74/7.97 inference(symmetry,[status(thm)],[55])).
% 7.74/7.97 tff(57,plain,
% 7.74/7.97 (opt(y(d(n(addNat(s(z), s(z)))), n(z))) = opt(y(n(z), n(z)))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[12])).
% 7.74/7.97 tff(58,plain,
% 7.74/7.97 (opt(y(n(z), n(z))) = opt(y(d(n(addNat(s(z), s(z)))), n(z)))),
% 7.74/7.97 inference(symmetry,[status(thm)],[57])).
% 7.74/7.97 tff(59,plain,
% 7.74/7.97 (^[E2: $i] : refl((opt(y(n(z), E2)) = n(z)) <=> (opt(y(n(z), E2)) = n(z)))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(60,plain,
% 7.74/7.97 (![E2: $i] : (opt(y(n(z), E2)) = n(z)) <=> ![E2: $i] : (opt(y(n(z), E2)) = n(z))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[59])).
% 7.74/7.97 tff(61,plain,
% 7.74/7.97 (![E2: $i] : (opt(y(n(z), E2)) = n(z)) <=> ![E2: $i] : (opt(y(n(z), E2)) = n(z))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(62,axiom,(![E2: $i] : (opt(y(n(z), E2)) = n(z))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_053')).
% 7.74/7.97 tff(63,plain,
% 7.74/7.97 (![E2: $i] : (opt(y(n(z), E2)) = n(z))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[62, 61])).
% 7.74/7.97 tff(64,plain,(
% 7.74/7.97 ![E2: $i] : (opt(y(n(z), E2)) = n(z))),
% 7.74/7.97 inference(skolemize,[status(sab)],[63])).
% 7.74/7.97 tff(65,plain,
% 7.74/7.97 (![E2: $i] : (opt(y(n(z), E2)) = n(z))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[64, 60])).
% 7.74/7.97 tff(66,plain,
% 7.74/7.97 ((~![E2: $i] : (opt(y(n(z), E2)) = n(z))) | (opt(y(n(z), n(z))) = n(z))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(67,plain,
% 7.74/7.97 (opt(y(n(z), n(z))) = n(z)),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[66, 65])).
% 7.74/7.97 tff(68,plain,
% 7.74/7.97 (n(z) = opt(y(n(z), n(z)))),
% 7.74/7.97 inference(symmetry,[status(thm)],[67])).
% 7.74/7.97 tff(69,plain,
% 7.74/7.97 (opt(x(d(n(s(z))), d(n(s(z))))) = opt(y(d(n(addNat(s(z), s(z)))), n(z)))),
% 7.74/7.97 inference(transitivity,[status(thm)],[18, 28, 68, 58])).
% 7.74/7.97 tff(70,plain,
% 7.74/7.97 (y(n(s(s(z))), opt(x(d(n(s(z))), d(n(s(z)))))) = y(n(s(s(z))), opt(y(d(n(addNat(s(z), s(z)))), n(z))))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[69])).
% 7.74/7.97 tff(71,plain,
% 7.74/7.97 (y(n(s(s(z))), opt(y(d(n(addNat(s(z), s(z)))), n(z)))) = y(n(s(s(z))), opt(x(d(n(s(z))), d(n(s(z))))))),
% 7.74/7.97 inference(symmetry,[status(thm)],[70])).
% 7.74/7.97 tff(72,plain,
% 7.74/7.97 (^[E: $i] : refl((fail2(E, E) = y(n(s(s(z))), opt(E))) <=> (fail2(E, E) = y(n(s(s(z))), opt(E))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(73,plain,
% 7.74/7.97 (![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E))) <=> ![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[72])).
% 7.74/7.97 tff(74,plain,
% 7.74/7.97 (![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E))) <=> ![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(75,plain,
% 7.74/7.97 (![Y: $i, E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E))) <=> ![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(elim_unused_vars,[status(thm)],[])).
% 7.74/7.97 tff(76,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((~(Y = E)) | (fail2(Y, E) = y(n(s(s(z))), opt(Y)))) <=> ![Y: $i, E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(destructive_equality_resolution,[status(thm)],[])).
% 7.74/7.97 tff(77,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((~(Y = E)) | (fail2(Y, E) = y(n(s(s(z))), opt(Y)))) <=> ![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(transitivity,[status(thm)],[76, 75])).
% 7.74/7.97 tff(78,plain,
% 7.74/7.97 (^[Y: $i, E: $i] : rewrite(((Y = E) => (fail2(Y, E) = y(n(s(s(z))), opt(Y)))) <=> ((~(Y = E)) | (fail2(Y, E) = y(n(s(s(z))), opt(Y)))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(79,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((Y = E) => (fail2(Y, E) = y(n(s(s(z))), opt(Y)))) <=> ![Y: $i, E: $i] : ((~(Y = E)) | (fail2(Y, E) = y(n(s(s(z))), opt(Y))))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[78])).
% 7.74/7.97 tff(80,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((Y = E) => (fail2(Y, E) = y(n(s(s(z))), opt(Y)))) <=> ![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(transitivity,[status(thm)],[79, 77])).
% 7.74/7.97 tff(81,axiom,(![Y: $i, E: $i] : ((Y = E) => (fail2(Y, E) = y(n(s(s(z))), opt(Y))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_014')).
% 7.74/7.97 tff(82,plain,
% 7.74/7.97 (![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[81, 80])).
% 7.74/7.97 tff(83,plain,
% 7.74/7.97 (![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[82, 74])).
% 7.74/7.97 tff(84,plain,(
% 7.74/7.97 ![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(skolemize,[status(sab)],[83])).
% 7.74/7.97 tff(85,plain,
% 7.74/7.97 (![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[84, 73])).
% 7.74/7.97 tff(86,plain,
% 7.74/7.97 ((~![E: $i] : (fail2(E, E) = y(n(s(s(z))), opt(E)))) | (fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = y(n(s(s(z))), opt(y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(87,plain,
% 7.74/7.97 (fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = y(n(s(s(z))), opt(y(d(n(addNat(s(z), s(z)))), n(z))))),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[86, 85])).
% 7.74/7.97 tff(88,assumption,(~(y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z)))))), introduced(assumption)).
% 7.74/7.97 tff(89,plain,
% 7.74/7.97 (^[Y: $i, E: $i] : refl(((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y)))) <=> ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y)))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(90,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y)))) <=> ![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[89])).
% 7.74/7.97 tff(91,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y)))) <=> ![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(92,plain,
% 7.74/7.97 (^[Y: $i, E: $i] : rewrite(((~(Y = n(proj1N(Y)))) => (fail1(Y, E) = fail2(Y, E))) <=> ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y)))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(93,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((~(Y = n(proj1N(Y)))) => (fail1(Y, E) = fail2(Y, E))) <=> ![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[92])).
% 7.74/7.97 tff(94,axiom,(![Y: $i, E: $i] : ((~(Y = n(proj1N(Y)))) => (fail1(Y, E) = fail2(Y, E)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_017')).
% 7.74/7.97 tff(95,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[94, 93])).
% 7.74/7.97 tff(96,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[95, 91])).
% 7.74/7.97 tff(97,plain,(
% 7.74/7.97 ![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))),
% 7.74/7.97 inference(skolemize,[status(sab)],[96])).
% 7.74/7.97 tff(98,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[97, 90])).
% 7.74/7.97 tff(99,plain,
% 7.74/7.97 (((~![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))) | ((fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))))) <=> ((~![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))) | (fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(100,plain,
% 7.74/7.97 ((~![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))) | ((fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(101,plain,
% 7.74/7.97 ((~![Y: $i, E: $i] : ((fail1(Y, E) = fail2(Y, E)) | (Y = n(proj1N(Y))))) | (fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[100, 99])).
% 7.74/7.97 tff(102,plain,
% 7.74/7.97 ((fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[101, 98])).
% 7.74/7.97 tff(103,plain,
% 7.74/7.97 (fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail2(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[102, 88])).
% 7.74/7.97 tff(104,plain,
% 7.74/7.97 (^[Y: $i, E: $i] : refl(((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E)))) <=> ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E)))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(105,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E)))) <=> ![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[104])).
% 7.74/7.97 tff(106,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E)))) <=> ![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(107,plain,
% 7.74/7.97 (^[Y: $i, E: $i] : rewrite(((~(E = n(proj1N(E)))) => (fail(Y, E) = fail1(Y, E))) <=> ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E)))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(108,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((~(E = n(proj1N(E)))) => (fail(Y, E) = fail1(Y, E))) <=> ![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[107])).
% 7.74/7.97 tff(109,axiom,(![Y: $i, E: $i] : ((~(E = n(proj1N(E)))) => (fail(Y, E) = fail1(Y, E)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_020')).
% 7.74/7.97 tff(110,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[109, 108])).
% 7.74/7.97 tff(111,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[110, 106])).
% 7.74/7.97 tff(112,plain,(
% 7.74/7.97 ![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))),
% 7.74/7.97 inference(skolemize,[status(sab)],[111])).
% 7.74/7.97 tff(113,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[112, 105])).
% 7.74/7.97 tff(114,plain,
% 7.74/7.97 (((~![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))) | ((fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))))) <=> ((~![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))) | (fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(115,plain,
% 7.74/7.97 ((~![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))) | ((fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(116,plain,
% 7.74/7.97 ((~![Y: $i, E: $i] : ((fail(Y, E) = fail1(Y, E)) | (E = n(proj1N(E))))) | (fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[115, 114])).
% 7.74/7.97 tff(117,plain,
% 7.74/7.97 (fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = fail1(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[116, 113, 88])).
% 7.74/7.97 tff(118,plain,
% 7.74/7.97 (^[Y: $i, E: $i] : refl(((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E))) <=> ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(119,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E))) <=> ![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[118])).
% 7.74/7.97 tff(120,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E))) <=> ![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(121,plain,
% 7.74/7.97 (^[Y: $i, E: $i] : rewrite(((~(Y = n(proj1N(Y)))) => (opt(x(Y, E)) = fail(Y, E))) <=> ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(122,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((~(Y = n(proj1N(Y)))) => (opt(x(Y, E)) = fail(Y, E))) <=> ![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[121])).
% 7.74/7.97 tff(123,axiom,(![Y: $i, E: $i] : ((~(Y = n(proj1N(Y)))) => (opt(x(Y, E)) = fail(Y, E)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_048')).
% 7.74/7.97 tff(124,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[123, 122])).
% 7.74/7.97 tff(125,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[124, 120])).
% 7.74/7.97 tff(126,plain,(
% 7.74/7.97 ![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))),
% 7.74/7.97 inference(skolemize,[status(sab)],[125])).
% 7.74/7.97 tff(127,plain,
% 7.74/7.97 (![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[126, 119])).
% 7.74/7.97 tff(128,plain,
% 7.74/7.97 (((~![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))) | ((y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))) | (opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) = fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))))) <=> ((~![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))) | (opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) = fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(129,plain,
% 7.74/7.97 ((~![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))) | ((y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))) | (opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) = fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.97 inference(quant_inst,[status(thm)],[])).
% 7.74/7.97 tff(130,plain,
% 7.74/7.97 ((~![Y: $i, E: $i] : ((Y = n(proj1N(Y))) | (opt(x(Y, E)) = fail(Y, E)))) | (y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))) | (opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) = fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[129, 128])).
% 7.74/7.97 tff(131,plain,
% 7.74/7.97 ((y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))) | (opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) = fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))))),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[130, 127])).
% 7.74/7.97 tff(132,plain,
% 7.74/7.97 (opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) = fail(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))),
% 7.74/7.97 inference(unit_resolution,[status(thm)],[131, 88])).
% 7.74/7.97 tff(133,plain,
% 7.74/7.97 (d(y(d(n(addNat(s(z), s(z)))), n(z))) = d(y(n(z), n(z)))),
% 7.74/7.97 inference(monotonicity,[status(thm)],[12])).
% 7.74/7.97 tff(134,plain,
% 7.74/7.97 (d(y(n(z), n(z))) = d(y(d(n(addNat(s(z), s(z)))), n(z)))),
% 7.74/7.97 inference(symmetry,[status(thm)],[133])).
% 7.74/7.97 tff(135,plain,
% 7.74/7.97 (^[H: $i, G2: $i] : refl((d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2)))) <=> (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2)))))),
% 7.74/7.97 inference(bind,[status(th)],[])).
% 7.74/7.97 tff(136,plain,
% 7.74/7.97 (![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2)))) <=> ![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2))))),
% 7.74/7.97 inference(quant_intro,[status(thm)],[135])).
% 7.74/7.97 tff(137,plain,
% 7.74/7.97 (![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2)))) <=> ![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2))))),
% 7.74/7.97 inference(rewrite,[status(thm)],[])).
% 7.74/7.97 tff(138,axiom,(![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_041')).
% 7.74/7.97 tff(139,plain,
% 7.74/7.97 (![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[138, 137])).
% 7.74/7.97 tff(140,plain,(
% 7.74/7.97 ![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2))))),
% 7.74/7.97 inference(skolemize,[status(sab)],[139])).
% 7.74/7.97 tff(141,plain,
% 7.74/7.97 (![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2))))),
% 7.74/7.97 inference(modus_ponens,[status(thm)],[140, 136])).
% 7.74/7.97 tff(142,plain,
% 7.74/7.97 ((~![H: $i, G2: $i] : (d(y(H, G2)) = x(y(d(H), G2), y(H, d(G2))))) | (d(y(n(z), n(z))) = x(y(d(n(z)), n(z)), y(n(z), d(n(z)))))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(143,plain,
% 7.74/7.98 (d(y(n(z), n(z))) = x(y(d(n(z)), n(z)), y(n(z), d(n(z))))),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[142, 141])).
% 7.74/7.98 tff(144,plain,
% 7.74/7.98 (x(y(d(n(z)), n(z)), y(n(z), d(n(z)))) = d(y(n(z), n(z)))),
% 7.74/7.98 inference(symmetry,[status(thm)],[143])).
% 7.74/7.98 tff(145,plain,
% 7.74/7.98 ((~![Y: $i] : (d(n(Y)) = n(z))) | (d(n(z)) = n(z))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(146,plain,
% 7.74/7.98 (d(n(z)) = n(z)),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[145, 7])).
% 7.74/7.98 tff(147,plain,
% 7.74/7.98 (y(n(z), d(n(z))) = y(d(n(addNat(s(z), s(z)))), n(z))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[10, 146])).
% 7.74/7.98 tff(148,plain,
% 7.74/7.98 (y(d(n(addNat(s(z), s(z)))), n(z)) = y(n(z), d(n(z)))),
% 7.74/7.98 inference(symmetry,[status(thm)],[147])).
% 7.74/7.98 tff(149,plain,
% 7.74/7.98 (d(n(z)) = d(n(addNat(s(z), s(z))))),
% 7.74/7.98 inference(transitivity,[status(thm)],[146, 10])).
% 7.74/7.98 tff(150,plain,
% 7.74/7.98 (y(d(n(z)), n(z)) = y(d(n(addNat(s(z), s(z)))), n(z))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[149])).
% 7.74/7.98 tff(151,plain,
% 7.74/7.98 (y(d(n(addNat(s(z), s(z)))), n(z)) = y(d(n(z)), n(z))),
% 7.74/7.98 inference(symmetry,[status(thm)],[150])).
% 7.74/7.98 tff(152,plain,
% 7.74/7.98 (x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = x(y(d(n(z)), n(z)), y(n(z), d(n(z))))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[151, 148])).
% 7.74/7.98 tff(153,plain,
% 7.74/7.98 (x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))) = d(y(d(n(addNat(s(z), s(z)))), n(z)))),
% 7.74/7.98 inference(transitivity,[status(thm)],[152, 144, 134])).
% 7.74/7.98 tff(154,plain,
% 7.74/7.98 (opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z)))) = opt(d(y(d(n(addNat(s(z), s(z)))), n(z))))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[153])).
% 7.74/7.98 tff(155,plain,
% 7.74/7.98 (opt(d(y(d(n(addNat(s(z), s(z)))), n(z)))) = opt(x(y(d(n(addNat(s(z), s(z)))), n(z)), y(d(n(addNat(s(z), s(z)))), n(z))))),
% 7.74/7.98 inference(symmetry,[status(thm)],[154])).
% 7.74/7.98 tff(156,plain,
% 7.74/7.98 (^[E: $i] : refl((opt(d(E)) = opt(d(opt(E)))) <=> (opt(d(E)) = opt(d(opt(E)))))),
% 7.74/7.98 inference(bind,[status(th)],[])).
% 7.74/7.98 tff(157,plain,
% 7.74/7.98 (![E: $i] : (opt(d(E)) = opt(d(opt(E)))) <=> ![E: $i] : (opt(d(E)) = opt(d(opt(E))))),
% 7.74/7.98 inference(quant_intro,[status(thm)],[156])).
% 7.74/7.98 tff(158,plain,
% 7.74/7.98 ((~?[E: $i] : (~(opt(d(E)) = opt(d(opt(E)))))) <=> (~?[E: $i] : (~(opt(d(E)) = opt(d(opt(E))))))),
% 7.74/7.98 inference(rewrite,[status(thm)],[])).
% 7.74/7.98 tff(159,axiom,(~?[E: $i] : (~(opt(d(E)) = opt(d(opt(E)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','goal_054')).
% 7.74/7.98 tff(160,plain,
% 7.74/7.98 (~?[E: $i] : (~(opt(d(E)) = opt(d(opt(E)))))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[159, 158])).
% 7.74/7.98 tff(161,plain,
% 7.74/7.98 (~?[E: $i] : (~(opt(d(E)) = opt(d(opt(E)))))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[160, 158])).
% 7.74/7.98 tff(162,plain,
% 7.74/7.98 (~?[E: $i] : (~(opt(d(E)) = opt(d(opt(E)))))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[161, 158])).
% 7.74/7.98 tff(163,plain,
% 7.74/7.98 (~?[E: $i] : (~(opt(d(E)) = opt(d(opt(E)))))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[162, 158])).
% 7.74/7.98 tff(164,plain,
% 7.74/7.98 (^[E: $i] : refl($oeq((opt(d(E)) = opt(d(opt(E)))), (opt(d(E)) = opt(d(opt(E))))))),
% 7.74/7.98 inference(bind,[status(th)],[])).
% 7.74/7.98 tff(165,plain,(
% 7.74/7.98 ![E: $i] : (opt(d(E)) = opt(d(opt(E))))),
% 7.74/7.98 inference(nnf-neg,[status(sab)],[163, 164])).
% 7.74/7.98 tff(166,plain,
% 7.74/7.98 (![E: $i] : (opt(d(E)) = opt(d(opt(E))))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[165, 157])).
% 7.74/7.98 tff(167,plain,
% 7.74/7.98 ((~![E: $i] : (opt(d(E)) = opt(d(opt(E))))) | (opt(d(y(d(n(addNat(s(z), s(z)))), n(z)))) = opt(d(opt(y(d(n(addNat(s(z), s(z)))), n(z))))))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(168,plain,
% 7.74/7.98 (opt(d(y(d(n(addNat(s(z), s(z)))), n(z)))) = opt(d(opt(y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[167, 166])).
% 7.74/7.98 tff(169,plain,
% 7.74/7.98 (opt(d(opt(y(d(n(addNat(s(z), s(z)))), n(z))))) = opt(d(y(d(n(addNat(s(z), s(z)))), n(z))))),
% 7.74/7.98 inference(symmetry,[status(thm)],[168])).
% 7.74/7.98 tff(170,plain,
% 7.74/7.98 (^[C: $i, B2: $i] : refl((fail1(n(C), n(B2)) = n(addNat(C, B2))) <=> (fail1(n(C), n(B2)) = n(addNat(C, B2))))),
% 7.74/7.98 inference(bind,[status(th)],[])).
% 7.74/7.98 tff(171,plain,
% 7.74/7.98 (![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2))) <=> ![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2)))),
% 7.74/7.98 inference(quant_intro,[status(thm)],[170])).
% 7.74/7.98 tff(172,plain,
% 7.74/7.98 (![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2))) <=> ![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2)))),
% 7.74/7.98 inference(rewrite,[status(thm)],[])).
% 7.74/7.98 tff(173,axiom,(![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_019')).
% 7.74/7.98 tff(174,plain,
% 7.74/7.98 (![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2)))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[173, 172])).
% 7.74/7.98 tff(175,plain,(
% 7.74/7.98 ![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2)))),
% 7.74/7.98 inference(skolemize,[status(sab)],[174])).
% 7.74/7.98 tff(176,plain,
% 7.74/7.98 (![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2)))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[175, 171])).
% 7.74/7.98 tff(177,plain,
% 7.74/7.98 ((~![C: $i, B2: $i] : (fail1(n(C), n(B2)) = n(addNat(C, B2)))) | (fail1(n(s(z)), n(s(z))) = n(addNat(s(z), s(z))))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(178,plain,
% 7.74/7.98 (fail1(n(s(z)), n(s(z))) = n(addNat(s(z), s(z)))),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[177, 176])).
% 7.74/7.98 tff(179,plain,
% 7.74/7.98 (^[Y: $i, X2: $i] : refl((fail(Y, n(s(X2))) = fail1(Y, n(s(X2)))) <=> (fail(Y, n(s(X2))) = fail1(Y, n(s(X2)))))),
% 7.74/7.98 inference(bind,[status(th)],[])).
% 7.74/7.98 tff(180,plain,
% 7.74/7.98 (![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2)))) <=> ![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2))))),
% 7.74/7.98 inference(quant_intro,[status(thm)],[179])).
% 7.74/7.98 tff(181,plain,
% 7.74/7.98 (![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2)))) <=> ![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2))))),
% 7.74/7.98 inference(rewrite,[status(thm)],[])).
% 7.74/7.98 tff(182,axiom,(![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_021')).
% 7.74/7.98 tff(183,plain,
% 7.74/7.98 (![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2))))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[182, 181])).
% 7.74/7.98 tff(184,plain,(
% 7.74/7.98 ![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2))))),
% 7.74/7.98 inference(skolemize,[status(sab)],[183])).
% 7.74/7.98 tff(185,plain,
% 7.74/7.98 (![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2))))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[184, 180])).
% 7.74/7.98 tff(186,plain,
% 7.74/7.98 ((~![Y: $i, X2: $i] : (fail(Y, n(s(X2))) = fail1(Y, n(s(X2))))) | (fail(n(s(z)), n(s(z))) = fail1(n(s(z)), n(s(z))))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(187,plain,
% 7.74/7.98 (fail(n(s(z)), n(s(z))) = fail1(n(s(z)), n(s(z)))),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[186, 185])).
% 7.74/7.98 tff(188,plain,
% 7.74/7.98 (^[E: $i, X4: $i] : refl((opt(x(n(s(X4)), E)) = fail(n(s(X4)), E)) <=> (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E)))),
% 7.74/7.98 inference(bind,[status(th)],[])).
% 7.74/7.98 tff(189,plain,
% 7.74/7.98 (![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E)) <=> ![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E))),
% 7.74/7.98 inference(quant_intro,[status(thm)],[188])).
% 7.74/7.98 tff(190,plain,
% 7.74/7.98 (![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E)) <=> ![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E))),
% 7.74/7.98 inference(rewrite,[status(thm)],[])).
% 7.74/7.98 tff(191,axiom,(![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_049')).
% 7.74/7.98 tff(192,plain,
% 7.74/7.98 (![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[191, 190])).
% 7.74/7.98 tff(193,plain,(
% 7.74/7.98 ![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E))),
% 7.74/7.98 inference(skolemize,[status(sab)],[192])).
% 7.74/7.98 tff(194,plain,
% 7.74/7.98 (![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[193, 189])).
% 7.74/7.98 tff(195,plain,
% 7.74/7.98 ((~![E: $i, X4: $i] : (opt(x(n(s(X4)), E)) = fail(n(s(X4)), E))) | (opt(x(n(s(z)), n(s(z)))) = fail(n(s(z)), n(s(z))))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(196,plain,
% 7.74/7.98 (opt(x(n(s(z)), n(s(z)))) = fail(n(s(z)), n(s(z)))),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[195, 194])).
% 7.74/7.98 tff(197,plain,
% 7.74/7.98 ((d(x2) = n(s(z))) <=> (d(x2) = n(s(z)))),
% 7.74/7.98 inference(rewrite,[status(thm)],[])).
% 7.74/7.98 tff(198,axiom,(d(x2) = n(s(z))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_042')).
% 7.74/7.98 tff(199,plain,
% 7.74/7.98 (d(x2) = n(s(z))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[198, 197])).
% 7.74/7.98 tff(200,plain,
% 7.74/7.98 (n(s(z)) = d(x2)),
% 7.74/7.98 inference(symmetry,[status(thm)],[199])).
% 7.74/7.98 tff(201,plain,
% 7.74/7.98 (x(n(s(z)), n(s(z))) = x(d(x2), d(x2))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[200, 200])).
% 7.74/7.98 tff(202,plain,
% 7.74/7.98 (x(d(x2), d(x2)) = x(n(s(z)), n(s(z)))),
% 7.74/7.98 inference(symmetry,[status(thm)],[201])).
% 7.74/7.98 tff(203,plain,
% 7.74/7.98 (opt(x(d(x2), d(x2))) = opt(x(n(s(z)), n(s(z))))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[202])).
% 7.74/7.98 tff(204,plain,
% 7.74/7.98 (opt(x(d(x2), d(x2))) = n(addNat(s(z), s(z)))),
% 7.74/7.98 inference(transitivity,[status(thm)],[203, 196, 187, 178])).
% 7.74/7.98 tff(205,plain,
% 7.74/7.98 (d(opt(x(d(x2), d(x2)))) = d(n(addNat(s(z), s(z))))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[204])).
% 7.74/7.98 tff(206,plain,
% 7.74/7.98 (d(n(addNat(s(z), s(z)))) = d(opt(x(d(x2), d(x2))))),
% 7.74/7.98 inference(symmetry,[status(thm)],[205])).
% 7.74/7.98 tff(207,plain,
% 7.74/7.98 (opt(y(d(n(addNat(s(z), s(z)))), n(z))) = n(z)),
% 7.74/7.98 inference(transitivity,[status(thm)],[57, 67])).
% 7.74/7.98 tff(208,plain,
% 7.74/7.98 (d(opt(y(d(n(addNat(s(z), s(z)))), n(z)))) = d(n(z))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[207])).
% 7.74/7.98 tff(209,plain,
% 7.74/7.98 (d(opt(y(d(n(addNat(s(z), s(z)))), n(z)))) = d(opt(x(d(x2), d(x2))))),
% 7.74/7.98 inference(transitivity,[status(thm)],[208, 146, 10, 206])).
% 7.74/7.98 tff(210,plain,
% 7.74/7.98 (opt(d(opt(y(d(n(addNat(s(z), s(z)))), n(z))))) = opt(d(opt(x(d(x2), d(x2)))))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[209])).
% 7.74/7.98 tff(211,plain,
% 7.74/7.98 (opt(d(opt(x(d(x2), d(x2))))) = opt(d(opt(y(d(n(addNat(s(z), s(z)))), n(z)))))),
% 7.74/7.98 inference(symmetry,[status(thm)],[210])).
% 7.74/7.98 tff(212,plain,
% 7.74/7.98 ((~![E: $i] : (opt(d(E)) = opt(d(opt(E))))) | (opt(d(x(d(x2), d(x2)))) = opt(d(opt(x(d(x2), d(x2))))))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(213,plain,
% 7.74/7.98 (opt(d(x(d(x2), d(x2)))) = opt(d(opt(x(d(x2), d(x2)))))),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[212, 166])).
% 7.74/7.98 tff(214,plain,
% 7.74/7.98 (^[F: $i, G: $i] : refl((d(x(F, G)) = x(d(F), d(G))) <=> (d(x(F, G)) = x(d(F), d(G))))),
% 7.74/7.98 inference(bind,[status(th)],[])).
% 7.74/7.98 tff(215,plain,
% 7.74/7.98 (![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G))) <=> ![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G)))),
% 7.74/7.98 inference(quant_intro,[status(thm)],[214])).
% 7.74/7.98 tff(216,plain,
% 7.74/7.98 (![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G))) <=> ![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G)))),
% 7.74/7.98 inference(rewrite,[status(thm)],[])).
% 7.74/7.98 tff(217,axiom,(![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_040')).
% 7.74/7.98 tff(218,plain,
% 7.74/7.98 (![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G)))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[217, 216])).
% 7.74/7.98 tff(219,plain,(
% 7.74/7.98 ![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G)))),
% 7.74/7.98 inference(skolemize,[status(sab)],[218])).
% 7.74/7.98 tff(220,plain,
% 7.74/7.98 (![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G)))),
% 7.74/7.98 inference(modus_ponens,[status(thm)],[219, 215])).
% 7.74/7.98 tff(221,plain,
% 7.74/7.98 ((~![F: $i, G: $i] : (d(x(F, G)) = x(d(F), d(G)))) | (d(x(n(s(z)), n(s(z)))) = x(d(n(s(z))), d(n(s(z)))))),
% 7.74/7.98 inference(quant_inst,[status(thm)],[])).
% 7.74/7.98 tff(222,plain,
% 7.74/7.98 (d(x(n(s(z)), n(s(z)))) = x(d(n(s(z))), d(n(s(z))))),
% 7.74/7.98 inference(unit_resolution,[status(thm)],[221, 220])).
% 7.74/7.98 tff(223,plain,
% 7.74/7.98 (d(x(d(x2), d(x2))) = d(x(n(s(z)), n(s(z))))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[202])).
% 7.74/7.98 tff(224,plain,
% 7.74/7.98 (d(x(d(x2), d(x2))) = x(n(z), n(z))),
% 7.74/7.98 inference(transitivity,[status(thm)],[223, 222, 17])).
% 7.74/7.98 tff(225,plain,
% 7.74/7.98 (opt(d(x(d(x2), d(x2)))) = opt(x(n(z), n(z)))),
% 7.74/7.98 inference(monotonicity,[status(thm)],[224])).
% 7.74/7.98 tff(226,plain,
% 7.74/7.98 (opt(x(n(z), n(z))) = opt(d(x(d(x2), d(x2))))),
% 7.74/7.98 inference(symmetry,[status(thm)],[225])).
% 7.74/7.98 tff(227,plain,
% 7.74/7.98 (n(z) = y(n(addNat(s(z), s(z))), n(z))),
% 7.74/7.98 inference(transitivity,[status(thm)],[29, 226, 213, 211, 169, 155, 132, 117, 103, 87, 71, 56])).
% 7.74/7.98 tff(228,plain,
% 7.74/7.98 (^[X: $i, X2: $i, X3: $i] : refl((~(n(X) = y(X2, X3))) <=> (~(n(X) = y(X2, X3))))),
% 7.74/8.02 inference(bind,[status(th)],[])).
% 7.74/8.02 tff(229,plain,
% 7.74/8.02 (![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3))) <=> ![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))),
% 7.74/8.02 inference(quant_intro,[status(thm)],[228])).
% 7.74/8.02 tff(230,plain,
% 7.74/8.02 (![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3))) <=> ![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))),
% 7.74/8.02 inference(rewrite,[status(thm)],[])).
% 7.74/8.02 tff(231,axiom,(![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_009')).
% 7.74/8.02 tff(232,plain,
% 7.74/8.02 (![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))),
% 7.74/8.02 inference(modus_ponens,[status(thm)],[231, 230])).
% 7.74/8.02 tff(233,plain,(
% 7.74/8.02 ![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))),
% 7.74/8.02 inference(skolemize,[status(sab)],[232])).
% 7.74/8.02 tff(234,plain,
% 7.74/8.02 (![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))),
% 7.74/8.02 inference(modus_ponens,[status(thm)],[233, 229])).
% 7.74/8.02 tff(235,plain,
% 7.74/8.02 ((~![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))) | (~(n(z) = y(n(addNat(s(z), s(z))), n(z))))),
% 7.74/8.02 inference(quant_inst,[status(thm)],[])).
% 7.74/8.02 tff(236,plain,
% 7.74/8.02 (~(n(z) = y(n(addNat(s(z), s(z))), n(z)))),
% 7.74/8.02 inference(unit_resolution,[status(thm)],[235, 234])).
% 7.74/8.02 tff(237,plain,
% 7.74/8.02 ($false),
% 7.74/8.02 inference(unit_resolution,[status(thm)],[236, 227])).
% 7.74/8.02 tff(238,plain,(y(d(n(addNat(s(z), s(z)))), n(z)) = n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z))))), inference(lemma,lemma(discharge,[]))).
% 7.74/8.02 tff(239,plain,
% 7.74/8.02 (n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z)))) = y(d(n(addNat(s(z), s(z)))), n(z))),
% 7.74/8.02 inference(symmetry,[status(thm)],[238])).
% 7.74/8.02 tff(240,plain,
% 7.74/8.02 (n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z)))) = y(n(z), n(z))),
% 7.74/8.02 inference(transitivity,[status(thm)],[239, 12])).
% 7.74/8.02 tff(241,plain,
% 7.74/8.02 ((~![X: $i, X2: $i, X3: $i] : (~(n(X) = y(X2, X3)))) | (~(n(proj1N(y(d(n(addNat(s(z), s(z)))), n(z)))) = y(n(z), n(z))))),
% 7.74/8.02 inference(quant_inst,[status(thm)],[])).
% 7.74/8.02 tff(242,plain,
% 7.74/8.02 ($false),
% 7.74/8.02 inference(unit_resolution,[status(thm)],[241, 234, 240])).
% 7.74/8.02 % SZS output end Proof
% 7.74/8.03 % E exiting
%------------------------------------------------------------------------------