%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS102+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.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:13:23 AM UTC 2025
% Result : Unsatisfiable 0.18s 0.39s
% Output : Proof 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : KRS102+1 : TPTP v9.0.0. Released v3.1.0.
% 0.03/0.11 % Command : run_E %s %d THM
% 0.11/0.31 % Computer : n011.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 19 19:11:27 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.18/0.39 % SZS status Unsatisfiable
% 0.18/0.39 % SZS output start Proof
% 0.18/0.39 tff(iminus3_type, type, (
% 0.18/0.39 iminus3: $i)).
% 0.18/0.39 tff(iplus6_type, type, (
% 0.18/0.39 iplus6: $i)).
% 0.18/0.39 tff(iT_type, type, (
% 0.18/0.39 iT: $i)).
% 0.18/0.39 tff(iminus4_type, type, (
% 0.18/0.39 iminus4: $i)).
% 0.18/0.39 tff(iminus6_type, type, (
% 0.18/0.39 iminus6: $i)).
% 0.18/0.39 tff(iplus9_type, type, (
% 0.18/0.39 iplus9: $i)).
% 0.18/0.39 tff(iF_type, type, (
% 0.18/0.39 iF: $i)).
% 0.18/0.39 tff(iminus1_type, type, (
% 0.18/0.39 iminus1: $i)).
% 0.18/0.39 tff(iminus5_type, type, (
% 0.18/0.39 iminus5: $i)).
% 0.18/0.39 tff(iminus2_type, type, (
% 0.18/0.39 iminus2: $i)).
% 0.18/0.39 tff(iminus7_type, type, (
% 0.18/0.39 iminus7: $i)).
% 0.18/0.39 tff(iminus9_type, type, (
% 0.18/0.39 iminus9: $i)).
% 0.18/0.39 tff(cTorF_type, type, (
% 0.18/0.39 cTorF: $i > $o)).
% 0.18/0.39 tff(iplus7_type, type, (
% 0.18/0.39 iplus7: $i)).
% 0.18/0.39 tff(iplus1_type, type, (
% 0.18/0.39 iplus1: $i)).
% 0.18/0.39 tff(iplus4_type, type, (
% 0.18/0.39 iplus4: $i)).
% 0.18/0.39 tff(iplus2_type, type, (
% 0.18/0.39 iplus2: $i)).
% 0.18/0.39 tff(iminus8_type, type, (
% 0.18/0.39 iminus8: $i)).
% 0.18/0.39 tff(iplus8_type, type, (
% 0.18/0.39 iplus8: $i)).
% 0.18/0.39 tff(iplus5_type, type, (
% 0.18/0.39 iplus5: $i)).
% 0.18/0.39 tff(iplus3_type, type, (
% 0.18/0.39 iplus3: $i)).
% 0.18/0.39 tff(1,plain,
% 0.18/0.39 ((iplus6 = iT) <=> (iT = iplus6)),
% 0.18/0.39 inference(commutativity,[status(thm)],[])).
% 0.18/0.39 tff(2,plain,
% 0.18/0.39 ((iF = iminus1) <=> (iminus1 = iF)),
% 0.18/0.39 inference(commutativity,[status(thm)],[])).
% 0.18/0.39 tff(3,assumption,(~(iT = iminus6)), introduced(assumption)).
% 0.18/0.39 tff(4,assumption,(~(iT = iminus1)), introduced(assumption)).
% 0.18/0.39 tff(5,assumption,(~(iT = iminus5)), introduced(assumption)).
% 0.18/0.39 tff(6,plain,
% 0.18/0.39 ((iplus9 = iT) <=> (iT = iplus9)),
% 0.18/0.39 inference(commutativity,[status(thm)],[])).
% 0.18/0.39 tff(7,plain,
% 0.18/0.39 ((iminus9 = iminus6) <=> (iminus6 = iminus9)),
% 0.18/0.39 inference(commutativity,[status(thm)],[])).
% 0.18/0.39 tff(8,plain,
% 0.18/0.39 ((iminus6 = iT) <=> (iT = iminus6)),
% 0.18/0.39 inference(commutativity,[status(thm)],[])).
% 0.18/0.39 tff(9,assumption,(~(iT = iminus2)), introduced(assumption)).
% 0.18/0.39 tff(10,plain,
% 0.18/0.39 (((iT = iminus9) | (iT = iminus2) | (iT = iminus5)) <=> ((iT = iminus9) | (iT = iminus2) | (iT = iminus5))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(11,plain,
% 0.18/0.39 ((((iT = iminus5) | (iT = iminus9)) | (iT = iminus2)) <=> ((iT = iminus9) | (iT = iminus2) | (iT = iminus5))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(12,axiom,(((iT = iminus5) | (iT = iminus9)) | (iT = iminus2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_35')).
% 0.18/0.39 tff(13,plain,
% 0.18/0.39 ((iT = iminus9) | (iT = iminus2) | (iT = iminus5)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.18/0.39 tff(14,plain,
% 0.18/0.39 ((iT = iminus9) | (iT = iminus2) | (iT = iminus5)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[13, 10])).
% 0.18/0.39 tff(15,plain,
% 0.18/0.39 ((iT = iminus9) | (iT = iminus2) | (iT = iminus5)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[14, 10])).
% 0.18/0.39 tff(16,plain,
% 0.18/0.39 ((iT = iminus9) | (iT = iminus2) | (iT = iminus5)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[15, 10])).
% 0.18/0.39 tff(17,plain,
% 0.18/0.39 ((iT = iminus9) | (iT = iminus2) | (iT = iminus5)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[16, 10])).
% 0.18/0.39 tff(18,plain,
% 0.18/0.39 (iT = iminus9),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[17, 9, 5])).
% 0.18/0.39 tff(19,plain,
% 0.18/0.39 (iminus9 = iT),
% 0.18/0.39 inference(symmetry,[status(thm)],[18])).
% 0.18/0.39 tff(20,plain,
% 0.18/0.39 ((iminus6 = iminus9) <=> (iminus6 = iT)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[19])).
% 0.18/0.39 tff(21,plain,
% 0.18/0.39 ((iminus6 = iminus9) <=> (iT = iminus6)),
% 0.18/0.39 inference(transitivity,[status(thm)],[20, 8])).
% 0.18/0.39 tff(22,plain,
% 0.18/0.39 ((iT = iminus6) <=> (iminus6 = iminus9)),
% 0.18/0.39 inference(symmetry,[status(thm)],[21])).
% 0.18/0.39 tff(23,plain,
% 0.18/0.39 ((~(iT = iminus6)) <=> (~(iminus6 = iminus9))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[22])).
% 0.18/0.39 tff(24,plain,
% 0.18/0.39 (~(iminus6 = iminus9)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[3, 23])).
% 0.18/0.39 tff(25,plain,
% 0.18/0.39 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus9) | (X = iplus9))) <=> (cTorF(X) <=> ((X = iminus9) | (X = iplus9))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(26,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[25])).
% 0.18/0.39 tff(27,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(28,axiom,(![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_11')).
% 0.18/0.39 tff(29,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.18/0.39 tff(30,plain,(
% 0.18/0.39 ![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))),
% 0.18/0.39 inference(skolemize,[status(sab)],[29])).
% 0.18/0.39 tff(31,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[30, 26])).
% 0.18/0.39 tff(32,plain,
% 0.18/0.39 ((~![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))) | (cTorF(iminus6) <=> ((iminus6 = iminus9) | (iminus6 = iplus9)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(33,plain,
% 0.18/0.39 (cTorF(iminus6) <=> ((iminus6 = iminus9) | (iminus6 = iplus9))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[32, 31])).
% 0.18/0.39 tff(34,plain,
% 0.18/0.39 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus6) | (X = iplus6))) <=> (cTorF(X) <=> ((X = iminus6) | (X = iplus6))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(35,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[34])).
% 0.18/0.39 tff(36,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(37,axiom,(![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_10')).
% 0.18/0.39 tff(38,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.18/0.39 tff(39,plain,(
% 0.18/0.39 ![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))),
% 0.18/0.39 inference(skolemize,[status(sab)],[38])).
% 0.18/0.39 tff(40,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.18/0.39 tff(41,plain,
% 0.18/0.39 (((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iminus6)) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iminus6))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(42,plain,
% 0.18/0.39 ((cTorF(iminus6) <=> $true) <=> cTorF(iminus6)),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(43,plain,
% 0.18/0.39 (($true | (iminus6 = iplus6)) <=> $true),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(44,plain,
% 0.18/0.39 ((iminus6 = iminus6) <=> $true),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(45,plain,
% 0.18/0.39 (((iminus6 = iminus6) | (iminus6 = iplus6)) <=> ($true | (iminus6 = iplus6))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[44])).
% 0.18/0.39 tff(46,plain,
% 0.18/0.39 (((iminus6 = iminus6) | (iminus6 = iplus6)) <=> $true),
% 0.18/0.39 inference(transitivity,[status(thm)],[45, 43])).
% 0.18/0.39 tff(47,plain,
% 0.18/0.39 ((cTorF(iminus6) <=> ((iminus6 = iminus6) | (iminus6 = iplus6))) <=> (cTorF(iminus6) <=> $true)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[46])).
% 0.18/0.39 tff(48,plain,
% 0.18/0.39 ((cTorF(iminus6) <=> ((iminus6 = iminus6) | (iminus6 = iplus6))) <=> cTorF(iminus6)),
% 0.18/0.39 inference(transitivity,[status(thm)],[47, 42])).
% 0.18/0.39 tff(49,plain,
% 0.18/0.39 (((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | (cTorF(iminus6) <=> ((iminus6 = iminus6) | (iminus6 = iplus6)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iminus6))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[48])).
% 0.18/0.39 tff(50,plain,
% 0.18/0.39 (((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | (cTorF(iminus6) <=> ((iminus6 = iminus6) | (iminus6 = iplus6)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iminus6))),
% 0.18/0.39 inference(transitivity,[status(thm)],[49, 41])).
% 0.18/0.39 tff(51,plain,
% 0.18/0.39 ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | (cTorF(iminus6) <=> ((iminus6 = iminus6) | (iminus6 = iplus6)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(52,plain,
% 0.18/0.39 ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iminus6)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[51, 50])).
% 0.18/0.39 tff(53,plain,
% 0.18/0.39 (cTorF(iminus6)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[52, 40])).
% 0.18/0.39 tff(54,plain,
% 0.18/0.39 ((~(cTorF(iminus6) <=> ((iminus6 = iminus9) | (iminus6 = iplus9)))) | (~cTorF(iminus6)) | ((iminus6 = iminus9) | (iminus6 = iplus9))),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(55,plain,
% 0.18/0.39 ((iminus6 = iminus9) | (iminus6 = iplus9)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[54, 53, 33])).
% 0.18/0.39 tff(56,plain,
% 0.18/0.39 ((~((iminus6 = iminus9) | (iminus6 = iplus9))) | (iminus6 = iminus9) | (iminus6 = iplus9)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(57,plain,
% 0.18/0.39 ((iminus6 = iminus9) | (iminus6 = iplus9)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[56, 55])).
% 0.18/0.39 tff(58,plain,
% 0.18/0.39 (iminus6 = iplus9),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[57, 24])).
% 0.18/0.39 tff(59,plain,
% 0.18/0.39 (iplus9 = iminus6),
% 0.18/0.39 inference(symmetry,[status(thm)],[58])).
% 0.18/0.39 tff(60,plain,
% 0.18/0.39 ((iT = iplus9) <=> (iminus9 = iminus6)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[18, 59])).
% 0.18/0.39 tff(61,plain,
% 0.18/0.39 ((iT = iplus9) <=> (iminus6 = iminus9)),
% 0.18/0.39 inference(transitivity,[status(thm)],[60, 7])).
% 0.18/0.39 tff(62,plain,
% 0.18/0.39 ((iminus6 = iminus9) <=> (iT = iplus9)),
% 0.18/0.39 inference(symmetry,[status(thm)],[61])).
% 0.18/0.39 tff(63,plain,
% 0.18/0.39 ((~(iminus6 = iminus9)) <=> (~(iT = iplus9))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[62])).
% 0.18/0.39 tff(64,plain,
% 0.18/0.39 (~(iT = iplus9)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[24, 63])).
% 0.18/0.39 tff(65,plain,
% 0.18/0.39 (((iT = iminus6) | (iT = iplus9) | (iT = iminus7)) <=> ((iT = iminus6) | (iT = iplus9) | (iT = iminus7))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(66,plain,
% 0.18/0.39 ((((iT = iminus6) | (iT = iplus9)) | (iT = iminus7)) <=> ((iT = iminus6) | (iT = iplus9) | (iT = iminus7))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(67,axiom,(((iT = iminus6) | (iT = iplus9)) | (iT = iminus7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_14')).
% 0.18/0.39 tff(68,plain,
% 0.18/0.39 ((iT = iminus6) | (iT = iplus9) | (iT = iminus7)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.18/0.39 tff(69,plain,
% 0.18/0.39 ((iT = iminus6) | (iT = iplus9) | (iT = iminus7)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[68, 65])).
% 0.18/0.39 tff(70,plain,
% 0.18/0.39 ((iT = iminus6) | (iT = iplus9) | (iT = iminus7)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[69, 65])).
% 0.18/0.39 tff(71,plain,
% 0.18/0.39 ((iT = iminus6) | (iT = iplus9) | (iT = iminus7)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[70, 65])).
% 0.18/0.39 tff(72,plain,
% 0.18/0.39 ((iT = iminus6) | (iT = iplus9) | (iT = iminus7)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[71, 65])).
% 0.18/0.39 tff(73,plain,
% 0.18/0.39 (iT = iminus7),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[72, 64, 3])).
% 0.18/0.39 tff(74,plain,
% 0.18/0.39 (iminus7 = iT),
% 0.18/0.39 inference(symmetry,[status(thm)],[73])).
% 0.18/0.39 tff(75,plain,
% 0.18/0.39 ((iminus6 = iminus7) <=> (iplus9 = iT)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[58, 74])).
% 0.18/0.39 tff(76,plain,
% 0.18/0.39 ((iminus6 = iminus7) <=> (iT = iplus9)),
% 0.18/0.39 inference(transitivity,[status(thm)],[75, 6])).
% 0.18/0.39 tff(77,plain,
% 0.18/0.39 ((iT = iplus9) <=> (iminus6 = iminus7)),
% 0.18/0.39 inference(symmetry,[status(thm)],[76])).
% 0.18/0.39 tff(78,plain,
% 0.18/0.39 ((~(iT = iplus9)) <=> (~(iminus6 = iminus7))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[77])).
% 0.18/0.39 tff(79,plain,
% 0.18/0.39 (~(iminus6 = iminus7)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[64, 78])).
% 0.18/0.39 tff(80,plain,
% 0.18/0.39 ((iplus9 = iplus7) <=> (iplus7 = iplus9)),
% 0.18/0.39 inference(commutativity,[status(thm)],[])).
% 0.18/0.39 tff(81,plain,
% 0.18/0.39 ((iminus6 = iplus7) <=> (iplus9 = iplus7)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[58])).
% 0.18/0.39 tff(82,plain,
% 0.18/0.39 ((iminus6 = iplus7) <=> (iplus7 = iplus9)),
% 0.18/0.39 inference(transitivity,[status(thm)],[81, 80])).
% 0.18/0.39 tff(83,plain,
% 0.18/0.39 ((iplus7 = iplus9) <=> (iminus6 = iplus7)),
% 0.18/0.39 inference(symmetry,[status(thm)],[82])).
% 0.18/0.39 tff(84,plain,
% 0.18/0.39 ((iminus9 = iminus1) <=> (iminus1 = iminus9)),
% 0.18/0.39 inference(commutativity,[status(thm)],[])).
% 0.18/0.39 tff(85,plain,
% 0.18/0.39 ((iT = iminus1) <=> (iminus9 = iminus1)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[18])).
% 0.18/0.39 tff(86,plain,
% 0.18/0.39 ((iT = iminus1) <=> (iminus1 = iminus9)),
% 0.18/0.39 inference(transitivity,[status(thm)],[85, 84])).
% 0.18/0.39 tff(87,plain,
% 0.18/0.39 ((~(iT = iminus1)) <=> (~(iminus1 = iminus9))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[86])).
% 0.18/0.39 tff(88,plain,
% 0.18/0.39 (~(iminus1 = iminus9)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[4, 87])).
% 0.18/0.39 tff(89,plain,
% 0.18/0.39 ((~![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))) | (cTorF(iminus1) <=> ((iminus1 = iminus9) | (iminus1 = iplus9)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(90,plain,
% 0.18/0.39 (cTorF(iminus1) <=> ((iminus1 = iminus9) | (iminus1 = iplus9))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[89, 31])).
% 0.18/0.39 tff(91,plain,
% 0.18/0.39 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus1) | (X = iplus1))) <=> (cTorF(X) <=> ((X = iminus1) | (X = iplus1))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(92,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[91])).
% 0.18/0.39 tff(93,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(94,plain,
% 0.18/0.39 (^[X: $i] : rewrite((cTorF(X) <=> ((X = iplus1) | (X = iminus1))) <=> (cTorF(X) <=> ((X = iminus1) | (X = iplus1))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(95,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iplus1) | (X = iminus1))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[94])).
% 0.18/0.39 tff(96,axiom,(![X: $i] : (cTorF(X) <=> ((X = iplus1) | (X = iminus1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_2')).
% 0.18/0.39 tff(97,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.18/0.39 tff(98,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[97, 93])).
% 0.18/0.39 tff(99,plain,(
% 0.18/0.39 ![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))),
% 0.18/0.39 inference(skolemize,[status(sab)],[98])).
% 0.18/0.39 tff(100,plain,
% 0.18/0.39 (![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[99, 92])).
% 0.18/0.39 tff(101,plain,
% 0.18/0.39 (((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iminus1)) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iminus1))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(102,plain,
% 0.18/0.39 ((cTorF(iminus1) <=> $true) <=> cTorF(iminus1)),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(103,plain,
% 0.18/0.39 (($true | (iminus1 = iplus1)) <=> $true),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(104,plain,
% 0.18/0.39 ((iminus1 = iminus1) <=> $true),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(105,plain,
% 0.18/0.39 (((iminus1 = iminus1) | (iminus1 = iplus1)) <=> ($true | (iminus1 = iplus1))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[104])).
% 0.18/0.39 tff(106,plain,
% 0.18/0.39 (((iminus1 = iminus1) | (iminus1 = iplus1)) <=> $true),
% 0.18/0.39 inference(transitivity,[status(thm)],[105, 103])).
% 0.18/0.39 tff(107,plain,
% 0.18/0.39 ((cTorF(iminus1) <=> ((iminus1 = iminus1) | (iminus1 = iplus1))) <=> (cTorF(iminus1) <=> $true)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[106])).
% 0.18/0.39 tff(108,plain,
% 0.18/0.39 ((cTorF(iminus1) <=> ((iminus1 = iminus1) | (iminus1 = iplus1))) <=> cTorF(iminus1)),
% 0.18/0.39 inference(transitivity,[status(thm)],[107, 102])).
% 0.18/0.39 tff(109,plain,
% 0.18/0.39 (((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iminus1) <=> ((iminus1 = iminus1) | (iminus1 = iplus1)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iminus1))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[108])).
% 0.18/0.39 tff(110,plain,
% 0.18/0.39 (((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iminus1) <=> ((iminus1 = iminus1) | (iminus1 = iplus1)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iminus1))),
% 0.18/0.39 inference(transitivity,[status(thm)],[109, 101])).
% 0.18/0.39 tff(111,plain,
% 0.18/0.39 ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iminus1) <=> ((iminus1 = iminus1) | (iminus1 = iplus1)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(112,plain,
% 0.18/0.39 ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iminus1)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.18/0.39 tff(113,plain,
% 0.18/0.39 (cTorF(iminus1)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[112, 100])).
% 0.18/0.39 tff(114,plain,
% 0.18/0.39 ((~(cTorF(iminus1) <=> ((iminus1 = iminus9) | (iminus1 = iplus9)))) | (~cTorF(iminus1)) | ((iminus1 = iminus9) | (iminus1 = iplus9))),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(115,plain,
% 0.18/0.40 ((iminus1 = iminus9) | (iminus1 = iplus9)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[114, 113, 90])).
% 0.18/0.40 tff(116,plain,
% 0.18/0.40 ((~((iminus1 = iminus9) | (iminus1 = iplus9))) | (iminus1 = iminus9) | (iminus1 = iplus9)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(117,plain,
% 0.18/0.40 ((iminus1 = iminus9) | (iminus1 = iplus9)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[116, 115])).
% 0.18/0.40 tff(118,plain,
% 0.18/0.40 (iminus1 = iplus9),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[117, 88])).
% 0.18/0.40 tff(119,plain,
% 0.18/0.40 (((iT = iminus6) | (iT = iplus4) | (iT = iminus2)) <=> ((iT = iminus6) | (iT = iplus4) | (iT = iminus2))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(120,plain,
% 0.18/0.40 ((((iT = iminus6) | (iT = iminus2)) | (iT = iplus4)) <=> ((iT = iminus6) | (iT = iplus4) | (iT = iminus2))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(121,plain,
% 0.18/0.40 (((iT = iminus6) | (iT = iminus2)) <=> ((iT = iminus6) | (iT = iminus2))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(122,plain,
% 0.18/0.40 ((((iT = iminus6) | (iT = iminus2)) | (iT = iplus4)) <=> (((iT = iminus6) | (iT = iminus2)) | (iT = iplus4))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[121])).
% 0.18/0.40 tff(123,plain,
% 0.18/0.40 ((((iT = iminus6) | (iT = iminus2)) | (iT = iplus4)) <=> ((iT = iminus6) | (iT = iplus4) | (iT = iminus2))),
% 0.18/0.40 inference(transitivity,[status(thm)],[122, 120])).
% 0.18/0.40 tff(124,axiom,(((iT = iminus6) | (iT = iminus2)) | (iT = iplus4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_56')).
% 0.18/0.40 tff(125,plain,
% 0.18/0.40 ((iT = iminus6) | (iT = iplus4) | (iT = iminus2)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.18/0.40 tff(126,plain,
% 0.18/0.40 ((iT = iminus6) | (iT = iplus4) | (iT = iminus2)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[125, 119])).
% 0.18/0.40 tff(127,plain,
% 0.18/0.40 ((iT = iminus6) | (iT = iplus4) | (iT = iminus2)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[126, 119])).
% 0.18/0.40 tff(128,plain,
% 0.18/0.40 ((iT = iminus6) | (iT = iplus4) | (iT = iminus2)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[127, 119])).
% 0.18/0.40 tff(129,plain,
% 0.18/0.40 ((iT = iminus6) | (iT = iplus4) | (iT = iminus2)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[128, 119])).
% 0.18/0.40 tff(130,plain,
% 0.18/0.40 (iT = iplus4),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[129, 9, 3])).
% 0.18/0.40 tff(131,plain,
% 0.18/0.40 (iplus4 = iT),
% 0.18/0.40 inference(symmetry,[status(thm)],[130])).
% 0.18/0.40 tff(132,plain,
% 0.18/0.40 (iplus4 = iminus9),
% 0.18/0.40 inference(transitivity,[status(thm)],[131, 18])).
% 0.18/0.40 tff(133,plain,
% 0.18/0.40 ((iminus1 = iplus4) <=> (iminus1 = iminus9)),
% 0.18/0.40 inference(monotonicity,[status(thm)],[132])).
% 0.18/0.40 tff(134,plain,
% 0.18/0.40 ((iminus1 = iminus9) <=> (iminus1 = iplus4)),
% 0.18/0.40 inference(symmetry,[status(thm)],[133])).
% 0.18/0.40 tff(135,plain,
% 0.18/0.40 ((~(iminus1 = iminus9)) <=> (~(iminus1 = iplus4))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[134])).
% 0.18/0.40 tff(136,plain,
% 0.18/0.40 (~(iminus1 = iplus4)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[88, 135])).
% 0.18/0.40 tff(137,plain,
% 0.18/0.40 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus4) | (X = iplus4))) <=> (cTorF(X) <=> ((X = iminus4) | (X = iplus4))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(138,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[137])).
% 0.18/0.40 tff(139,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(140,axiom,(![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_3')).
% 0.18/0.40 tff(141,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[140, 139])).
% 0.18/0.40 tff(142,plain,(
% 0.18/0.40 ![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))),
% 0.18/0.40 inference(skolemize,[status(sab)],[141])).
% 0.18/0.40 tff(143,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[142, 138])).
% 0.18/0.40 tff(144,plain,
% 0.18/0.40 ((~![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))) | (cTorF(iminus1) <=> ((iminus1 = iminus4) | (iminus1 = iplus4)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(145,plain,
% 0.18/0.40 (cTorF(iminus1) <=> ((iminus1 = iminus4) | (iminus1 = iplus4))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[144, 143])).
% 0.18/0.40 tff(146,plain,
% 0.18/0.40 ((~(cTorF(iminus1) <=> ((iminus1 = iminus4) | (iminus1 = iplus4)))) | (~cTorF(iminus1)) | ((iminus1 = iminus4) | (iminus1 = iplus4))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(147,plain,
% 0.18/0.40 ((iminus1 = iminus4) | (iminus1 = iplus4)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[146, 113, 145])).
% 0.18/0.40 tff(148,plain,
% 0.18/0.40 ((~((iminus1 = iminus4) | (iminus1 = iplus4))) | (iminus1 = iminus4) | (iminus1 = iplus4)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(149,plain,
% 0.18/0.40 ((iminus1 = iminus4) | (iminus1 = iplus4)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[148, 147])).
% 0.18/0.40 tff(150,plain,
% 0.18/0.40 (iminus1 = iminus4),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[149, 136])).
% 0.18/0.40 tff(151,plain,
% 0.18/0.40 (iminus4 = iminus1),
% 0.18/0.40 inference(symmetry,[status(thm)],[150])).
% 0.18/0.40 tff(152,plain,
% 0.18/0.40 (iminus4 = iplus9),
% 0.18/0.40 inference(transitivity,[status(thm)],[151, 118])).
% 0.18/0.40 tff(153,plain,
% 0.18/0.40 ((iT = iminus4) <=> (iT = iplus9)),
% 0.18/0.40 inference(monotonicity,[status(thm)],[152])).
% 0.18/0.40 tff(154,plain,
% 0.18/0.40 ((iT = iplus9) <=> (iT = iminus4)),
% 0.18/0.40 inference(symmetry,[status(thm)],[153])).
% 0.18/0.40 tff(155,plain,
% 0.18/0.40 ((~(iT = iplus9)) <=> (~(iT = iminus4))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[154])).
% 0.18/0.40 tff(156,plain,
% 0.18/0.40 (~(iT = iminus4)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[64, 155])).
% 0.18/0.40 tff(157,plain,
% 0.18/0.40 (((iT = iplus9) | (iT = iplus7) | (iT = iminus4)) <=> ((iT = iplus9) | (iT = iplus7) | (iT = iminus4))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(158,plain,
% 0.18/0.40 ((((iT = iminus4) | (iT = iplus7)) | (iT = iplus9)) <=> ((iT = iplus9) | (iT = iplus7) | (iT = iminus4))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(159,axiom,(((iT = iminus4) | (iT = iplus7)) | (iT = iplus9)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_58')).
% 0.18/0.40 tff(160,plain,
% 0.18/0.40 ((iT = iplus9) | (iT = iplus7) | (iT = iminus4)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[159, 158])).
% 0.18/0.40 tff(161,plain,
% 0.18/0.40 ((iT = iplus9) | (iT = iplus7) | (iT = iminus4)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[160, 157])).
% 0.18/0.40 tff(162,plain,
% 0.18/0.40 ((iT = iplus9) | (iT = iplus7) | (iT = iminus4)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[161, 157])).
% 0.18/0.40 tff(163,plain,
% 0.18/0.40 ((iT = iplus9) | (iT = iplus7) | (iT = iminus4)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[162, 157])).
% 0.18/0.40 tff(164,plain,
% 0.18/0.40 ((iT = iplus9) | (iT = iplus7) | (iT = iminus4)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[163, 157])).
% 0.18/0.40 tff(165,plain,
% 0.18/0.40 (iT = iplus7),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[164, 64, 156])).
% 0.18/0.40 tff(166,plain,
% 0.18/0.40 (iplus7 = iT),
% 0.18/0.40 inference(symmetry,[status(thm)],[165])).
% 0.18/0.40 tff(167,plain,
% 0.18/0.40 ((iplus7 = iplus9) <=> (iT = iplus9)),
% 0.18/0.40 inference(monotonicity,[status(thm)],[166])).
% 0.18/0.40 tff(168,plain,
% 0.18/0.40 ((iT = iplus9) <=> (iplus7 = iplus9)),
% 0.18/0.40 inference(symmetry,[status(thm)],[167])).
% 0.18/0.40 tff(169,plain,
% 0.18/0.40 ((iT = iplus9) <=> (iminus6 = iplus7)),
% 0.18/0.40 inference(transitivity,[status(thm)],[168, 83])).
% 0.18/0.40 tff(170,plain,
% 0.18/0.40 ((~(iT = iplus9)) <=> (~(iminus6 = iplus7))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[169])).
% 0.18/0.40 tff(171,plain,
% 0.18/0.40 (~(iminus6 = iplus7)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[64, 170])).
% 0.18/0.40 tff(172,plain,
% 0.18/0.40 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus7) | (X = iplus7))) <=> (cTorF(X) <=> ((X = iminus7) | (X = iplus7))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(173,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[172])).
% 0.18/0.40 tff(174,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(175,plain,
% 0.18/0.40 (^[X: $i] : rewrite((cTorF(X) <=> ((X = iplus7) | (X = iminus7))) <=> (cTorF(X) <=> ((X = iminus7) | (X = iplus7))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(176,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iplus7) | (X = iminus7))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[175])).
% 0.18/0.40 tff(177,axiom,(![X: $i] : (cTorF(X) <=> ((X = iplus7) | (X = iminus7)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_5')).
% 0.18/0.40 tff(178,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[177, 176])).
% 0.18/0.40 tff(179,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[178, 174])).
% 0.18/0.40 tff(180,plain,(
% 0.18/0.40 ![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))),
% 0.18/0.40 inference(skolemize,[status(sab)],[179])).
% 0.18/0.40 tff(181,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[180, 173])).
% 0.18/0.40 tff(182,plain,
% 0.18/0.40 ((~![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))) | (cTorF(iminus6) <=> ((iminus6 = iminus7) | (iminus6 = iplus7)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(183,plain,
% 0.18/0.40 (cTorF(iminus6) <=> ((iminus6 = iminus7) | (iminus6 = iplus7))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[182, 181])).
% 0.18/0.40 tff(184,plain,
% 0.18/0.40 ((~(cTorF(iminus6) <=> ((iminus6 = iminus7) | (iminus6 = iplus7)))) | (~cTorF(iminus6)) | ((iminus6 = iminus7) | (iminus6 = iplus7))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(185,plain,
% 0.18/0.40 ((~(cTorF(iminus6) <=> ((iminus6 = iminus7) | (iminus6 = iplus7)))) | ((iminus6 = iminus7) | (iminus6 = iplus7))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[184, 53])).
% 0.18/0.40 tff(186,plain,
% 0.18/0.40 ((iminus6 = iminus7) | (iminus6 = iplus7)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[185, 183])).
% 0.18/0.40 tff(187,plain,
% 0.18/0.40 ((~((iminus6 = iminus7) | (iminus6 = iplus7))) | (iminus6 = iminus7) | (iminus6 = iplus7)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(188,plain,
% 0.18/0.40 ((iminus6 = iminus7) | (iminus6 = iplus7)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[187, 186])).
% 0.18/0.40 tff(189,plain,
% 0.18/0.40 ($false),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[188, 171, 79])).
% 0.18/0.40 tff(190,plain,((iT = iminus2) | (iT = iminus6) | (iT = iminus1) | (iT = iminus5)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.40 tff(191,plain,
% 0.18/0.40 (iT = iminus2),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[190, 5, 4, 3])).
% 0.18/0.40 tff(192,plain,
% 0.18/0.40 ((iT = iminus4) <=> (iminus2 = iminus4)),
% 0.18/0.40 inference(monotonicity,[status(thm)],[191])).
% 0.18/0.40 tff(193,plain,
% 0.18/0.40 ((iminus2 = iminus4) <=> (iT = iminus4)),
% 0.18/0.40 inference(symmetry,[status(thm)],[192])).
% 0.18/0.40 tff(194,plain,
% 0.18/0.40 ((iminus2 = iF) <=> (iF = iminus2)),
% 0.18/0.40 inference(commutativity,[status(thm)],[])).
% 0.18/0.40 tff(195,plain,
% 0.18/0.40 ((iT = iminus6) <=> (iminus6 = iT)),
% 0.18/0.40 inference(symmetry,[status(thm)],[8])).
% 0.18/0.40 tff(196,plain,
% 0.18/0.40 ((~(iT = iminus6)) <=> (~(iminus6 = iT))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[195])).
% 0.18/0.40 tff(197,plain,
% 0.18/0.40 (~(iminus6 = iT)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[3, 196])).
% 0.18/0.40 tff(198,plain,
% 0.18/0.40 (^[X: $i] : refl((cTorF(X) <=> ((X = iF) | (X = iT))) <=> (cTorF(X) <=> ((X = iF) | (X = iT))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(199,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT))) <=> ![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[198])).
% 0.18/0.40 tff(200,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT))) <=> ![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(201,plain,
% 0.18/0.40 (^[X: $i] : rewrite((cTorF(X) <=> ((X = iT) | (X = iF))) <=> (cTorF(X) <=> ((X = iF) | (X = iT))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(202,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iT) | (X = iF))) <=> ![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[201])).
% 0.18/0.40 tff(203,axiom,(![X: $i] : (cTorF(X) <=> ((X = iT) | (X = iF)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_8')).
% 0.18/0.40 tff(204,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[203, 202])).
% 0.18/0.40 tff(205,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[204, 200])).
% 0.18/0.40 tff(206,plain,(
% 0.18/0.40 ![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))),
% 0.18/0.40 inference(skolemize,[status(sab)],[205])).
% 0.18/0.40 tff(207,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[206, 199])).
% 0.18/0.40 tff(208,plain,
% 0.18/0.40 ((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | (cTorF(iminus6) <=> ((iminus6 = iF) | (iminus6 = iT)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(209,plain,
% 0.18/0.40 (cTorF(iminus6) <=> ((iminus6 = iF) | (iminus6 = iT))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[208, 207])).
% 0.18/0.40 tff(210,plain,
% 0.18/0.40 ((~(cTorF(iminus6) <=> ((iminus6 = iF) | (iminus6 = iT)))) | (~cTorF(iminus6)) | ((iminus6 = iF) | (iminus6 = iT))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(211,plain,
% 0.18/0.40 ((~(cTorF(iminus6) <=> ((iminus6 = iF) | (iminus6 = iT)))) | ((iminus6 = iF) | (iminus6 = iT))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[210, 53])).
% 0.18/0.40 tff(212,plain,
% 0.18/0.40 ((iminus6 = iF) | (iminus6 = iT)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[211, 209])).
% 0.18/0.40 tff(213,plain,
% 0.18/0.40 ((~((iminus6 = iF) | (iminus6 = iT))) | (iminus6 = iF) | (iminus6 = iT)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(214,plain,
% 0.18/0.40 ((iminus6 = iF) | (iminus6 = iT)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[213, 212])).
% 0.18/0.40 tff(215,plain,
% 0.18/0.40 (iminus6 = iF),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[214, 197])).
% 0.18/0.40 tff(216,plain,
% 0.18/0.40 ((iminus2 = iminus6) <=> (iminus6 = iminus2)),
% 0.18/0.40 inference(commutativity,[status(thm)],[])).
% 0.18/0.40 tff(217,plain,
% 0.18/0.40 ((iT = iminus6) <=> (iminus2 = iminus6)),
% 0.18/0.40 inference(monotonicity,[status(thm)],[191])).
% 0.18/0.40 tff(218,plain,
% 0.18/0.40 ((iT = iminus6) <=> (iminus6 = iminus2)),
% 0.18/0.40 inference(transitivity,[status(thm)],[217, 216])).
% 0.18/0.40 tff(219,plain,
% 0.18/0.40 ((~(iT = iminus6)) <=> (~(iminus6 = iminus2))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[218])).
% 0.18/0.40 tff(220,plain,
% 0.18/0.40 (~(iminus6 = iminus2)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[3, 219])).
% 0.18/0.40 tff(221,plain,
% 0.18/0.40 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus2) | (X = iplus2))) <=> (cTorF(X) <=> ((X = iminus2) | (X = iplus2))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(222,plain,
% 0.18/0.40 (![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[221])).
% 0.18/0.41 tff(223,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(224,plain,
% 0.18/0.41 (^[X: $i] : rewrite((cTorF(X) <=> ((X = iplus2) | (X = iminus2))) <=> (cTorF(X) <=> ((X = iminus2) | (X = iplus2))))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(225,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iplus2) | (X = iminus2))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[224])).
% 0.18/0.41 tff(226,axiom,(![X: $i] : (cTorF(X) <=> ((X = iplus2) | (X = iminus2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_4')).
% 0.18/0.41 tff(227,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[226, 225])).
% 0.18/0.41 tff(228,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[227, 223])).
% 0.18/0.41 tff(229,plain,(
% 0.18/0.41 ![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))),
% 0.18/0.41 inference(skolemize,[status(sab)],[228])).
% 0.18/0.41 tff(230,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[229, 222])).
% 0.18/0.41 tff(231,plain,
% 0.18/0.41 ((~![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))) | (cTorF(iminus6) <=> ((iminus6 = iminus2) | (iminus6 = iplus2)))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(232,plain,
% 0.18/0.41 (cTorF(iminus6) <=> ((iminus6 = iminus2) | (iminus6 = iplus2))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[231, 230])).
% 0.18/0.41 tff(233,plain,
% 0.18/0.41 ((~(cTorF(iminus6) <=> ((iminus6 = iminus2) | (iminus6 = iplus2)))) | (~cTorF(iminus6)) | ((iminus6 = iminus2) | (iminus6 = iplus2))),
% 0.18/0.41 inference(tautology,[status(thm)],[])).
% 0.18/0.41 tff(234,plain,
% 0.18/0.41 ((iminus6 = iminus2) | (iminus6 = iplus2)),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[233, 53, 232])).
% 0.18/0.41 tff(235,plain,
% 0.18/0.41 ((~((iminus6 = iminus2) | (iminus6 = iplus2))) | (iminus6 = iminus2) | (iminus6 = iplus2)),
% 0.18/0.41 inference(tautology,[status(thm)],[])).
% 0.18/0.41 tff(236,plain,
% 0.18/0.41 ((iminus6 = iminus2) | (iminus6 = iplus2)),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[235, 234])).
% 0.18/0.41 tff(237,plain,
% 0.18/0.41 (iminus6 = iplus2),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[236, 220])).
% 0.18/0.41 tff(238,plain,
% 0.18/0.41 (iplus2 = iminus6),
% 0.18/0.41 inference(symmetry,[status(thm)],[237])).
% 0.18/0.41 tff(239,plain,
% 0.18/0.41 (iplus2 = iF),
% 0.18/0.41 inference(transitivity,[status(thm)],[238, 215])).
% 0.18/0.41 tff(240,plain,
% 0.18/0.41 ((iT = iplus2) <=> (iminus2 = iF)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[191, 239])).
% 0.18/0.41 tff(241,plain,
% 0.18/0.41 ((iT = iplus2) <=> (iF = iminus2)),
% 0.18/0.41 inference(transitivity,[status(thm)],[240, 194])).
% 0.18/0.41 tff(242,plain,
% 0.18/0.41 ((iF = iminus2) <=> (iT = iplus2)),
% 0.18/0.41 inference(symmetry,[status(thm)],[241])).
% 0.18/0.41 tff(243,plain,
% 0.18/0.41 ((~(iF = iminus2)) <=> (~(iT = iplus2))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[242])).
% 0.18/0.41 tff(244,plain,
% 0.18/0.41 ((iT = iF) <=> (iminus2 = iF)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[191])).
% 0.18/0.41 tff(245,plain,
% 0.18/0.41 ((iT = iF) <=> (iF = iminus2)),
% 0.18/0.41 inference(transitivity,[status(thm)],[244, 194])).
% 0.18/0.41 tff(246,plain,
% 0.18/0.41 ((~(iT = iF)) <=> (~(iF = iminus2))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[245])).
% 0.18/0.41 tff(247,plain,
% 0.18/0.41 ((~(iT = iF)) <=> (~(iT = iF))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(248,axiom,(~(iT = iF)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_77')).
% 0.18/0.41 tff(249,plain,
% 0.18/0.41 (~(iT = iF)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[248, 247])).
% 0.18/0.41 tff(250,plain,
% 0.18/0.41 (~(iF = iminus2)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[249, 246])).
% 0.18/0.41 tff(251,plain,
% 0.18/0.41 (~(iT = iplus2)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[250, 243])).
% 0.18/0.41 tff(252,plain,
% 0.18/0.41 (((iT = iplus2) | (iT = iplus4) | (iT = iminus1)) <=> ((iT = iplus2) | (iT = iplus4) | (iT = iminus1))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(253,plain,
% 0.18/0.41 ((((iT = iplus2) | (iT = iplus4)) | (iT = iminus1)) <=> ((iT = iplus2) | (iT = iplus4) | (iT = iminus1))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(254,axiom,(((iT = iplus2) | (iT = iplus4)) | (iT = iminus1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_37')).
% 0.18/0.41 tff(255,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus4) | (iT = iminus1)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[254, 253])).
% 0.18/0.41 tff(256,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus4) | (iT = iminus1)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[255, 252])).
% 0.18/0.41 tff(257,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus4) | (iT = iminus1)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[256, 252])).
% 0.18/0.41 tff(258,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus4) | (iT = iminus1)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[257, 252])).
% 0.18/0.41 tff(259,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus4) | (iT = iminus1)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[258, 252])).
% 0.18/0.41 tff(260,plain,
% 0.18/0.41 (iT = iplus4),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[259, 251, 4])).
% 0.18/0.41 tff(261,plain,
% 0.18/0.41 (iplus4 = iT),
% 0.18/0.41 inference(symmetry,[status(thm)],[260])).
% 0.18/0.41 tff(262,plain,
% 0.18/0.41 (iplus4 = iminus2),
% 0.18/0.41 inference(transitivity,[status(thm)],[261, 191])).
% 0.18/0.41 tff(263,plain,
% 0.18/0.41 ((iF = iplus4) <=> (iF = iminus2)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[262])).
% 0.18/0.41 tff(264,plain,
% 0.18/0.41 ((iF = iminus2) <=> (iF = iplus4)),
% 0.18/0.41 inference(symmetry,[status(thm)],[263])).
% 0.18/0.41 tff(265,plain,
% 0.18/0.41 ((~(iF = iminus2)) <=> (~(iF = iplus4))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[264])).
% 0.18/0.41 tff(266,plain,
% 0.18/0.41 (~(iF = iplus4)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[250, 265])).
% 0.18/0.41 tff(267,plain,
% 0.18/0.41 ((~![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))) | (cTorF(iF) <=> ((iF = iminus4) | (iF = iplus4)))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(268,plain,
% 0.18/0.41 (cTorF(iF) <=> ((iF = iminus4) | (iF = iplus4))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[267, 143])).
% 0.18/0.41 tff(269,plain,
% 0.18/0.41 (((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | cTorF(iF)) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | cTorF(iF))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(270,plain,
% 0.18/0.41 ((cTorF(iF) <=> $true) <=> cTorF(iF)),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(271,plain,
% 0.18/0.41 (($true | (iF = iT)) <=> $true),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(272,plain,
% 0.18/0.41 ((iF = iF) <=> $true),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(273,plain,
% 0.18/0.41 (((iF = iF) | (iF = iT)) <=> ($true | (iF = iT))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[272])).
% 0.18/0.41 tff(274,plain,
% 0.18/0.41 (((iF = iF) | (iF = iT)) <=> $true),
% 0.18/0.41 inference(transitivity,[status(thm)],[273, 271])).
% 0.18/0.41 tff(275,plain,
% 0.18/0.41 ((cTorF(iF) <=> ((iF = iF) | (iF = iT))) <=> (cTorF(iF) <=> $true)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[274])).
% 0.18/0.41 tff(276,plain,
% 0.18/0.41 ((cTorF(iF) <=> ((iF = iF) | (iF = iT))) <=> cTorF(iF)),
% 0.18/0.41 inference(transitivity,[status(thm)],[275, 270])).
% 0.18/0.41 tff(277,plain,
% 0.18/0.41 (((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | (cTorF(iF) <=> ((iF = iF) | (iF = iT)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | cTorF(iF))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[276])).
% 0.18/0.41 tff(278,plain,
% 0.18/0.41 (((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | (cTorF(iF) <=> ((iF = iF) | (iF = iT)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | cTorF(iF))),
% 0.18/0.41 inference(transitivity,[status(thm)],[277, 269])).
% 0.18/0.41 tff(279,plain,
% 0.18/0.41 ((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | (cTorF(iF) <=> ((iF = iF) | (iF = iT)))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(280,plain,
% 0.18/0.41 ((~![X: $i] : (cTorF(X) <=> ((X = iF) | (X = iT)))) | cTorF(iF)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[279, 278])).
% 0.18/0.41 tff(281,plain,
% 0.18/0.41 (cTorF(iF)),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[280, 207])).
% 0.18/0.41 tff(282,plain,
% 0.18/0.41 ((~(cTorF(iF) <=> ((iF = iminus4) | (iF = iplus4)))) | (~cTorF(iF)) | ((iF = iminus4) | (iF = iplus4))),
% 0.18/0.41 inference(tautology,[status(thm)],[])).
% 0.18/0.41 tff(283,plain,
% 0.18/0.41 ((~(cTorF(iF) <=> ((iF = iminus4) | (iF = iplus4)))) | ((iF = iminus4) | (iF = iplus4))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[282, 281])).
% 0.18/0.41 tff(284,plain,
% 0.18/0.41 ((iF = iminus4) | (iF = iplus4)),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[283, 268])).
% 0.18/0.41 tff(285,plain,
% 0.18/0.41 ((~((iF = iminus4) | (iF = iplus4))) | (iF = iminus4) | (iF = iplus4)),
% 0.18/0.41 inference(tautology,[status(thm)],[])).
% 0.18/0.41 tff(286,plain,
% 0.18/0.41 ((iF = iminus4) | (iF = iplus4)),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[285, 284])).
% 0.18/0.41 tff(287,plain,
% 0.18/0.41 (iF = iminus4),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[286, 266])).
% 0.18/0.41 tff(288,plain,
% 0.18/0.41 (iminus4 = iF),
% 0.18/0.41 inference(symmetry,[status(thm)],[287])).
% 0.18/0.41 tff(289,plain,
% 0.18/0.41 ((iminus2 = iminus4) <=> (iminus2 = iF)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[288])).
% 0.18/0.41 tff(290,plain,
% 0.18/0.41 ((iminus2 = iminus4) <=> (iF = iminus2)),
% 0.18/0.41 inference(transitivity,[status(thm)],[289, 194])).
% 0.18/0.41 tff(291,plain,
% 0.18/0.41 ((iF = iminus2) <=> (iminus2 = iminus4)),
% 0.18/0.41 inference(symmetry,[status(thm)],[290])).
% 0.18/0.41 tff(292,plain,
% 0.18/0.41 ((iF = iminus2) <=> (iT = iminus4)),
% 0.18/0.41 inference(transitivity,[status(thm)],[291, 193])).
% 0.18/0.41 tff(293,plain,
% 0.18/0.41 ((~(iF = iminus2)) <=> (~(iT = iminus4))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[292])).
% 0.18/0.41 tff(294,plain,
% 0.18/0.41 (~(iT = iminus4)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[250, 293])).
% 0.18/0.41 tff(295,plain,
% 0.18/0.41 ((iT = iminus8) <=> (iminus2 = iminus8)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[191])).
% 0.18/0.41 tff(296,plain,
% 0.18/0.41 ((iminus2 = iminus8) <=> (iT = iminus8)),
% 0.18/0.41 inference(symmetry,[status(thm)],[295])).
% 0.18/0.41 tff(297,plain,
% 0.18/0.41 (((iT = iplus2) | (iT = iplus8) | (iT = iminus4)) <=> ((iT = iplus2) | (iT = iplus8) | (iT = iminus4))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(298,plain,
% 0.18/0.41 ((((iT = iplus2) | (iT = iplus8)) | (iT = iminus4)) <=> ((iT = iplus2) | (iT = iplus8) | (iT = iminus4))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(299,plain,
% 0.18/0.41 (((iT = iplus8) | (iT = iplus2)) <=> ((iT = iplus2) | (iT = iplus8))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(300,plain,
% 0.18/0.41 ((((iT = iplus8) | (iT = iplus2)) | (iT = iminus4)) <=> (((iT = iplus2) | (iT = iplus8)) | (iT = iminus4))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[299])).
% 0.18/0.41 tff(301,plain,
% 0.18/0.41 ((((iT = iplus8) | (iT = iplus2)) | (iT = iminus4)) <=> ((iT = iplus2) | (iT = iplus8) | (iT = iminus4))),
% 0.18/0.41 inference(transitivity,[status(thm)],[300, 298])).
% 0.18/0.41 tff(302,axiom,(((iT = iplus8) | (iT = iplus2)) | (iT = iminus4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_31')).
% 0.18/0.41 tff(303,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus8) | (iT = iminus4)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[302, 301])).
% 0.18/0.41 tff(304,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus8) | (iT = iminus4)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[303, 297])).
% 0.18/0.41 tff(305,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus8) | (iT = iminus4)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[304, 297])).
% 0.18/0.41 tff(306,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus8) | (iT = iminus4)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[305, 297])).
% 0.18/0.41 tff(307,plain,
% 0.18/0.41 ((iT = iplus2) | (iT = iplus8) | (iT = iminus4)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[306, 297])).
% 0.18/0.41 tff(308,plain,
% 0.18/0.41 (iT = iplus8),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[307, 294, 251])).
% 0.18/0.41 tff(309,plain,
% 0.18/0.41 (iplus8 = iT),
% 0.18/0.41 inference(symmetry,[status(thm)],[308])).
% 0.18/0.41 tff(310,plain,
% 0.18/0.41 (iplus8 = iminus2),
% 0.18/0.41 inference(transitivity,[status(thm)],[309, 191])).
% 0.18/0.41 tff(311,plain,
% 0.18/0.41 ((iF = iplus8) <=> (iF = iminus2)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[310])).
% 0.18/0.41 tff(312,plain,
% 0.18/0.41 ((iF = iminus2) <=> (iF = iplus8)),
% 0.18/0.41 inference(symmetry,[status(thm)],[311])).
% 0.18/0.41 tff(313,plain,
% 0.18/0.41 ((~(iF = iminus2)) <=> (~(iF = iplus8))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[312])).
% 0.18/0.41 tff(314,plain,
% 0.18/0.41 (~(iF = iplus8)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[250, 313])).
% 0.18/0.41 tff(315,plain,
% 0.18/0.41 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus8) | (X = iplus8))) <=> (cTorF(X) <=> ((X = iminus8) | (X = iplus8))))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(316,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[315])).
% 0.18/0.41 tff(317,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(318,plain,
% 0.18/0.41 (^[X: $i] : rewrite((cTorF(X) <=> ((X = iplus8) | (X = iminus8))) <=> (cTorF(X) <=> ((X = iminus8) | (X = iplus8))))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(319,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iplus8) | (X = iminus8))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[318])).
% 0.18/0.41 tff(320,axiom,(![X: $i] : (cTorF(X) <=> ((X = iplus8) | (X = iminus8)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_9')).
% 0.18/0.41 tff(321,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[320, 319])).
% 0.18/0.41 tff(322,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[321, 317])).
% 0.18/0.41 tff(323,plain,(
% 0.18/0.41 ![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))),
% 0.18/0.41 inference(skolemize,[status(sab)],[322])).
% 0.18/0.41 tff(324,plain,
% 0.18/0.41 (![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[323, 316])).
% 0.18/0.41 tff(325,plain,
% 0.18/0.41 ((~![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))) | (cTorF(iF) <=> ((iF = iminus8) | (iF = iplus8)))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(326,plain,
% 0.18/0.41 (cTorF(iF) <=> ((iF = iminus8) | (iF = iplus8))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[325, 324])).
% 0.18/0.41 tff(327,plain,
% 0.18/0.41 ((~(cTorF(iF) <=> ((iF = iminus8) | (iF = iplus8)))) | (~cTorF(iF)) | ((iF = iminus8) | (iF = iplus8))),
% 0.18/0.41 inference(tautology,[status(thm)],[])).
% 0.18/0.41 tff(328,plain,
% 0.18/0.41 ((iF = iminus8) | (iF = iplus8)),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[327, 281, 326])).
% 0.18/0.41 tff(329,plain,
% 0.18/0.41 ((~((iF = iminus8) | (iF = iplus8))) | (iF = iminus8) | (iF = iplus8)),
% 0.18/0.41 inference(tautology,[status(thm)],[])).
% 0.18/0.41 tff(330,plain,
% 0.18/0.41 ((iF = iminus8) | (iF = iplus8)),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[329, 328])).
% 0.18/0.41 tff(331,plain,
% 0.18/0.41 (iF = iminus8),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[330, 314])).
% 0.18/0.41 tff(332,plain,
% 0.18/0.41 (iminus8 = iF),
% 0.18/0.41 inference(symmetry,[status(thm)],[331])).
% 0.18/0.41 tff(333,plain,
% 0.18/0.41 ((iminus2 = iminus8) <=> (iminus2 = iF)),
% 0.18/0.41 inference(monotonicity,[status(thm)],[332])).
% 0.18/0.42 tff(334,plain,
% 0.18/0.42 ((iminus2 = iminus8) <=> (iF = iminus2)),
% 0.18/0.42 inference(transitivity,[status(thm)],[333, 194])).
% 0.18/0.42 tff(335,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iminus2 = iminus8)),
% 0.18/0.42 inference(symmetry,[status(thm)],[334])).
% 0.18/0.42 tff(336,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iT = iminus8)),
% 0.18/0.42 inference(transitivity,[status(thm)],[335, 296])).
% 0.18/0.42 tff(337,plain,
% 0.18/0.42 ((~(iF = iminus2)) <=> (~(iT = iminus8))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[336])).
% 0.18/0.42 tff(338,plain,
% 0.18/0.42 (~(iT = iminus8)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[250, 337])).
% 0.18/0.42 tff(339,plain,
% 0.18/0.42 ((iT = iminus9) <=> (iminus2 = iminus9)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[191])).
% 0.18/0.42 tff(340,plain,
% 0.18/0.42 ((iminus2 = iminus9) <=> (iT = iminus9)),
% 0.18/0.42 inference(symmetry,[status(thm)],[339])).
% 0.18/0.42 tff(341,plain,
% 0.18/0.42 ((iT = iplus7) <=> (iminus2 = iplus7)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[191])).
% 0.18/0.42 tff(342,plain,
% 0.18/0.42 ((iminus2 = iplus7) <=> (iT = iplus7)),
% 0.18/0.42 inference(symmetry,[status(thm)],[341])).
% 0.18/0.42 tff(343,plain,
% 0.18/0.42 (((iT = iplus2) | (iT = iminus7) | (iT = iminus5)) <=> ((iT = iplus2) | (iT = iminus7) | (iT = iminus5))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(344,plain,
% 0.18/0.42 ((((iT = iminus5) | (iT = iplus2)) | (iT = iminus7)) <=> ((iT = iplus2) | (iT = iminus7) | (iT = iminus5))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(345,axiom,(((iT = iminus5) | (iT = iplus2)) | (iT = iminus7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_50')).
% 0.18/0.42 tff(346,plain,
% 0.18/0.42 ((iT = iplus2) | (iT = iminus7) | (iT = iminus5)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[345, 344])).
% 0.18/0.42 tff(347,plain,
% 0.18/0.42 ((iT = iplus2) | (iT = iminus7) | (iT = iminus5)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[346, 343])).
% 0.18/0.42 tff(348,plain,
% 0.18/0.42 ((iT = iplus2) | (iT = iminus7) | (iT = iminus5)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[347, 343])).
% 0.18/0.42 tff(349,plain,
% 0.18/0.42 ((iT = iplus2) | (iT = iminus7) | (iT = iminus5)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[348, 343])).
% 0.18/0.42 tff(350,plain,
% 0.18/0.42 ((iT = iplus2) | (iT = iminus7) | (iT = iminus5)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[349, 343])).
% 0.18/0.42 tff(351,plain,
% 0.18/0.42 (iT = iminus7),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[350, 251, 5])).
% 0.18/0.42 tff(352,plain,
% 0.18/0.42 (iminus7 = iT),
% 0.18/0.42 inference(symmetry,[status(thm)],[351])).
% 0.18/0.42 tff(353,plain,
% 0.18/0.42 (iminus7 = iminus2),
% 0.18/0.42 inference(transitivity,[status(thm)],[352, 191])).
% 0.18/0.42 tff(354,plain,
% 0.18/0.42 ((iF = iminus7) <=> (iF = iminus2)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[353])).
% 0.18/0.42 tff(355,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iF = iminus7)),
% 0.18/0.42 inference(symmetry,[status(thm)],[354])).
% 0.18/0.42 tff(356,plain,
% 0.18/0.42 ((~(iF = iminus2)) <=> (~(iF = iminus7))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[355])).
% 0.18/0.42 tff(357,plain,
% 0.18/0.42 (~(iF = iminus7)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[250, 356])).
% 0.18/0.42 tff(358,plain,
% 0.18/0.42 ((~![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))) | (cTorF(iF) <=> ((iF = iminus7) | (iF = iplus7)))),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(359,plain,
% 0.18/0.42 (cTorF(iF) <=> ((iF = iminus7) | (iF = iplus7))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[358, 181])).
% 0.18/0.42 tff(360,plain,
% 0.18/0.42 ((~(cTorF(iF) <=> ((iF = iminus7) | (iF = iplus7)))) | (~cTorF(iF)) | ((iF = iminus7) | (iF = iplus7))),
% 0.18/0.42 inference(tautology,[status(thm)],[])).
% 0.18/0.42 tff(361,plain,
% 0.18/0.42 ((iF = iminus7) | (iF = iplus7)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[360, 281, 359])).
% 0.18/0.42 tff(362,plain,
% 0.18/0.42 ((~((iF = iminus7) | (iF = iplus7))) | (iF = iminus7) | (iF = iplus7)),
% 0.18/0.42 inference(tautology,[status(thm)],[])).
% 0.18/0.42 tff(363,plain,
% 0.18/0.42 ((iF = iminus7) | (iF = iplus7)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[362, 361])).
% 0.18/0.42 tff(364,plain,
% 0.18/0.42 (iF = iplus7),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[363, 357])).
% 0.18/0.42 tff(365,plain,
% 0.18/0.42 (iplus7 = iF),
% 0.18/0.42 inference(symmetry,[status(thm)],[364])).
% 0.18/0.42 tff(366,plain,
% 0.18/0.42 ((iminus2 = iplus7) <=> (iminus2 = iF)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[365])).
% 0.18/0.42 tff(367,plain,
% 0.18/0.42 ((iminus2 = iplus7) <=> (iF = iminus2)),
% 0.18/0.42 inference(transitivity,[status(thm)],[366, 194])).
% 0.18/0.42 tff(368,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iminus2 = iplus7)),
% 0.18/0.42 inference(symmetry,[status(thm)],[367])).
% 0.18/0.42 tff(369,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iT = iplus7)),
% 0.18/0.42 inference(transitivity,[status(thm)],[368, 342])).
% 0.18/0.42 tff(370,plain,
% 0.18/0.42 ((~(iF = iminus2)) <=> (~(iT = iplus7))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[369])).
% 0.18/0.42 tff(371,plain,
% 0.18/0.42 (~(iT = iplus7)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[250, 370])).
% 0.18/0.42 tff(372,plain,
% 0.18/0.42 (iT = iplus9),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[164, 371, 294])).
% 0.18/0.42 tff(373,plain,
% 0.18/0.42 (iplus9 = iT),
% 0.18/0.42 inference(symmetry,[status(thm)],[372])).
% 0.18/0.42 tff(374,plain,
% 0.18/0.42 (iplus9 = iminus2),
% 0.18/0.42 inference(transitivity,[status(thm)],[373, 191])).
% 0.18/0.42 tff(375,plain,
% 0.18/0.42 ((iF = iplus9) <=> (iF = iminus2)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[374])).
% 0.18/0.42 tff(376,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iF = iplus9)),
% 0.18/0.42 inference(symmetry,[status(thm)],[375])).
% 0.18/0.42 tff(377,plain,
% 0.18/0.42 ((~(iF = iminus2)) <=> (~(iF = iplus9))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[376])).
% 0.18/0.42 tff(378,plain,
% 0.18/0.42 (~(iF = iplus9)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[250, 377])).
% 0.18/0.42 tff(379,plain,
% 0.18/0.42 ((~![X: $i] : (cTorF(X) <=> ((X = iminus9) | (X = iplus9)))) | (cTorF(iF) <=> ((iF = iminus9) | (iF = iplus9)))),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(380,plain,
% 0.18/0.42 (cTorF(iF) <=> ((iF = iminus9) | (iF = iplus9))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[379, 31])).
% 0.18/0.42 tff(381,plain,
% 0.18/0.42 ((~(cTorF(iF) <=> ((iF = iminus9) | (iF = iplus9)))) | (~cTorF(iF)) | ((iF = iminus9) | (iF = iplus9))),
% 0.18/0.42 inference(tautology,[status(thm)],[])).
% 0.18/0.42 tff(382,plain,
% 0.18/0.42 ((iF = iminus9) | (iF = iplus9)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[381, 281, 380])).
% 0.18/0.42 tff(383,plain,
% 0.18/0.42 ((~((iF = iminus9) | (iF = iplus9))) | (iF = iminus9) | (iF = iplus9)),
% 0.18/0.42 inference(tautology,[status(thm)],[])).
% 0.18/0.42 tff(384,plain,
% 0.18/0.42 ((iF = iminus9) | (iF = iplus9)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[383, 382])).
% 0.18/0.42 tff(385,plain,
% 0.18/0.42 (iF = iminus9),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[384, 378])).
% 0.18/0.42 tff(386,plain,
% 0.18/0.42 (iminus9 = iF),
% 0.18/0.42 inference(symmetry,[status(thm)],[385])).
% 0.18/0.42 tff(387,plain,
% 0.18/0.42 ((iminus2 = iminus9) <=> (iminus2 = iF)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[386])).
% 0.18/0.42 tff(388,plain,
% 0.18/0.42 ((iminus2 = iminus9) <=> (iF = iminus2)),
% 0.18/0.42 inference(transitivity,[status(thm)],[387, 194])).
% 0.18/0.42 tff(389,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iminus2 = iminus9)),
% 0.18/0.42 inference(symmetry,[status(thm)],[388])).
% 0.18/0.42 tff(390,plain,
% 0.18/0.42 ((iF = iminus2) <=> (iT = iminus9)),
% 0.18/0.42 inference(transitivity,[status(thm)],[389, 340])).
% 0.18/0.42 tff(391,plain,
% 0.18/0.42 ((~(iF = iminus2)) <=> (~(iT = iminus9))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[390])).
% 0.18/0.42 tff(392,plain,
% 0.18/0.42 (~(iT = iminus9)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[250, 391])).
% 0.18/0.42 tff(393,plain,
% 0.18/0.42 (((iT = iminus9) | (iT = iminus8) | (iT = iminus4)) <=> ((iT = iminus9) | (iT = iminus8) | (iT = iminus4))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(394,plain,
% 0.18/0.42 ((((iT = iminus8) | (iT = iminus9)) | (iT = iminus4)) <=> ((iT = iminus9) | (iT = iminus8) | (iT = iminus4))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(395,axiom,(((iT = iminus8) | (iT = iminus9)) | (iT = iminus4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_40')).
% 0.18/0.42 tff(396,plain,
% 0.18/0.42 ((iT = iminus9) | (iT = iminus8) | (iT = iminus4)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[395, 394])).
% 0.18/0.42 tff(397,plain,
% 0.18/0.42 ((iT = iminus9) | (iT = iminus8) | (iT = iminus4)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[396, 393])).
% 0.18/0.42 tff(398,plain,
% 0.18/0.42 ((iT = iminus9) | (iT = iminus8) | (iT = iminus4)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[397, 393])).
% 0.18/0.42 tff(399,plain,
% 0.18/0.42 ((iT = iminus9) | (iT = iminus8) | (iT = iminus4)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[398, 393])).
% 0.18/0.42 tff(400,plain,
% 0.18/0.42 ((iT = iminus9) | (iT = iminus8) | (iT = iminus4)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[399, 393])).
% 0.18/0.42 tff(401,plain,
% 0.18/0.42 ($false),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[400, 392, 338, 294])).
% 0.18/0.42 tff(402,plain,((iT = iminus5) | (iT = iminus1) | (iT = iminus6)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.42 tff(403,plain,
% 0.18/0.42 (iT = iminus5),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[402, 4, 3])).
% 0.18/0.42 tff(404,plain,
% 0.18/0.42 ((iminus5 = iF) <=> (iF = iminus5)),
% 0.18/0.42 inference(commutativity,[status(thm)],[])).
% 0.18/0.42 tff(405,plain,
% 0.18/0.42 ((iminus5 = iminus6) <=> (iminus6 = iminus5)),
% 0.18/0.42 inference(commutativity,[status(thm)],[])).
% 0.18/0.42 tff(406,plain,
% 0.18/0.42 ((iT = iminus6) <=> (iminus5 = iminus6)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[403])).
% 0.18/0.42 tff(407,plain,
% 0.18/0.42 ((iT = iminus6) <=> (iminus6 = iminus5)),
% 0.18/0.42 inference(transitivity,[status(thm)],[406, 405])).
% 0.18/0.42 tff(408,plain,
% 0.18/0.42 ((~(iT = iminus6)) <=> (~(iminus6 = iminus5))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[407])).
% 0.18/0.42 tff(409,plain,
% 0.18/0.42 (~(iminus6 = iminus5)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[3, 408])).
% 0.18/0.42 tff(410,plain,
% 0.18/0.42 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus5) | (X = iplus5))) <=> (cTorF(X) <=> ((X = iminus5) | (X = iplus5))))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(411,plain,
% 0.18/0.42 (![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[410])).
% 0.18/0.42 tff(412,plain,
% 0.18/0.42 (![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(413,plain,
% 0.18/0.42 (^[X: $i] : rewrite((cTorF(X) <=> ((X = iplus5) | (X = iminus5))) <=> (cTorF(X) <=> ((X = iminus5) | (X = iplus5))))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(414,plain,
% 0.18/0.42 (![X: $i] : (cTorF(X) <=> ((X = iplus5) | (X = iminus5))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[413])).
% 0.18/0.42 tff(415,axiom,(![X: $i] : (cTorF(X) <=> ((X = iplus5) | (X = iminus5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_6')).
% 0.18/0.42 tff(416,plain,
% 0.18/0.42 (![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[415, 414])).
% 0.18/0.42 tff(417,plain,
% 0.18/0.42 (![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[416, 412])).
% 0.18/0.42 tff(418,plain,(
% 0.18/0.42 ![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))),
% 0.18/0.42 inference(skolemize,[status(sab)],[417])).
% 0.18/0.42 tff(419,plain,
% 0.18/0.42 (![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[418, 411])).
% 0.18/0.42 tff(420,plain,
% 0.18/0.42 ((~![X: $i] : (cTorF(X) <=> ((X = iminus5) | (X = iplus5)))) | (cTorF(iminus6) <=> ((iminus6 = iminus5) | (iminus6 = iplus5)))),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(421,plain,
% 0.18/0.42 (cTorF(iminus6) <=> ((iminus6 = iminus5) | (iminus6 = iplus5))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[420, 419])).
% 0.18/0.42 tff(422,plain,
% 0.18/0.42 ((~(cTorF(iminus6) <=> ((iminus6 = iminus5) | (iminus6 = iplus5)))) | (~cTorF(iminus6)) | ((iminus6 = iminus5) | (iminus6 = iplus5))),
% 0.18/0.42 inference(tautology,[status(thm)],[])).
% 0.18/0.42 tff(423,plain,
% 0.18/0.42 ((~(cTorF(iminus6) <=> ((iminus6 = iminus5) | (iminus6 = iplus5)))) | ((iminus6 = iminus5) | (iminus6 = iplus5))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[422, 53])).
% 0.18/0.42 tff(424,plain,
% 0.18/0.42 ((iminus6 = iminus5) | (iminus6 = iplus5)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[423, 421])).
% 0.18/0.42 tff(425,plain,
% 0.18/0.42 ((~((iminus6 = iminus5) | (iminus6 = iplus5))) | (iminus6 = iminus5) | (iminus6 = iplus5)),
% 0.18/0.42 inference(tautology,[status(thm)],[])).
% 0.18/0.42 tff(426,plain,
% 0.18/0.42 ((iminus6 = iminus5) | (iminus6 = iplus5)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[425, 424])).
% 0.18/0.42 tff(427,plain,
% 0.18/0.42 (iminus6 = iplus5),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[426, 409])).
% 0.18/0.42 tff(428,plain,
% 0.18/0.42 (iplus5 = iminus6),
% 0.18/0.42 inference(symmetry,[status(thm)],[427])).
% 0.18/0.42 tff(429,plain,
% 0.18/0.42 (iplus5 = iF),
% 0.18/0.42 inference(transitivity,[status(thm)],[428, 215])).
% 0.18/0.42 tff(430,plain,
% 0.18/0.42 ((iT = iplus5) <=> (iminus5 = iF)),
% 0.18/0.42 inference(monotonicity,[status(thm)],[403, 429])).
% 0.18/0.42 tff(431,plain,
% 0.18/0.42 ((iT = iplus5) <=> (iF = iminus5)),
% 0.18/0.42 inference(transitivity,[status(thm)],[430, 404])).
% 0.18/0.42 tff(432,plain,
% 0.18/0.42 ((iF = iminus5) <=> (iT = iplus5)),
% 0.18/0.42 inference(symmetry,[status(thm)],[431])).
% 0.18/0.42 tff(433,plain,
% 0.18/0.42 ((~(iF = iminus5)) <=> (~(iT = iplus5))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[432])).
% 0.18/0.42 tff(434,plain,
% 0.18/0.42 ((iT = iF) <=> (iminus5 = iF)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[403])).
% 0.18/0.43 tff(435,plain,
% 0.18/0.43 ((iT = iF) <=> (iF = iminus5)),
% 0.18/0.43 inference(transitivity,[status(thm)],[434, 404])).
% 0.18/0.43 tff(436,plain,
% 0.18/0.43 ((~(iT = iF)) <=> (~(iF = iminus5))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[435])).
% 0.18/0.43 tff(437,plain,
% 0.18/0.43 (~(iF = iminus5)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[249, 436])).
% 0.18/0.43 tff(438,plain,
% 0.18/0.43 (~(iT = iplus5)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[437, 433])).
% 0.18/0.43 tff(439,assumption,(~(iT = iplus4)), introduced(assumption)).
% 0.18/0.43 tff(440,plain,
% 0.18/0.43 (iT = iplus2),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[259, 439, 4])).
% 0.18/0.43 tff(441,plain,
% 0.18/0.43 (iplus2 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[440])).
% 0.18/0.43 tff(442,plain,
% 0.18/0.43 (iplus2 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[441, 403])).
% 0.18/0.43 tff(443,plain,
% 0.18/0.43 ((iF = iplus2) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[442])).
% 0.18/0.43 tff(444,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iplus2)),
% 0.18/0.43 inference(symmetry,[status(thm)],[443])).
% 0.18/0.43 tff(445,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iplus2))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[444])).
% 0.18/0.43 tff(446,plain,
% 0.18/0.43 (~(iF = iplus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[437, 445])).
% 0.18/0.43 tff(447,plain,
% 0.18/0.43 (iT = iminus2),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[129, 439, 3])).
% 0.18/0.43 tff(448,plain,
% 0.18/0.43 (iminus2 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[447])).
% 0.18/0.43 tff(449,plain,
% 0.18/0.43 (iminus2 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[448, 403])).
% 0.18/0.43 tff(450,plain,
% 0.18/0.43 ((iF = iminus2) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[449])).
% 0.18/0.43 tff(451,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iminus2)),
% 0.18/0.43 inference(symmetry,[status(thm)],[450])).
% 0.18/0.43 tff(452,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iminus2))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[451])).
% 0.18/0.43 tff(453,plain,
% 0.18/0.43 (~(iF = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[437, 452])).
% 0.18/0.43 tff(454,plain,
% 0.18/0.43 ((~![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))) | (cTorF(iF) <=> ((iF = iminus2) | (iF = iplus2)))),
% 0.18/0.43 inference(quant_inst,[status(thm)],[])).
% 0.18/0.43 tff(455,plain,
% 0.18/0.43 (cTorF(iF) <=> ((iF = iminus2) | (iF = iplus2))),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[454, 230])).
% 0.18/0.43 tff(456,plain,
% 0.18/0.43 ((~(cTorF(iF) <=> ((iF = iminus2) | (iF = iplus2)))) | (~cTorF(iF)) | ((iF = iminus2) | (iF = iplus2))),
% 0.18/0.43 inference(tautology,[status(thm)],[])).
% 0.18/0.43 tff(457,plain,
% 0.18/0.43 ((~(cTorF(iF) <=> ((iF = iminus2) | (iF = iplus2)))) | ((iF = iminus2) | (iF = iplus2))),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[456, 281])).
% 0.18/0.43 tff(458,plain,
% 0.18/0.43 ((iF = iminus2) | (iF = iplus2)),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[457, 455])).
% 0.18/0.43 tff(459,plain,
% 0.18/0.43 ((~((iF = iminus2) | (iF = iplus2))) | (iF = iminus2) | (iF = iplus2)),
% 0.18/0.43 inference(tautology,[status(thm)],[])).
% 0.18/0.43 tff(460,plain,
% 0.18/0.43 ((iF = iminus2) | (iF = iplus2)),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[459, 458])).
% 0.18/0.43 tff(461,plain,
% 0.18/0.43 ($false),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[460, 453, 446])).
% 0.18/0.43 tff(462,plain,((iT = iplus4) | (iT = iminus6) | (iT = iminus1)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.43 tff(463,plain,
% 0.18/0.43 (iT = iplus4),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[462, 4, 3])).
% 0.18/0.43 tff(464,plain,
% 0.18/0.43 (iplus4 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[463])).
% 0.18/0.43 tff(465,plain,
% 0.18/0.43 (iplus4 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[464, 403])).
% 0.18/0.43 tff(466,plain,
% 0.18/0.43 ((iF = iplus4) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[465])).
% 0.18/0.43 tff(467,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iplus4)),
% 0.18/0.43 inference(symmetry,[status(thm)],[466])).
% 0.18/0.43 tff(468,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iplus4))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[467])).
% 0.18/0.43 tff(469,plain,
% 0.18/0.43 (~(iF = iplus4)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[437, 468])).
% 0.18/0.43 tff(470,plain,
% 0.18/0.43 (iF = iminus4),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[286, 469])).
% 0.18/0.43 tff(471,plain,
% 0.18/0.43 (iminus4 = iF),
% 0.18/0.43 inference(symmetry,[status(thm)],[470])).
% 0.18/0.43 tff(472,plain,
% 0.18/0.43 ((iT = iminus4) <=> (iminus5 = iF)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[403, 471])).
% 0.18/0.43 tff(473,plain,
% 0.18/0.43 ((iT = iminus4) <=> (iF = iminus5)),
% 0.18/0.43 inference(transitivity,[status(thm)],[472, 404])).
% 0.18/0.43 tff(474,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iT = iminus4)),
% 0.18/0.43 inference(symmetry,[status(thm)],[473])).
% 0.18/0.43 tff(475,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iT = iminus4))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[474])).
% 0.18/0.43 tff(476,plain,
% 0.18/0.43 (~(iT = iminus4)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[437, 475])).
% 0.18/0.43 tff(477,plain,
% 0.18/0.43 (((iT = iplus9) | (iT = iplus5) | (iT = iminus4)) <=> ((iT = iplus9) | (iT = iplus5) | (iT = iminus4))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(478,plain,
% 0.18/0.43 ((((iT = iplus5) | (iT = iminus4)) | (iT = iplus9)) <=> ((iT = iplus9) | (iT = iplus5) | (iT = iminus4))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(479,plain,
% 0.18/0.43 (((iT = iplus5) | (iT = iminus4)) <=> ((iT = iplus5) | (iT = iminus4))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(480,plain,
% 0.18/0.43 ((((iT = iplus5) | (iT = iminus4)) | (iT = iplus9)) <=> (((iT = iplus5) | (iT = iminus4)) | (iT = iplus9))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[479])).
% 0.18/0.43 tff(481,plain,
% 0.18/0.43 ((((iT = iplus5) | (iT = iminus4)) | (iT = iplus9)) <=> ((iT = iplus9) | (iT = iplus5) | (iT = iminus4))),
% 0.18/0.43 inference(transitivity,[status(thm)],[480, 478])).
% 0.18/0.43 tff(482,axiom,(((iT = iplus5) | (iT = iminus4)) | (iT = iplus9)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_32')).
% 0.18/0.43 tff(483,plain,
% 0.18/0.43 ((iT = iplus9) | (iT = iplus5) | (iT = iminus4)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[482, 481])).
% 0.18/0.43 tff(484,plain,
% 0.18/0.43 ((iT = iplus9) | (iT = iplus5) | (iT = iminus4)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[483, 477])).
% 0.18/0.43 tff(485,plain,
% 0.18/0.43 ((iT = iplus9) | (iT = iplus5) | (iT = iminus4)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[484, 477])).
% 0.18/0.43 tff(486,plain,
% 0.18/0.43 ((iT = iplus9) | (iT = iplus5) | (iT = iminus4)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[485, 477])).
% 0.18/0.43 tff(487,plain,
% 0.18/0.43 ((iT = iplus9) | (iT = iplus5) | (iT = iminus4)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[486, 477])).
% 0.18/0.43 tff(488,plain,
% 0.18/0.43 (iT = iplus9),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[487, 476, 438])).
% 0.18/0.43 tff(489,plain,
% 0.18/0.43 (iplus9 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[488])).
% 0.18/0.43 tff(490,plain,
% 0.18/0.43 (iplus9 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[489, 403])).
% 0.18/0.43 tff(491,plain,
% 0.18/0.43 ((iF = iplus9) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[490])).
% 0.18/0.43 tff(492,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iplus9)),
% 0.18/0.43 inference(symmetry,[status(thm)],[491])).
% 0.18/0.43 tff(493,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iplus9))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[492])).
% 0.18/0.43 tff(494,plain,
% 0.18/0.43 (~(iF = iplus9)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[437, 493])).
% 0.18/0.43 tff(495,assumption,(~(iT = iminus4)), introduced(assumption)).
% 0.18/0.43 tff(496,assumption,(iT = iminus5), introduced(assumption)).
% 0.18/0.43 tff(497,assumption,(~(iT = iminus9)), introduced(assumption)).
% 0.18/0.43 tff(498,plain,
% 0.18/0.43 ((iminus5 = iminus2) <=> (iminus2 = iminus5)),
% 0.18/0.43 inference(commutativity,[status(thm)],[])).
% 0.18/0.43 tff(499,plain,
% 0.18/0.43 ((iT = iminus2) <=> (iminus5 = iminus2)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[496])).
% 0.18/0.43 tff(500,plain,
% 0.18/0.43 ((iT = iminus2) <=> (iminus2 = iminus5)),
% 0.18/0.43 inference(transitivity,[status(thm)],[499, 498])).
% 0.18/0.43 tff(501,plain,
% 0.18/0.43 ((iminus2 = iminus5) <=> (iT = iminus2)),
% 0.18/0.43 inference(symmetry,[status(thm)],[500])).
% 0.18/0.43 tff(502,plain,
% 0.18/0.43 (iT = iminus8),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[400, 495, 497])).
% 0.18/0.43 tff(503,plain,
% 0.18/0.43 (iminus8 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[502])).
% 0.18/0.43 tff(504,plain,
% 0.18/0.43 (iminus8 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[503, 496])).
% 0.18/0.43 tff(505,plain,
% 0.18/0.43 ((iF = iminus8) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[504])).
% 0.18/0.43 tff(506,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iminus8)),
% 0.18/0.43 inference(symmetry,[status(thm)],[505])).
% 0.18/0.43 tff(507,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iminus8))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[506])).
% 0.18/0.43 tff(508,plain,
% 0.18/0.43 ((iT = iF) <=> (iminus5 = iF)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[496])).
% 0.18/0.43 tff(509,plain,
% 0.18/0.43 ((iT = iF) <=> (iF = iminus5)),
% 0.18/0.43 inference(transitivity,[status(thm)],[508, 404])).
% 0.18/0.43 tff(510,plain,
% 0.18/0.43 ((~(iT = iF)) <=> (~(iF = iminus5))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[509])).
% 0.18/0.43 tff(511,plain,
% 0.18/0.43 (~(iF = iminus5)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[249, 510])).
% 0.18/0.43 tff(512,plain,
% 0.18/0.43 (~(iF = iminus8)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[511, 507])).
% 0.18/0.43 tff(513,plain,
% 0.18/0.43 (iF = iplus8),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[330, 512])).
% 0.18/0.43 tff(514,plain,
% 0.18/0.43 (iplus8 = iF),
% 0.18/0.43 inference(symmetry,[status(thm)],[513])).
% 0.18/0.43 tff(515,plain,
% 0.18/0.43 ((iT = iplus8) <=> (iminus5 = iF)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[496, 514])).
% 0.18/0.43 tff(516,plain,
% 0.18/0.43 ((iT = iplus8) <=> (iF = iminus5)),
% 0.18/0.43 inference(transitivity,[status(thm)],[515, 404])).
% 0.18/0.43 tff(517,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iT = iplus8)),
% 0.18/0.43 inference(symmetry,[status(thm)],[516])).
% 0.18/0.43 tff(518,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iT = iplus8))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[517])).
% 0.18/0.43 tff(519,plain,
% 0.18/0.43 (~(iT = iplus8)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[511, 518])).
% 0.18/0.43 tff(520,plain,
% 0.18/0.43 (iT = iplus2),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[307, 519, 495])).
% 0.18/0.43 tff(521,plain,
% 0.18/0.43 (iplus2 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[520])).
% 0.18/0.43 tff(522,plain,
% 0.18/0.43 (iplus2 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[521, 496])).
% 0.18/0.43 tff(523,plain,
% 0.18/0.43 ((iF = iplus2) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[522])).
% 0.18/0.43 tff(524,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iplus2)),
% 0.18/0.43 inference(symmetry,[status(thm)],[523])).
% 0.18/0.43 tff(525,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iplus2))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[524])).
% 0.18/0.43 tff(526,plain,
% 0.18/0.43 (~(iF = iplus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[511, 525])).
% 0.18/0.43 tff(527,plain,
% 0.18/0.43 (iF = iminus2),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[460, 526])).
% 0.18/0.43 tff(528,plain,
% 0.18/0.43 (iminus2 = iF),
% 0.18/0.43 inference(symmetry,[status(thm)],[527])).
% 0.18/0.43 tff(529,plain,
% 0.18/0.43 ((iminus2 = iminus5) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[528])).
% 0.18/0.43 tff(530,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iminus2 = iminus5)),
% 0.18/0.43 inference(symmetry,[status(thm)],[529])).
% 0.18/0.43 tff(531,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iT = iminus2)),
% 0.18/0.43 inference(transitivity,[status(thm)],[530, 501])).
% 0.18/0.43 tff(532,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iT = iminus2))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[531])).
% 0.18/0.43 tff(533,plain,
% 0.18/0.43 (~(iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[511, 532])).
% 0.18/0.43 tff(534,plain,
% 0.18/0.43 (((iT = iplus7) | (iT = iminus9) | (iT = iminus2)) <=> ((iT = iplus7) | (iT = iminus9) | (iT = iminus2))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(535,plain,
% 0.18/0.43 ((((iT = iminus9) | (iT = iminus2)) | (iT = iplus7)) <=> ((iT = iplus7) | (iT = iminus9) | (iT = iminus2))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(536,plain,
% 0.18/0.43 (((iT = iminus9) | (iT = iminus2)) <=> ((iT = iminus9) | (iT = iminus2))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(537,plain,
% 0.18/0.43 ((((iT = iminus9) | (iT = iminus2)) | (iT = iplus7)) <=> (((iT = iminus9) | (iT = iminus2)) | (iT = iplus7))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[536])).
% 0.18/0.43 tff(538,plain,
% 0.18/0.43 ((((iT = iminus9) | (iT = iminus2)) | (iT = iplus7)) <=> ((iT = iplus7) | (iT = iminus9) | (iT = iminus2))),
% 0.18/0.43 inference(transitivity,[status(thm)],[537, 535])).
% 0.18/0.43 tff(539,axiom,(((iT = iminus9) | (iT = iminus2)) | (iT = iplus7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_48')).
% 0.18/0.43 tff(540,plain,
% 0.18/0.43 ((iT = iplus7) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[539, 538])).
% 0.18/0.43 tff(541,plain,
% 0.18/0.43 ((iT = iplus7) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[540, 534])).
% 0.18/0.43 tff(542,plain,
% 0.18/0.43 ((iT = iplus7) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[541, 534])).
% 0.18/0.43 tff(543,plain,
% 0.18/0.43 ((iT = iplus7) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[542, 534])).
% 0.18/0.43 tff(544,plain,
% 0.18/0.43 ((iT = iplus7) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[543, 534])).
% 0.18/0.43 tff(545,plain,
% 0.18/0.43 (iT = iplus7),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[544, 533, 497])).
% 0.18/0.43 tff(546,plain,
% 0.18/0.43 (iplus7 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[545])).
% 0.18/0.43 tff(547,plain,
% 0.18/0.43 (iplus7 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[546, 496])).
% 0.18/0.43 tff(548,plain,
% 0.18/0.43 ((iF = iplus7) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[547])).
% 0.18/0.43 tff(549,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iplus7)),
% 0.18/0.43 inference(symmetry,[status(thm)],[548])).
% 0.18/0.43 tff(550,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iplus7))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[549])).
% 0.18/0.43 tff(551,plain,
% 0.18/0.43 (~(iF = iplus7)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[511, 550])).
% 0.18/0.43 tff(552,plain,
% 0.18/0.43 (iF = iminus7),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[363, 551])).
% 0.18/0.43 tff(553,plain,
% 0.18/0.43 (iminus7 = iF),
% 0.18/0.43 inference(symmetry,[status(thm)],[552])).
% 0.18/0.43 tff(554,plain,
% 0.18/0.43 ((iT = iminus7) <=> (iminus5 = iF)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[496, 553])).
% 0.18/0.43 tff(555,plain,
% 0.18/0.43 ((iT = iminus7) <=> (iF = iminus5)),
% 0.18/0.43 inference(transitivity,[status(thm)],[554, 404])).
% 0.18/0.43 tff(556,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iT = iminus7)),
% 0.18/0.43 inference(symmetry,[status(thm)],[555])).
% 0.18/0.43 tff(557,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iT = iminus7))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[556])).
% 0.18/0.43 tff(558,plain,
% 0.18/0.43 (~(iT = iminus7)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[511, 557])).
% 0.18/0.43 tff(559,plain,
% 0.18/0.43 (((iT = iplus3) | (iT = iminus9) | (iT = iminus2)) <=> ((iT = iplus3) | (iT = iminus9) | (iT = iminus2))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(560,plain,
% 0.18/0.43 ((((iT = iplus3) | (iT = iminus9)) | (iT = iminus2)) <=> ((iT = iplus3) | (iT = iminus9) | (iT = iminus2))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(561,plain,
% 0.18/0.43 (((iT = iplus3) | (iT = iminus9)) <=> ((iT = iplus3) | (iT = iminus9))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(562,plain,
% 0.18/0.43 ((((iT = iplus3) | (iT = iminus9)) | (iT = iminus2)) <=> (((iT = iplus3) | (iT = iminus9)) | (iT = iminus2))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[561])).
% 0.18/0.43 tff(563,plain,
% 0.18/0.43 ((((iT = iplus3) | (iT = iminus9)) | (iT = iminus2)) <=> ((iT = iplus3) | (iT = iminus9) | (iT = iminus2))),
% 0.18/0.43 inference(transitivity,[status(thm)],[562, 560])).
% 0.18/0.43 tff(564,axiom,(((iT = iplus3) | (iT = iminus9)) | (iT = iminus2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_26')).
% 0.18/0.43 tff(565,plain,
% 0.18/0.43 ((iT = iplus3) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[564, 563])).
% 0.18/0.43 tff(566,plain,
% 0.18/0.43 ((iT = iplus3) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[565, 559])).
% 0.18/0.43 tff(567,plain,
% 0.18/0.43 ((iT = iplus3) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[566, 559])).
% 0.18/0.43 tff(568,plain,
% 0.18/0.43 ((iT = iplus3) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[567, 559])).
% 0.18/0.43 tff(569,plain,
% 0.18/0.43 ((iT = iplus3) | (iT = iminus9) | (iT = iminus2)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[568, 559])).
% 0.18/0.43 tff(570,plain,
% 0.18/0.43 (iT = iplus3),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[569, 533, 497])).
% 0.18/0.43 tff(571,plain,
% 0.18/0.43 (iplus3 = iT),
% 0.18/0.43 inference(symmetry,[status(thm)],[570])).
% 0.18/0.43 tff(572,plain,
% 0.18/0.43 (iplus3 = iminus5),
% 0.18/0.43 inference(transitivity,[status(thm)],[571, 496])).
% 0.18/0.43 tff(573,plain,
% 0.18/0.43 ((iF = iplus3) <=> (iF = iminus5)),
% 0.18/0.43 inference(monotonicity,[status(thm)],[572])).
% 0.18/0.43 tff(574,plain,
% 0.18/0.43 ((iF = iminus5) <=> (iF = iplus3)),
% 0.18/0.43 inference(symmetry,[status(thm)],[573])).
% 0.18/0.43 tff(575,plain,
% 0.18/0.43 ((~(iF = iminus5)) <=> (~(iF = iplus3))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[574])).
% 0.18/0.43 tff(576,plain,
% 0.18/0.43 (~(iF = iplus3)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[511, 575])).
% 0.18/0.43 tff(577,plain,
% 0.18/0.43 (^[X: $i] : refl((cTorF(X) <=> ((X = iminus3) | (X = iplus3))) <=> (cTorF(X) <=> ((X = iminus3) | (X = iplus3))))),
% 0.18/0.43 inference(bind,[status(th)],[])).
% 0.18/0.43 tff(578,plain,
% 0.18/0.43 (![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))),
% 0.18/0.43 inference(quant_intro,[status(thm)],[577])).
% 0.18/0.43 tff(579,plain,
% 0.18/0.43 (![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(580,plain,
% 0.18/0.43 (^[X: $i] : rewrite((cTorF(X) <=> ((X = iplus3) | (X = iminus3))) <=> (cTorF(X) <=> ((X = iminus3) | (X = iplus3))))),
% 0.18/0.44 inference(bind,[status(th)],[])).
% 0.18/0.44 tff(581,plain,
% 0.18/0.44 (![X: $i] : (cTorF(X) <=> ((X = iplus3) | (X = iminus3))) <=> ![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))),
% 0.18/0.44 inference(quant_intro,[status(thm)],[580])).
% 0.18/0.44 tff(582,axiom,(![X: $i] : (cTorF(X) <=> ((X = iplus3) | (X = iminus3)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_7')).
% 0.18/0.44 tff(583,plain,
% 0.18/0.44 (![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[582, 581])).
% 0.18/0.44 tff(584,plain,
% 0.18/0.44 (![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[583, 579])).
% 0.18/0.44 tff(585,plain,(
% 0.18/0.44 ![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))),
% 0.18/0.44 inference(skolemize,[status(sab)],[584])).
% 0.18/0.44 tff(586,plain,
% 0.18/0.44 (![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[585, 578])).
% 0.18/0.44 tff(587,plain,
% 0.18/0.44 ((~![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))) | (cTorF(iF) <=> ((iF = iminus3) | (iF = iplus3)))),
% 0.18/0.44 inference(quant_inst,[status(thm)],[])).
% 0.18/0.44 tff(588,plain,
% 0.18/0.44 (cTorF(iF) <=> ((iF = iminus3) | (iF = iplus3))),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[587, 586])).
% 0.18/0.44 tff(589,plain,
% 0.18/0.44 ((~(cTorF(iF) <=> ((iF = iminus3) | (iF = iplus3)))) | (~cTorF(iF)) | ((iF = iminus3) | (iF = iplus3))),
% 0.18/0.44 inference(tautology,[status(thm)],[])).
% 0.18/0.44 tff(590,plain,
% 0.18/0.44 ((~(cTorF(iF) <=> ((iF = iminus3) | (iF = iplus3)))) | ((iF = iminus3) | (iF = iplus3))),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[589, 281])).
% 0.18/0.44 tff(591,plain,
% 0.18/0.44 ((iF = iminus3) | (iF = iplus3)),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[590, 588])).
% 0.18/0.44 tff(592,plain,
% 0.18/0.44 ((~((iF = iminus3) | (iF = iplus3))) | (iF = iminus3) | (iF = iplus3)),
% 0.18/0.44 inference(tautology,[status(thm)],[])).
% 0.18/0.44 tff(593,plain,
% 0.18/0.44 ((iF = iminus3) | (iF = iplus3)),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[592, 591])).
% 0.18/0.44 tff(594,plain,
% 0.18/0.44 (iF = iminus3),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[593, 576])).
% 0.18/0.44 tff(595,plain,
% 0.18/0.44 (iminus3 = iF),
% 0.18/0.44 inference(symmetry,[status(thm)],[594])).
% 0.18/0.44 tff(596,plain,
% 0.18/0.44 ((iT = iminus3) <=> (iminus5 = iF)),
% 0.18/0.44 inference(monotonicity,[status(thm)],[496, 595])).
% 0.18/0.44 tff(597,plain,
% 0.18/0.44 ((iT = iminus3) <=> (iF = iminus5)),
% 0.18/0.44 inference(transitivity,[status(thm)],[596, 404])).
% 0.18/0.44 tff(598,plain,
% 0.18/0.44 ((iF = iminus5) <=> (iT = iminus3)),
% 0.18/0.44 inference(symmetry,[status(thm)],[597])).
% 0.18/0.44 tff(599,plain,
% 0.18/0.44 ((~(iF = iminus5)) <=> (~(iT = iminus3))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[598])).
% 0.18/0.44 tff(600,plain,
% 0.18/0.44 (~(iT = iminus3)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[511, 599])).
% 0.18/0.44 tff(601,plain,
% 0.18/0.44 (((iT = iminus7) | (iT = iminus3) | (iT = iminus4)) <=> ((iT = iminus7) | (iT = iminus3) | (iT = iminus4))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(602,plain,
% 0.18/0.44 ((((iT = iminus3) | (iT = iminus4)) | (iT = iminus7)) <=> ((iT = iminus7) | (iT = iminus3) | (iT = iminus4))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(603,plain,
% 0.18/0.44 (((iT = iminus4) | (iT = iminus3)) <=> ((iT = iminus3) | (iT = iminus4))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(604,plain,
% 0.18/0.44 ((((iT = iminus4) | (iT = iminus3)) | (iT = iminus7)) <=> (((iT = iminus3) | (iT = iminus4)) | (iT = iminus7))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[603])).
% 0.18/0.44 tff(605,plain,
% 0.18/0.44 ((((iT = iminus4) | (iT = iminus3)) | (iT = iminus7)) <=> ((iT = iminus7) | (iT = iminus3) | (iT = iminus4))),
% 0.18/0.44 inference(transitivity,[status(thm)],[604, 602])).
% 0.18/0.44 tff(606,axiom,(((iT = iminus4) | (iT = iminus3)) | (iT = iminus7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_36')).
% 0.18/0.44 tff(607,plain,
% 0.18/0.44 ((iT = iminus7) | (iT = iminus3) | (iT = iminus4)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[606, 605])).
% 0.18/0.44 tff(608,plain,
% 0.18/0.44 ((iT = iminus7) | (iT = iminus3) | (iT = iminus4)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[607, 601])).
% 0.18/0.44 tff(609,plain,
% 0.18/0.44 ((iT = iminus7) | (iT = iminus3) | (iT = iminus4)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[608, 601])).
% 0.18/0.44 tff(610,plain,
% 0.18/0.44 ((iT = iminus7) | (iT = iminus3) | (iT = iminus4)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[609, 601])).
% 0.18/0.44 tff(611,plain,
% 0.18/0.44 ((iT = iminus7) | (iT = iminus3) | (iT = iminus4)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[610, 601])).
% 0.18/0.44 tff(612,plain,
% 0.18/0.44 ($false),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[611, 600, 558, 495])).
% 0.18/0.44 tff(613,plain,((iT = iminus4) | (~(iT = iminus5)) | (iT = iminus9)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.44 tff(614,plain,
% 0.18/0.44 (iT = iminus9),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[613, 476, 403])).
% 0.18/0.44 tff(615,plain,
% 0.18/0.44 (iminus9 = iT),
% 0.18/0.44 inference(symmetry,[status(thm)],[614])).
% 0.18/0.44 tff(616,plain,
% 0.18/0.44 (iminus9 = iminus5),
% 0.18/0.44 inference(transitivity,[status(thm)],[615, 403])).
% 0.18/0.44 tff(617,plain,
% 0.18/0.44 ((iF = iminus9) <=> (iF = iminus5)),
% 0.18/0.44 inference(monotonicity,[status(thm)],[616])).
% 0.18/0.44 tff(618,plain,
% 0.18/0.44 ((iF = iminus5) <=> (iF = iminus9)),
% 0.18/0.44 inference(symmetry,[status(thm)],[617])).
% 0.18/0.44 tff(619,plain,
% 0.18/0.44 ((~(iF = iminus5)) <=> (~(iF = iminus9))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[618])).
% 0.18/0.44 tff(620,plain,
% 0.18/0.44 (~(iF = iminus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[437, 619])).
% 0.18/0.44 tff(621,plain,
% 0.18/0.44 ($false),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[384, 620, 494])).
% 0.18/0.44 tff(622,plain,((iT = iminus1) | (iT = iminus6)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.44 tff(623,plain,
% 0.18/0.44 (iT = iminus1),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[622, 3])).
% 0.18/0.44 tff(624,plain,
% 0.18/0.44 ((iminus6 = iminus1) <=> (iminus1 = iminus6)),
% 0.18/0.44 inference(commutativity,[status(thm)],[])).
% 0.18/0.44 tff(625,plain,
% 0.18/0.44 ((iminus1 = iminus6) <=> (iminus6 = iminus1)),
% 0.18/0.44 inference(symmetry,[status(thm)],[624])).
% 0.18/0.44 tff(626,plain,
% 0.18/0.44 ((iT = iminus6) <=> (iminus1 = iminus6)),
% 0.18/0.44 inference(monotonicity,[status(thm)],[623])).
% 0.18/0.44 tff(627,plain,
% 0.18/0.44 ((iT = iminus6) <=> (iminus6 = iminus1)),
% 0.18/0.44 inference(transitivity,[status(thm)],[626, 625])).
% 0.18/0.44 tff(628,plain,
% 0.18/0.44 ((~(iT = iminus6)) <=> (~(iminus6 = iminus1))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[627])).
% 0.18/0.44 tff(629,plain,
% 0.18/0.44 (~(iminus6 = iminus1)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[3, 628])).
% 0.18/0.44 tff(630,plain,
% 0.18/0.44 ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iminus6) <=> ((iminus6 = iminus1) | (iminus6 = iplus1)))),
% 0.18/0.44 inference(quant_inst,[status(thm)],[])).
% 0.18/0.44 tff(631,plain,
% 0.18/0.44 (cTorF(iminus6) <=> ((iminus6 = iminus1) | (iminus6 = iplus1))),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[630, 100])).
% 0.18/0.44 tff(632,plain,
% 0.18/0.44 ((~(cTorF(iminus6) <=> ((iminus6 = iminus1) | (iminus6 = iplus1)))) | (~cTorF(iminus6)) | ((iminus6 = iminus1) | (iminus6 = iplus1))),
% 0.18/0.44 inference(tautology,[status(thm)],[])).
% 0.18/0.44 tff(633,plain,
% 0.18/0.44 ((~(cTorF(iminus6) <=> ((iminus6 = iminus1) | (iminus6 = iplus1)))) | ((iminus6 = iminus1) | (iminus6 = iplus1))),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[632, 53])).
% 0.18/0.44 tff(634,plain,
% 0.18/0.44 ((iminus6 = iminus1) | (iminus6 = iplus1)),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[633, 631])).
% 0.18/0.44 tff(635,plain,
% 0.18/0.44 ((~((iminus6 = iminus1) | (iminus6 = iplus1))) | (iminus6 = iminus1) | (iminus6 = iplus1)),
% 0.18/0.44 inference(tautology,[status(thm)],[])).
% 0.18/0.44 tff(636,plain,
% 0.18/0.44 ((iminus6 = iminus1) | (iminus6 = iplus1)),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[635, 634])).
% 0.18/0.44 tff(637,plain,
% 0.18/0.44 (iminus6 = iplus1),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[636, 629])).
% 0.18/0.44 tff(638,plain,
% 0.18/0.44 (iplus1 = iminus6),
% 0.18/0.44 inference(symmetry,[status(thm)],[637])).
% 0.18/0.44 tff(639,plain,
% 0.18/0.44 (iplus1 = iF),
% 0.18/0.44 inference(transitivity,[status(thm)],[638, 215])).
% 0.18/0.44 tff(640,plain,
% 0.18/0.44 ((iT = iplus1) <=> (iminus1 = iF)),
% 0.18/0.44 inference(monotonicity,[status(thm)],[623, 639])).
% 0.18/0.44 tff(641,plain,
% 0.18/0.44 ((iminus1 = iF) <=> (iT = iplus1)),
% 0.18/0.44 inference(symmetry,[status(thm)],[640])).
% 0.18/0.44 tff(642,plain,
% 0.18/0.44 ((~(iminus1 = iF)) <=> (~(iT = iplus1))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[641])).
% 0.18/0.44 tff(643,plain,
% 0.18/0.44 ((iT = iF) <=> (iminus1 = iF)),
% 0.18/0.44 inference(monotonicity,[status(thm)],[623])).
% 0.18/0.44 tff(644,plain,
% 0.18/0.44 ((~(iT = iF)) <=> (~(iminus1 = iF))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[643])).
% 0.18/0.44 tff(645,plain,
% 0.18/0.44 (~(iminus1 = iF)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[249, 644])).
% 0.18/0.44 tff(646,plain,
% 0.18/0.44 (~(iT = iplus1)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[645, 642])).
% 0.18/0.44 tff(647,plain,
% 0.18/0.44 (((iT = iminus6) | (iT = iplus1) | (iT = iplus9)) <=> ((iT = iminus6) | (iT = iplus1) | (iT = iplus9))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(648,plain,
% 0.18/0.44 ((((iT = iminus6) | (iT = iplus1)) | (iT = iplus9)) <=> ((iT = iminus6) | (iT = iplus1) | (iT = iplus9))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(649,axiom,(((iT = iminus6) | (iT = iplus1)) | (iT = iplus9)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_17')).
% 0.18/0.44 tff(650,plain,
% 0.18/0.44 ((iT = iminus6) | (iT = iplus1) | (iT = iplus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[649, 648])).
% 0.18/0.44 tff(651,plain,
% 0.18/0.44 ((iT = iminus6) | (iT = iplus1) | (iT = iplus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[650, 647])).
% 0.18/0.44 tff(652,plain,
% 0.18/0.44 (iT = iplus9),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[651, 646, 3])).
% 0.18/0.44 tff(653,plain,
% 0.18/0.44 (iplus9 = iT),
% 0.18/0.44 inference(symmetry,[status(thm)],[652])).
% 0.18/0.44 tff(654,plain,
% 0.18/0.44 (iplus9 = iminus1),
% 0.18/0.44 inference(transitivity,[status(thm)],[653, 623])).
% 0.18/0.44 tff(655,plain,
% 0.18/0.44 ((iF = iplus9) <=> (iF = iminus1)),
% 0.18/0.44 inference(monotonicity,[status(thm)],[654])).
% 0.18/0.44 tff(656,plain,
% 0.18/0.44 ((iF = iplus9) <=> (iminus1 = iF)),
% 0.18/0.44 inference(transitivity,[status(thm)],[655, 2])).
% 0.18/0.44 tff(657,plain,
% 0.18/0.44 ((iminus1 = iF) <=> (iF = iplus9)),
% 0.18/0.44 inference(symmetry,[status(thm)],[656])).
% 0.18/0.44 tff(658,plain,
% 0.18/0.44 ((~(iminus1 = iF)) <=> (~(iF = iplus9))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[657])).
% 0.18/0.44 tff(659,plain,
% 0.18/0.44 (~(iF = iplus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[645, 658])).
% 0.18/0.44 tff(660,plain,
% 0.18/0.44 (((iT = iminus6) | (iT = iplus1) | (iT = iminus9)) <=> ((iT = iminus6) | (iT = iplus1) | (iT = iminus9))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(661,plain,
% 0.18/0.44 ((((iT = iminus6) | (iT = iminus9)) | (iT = iplus1)) <=> ((iT = iminus6) | (iT = iplus1) | (iT = iminus9))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(662,plain,
% 0.18/0.44 (((iT = iminus9) | (iT = iminus6)) <=> ((iT = iminus6) | (iT = iminus9))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(663,plain,
% 0.18/0.44 ((((iT = iminus9) | (iT = iminus6)) | (iT = iplus1)) <=> (((iT = iminus6) | (iT = iminus9)) | (iT = iplus1))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[662])).
% 0.18/0.44 tff(664,plain,
% 0.18/0.44 ((((iT = iminus9) | (iT = iminus6)) | (iT = iplus1)) <=> ((iT = iminus6) | (iT = iplus1) | (iT = iminus9))),
% 0.18/0.44 inference(transitivity,[status(thm)],[663, 661])).
% 0.18/0.44 tff(665,axiom,(((iT = iminus9) | (iT = iminus6)) | (iT = iplus1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_19')).
% 0.18/0.44 tff(666,plain,
% 0.18/0.44 ((iT = iminus6) | (iT = iplus1) | (iT = iminus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[665, 664])).
% 0.18/0.44 tff(667,plain,
% 0.18/0.44 ((iT = iminus6) | (iT = iplus1) | (iT = iminus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[666, 660])).
% 0.18/0.44 tff(668,plain,
% 0.18/0.44 ((iT = iminus6) | (iT = iplus1) | (iT = iminus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[667, 660])).
% 0.18/0.44 tff(669,plain,
% 0.18/0.44 ((iT = iminus6) | (iT = iplus1) | (iT = iminus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[668, 660])).
% 0.18/0.44 tff(670,plain,
% 0.18/0.44 ((iT = iminus6) | (iT = iplus1) | (iT = iminus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[669, 660])).
% 0.18/0.44 tff(671,plain,
% 0.18/0.44 (iT = iminus9),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[670, 646, 3])).
% 0.18/0.44 tff(672,plain,
% 0.18/0.44 (iminus9 = iT),
% 0.18/0.44 inference(symmetry,[status(thm)],[671])).
% 0.18/0.44 tff(673,plain,
% 0.18/0.44 (iminus9 = iminus1),
% 0.18/0.44 inference(transitivity,[status(thm)],[672, 623])).
% 0.18/0.44 tff(674,plain,
% 0.18/0.44 ((iF = iminus9) <=> (iF = iminus1)),
% 0.18/0.44 inference(monotonicity,[status(thm)],[673])).
% 0.18/0.44 tff(675,plain,
% 0.18/0.44 ((iF = iminus9) <=> (iminus1 = iF)),
% 0.18/0.44 inference(transitivity,[status(thm)],[674, 2])).
% 0.18/0.44 tff(676,plain,
% 0.18/0.44 ((iminus1 = iF) <=> (iF = iminus9)),
% 0.18/0.44 inference(symmetry,[status(thm)],[675])).
% 0.18/0.44 tff(677,plain,
% 0.18/0.44 ((~(iminus1 = iF)) <=> (~(iF = iminus9))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[676])).
% 0.18/0.44 tff(678,plain,
% 0.18/0.44 (~(iF = iminus9)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[645, 677])).
% 0.18/0.44 tff(679,plain,
% 0.18/0.44 ($false),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[384, 678, 659])).
% 0.18/0.44 tff(680,plain,(iT = iminus6), inference(lemma,lemma(discharge,[]))).
% 0.18/0.45 tff(681,plain,
% 0.18/0.45 ((iT = iminus4) <=> (iminus6 = iminus4)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[680])).
% 0.18/0.45 tff(682,plain,
% 0.18/0.45 ((iminus6 = iminus4) <=> (iT = iminus4)),
% 0.18/0.45 inference(symmetry,[status(thm)],[681])).
% 0.18/0.45 tff(683,plain,
% 0.18/0.45 ((iT = iplus8) <=> (iminus6 = iplus8)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[680])).
% 0.18/0.45 tff(684,plain,
% 0.18/0.45 ((iminus6 = iplus8) <=> (iT = iplus8)),
% 0.18/0.45 inference(symmetry,[status(thm)],[683])).
% 0.18/0.45 tff(685,plain,
% 0.18/0.45 ((iF = iminus6) <=> (iminus6 = iF)),
% 0.18/0.45 inference(commutativity,[status(thm)],[])).
% 0.18/0.45 tff(686,plain,
% 0.18/0.45 ((iminus6 = iF) <=> (iF = iminus6)),
% 0.18/0.45 inference(symmetry,[status(thm)],[685])).
% 0.18/0.45 tff(687,plain,
% 0.18/0.45 ((iT = iF) <=> (iminus6 = iF)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[680])).
% 0.18/0.45 tff(688,plain,
% 0.18/0.45 ((iT = iF) <=> (iF = iminus6)),
% 0.18/0.45 inference(transitivity,[status(thm)],[687, 686])).
% 0.18/0.45 tff(689,plain,
% 0.18/0.45 ((~(iT = iF)) <=> (~(iF = iminus6))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[688])).
% 0.18/0.45 tff(690,plain,
% 0.18/0.45 (~(iF = iminus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[249, 689])).
% 0.18/0.45 tff(691,plain,
% 0.18/0.45 ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | (cTorF(iF) <=> ((iF = iminus6) | (iF = iplus6)))),
% 0.18/0.45 inference(quant_inst,[status(thm)],[])).
% 0.18/0.45 tff(692,plain,
% 0.18/0.45 (cTorF(iF) <=> ((iF = iminus6) | (iF = iplus6))),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[691, 40])).
% 0.18/0.45 tff(693,plain,
% 0.18/0.45 ((~(cTorF(iF) <=> ((iF = iminus6) | (iF = iplus6)))) | (~cTorF(iF)) | ((iF = iminus6) | (iF = iplus6))),
% 0.18/0.45 inference(tautology,[status(thm)],[])).
% 0.18/0.45 tff(694,plain,
% 0.18/0.45 ((iF = iminus6) | (iF = iplus6)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[693, 281, 692])).
% 0.18/0.45 tff(695,plain,
% 0.18/0.45 ((~((iF = iminus6) | (iF = iplus6))) | (iF = iminus6) | (iF = iplus6)),
% 0.18/0.45 inference(tautology,[status(thm)],[])).
% 0.18/0.45 tff(696,plain,
% 0.18/0.45 ((iF = iminus6) | (iF = iplus6)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[695, 694])).
% 0.18/0.45 tff(697,plain,
% 0.18/0.45 (iF = iplus6),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[696, 690])).
% 0.18/0.45 tff(698,plain,
% 0.18/0.45 ((iplus6 = iminus8) <=> (iminus8 = iplus6)),
% 0.18/0.45 inference(commutativity,[status(thm)],[])).
% 0.18/0.45 tff(699,plain,
% 0.18/0.45 ((iF = iminus8) <=> (iplus6 = iminus8)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[697])).
% 0.18/0.45 tff(700,plain,
% 0.18/0.45 ((iF = iminus8) <=> (iminus8 = iplus6)),
% 0.18/0.45 inference(transitivity,[status(thm)],[699, 698])).
% 0.18/0.45 tff(701,plain,
% 0.18/0.45 ((iminus8 = iplus6) <=> (iF = iminus8)),
% 0.18/0.45 inference(symmetry,[status(thm)],[700])).
% 0.18/0.45 tff(702,plain,
% 0.18/0.45 ((iT = iplus4) <=> (iminus6 = iplus4)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[680])).
% 0.18/0.45 tff(703,plain,
% 0.18/0.45 ((iminus6 = iplus4) <=> (iT = iplus4)),
% 0.18/0.45 inference(symmetry,[status(thm)],[702])).
% 0.18/0.45 tff(704,plain,
% 0.18/0.45 (iplus6 = iF),
% 0.18/0.45 inference(symmetry,[status(thm)],[697])).
% 0.18/0.45 tff(705,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iminus6 = iF)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[680, 704])).
% 0.18/0.45 tff(706,plain,
% 0.18/0.45 ((iminus6 = iF) <=> (iT = iplus6)),
% 0.18/0.45 inference(symmetry,[status(thm)],[705])).
% 0.18/0.45 tff(707,plain,
% 0.18/0.45 ((~(iminus6 = iF)) <=> (~(iT = iplus6))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[706])).
% 0.18/0.45 tff(708,plain,
% 0.18/0.45 ((~(iT = iF)) <=> (~(iminus6 = iF))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[687])).
% 0.18/0.45 tff(709,plain,
% 0.18/0.45 (~(iminus6 = iF)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[249, 708])).
% 0.18/0.45 tff(710,plain,
% 0.18/0.45 (~(iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[709, 707])).
% 0.18/0.45 tff(711,plain,
% 0.18/0.45 (((iT = iminus4) | (iT = iplus6) | (iT = iminus1)) <=> ((iT = iminus4) | (iT = iplus6) | (iT = iminus1))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(712,plain,
% 0.18/0.45 ((((iT = iminus4) | (iT = iplus6)) | (iT = iminus1)) <=> ((iT = iminus4) | (iT = iplus6) | (iT = iminus1))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(713,plain,
% 0.18/0.45 (((iT = iplus6) | (iT = iminus4)) <=> ((iT = iminus4) | (iT = iplus6))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(714,plain,
% 0.18/0.45 ((((iT = iplus6) | (iT = iminus4)) | (iT = iminus1)) <=> (((iT = iminus4) | (iT = iplus6)) | (iT = iminus1))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[713])).
% 0.18/0.45 tff(715,plain,
% 0.18/0.45 ((((iT = iplus6) | (iT = iminus4)) | (iT = iminus1)) <=> ((iT = iminus4) | (iT = iplus6) | (iT = iminus1))),
% 0.18/0.45 inference(transitivity,[status(thm)],[714, 712])).
% 0.18/0.45 tff(716,axiom,(((iT = iplus6) | (iT = iminus4)) | (iT = iminus1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_53')).
% 0.18/0.45 tff(717,plain,
% 0.18/0.45 ((iT = iminus4) | (iT = iplus6) | (iT = iminus1)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[716, 715])).
% 0.18/0.45 tff(718,plain,
% 0.18/0.45 ((iT = iminus4) | (iT = iplus6) | (iT = iminus1)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[717, 711])).
% 0.18/0.45 tff(719,plain,
% 0.18/0.45 ((iT = iminus4) | (iT = iplus6) | (iT = iminus1)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[718, 711])).
% 0.18/0.45 tff(720,plain,
% 0.18/0.45 ((iT = iminus4) | (iT = iplus6) | (iT = iminus1)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[719, 711])).
% 0.18/0.45 tff(721,plain,
% 0.18/0.45 ((iT = iminus4) | (iT = iplus6) | (iT = iminus1)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[720, 711])).
% 0.18/0.45 tff(722,plain,
% 0.18/0.45 ((iT = iminus4) | (iT = iminus1)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[721, 710])).
% 0.18/0.45 tff(723,plain,
% 0.18/0.45 (iT = iminus4),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[722, 4])).
% 0.18/0.45 tff(724,plain,
% 0.18/0.45 (iminus4 = iT),
% 0.18/0.45 inference(symmetry,[status(thm)],[723])).
% 0.18/0.45 tff(725,plain,
% 0.18/0.45 ((iplus6 = iminus4) <=> (iplus6 = iT)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[724])).
% 0.18/0.45 tff(726,plain,
% 0.18/0.45 ((iplus6 = iminus4) <=> (iT = iplus6)),
% 0.18/0.45 inference(transitivity,[status(thm)],[725, 1])).
% 0.18/0.45 tff(727,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iplus6 = iminus4)),
% 0.18/0.45 inference(symmetry,[status(thm)],[726])).
% 0.18/0.45 tff(728,plain,
% 0.18/0.45 ((~(iT = iplus6)) <=> (~(iplus6 = iminus4))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[727])).
% 0.18/0.45 tff(729,plain,
% 0.18/0.45 (~(iplus6 = iminus4)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[710, 728])).
% 0.18/0.45 tff(730,plain,
% 0.18/0.45 ((~![X: $i] : (cTorF(X) <=> ((X = iminus4) | (X = iplus4)))) | (cTorF(iplus6) <=> ((iplus6 = iminus4) | (iplus6 = iplus4)))),
% 0.18/0.45 inference(quant_inst,[status(thm)],[])).
% 0.18/0.45 tff(731,plain,
% 0.18/0.45 (cTorF(iplus6) <=> ((iplus6 = iminus4) | (iplus6 = iplus4))),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[730, 143])).
% 0.18/0.45 tff(732,plain,
% 0.18/0.45 (((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iplus6)) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iplus6))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(733,plain,
% 0.18/0.45 ((cTorF(iplus6) <=> $true) <=> cTorF(iplus6)),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(734,plain,
% 0.18/0.45 (((iplus6 = iminus6) | $true) <=> $true),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(735,plain,
% 0.18/0.45 ((iplus6 = iplus6) <=> $true),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(736,plain,
% 0.18/0.45 (((iplus6 = iminus6) | (iplus6 = iplus6)) <=> ((iplus6 = iminus6) | $true)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[735])).
% 0.18/0.45 tff(737,plain,
% 0.18/0.45 (((iplus6 = iminus6) | (iplus6 = iplus6)) <=> $true),
% 0.18/0.45 inference(transitivity,[status(thm)],[736, 734])).
% 0.18/0.45 tff(738,plain,
% 0.18/0.45 ((cTorF(iplus6) <=> ((iplus6 = iminus6) | (iplus6 = iplus6))) <=> (cTorF(iplus6) <=> $true)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[737])).
% 0.18/0.45 tff(739,plain,
% 0.18/0.45 ((cTorF(iplus6) <=> ((iplus6 = iminus6) | (iplus6 = iplus6))) <=> cTorF(iplus6)),
% 0.18/0.45 inference(transitivity,[status(thm)],[738, 733])).
% 0.18/0.45 tff(740,plain,
% 0.18/0.45 (((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | (cTorF(iplus6) <=> ((iplus6 = iminus6) | (iplus6 = iplus6)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iplus6))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[739])).
% 0.18/0.45 tff(741,plain,
% 0.18/0.45 (((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | (cTorF(iplus6) <=> ((iplus6 = iminus6) | (iplus6 = iplus6)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iplus6))),
% 0.18/0.45 inference(transitivity,[status(thm)],[740, 732])).
% 0.18/0.45 tff(742,plain,
% 0.18/0.45 ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | (cTorF(iplus6) <=> ((iplus6 = iminus6) | (iplus6 = iplus6)))),
% 0.18/0.45 inference(quant_inst,[status(thm)],[])).
% 0.18/0.45 tff(743,plain,
% 0.18/0.45 ((~![X: $i] : (cTorF(X) <=> ((X = iminus6) | (X = iplus6)))) | cTorF(iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[742, 741])).
% 0.18/0.45 tff(744,plain,
% 0.18/0.45 (cTorF(iplus6)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[743, 40])).
% 0.18/0.45 tff(745,plain,
% 0.18/0.45 ((~(cTorF(iplus6) <=> ((iplus6 = iminus4) | (iplus6 = iplus4)))) | (~cTorF(iplus6)) | ((iplus6 = iminus4) | (iplus6 = iplus4))),
% 0.18/0.45 inference(tautology,[status(thm)],[])).
% 0.18/0.45 tff(746,plain,
% 0.18/0.45 ((~(cTorF(iplus6) <=> ((iplus6 = iminus4) | (iplus6 = iplus4)))) | ((iplus6 = iminus4) | (iplus6 = iplus4))),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[745, 744])).
% 0.18/0.45 tff(747,plain,
% 0.18/0.45 ((iplus6 = iminus4) | (iplus6 = iplus4)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[746, 731])).
% 0.18/0.45 tff(748,plain,
% 0.18/0.45 ((~((iplus6 = iminus4) | (iplus6 = iplus4))) | (iplus6 = iminus4) | (iplus6 = iplus4)),
% 0.18/0.45 inference(tautology,[status(thm)],[])).
% 0.18/0.45 tff(749,plain,
% 0.18/0.45 ((iplus6 = iminus4) | (iplus6 = iplus4)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[748, 747])).
% 0.18/0.45 tff(750,plain,
% 0.18/0.45 (iplus6 = iplus4),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[749, 729])).
% 0.18/0.45 tff(751,plain,
% 0.18/0.45 (iplus4 = iplus6),
% 0.18/0.45 inference(symmetry,[status(thm)],[750])).
% 0.18/0.45 tff(752,plain,
% 0.18/0.45 (iminus6 = iT),
% 0.18/0.45 inference(symmetry,[status(thm)],[680])).
% 0.18/0.45 tff(753,plain,
% 0.18/0.45 ((iminus6 = iplus4) <=> (iT = iplus6)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[752, 751])).
% 0.18/0.45 tff(754,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iminus6 = iplus4)),
% 0.18/0.45 inference(symmetry,[status(thm)],[753])).
% 0.18/0.45 tff(755,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iT = iplus4)),
% 0.18/0.45 inference(transitivity,[status(thm)],[754, 703])).
% 0.18/0.45 tff(756,plain,
% 0.18/0.45 ((~(iT = iplus6)) <=> (~(iT = iplus4))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[755])).
% 0.18/0.45 tff(757,plain,
% 0.18/0.45 (~(iT = iplus4)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[710, 756])).
% 0.18/0.45 tff(758,plain,
% 0.18/0.45 (((iT = iplus4) | (iT = iminus8) | (iT = iplus6)) <=> ((iT = iplus4) | (iT = iminus8) | (iT = iplus6))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(759,plain,
% 0.18/0.45 ((((iT = iminus8) | (iT = iplus6)) | (iT = iplus4)) <=> ((iT = iplus4) | (iT = iminus8) | (iT = iplus6))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(760,axiom,(((iT = iminus8) | (iT = iplus6)) | (iT = iplus4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_25')).
% 0.18/0.45 tff(761,plain,
% 0.18/0.45 ((iT = iplus4) | (iT = iminus8) | (iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[760, 759])).
% 0.18/0.45 tff(762,plain,
% 0.18/0.45 ((iT = iplus4) | (iT = iminus8) | (iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[761, 758])).
% 0.18/0.45 tff(763,plain,
% 0.18/0.45 ((iT = iplus4) | (iT = iminus8) | (iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[762, 758])).
% 0.18/0.45 tff(764,plain,
% 0.18/0.45 ((iT = iplus4) | (iT = iminus8) | (iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[763, 758])).
% 0.18/0.45 tff(765,plain,
% 0.18/0.45 ((iT = iplus4) | (iT = iminus8) | (iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[764, 758])).
% 0.18/0.45 tff(766,plain,
% 0.18/0.45 ((iT = iplus4) | (iT = iminus8)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[765, 710])).
% 0.18/0.45 tff(767,plain,
% 0.18/0.45 (iT = iminus8),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[766, 757])).
% 0.18/0.45 tff(768,plain,
% 0.18/0.45 (iminus8 = iT),
% 0.18/0.45 inference(symmetry,[status(thm)],[767])).
% 0.18/0.45 tff(769,plain,
% 0.18/0.45 ((iminus8 = iplus6) <=> (iT = iplus6)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[768])).
% 0.18/0.45 tff(770,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iminus8 = iplus6)),
% 0.18/0.45 inference(symmetry,[status(thm)],[769])).
% 0.18/0.45 tff(771,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iF = iminus8)),
% 0.18/0.45 inference(transitivity,[status(thm)],[770, 701])).
% 0.18/0.45 tff(772,plain,
% 0.18/0.45 ((~(iT = iplus6)) <=> (~(iF = iminus8))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[771])).
% 0.18/0.45 tff(773,plain,
% 0.18/0.45 (~(iF = iminus8)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[710, 772])).
% 0.18/0.45 tff(774,plain,
% 0.18/0.45 (iF = iplus8),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[330, 773])).
% 0.18/0.45 tff(775,plain,
% 0.18/0.45 (iplus8 = iF),
% 0.18/0.45 inference(symmetry,[status(thm)],[774])).
% 0.18/0.45 tff(776,plain,
% 0.18/0.45 (iplus8 = iplus6),
% 0.18/0.45 inference(transitivity,[status(thm)],[775, 697])).
% 0.18/0.45 tff(777,plain,
% 0.18/0.45 ((iminus6 = iplus8) <=> (iT = iplus6)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[752, 776])).
% 0.18/0.45 tff(778,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iminus6 = iplus8)),
% 0.18/0.45 inference(symmetry,[status(thm)],[777])).
% 0.18/0.45 tff(779,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iT = iplus8)),
% 0.18/0.45 inference(transitivity,[status(thm)],[778, 684])).
% 0.18/0.45 tff(780,plain,
% 0.18/0.45 ((~(iT = iplus6)) <=> (~(iT = iplus8))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[779])).
% 0.18/0.45 tff(781,plain,
% 0.18/0.45 (~(iT = iplus8)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[710, 780])).
% 0.18/0.45 tff(782,plain,
% 0.18/0.45 ((iT = iminus3) <=> (iminus6 = iminus3)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[680])).
% 0.18/0.45 tff(783,plain,
% 0.18/0.45 ((iminus6 = iminus3) <=> (iT = iminus3)),
% 0.18/0.45 inference(symmetry,[status(thm)],[782])).
% 0.18/0.45 tff(784,plain,
% 0.18/0.45 (((iT = iplus3) | (iT = iplus4) | (iT = iplus6)) <=> ((iT = iplus3) | (iT = iplus4) | (iT = iplus6))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(785,plain,
% 0.18/0.45 ((((iT = iplus3) | (iT = iplus6)) | (iT = iplus4)) <=> ((iT = iplus3) | (iT = iplus4) | (iT = iplus6))),
% 0.18/0.45 inference(rewrite,[status(thm)],[])).
% 0.18/0.45 tff(786,axiom,(((iT = iplus3) | (iT = iplus6)) | (iT = iplus4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_22')).
% 0.18/0.45 tff(787,plain,
% 0.18/0.45 ((iT = iplus3) | (iT = iplus4) | (iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[786, 785])).
% 0.18/0.45 tff(788,plain,
% 0.18/0.45 ((iT = iplus3) | (iT = iplus4) | (iT = iplus6)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[787, 784])).
% 0.18/0.45 tff(789,plain,
% 0.18/0.45 ((iT = iplus3) | (iT = iplus4)),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[788, 710])).
% 0.18/0.45 tff(790,plain,
% 0.18/0.45 (iT = iplus3),
% 0.18/0.45 inference(unit_resolution,[status(thm)],[789, 757])).
% 0.18/0.45 tff(791,plain,
% 0.18/0.45 (iplus3 = iT),
% 0.18/0.45 inference(symmetry,[status(thm)],[790])).
% 0.18/0.45 tff(792,plain,
% 0.18/0.45 ((iplus6 = iplus3) <=> (iplus6 = iT)),
% 0.18/0.45 inference(monotonicity,[status(thm)],[791])).
% 0.18/0.45 tff(793,plain,
% 0.18/0.45 ((iplus6 = iplus3) <=> (iT = iplus6)),
% 0.18/0.45 inference(transitivity,[status(thm)],[792, 1])).
% 0.18/0.45 tff(794,plain,
% 0.18/0.45 ((iT = iplus6) <=> (iplus6 = iplus3)),
% 0.18/0.45 inference(symmetry,[status(thm)],[793])).
% 0.18/0.45 tff(795,plain,
% 0.18/0.45 ((~(iT = iplus6)) <=> (~(iplus6 = iplus3))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[794])).
% 0.18/0.45 tff(796,plain,
% 0.18/0.45 (~(iplus6 = iplus3)),
% 0.18/0.45 inference(modus_ponens,[status(thm)],[710, 795])).
% 0.18/0.45 tff(797,plain,
% 0.18/0.45 ((~![X: $i] : (cTorF(X) <=> ((X = iminus3) | (X = iplus3)))) | (cTorF(iplus6) <=> ((iplus6 = iminus3) | (iplus6 = iplus3)))),
% 0.18/0.46 inference(quant_inst,[status(thm)],[])).
% 0.18/0.46 tff(798,plain,
% 0.18/0.46 (cTorF(iplus6) <=> ((iplus6 = iminus3) | (iplus6 = iplus3))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[797, 586])).
% 0.18/0.46 tff(799,plain,
% 0.18/0.46 ((~(cTorF(iplus6) <=> ((iplus6 = iminus3) | (iplus6 = iplus3)))) | (~cTorF(iplus6)) | ((iplus6 = iminus3) | (iplus6 = iplus3))),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(800,plain,
% 0.18/0.46 ((~(cTorF(iplus6) <=> ((iplus6 = iminus3) | (iplus6 = iplus3)))) | ((iplus6 = iminus3) | (iplus6 = iplus3))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[799, 744])).
% 0.18/0.46 tff(801,plain,
% 0.18/0.46 ((iplus6 = iminus3) | (iplus6 = iplus3)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[800, 798])).
% 0.18/0.46 tff(802,plain,
% 0.18/0.46 ((~((iplus6 = iminus3) | (iplus6 = iplus3))) | (iplus6 = iminus3) | (iplus6 = iplus3)),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(803,plain,
% 0.18/0.46 ((iplus6 = iminus3) | (iplus6 = iplus3)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[802, 801])).
% 0.18/0.46 tff(804,plain,
% 0.18/0.46 (iplus6 = iminus3),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[803, 796])).
% 0.18/0.46 tff(805,plain,
% 0.18/0.46 (iminus3 = iplus6),
% 0.18/0.46 inference(symmetry,[status(thm)],[804])).
% 0.18/0.46 tff(806,plain,
% 0.18/0.46 ((iminus6 = iminus3) <=> (iT = iplus6)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[752, 805])).
% 0.18/0.46 tff(807,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iminus6 = iminus3)),
% 0.18/0.46 inference(symmetry,[status(thm)],[806])).
% 0.18/0.46 tff(808,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iT = iminus3)),
% 0.18/0.46 inference(transitivity,[status(thm)],[807, 783])).
% 0.18/0.46 tff(809,plain,
% 0.18/0.46 ((~(iT = iplus6)) <=> (~(iT = iminus3))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[808])).
% 0.18/0.46 tff(810,plain,
% 0.18/0.46 (~(iT = iminus3)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[710, 809])).
% 0.18/0.46 tff(811,plain,
% 0.18/0.46 (((iT = iplus8) | (iT = iminus3) | (iT = iplus7)) <=> ((iT = iplus8) | (iT = iminus3) | (iT = iplus7))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(812,plain,
% 0.18/0.46 ((((iT = iplus8) | (iT = iminus3)) | (iT = iplus7)) <=> ((iT = iplus8) | (iT = iminus3) | (iT = iplus7))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(813,plain,
% 0.18/0.46 (((iT = iplus8) | (iT = iminus3)) <=> ((iT = iplus8) | (iT = iminus3))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(814,plain,
% 0.18/0.46 ((((iT = iplus8) | (iT = iminus3)) | (iT = iplus7)) <=> (((iT = iplus8) | (iT = iminus3)) | (iT = iplus7))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[813])).
% 0.18/0.46 tff(815,plain,
% 0.18/0.46 ((((iT = iplus8) | (iT = iminus3)) | (iT = iplus7)) <=> ((iT = iplus8) | (iT = iminus3) | (iT = iplus7))),
% 0.18/0.46 inference(transitivity,[status(thm)],[814, 812])).
% 0.18/0.46 tff(816,axiom,(((iT = iplus8) | (iT = iminus3)) | (iT = iplus7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_15')).
% 0.18/0.46 tff(817,plain,
% 0.18/0.46 ((iT = iplus8) | (iT = iminus3) | (iT = iplus7)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[816, 815])).
% 0.18/0.46 tff(818,plain,
% 0.18/0.46 ((iT = iplus8) | (iT = iminus3) | (iT = iplus7)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[817, 811])).
% 0.18/0.46 tff(819,plain,
% 0.18/0.46 ((iT = iplus8) | (iT = iminus3) | (iT = iplus7)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[818, 811])).
% 0.18/0.46 tff(820,plain,
% 0.18/0.46 ((iT = iplus8) | (iT = iminus3) | (iT = iplus7)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[819, 811])).
% 0.18/0.46 tff(821,plain,
% 0.18/0.46 ((iT = iplus8) | (iT = iminus3) | (iT = iplus7)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[820, 811])).
% 0.18/0.46 tff(822,plain,
% 0.18/0.46 (iT = iplus7),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[821, 810, 781])).
% 0.18/0.46 tff(823,plain,
% 0.18/0.46 (iplus7 = iT),
% 0.18/0.46 inference(symmetry,[status(thm)],[822])).
% 0.18/0.46 tff(824,plain,
% 0.18/0.46 ((iplus6 = iplus7) <=> (iplus6 = iT)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[823])).
% 0.18/0.46 tff(825,plain,
% 0.18/0.46 ((iplus6 = iplus7) <=> (iT = iplus6)),
% 0.18/0.46 inference(transitivity,[status(thm)],[824, 1])).
% 0.18/0.46 tff(826,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iplus6 = iplus7)),
% 0.18/0.46 inference(symmetry,[status(thm)],[825])).
% 0.18/0.46 tff(827,plain,
% 0.18/0.46 ((~(iT = iplus6)) <=> (~(iplus6 = iplus7))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[826])).
% 0.18/0.46 tff(828,plain,
% 0.18/0.46 (~(iplus6 = iplus7)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[710, 827])).
% 0.18/0.46 tff(829,plain,
% 0.18/0.46 ((iT = iminus2) <=> (iminus6 = iminus2)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[680])).
% 0.18/0.46 tff(830,plain,
% 0.18/0.46 ((iminus6 = iminus2) <=> (iT = iminus2)),
% 0.18/0.46 inference(symmetry,[status(thm)],[829])).
% 0.18/0.46 tff(831,plain,
% 0.18/0.46 (iT = iplus2),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[259, 757, 4])).
% 0.18/0.46 tff(832,plain,
% 0.18/0.46 (iplus2 = iT),
% 0.18/0.46 inference(symmetry,[status(thm)],[831])).
% 0.18/0.46 tff(833,plain,
% 0.18/0.46 ((iplus6 = iplus2) <=> (iplus6 = iT)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[832])).
% 0.18/0.46 tff(834,plain,
% 0.18/0.46 ((iplus6 = iplus2) <=> (iT = iplus6)),
% 0.18/0.46 inference(transitivity,[status(thm)],[833, 1])).
% 0.18/0.46 tff(835,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iplus6 = iplus2)),
% 0.18/0.46 inference(symmetry,[status(thm)],[834])).
% 0.18/0.46 tff(836,plain,
% 0.18/0.46 ((~(iT = iplus6)) <=> (~(iplus6 = iplus2))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[835])).
% 0.18/0.46 tff(837,plain,
% 0.18/0.46 (~(iplus6 = iplus2)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[710, 836])).
% 0.18/0.46 tff(838,plain,
% 0.18/0.46 ((~![X: $i] : (cTorF(X) <=> ((X = iminus2) | (X = iplus2)))) | (cTorF(iplus6) <=> ((iplus6 = iminus2) | (iplus6 = iplus2)))),
% 0.18/0.46 inference(quant_inst,[status(thm)],[])).
% 0.18/0.46 tff(839,plain,
% 0.18/0.46 (cTorF(iplus6) <=> ((iplus6 = iminus2) | (iplus6 = iplus2))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[838, 230])).
% 0.18/0.46 tff(840,plain,
% 0.18/0.46 ((~(cTorF(iplus6) <=> ((iplus6 = iminus2) | (iplus6 = iplus2)))) | (~cTorF(iplus6)) | ((iplus6 = iminus2) | (iplus6 = iplus2))),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(841,plain,
% 0.18/0.46 ((~(cTorF(iplus6) <=> ((iplus6 = iminus2) | (iplus6 = iplus2)))) | ((iplus6 = iminus2) | (iplus6 = iplus2))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[840, 744])).
% 0.18/0.46 tff(842,plain,
% 0.18/0.46 ((iplus6 = iminus2) | (iplus6 = iplus2)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[841, 839])).
% 0.18/0.46 tff(843,plain,
% 0.18/0.46 ((~((iplus6 = iminus2) | (iplus6 = iplus2))) | (iplus6 = iminus2) | (iplus6 = iplus2)),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(844,plain,
% 0.18/0.46 ((iplus6 = iminus2) | (iplus6 = iplus2)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[843, 842])).
% 0.18/0.46 tff(845,plain,
% 0.18/0.46 (iplus6 = iminus2),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[844, 837])).
% 0.18/0.46 tff(846,plain,
% 0.18/0.46 (iminus2 = iplus6),
% 0.18/0.46 inference(symmetry,[status(thm)],[845])).
% 0.18/0.46 tff(847,plain,
% 0.18/0.46 ((iminus6 = iminus2) <=> (iT = iplus6)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[752, 846])).
% 0.18/0.46 tff(848,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iminus6 = iminus2)),
% 0.18/0.46 inference(symmetry,[status(thm)],[847])).
% 0.18/0.46 tff(849,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iT = iminus2)),
% 0.18/0.46 inference(transitivity,[status(thm)],[848, 830])).
% 0.18/0.46 tff(850,plain,
% 0.18/0.46 ((~(iT = iplus6)) <=> (~(iT = iminus2))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[849])).
% 0.18/0.46 tff(851,plain,
% 0.18/0.46 (~(iT = iminus2)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[710, 850])).
% 0.18/0.46 tff(852,plain,
% 0.18/0.46 (((iT = iminus7) | (iT = iplus6) | (iT = iminus2)) <=> ((iT = iminus7) | (iT = iplus6) | (iT = iminus2))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(853,plain,
% 0.18/0.46 ((((iT = iplus6) | (iT = iminus2)) | (iT = iminus7)) <=> ((iT = iminus7) | (iT = iplus6) | (iT = iminus2))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(854,plain,
% 0.18/0.46 (((iT = iplus6) | (iT = iminus2)) <=> ((iT = iplus6) | (iT = iminus2))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(855,plain,
% 0.18/0.46 ((((iT = iplus6) | (iT = iminus2)) | (iT = iminus7)) <=> (((iT = iplus6) | (iT = iminus2)) | (iT = iminus7))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[854])).
% 0.18/0.46 tff(856,plain,
% 0.18/0.46 ((((iT = iplus6) | (iT = iminus2)) | (iT = iminus7)) <=> ((iT = iminus7) | (iT = iplus6) | (iT = iminus2))),
% 0.18/0.46 inference(transitivity,[status(thm)],[855, 853])).
% 0.18/0.46 tff(857,axiom,(((iT = iplus6) | (iT = iminus2)) | (iT = iminus7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_27')).
% 0.18/0.46 tff(858,plain,
% 0.18/0.46 ((iT = iminus7) | (iT = iplus6) | (iT = iminus2)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[857, 856])).
% 0.18/0.46 tff(859,plain,
% 0.18/0.46 ((iT = iminus7) | (iT = iplus6) | (iT = iminus2)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[858, 852])).
% 0.18/0.46 tff(860,plain,
% 0.18/0.46 ((iT = iminus7) | (iT = iplus6) | (iT = iminus2)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[859, 852])).
% 0.18/0.46 tff(861,plain,
% 0.18/0.46 ((iT = iminus7) | (iT = iplus6) | (iT = iminus2)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[860, 852])).
% 0.18/0.46 tff(862,plain,
% 0.18/0.46 ((iT = iminus7) | (iT = iplus6) | (iT = iminus2)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[861, 852])).
% 0.18/0.46 tff(863,plain,
% 0.18/0.46 ((iT = iminus7) | (iT = iminus2)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[862, 710])).
% 0.18/0.46 tff(864,plain,
% 0.18/0.46 (iT = iminus7),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[863, 851])).
% 0.18/0.46 tff(865,plain,
% 0.18/0.46 (iminus7 = iT),
% 0.18/0.46 inference(symmetry,[status(thm)],[864])).
% 0.18/0.46 tff(866,plain,
% 0.18/0.46 ((iplus6 = iminus7) <=> (iplus6 = iT)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[865])).
% 0.18/0.46 tff(867,plain,
% 0.18/0.46 ((iplus6 = iminus7) <=> (iT = iplus6)),
% 0.18/0.46 inference(transitivity,[status(thm)],[866, 1])).
% 0.18/0.46 tff(868,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iplus6 = iminus7)),
% 0.18/0.46 inference(symmetry,[status(thm)],[867])).
% 0.18/0.46 tff(869,plain,
% 0.18/0.46 ((~(iT = iplus6)) <=> (~(iplus6 = iminus7))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[868])).
% 0.18/0.46 tff(870,plain,
% 0.18/0.46 (~(iplus6 = iminus7)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[710, 869])).
% 0.18/0.46 tff(871,plain,
% 0.18/0.46 ((~![X: $i] : (cTorF(X) <=> ((X = iminus7) | (X = iplus7)))) | (cTorF(iplus6) <=> ((iplus6 = iminus7) | (iplus6 = iplus7)))),
% 0.18/0.46 inference(quant_inst,[status(thm)],[])).
% 0.18/0.46 tff(872,plain,
% 0.18/0.46 (cTorF(iplus6) <=> ((iplus6 = iminus7) | (iplus6 = iplus7))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[871, 181])).
% 0.18/0.46 tff(873,plain,
% 0.18/0.46 ((~(cTorF(iplus6) <=> ((iplus6 = iminus7) | (iplus6 = iplus7)))) | (~cTorF(iplus6)) | ((iplus6 = iminus7) | (iplus6 = iplus7))),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(874,plain,
% 0.18/0.46 ((~(cTorF(iplus6) <=> ((iplus6 = iminus7) | (iplus6 = iplus7)))) | ((iplus6 = iminus7) | (iplus6 = iplus7))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[873, 744])).
% 0.18/0.46 tff(875,plain,
% 0.18/0.46 ((iplus6 = iminus7) | (iplus6 = iplus7)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[874, 872])).
% 0.18/0.46 tff(876,plain,
% 0.18/0.46 ((~((iplus6 = iminus7) | (iplus6 = iplus7))) | (iplus6 = iminus7) | (iplus6 = iplus7)),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(877,plain,
% 0.18/0.46 ((iplus6 = iminus7) | (iplus6 = iplus7)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[876, 875])).
% 0.18/0.46 tff(878,plain,
% 0.18/0.46 ($false),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[877, 870, 828])).
% 0.18/0.46 tff(879,plain,(iT = iminus1), inference(lemma,lemma(discharge,[]))).
% 0.18/0.46 tff(880,plain,
% 0.18/0.46 (iminus1 = iT),
% 0.18/0.46 inference(symmetry,[status(thm)],[879])).
% 0.18/0.46 tff(881,plain,
% 0.18/0.46 ((iplus6 = iminus1) <=> (iplus6 = iT)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[880])).
% 0.18/0.46 tff(882,plain,
% 0.18/0.46 ((iplus6 = iminus1) <=> (iT = iplus6)),
% 0.18/0.46 inference(transitivity,[status(thm)],[881, 1])).
% 0.18/0.46 tff(883,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iplus6 = iminus1)),
% 0.18/0.46 inference(symmetry,[status(thm)],[882])).
% 0.18/0.46 tff(884,plain,
% 0.18/0.46 ((~(iT = iplus6)) <=> (~(iplus6 = iminus1))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[883])).
% 0.18/0.46 tff(885,plain,
% 0.18/0.46 (~(iplus6 = iminus1)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[710, 884])).
% 0.18/0.46 tff(886,plain,
% 0.18/0.46 ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iplus6) <=> ((iplus6 = iminus1) | (iplus6 = iplus1)))),
% 0.18/0.46 inference(quant_inst,[status(thm)],[])).
% 0.18/0.46 tff(887,plain,
% 0.18/0.46 (cTorF(iplus6) <=> ((iplus6 = iminus1) | (iplus6 = iplus1))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[886, 100])).
% 0.18/0.46 tff(888,plain,
% 0.18/0.46 ((~(cTorF(iplus6) <=> ((iplus6 = iminus1) | (iplus6 = iplus1)))) | (~cTorF(iplus6)) | ((iplus6 = iminus1) | (iplus6 = iplus1))),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(889,plain,
% 0.18/0.46 ((iplus6 = iminus1) | (iplus6 = iplus1)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[888, 744, 887])).
% 0.18/0.46 tff(890,plain,
% 0.18/0.46 ((~((iplus6 = iminus1) | (iplus6 = iplus1))) | (iplus6 = iminus1) | (iplus6 = iplus1)),
% 0.18/0.46 inference(tautology,[status(thm)],[])).
% 0.18/0.46 tff(891,plain,
% 0.18/0.46 ((iplus6 = iminus1) | (iplus6 = iplus1)),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[890, 889])).
% 0.18/0.46 tff(892,plain,
% 0.18/0.46 (iplus6 = iplus1),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[891, 885])).
% 0.18/0.46 tff(893,plain,
% 0.18/0.46 (iplus1 = iplus6),
% 0.18/0.46 inference(symmetry,[status(thm)],[892])).
% 0.18/0.46 tff(894,plain,
% 0.18/0.46 ((iplus1 = iminus8) <=> (iplus6 = iminus8)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[893])).
% 0.18/0.46 tff(895,plain,
% 0.18/0.46 ((iplus1 = iminus8) <=> (iminus8 = iplus6)),
% 0.18/0.46 inference(transitivity,[status(thm)],[894, 698])).
% 0.18/0.46 tff(896,plain,
% 0.18/0.46 ((iminus8 = iplus6) <=> (iplus1 = iminus8)),
% 0.18/0.46 inference(symmetry,[status(thm)],[895])).
% 0.18/0.46 tff(897,plain,
% 0.18/0.46 (iT = iminus8),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[766, 439])).
% 0.18/0.46 tff(898,plain,
% 0.18/0.46 (iminus8 = iT),
% 0.18/0.46 inference(symmetry,[status(thm)],[897])).
% 0.18/0.46 tff(899,plain,
% 0.18/0.46 ((iminus8 = iplus6) <=> (iT = iplus6)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[898])).
% 0.18/0.46 tff(900,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iminus8 = iplus6)),
% 0.18/0.46 inference(symmetry,[status(thm)],[899])).
% 0.18/0.46 tff(901,plain,
% 0.18/0.46 ((iT = iplus6) <=> (iplus1 = iminus8)),
% 0.18/0.46 inference(transitivity,[status(thm)],[900, 896])).
% 0.18/0.46 tff(902,plain,
% 0.18/0.46 ((~(iT = iplus6)) <=> (~(iplus1 = iminus8))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[901])).
% 0.18/0.46 tff(903,plain,
% 0.18/0.46 (~(iplus1 = iminus8)),
% 0.18/0.46 inference(modus_ponens,[status(thm)],[710, 902])).
% 0.18/0.46 tff(904,plain,
% 0.18/0.46 ((~![X: $i] : (cTorF(X) <=> ((X = iminus8) | (X = iplus8)))) | (cTorF(iplus1) <=> ((iplus1 = iminus8) | (iplus1 = iplus8)))),
% 0.18/0.46 inference(quant_inst,[status(thm)],[])).
% 0.18/0.46 tff(905,plain,
% 0.18/0.46 (cTorF(iplus1) <=> ((iplus1 = iminus8) | (iplus1 = iplus8))),
% 0.18/0.46 inference(unit_resolution,[status(thm)],[904, 324])).
% 0.18/0.46 tff(906,plain,
% 0.18/0.46 (((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iplus1)) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iplus1))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(907,plain,
% 0.18/0.46 ((cTorF(iplus1) <=> $true) <=> cTorF(iplus1)),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(908,plain,
% 0.18/0.46 (((iplus1 = iminus1) | $true) <=> $true),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(909,plain,
% 0.18/0.46 ((iplus1 = iplus1) <=> $true),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(910,plain,
% 0.18/0.46 (((iplus1 = iminus1) | (iplus1 = iplus1)) <=> ((iplus1 = iminus1) | $true)),
% 0.18/0.46 inference(monotonicity,[status(thm)],[909])).
% 0.18/0.46 tff(911,plain,
% 0.18/0.46 (((iplus1 = iminus1) | (iplus1 = iplus1)) <=> $true),
% 0.18/0.46 inference(transitivity,[status(thm)],[910, 908])).
% 0.18/0.46 tff(912,plain,
% 0.18/0.47 ((cTorF(iplus1) <=> ((iplus1 = iminus1) | (iplus1 = iplus1))) <=> (cTorF(iplus1) <=> $true)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[911])).
% 0.18/0.47 tff(913,plain,
% 0.18/0.47 ((cTorF(iplus1) <=> ((iplus1 = iminus1) | (iplus1 = iplus1))) <=> cTorF(iplus1)),
% 0.18/0.47 inference(transitivity,[status(thm)],[912, 907])).
% 0.18/0.47 tff(914,plain,
% 0.18/0.47 (((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iplus1) <=> ((iplus1 = iminus1) | (iplus1 = iplus1)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iplus1))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[913])).
% 0.18/0.47 tff(915,plain,
% 0.18/0.47 (((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iplus1) <=> ((iplus1 = iminus1) | (iplus1 = iplus1)))) <=> ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iplus1))),
% 0.18/0.47 inference(transitivity,[status(thm)],[914, 906])).
% 0.18/0.47 tff(916,plain,
% 0.18/0.47 ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | (cTorF(iplus1) <=> ((iplus1 = iminus1) | (iplus1 = iplus1)))),
% 0.18/0.47 inference(quant_inst,[status(thm)],[])).
% 0.18/0.47 tff(917,plain,
% 0.18/0.47 ((~![X: $i] : (cTorF(X) <=> ((X = iminus1) | (X = iplus1)))) | cTorF(iplus1)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[916, 915])).
% 0.18/0.47 tff(918,plain,
% 0.18/0.47 (cTorF(iplus1)),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[917, 100])).
% 0.18/0.47 tff(919,plain,
% 0.18/0.47 ((~(cTorF(iplus1) <=> ((iplus1 = iminus8) | (iplus1 = iplus8)))) | (~cTorF(iplus1)) | ((iplus1 = iminus8) | (iplus1 = iplus8))),
% 0.18/0.47 inference(tautology,[status(thm)],[])).
% 0.18/0.47 tff(920,plain,
% 0.18/0.47 ((iplus1 = iminus8) | (iplus1 = iplus8)),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[919, 918, 905])).
% 0.18/0.47 tff(921,plain,
% 0.18/0.47 ((~((iplus1 = iminus8) | (iplus1 = iplus8))) | (iplus1 = iminus8) | (iplus1 = iplus8)),
% 0.18/0.47 inference(tautology,[status(thm)],[])).
% 0.18/0.47 tff(922,plain,
% 0.18/0.47 ((iplus1 = iminus8) | (iplus1 = iplus8)),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[921, 920])).
% 0.18/0.47 tff(923,plain,
% 0.18/0.47 (iplus1 = iplus8),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[922, 903])).
% 0.18/0.47 tff(924,plain,
% 0.18/0.47 (iplus8 = iplus1),
% 0.18/0.47 inference(symmetry,[status(thm)],[923])).
% 0.18/0.47 tff(925,plain,
% 0.18/0.47 (iplus8 = iplus6),
% 0.18/0.47 inference(transitivity,[status(thm)],[924, 893])).
% 0.18/0.47 tff(926,plain,
% 0.18/0.47 ((iminus6 = iplus8) <=> (iT = iplus6)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[752, 925])).
% 0.18/0.47 tff(927,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iminus6 = iplus8)),
% 0.18/0.47 inference(symmetry,[status(thm)],[926])).
% 0.18/0.47 tff(928,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iT = iplus8)),
% 0.18/0.47 inference(transitivity,[status(thm)],[927, 684])).
% 0.18/0.47 tff(929,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iT = iplus8))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[928])).
% 0.18/0.47 tff(930,plain,
% 0.18/0.47 (~(iT = iplus8)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 929])).
% 0.18/0.47 tff(931,plain,
% 0.18/0.47 (iT = iplus3),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[789, 439])).
% 0.18/0.47 tff(932,plain,
% 0.18/0.47 (iplus3 = iT),
% 0.18/0.47 inference(symmetry,[status(thm)],[931])).
% 0.18/0.47 tff(933,plain,
% 0.18/0.47 ((iplus6 = iplus3) <=> (iplus6 = iT)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[932])).
% 0.18/0.47 tff(934,plain,
% 0.18/0.47 ((iplus6 = iplus3) <=> (iT = iplus6)),
% 0.18/0.47 inference(transitivity,[status(thm)],[933, 1])).
% 0.18/0.47 tff(935,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iplus6 = iplus3)),
% 0.18/0.47 inference(symmetry,[status(thm)],[934])).
% 0.18/0.47 tff(936,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iplus6 = iplus3))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[935])).
% 0.18/0.47 tff(937,plain,
% 0.18/0.47 (~(iplus6 = iplus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 936])).
% 0.18/0.47 tff(938,plain,
% 0.18/0.47 (iplus6 = iminus3),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[803, 937])).
% 0.18/0.47 tff(939,plain,
% 0.18/0.47 (iminus3 = iplus6),
% 0.18/0.47 inference(symmetry,[status(thm)],[938])).
% 0.18/0.47 tff(940,plain,
% 0.18/0.47 ((iminus6 = iminus3) <=> (iT = iplus6)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[752, 939])).
% 0.18/0.47 tff(941,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iminus6 = iminus3)),
% 0.18/0.47 inference(symmetry,[status(thm)],[940])).
% 0.18/0.47 tff(942,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iT = iminus3)),
% 0.18/0.47 inference(transitivity,[status(thm)],[941, 783])).
% 0.18/0.47 tff(943,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iT = iminus3))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[942])).
% 0.18/0.47 tff(944,plain,
% 0.18/0.47 (~(iT = iminus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 943])).
% 0.18/0.47 tff(945,plain,
% 0.18/0.47 (((iT = iplus2) | (iT = iplus8) | (iT = iminus3)) <=> ((iT = iplus2) | (iT = iplus8) | (iT = iminus3))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(946,plain,
% 0.18/0.47 ((((iT = iplus2) | (iT = iplus8)) | (iT = iminus3)) <=> ((iT = iplus2) | (iT = iplus8) | (iT = iminus3))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(947,plain,
% 0.18/0.47 ((((iT = iplus8) | (iT = iplus2)) | (iT = iminus3)) <=> (((iT = iplus2) | (iT = iplus8)) | (iT = iminus3))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[299])).
% 0.18/0.47 tff(948,plain,
% 0.18/0.47 ((((iT = iplus8) | (iT = iplus2)) | (iT = iminus3)) <=> ((iT = iplus2) | (iT = iplus8) | (iT = iminus3))),
% 0.18/0.47 inference(transitivity,[status(thm)],[947, 946])).
% 0.18/0.47 tff(949,axiom,(((iT = iplus8) | (iT = iplus2)) | (iT = iminus3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_42')).
% 0.18/0.47 tff(950,plain,
% 0.18/0.47 ((iT = iplus2) | (iT = iplus8) | (iT = iminus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[949, 948])).
% 0.18/0.47 tff(951,plain,
% 0.18/0.47 ((iT = iplus2) | (iT = iplus8) | (iT = iminus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[950, 945])).
% 0.18/0.47 tff(952,plain,
% 0.18/0.47 ((iT = iplus2) | (iT = iplus8) | (iT = iminus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[951, 945])).
% 0.18/0.47 tff(953,plain,
% 0.18/0.47 ((iT = iplus2) | (iT = iplus8) | (iT = iminus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[952, 945])).
% 0.18/0.47 tff(954,plain,
% 0.18/0.47 ((iT = iplus2) | (iT = iplus8) | (iT = iminus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[953, 945])).
% 0.18/0.47 tff(955,plain,
% 0.18/0.47 (iT = iplus2),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[954, 944, 930])).
% 0.18/0.47 tff(956,plain,
% 0.18/0.47 (iplus2 = iT),
% 0.18/0.47 inference(symmetry,[status(thm)],[955])).
% 0.18/0.47 tff(957,plain,
% 0.18/0.47 ((iplus6 = iplus2) <=> (iplus6 = iT)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[956])).
% 0.18/0.47 tff(958,plain,
% 0.18/0.47 ((iplus6 = iplus2) <=> (iT = iplus6)),
% 0.18/0.47 inference(transitivity,[status(thm)],[957, 1])).
% 0.18/0.47 tff(959,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iplus6 = iplus2)),
% 0.18/0.47 inference(symmetry,[status(thm)],[958])).
% 0.18/0.47 tff(960,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iplus6 = iplus2))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[959])).
% 0.18/0.47 tff(961,plain,
% 0.18/0.47 (~(iplus6 = iplus2)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 960])).
% 0.18/0.47 tff(962,plain,
% 0.18/0.47 ((iT = iplus1) <=> (iminus6 = iplus1)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[680])).
% 0.18/0.47 tff(963,plain,
% 0.18/0.47 ((iminus6 = iplus1) <=> (iT = iplus1)),
% 0.18/0.47 inference(symmetry,[status(thm)],[962])).
% 0.18/0.47 tff(964,plain,
% 0.18/0.47 ((iminus6 = iplus1) <=> (iT = iplus6)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[752, 893])).
% 0.18/0.47 tff(965,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iminus6 = iplus1)),
% 0.18/0.47 inference(symmetry,[status(thm)],[964])).
% 0.18/0.47 tff(966,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iT = iplus1)),
% 0.18/0.47 inference(transitivity,[status(thm)],[965, 963])).
% 0.18/0.47 tff(967,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iT = iplus1))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[966])).
% 0.18/0.47 tff(968,plain,
% 0.18/0.47 (~(iT = iplus1)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 967])).
% 0.18/0.47 tff(969,plain,
% 0.18/0.47 (((iT = iplus1) | (iT = iminus3) | (iT = iminus2)) <=> ((iT = iplus1) | (iT = iminus3) | (iT = iminus2))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(970,plain,
% 0.18/0.47 ((((iT = iminus2) | (iT = iplus1)) | (iT = iminus3)) <=> ((iT = iplus1) | (iT = iminus3) | (iT = iminus2))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(971,axiom,(((iT = iminus2) | (iT = iplus1)) | (iT = iminus3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_38')).
% 0.18/0.47 tff(972,plain,
% 0.18/0.47 ((iT = iplus1) | (iT = iminus3) | (iT = iminus2)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[971, 970])).
% 0.18/0.47 tff(973,plain,
% 0.18/0.47 ((iT = iplus1) | (iT = iminus3) | (iT = iminus2)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[972, 969])).
% 0.18/0.47 tff(974,plain,
% 0.18/0.47 ((iT = iplus1) | (iT = iminus3) | (iT = iminus2)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[973, 969])).
% 0.18/0.47 tff(975,plain,
% 0.18/0.47 ((iT = iplus1) | (iT = iminus3) | (iT = iminus2)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[974, 969])).
% 0.18/0.47 tff(976,plain,
% 0.18/0.47 ((iT = iplus1) | (iT = iminus3) | (iT = iminus2)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[975, 969])).
% 0.18/0.47 tff(977,plain,
% 0.18/0.47 (iT = iminus2),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[976, 944, 968])).
% 0.18/0.47 tff(978,plain,
% 0.18/0.47 (iminus2 = iT),
% 0.18/0.47 inference(symmetry,[status(thm)],[977])).
% 0.18/0.47 tff(979,plain,
% 0.18/0.47 ((iplus6 = iminus2) <=> (iplus6 = iT)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[978])).
% 0.18/0.47 tff(980,plain,
% 0.18/0.47 ((iplus6 = iminus2) <=> (iT = iplus6)),
% 0.18/0.47 inference(transitivity,[status(thm)],[979, 1])).
% 0.18/0.47 tff(981,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iplus6 = iminus2)),
% 0.18/0.47 inference(symmetry,[status(thm)],[980])).
% 0.18/0.47 tff(982,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iplus6 = iminus2))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[981])).
% 0.18/0.47 tff(983,plain,
% 0.18/0.47 (~(iplus6 = iminus2)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 982])).
% 0.18/0.47 tff(984,plain,
% 0.18/0.47 ($false),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[844, 983, 961])).
% 0.18/0.47 tff(985,plain,(iT = iplus4), inference(lemma,lemma(discharge,[]))).
% 0.18/0.47 tff(986,plain,
% 0.18/0.47 (iplus4 = iT),
% 0.18/0.47 inference(symmetry,[status(thm)],[985])).
% 0.18/0.47 tff(987,plain,
% 0.18/0.47 ((iplus6 = iplus4) <=> (iplus6 = iT)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[986])).
% 0.18/0.47 tff(988,plain,
% 0.18/0.47 ((iplus6 = iplus4) <=> (iT = iplus6)),
% 0.18/0.47 inference(transitivity,[status(thm)],[987, 1])).
% 0.18/0.47 tff(989,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iplus6 = iplus4)),
% 0.18/0.47 inference(symmetry,[status(thm)],[988])).
% 0.18/0.47 tff(990,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iplus6 = iplus4))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[989])).
% 0.18/0.47 tff(991,plain,
% 0.18/0.47 (~(iplus6 = iplus4)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 990])).
% 0.18/0.47 tff(992,plain,
% 0.18/0.47 (iplus6 = iminus4),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[749, 991])).
% 0.18/0.47 tff(993,plain,
% 0.18/0.47 (iminus4 = iplus6),
% 0.18/0.47 inference(symmetry,[status(thm)],[992])).
% 0.18/0.47 tff(994,plain,
% 0.18/0.47 ((iminus6 = iminus4) <=> (iT = iplus6)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[752, 993])).
% 0.18/0.47 tff(995,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iminus6 = iminus4)),
% 0.18/0.47 inference(symmetry,[status(thm)],[994])).
% 0.18/0.47 tff(996,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iT = iminus4)),
% 0.18/0.47 inference(transitivity,[status(thm)],[995, 682])).
% 0.18/0.47 tff(997,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iT = iminus4))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[996])).
% 0.18/0.47 tff(998,plain,
% 0.18/0.47 (~(iT = iminus4)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 997])).
% 0.18/0.47 tff(999,plain,
% 0.18/0.47 (((iT = iminus3) | (iT = iminus4) | (iT = iplus6)) <=> ((iT = iminus3) | (iT = iminus4) | (iT = iplus6))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(1000,plain,
% 0.18/0.47 ((((iT = iminus4) | (iT = iplus6)) | (iT = iminus3)) <=> ((iT = iminus3) | (iT = iminus4) | (iT = iplus6))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(1001,plain,
% 0.18/0.47 ((((iT = iplus6) | (iT = iminus4)) | (iT = iminus3)) <=> (((iT = iminus4) | (iT = iplus6)) | (iT = iminus3))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[713])).
% 0.18/0.47 tff(1002,plain,
% 0.18/0.47 ((((iT = iplus6) | (iT = iminus4)) | (iT = iminus3)) <=> ((iT = iminus3) | (iT = iminus4) | (iT = iplus6))),
% 0.18/0.47 inference(transitivity,[status(thm)],[1001, 1000])).
% 0.18/0.47 tff(1003,axiom,(((iT = iplus6) | (iT = iminus4)) | (iT = iminus3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_28')).
% 0.18/0.47 tff(1004,plain,
% 0.18/0.47 ((iT = iminus3) | (iT = iminus4) | (iT = iplus6)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[1003, 1002])).
% 0.18/0.47 tff(1005,plain,
% 0.18/0.47 ((iT = iminus3) | (iT = iminus4) | (iT = iplus6)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[1004, 999])).
% 0.18/0.47 tff(1006,plain,
% 0.18/0.47 ((iT = iminus3) | (iT = iminus4)),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[1005, 710])).
% 0.18/0.47 tff(1007,plain,
% 0.18/0.47 (iT = iminus3),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[1006, 998])).
% 0.18/0.47 tff(1008,plain,
% 0.18/0.47 (iminus3 = iT),
% 0.18/0.47 inference(symmetry,[status(thm)],[1007])).
% 0.18/0.47 tff(1009,plain,
% 0.18/0.47 ((iplus6 = iminus3) <=> (iplus6 = iT)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[1008])).
% 0.18/0.47 tff(1010,plain,
% 0.18/0.47 ((iplus6 = iminus3) <=> (iT = iplus6)),
% 0.18/0.47 inference(transitivity,[status(thm)],[1009, 1])).
% 0.18/0.47 tff(1011,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iplus6 = iminus3)),
% 0.18/0.47 inference(symmetry,[status(thm)],[1010])).
% 0.18/0.47 tff(1012,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iplus6 = iminus3))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[1011])).
% 0.18/0.47 tff(1013,plain,
% 0.18/0.47 (~(iplus6 = iminus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 1012])).
% 0.18/0.47 tff(1014,plain,
% 0.18/0.47 (((iT = iplus3) | (iT = iminus4) | (iT = iplus6)) <=> ((iT = iplus3) | (iT = iminus4) | (iT = iplus6))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(1015,plain,
% 0.18/0.47 ((((iT = iplus3) | (iT = iplus6)) | (iT = iminus4)) <=> ((iT = iplus3) | (iT = iminus4) | (iT = iplus6))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(1016,axiom,(((iT = iplus3) | (iT = iplus6)) | (iT = iminus4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_39')).
% 0.18/0.47 tff(1017,plain,
% 0.18/0.47 ((iT = iplus3) | (iT = iminus4) | (iT = iplus6)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[1016, 1015])).
% 0.18/0.47 tff(1018,plain,
% 0.18/0.47 ((iT = iplus3) | (iT = iminus4) | (iT = iplus6)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[1017, 1014])).
% 0.18/0.47 tff(1019,plain,
% 0.18/0.47 ((iT = iplus3) | (iT = iminus4) | (iT = iplus6)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[1018, 1014])).
% 0.18/0.47 tff(1020,plain,
% 0.18/0.47 ((iT = iplus3) | (iT = iminus4) | (iT = iplus6)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[1019, 1014])).
% 0.18/0.47 tff(1021,plain,
% 0.18/0.47 ((iT = iplus3) | (iT = iminus4) | (iT = iplus6)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[1020, 1014])).
% 0.18/0.47 tff(1022,plain,
% 0.18/0.47 ((iT = iplus3) | (iT = iminus4)),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[1021, 710])).
% 0.18/0.47 tff(1023,plain,
% 0.18/0.47 (iT = iplus3),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[1022, 998])).
% 0.18/0.47 tff(1024,plain,
% 0.18/0.47 (iplus3 = iT),
% 0.18/0.47 inference(symmetry,[status(thm)],[1023])).
% 0.18/0.47 tff(1025,plain,
% 0.18/0.47 ((iplus6 = iplus3) <=> (iplus6 = iT)),
% 0.18/0.47 inference(monotonicity,[status(thm)],[1024])).
% 0.18/0.47 tff(1026,plain,
% 0.18/0.47 ((iplus6 = iplus3) <=> (iT = iplus6)),
% 0.18/0.47 inference(transitivity,[status(thm)],[1025, 1])).
% 0.18/0.47 tff(1027,plain,
% 0.18/0.47 ((iT = iplus6) <=> (iplus6 = iplus3)),
% 0.18/0.47 inference(symmetry,[status(thm)],[1026])).
% 0.18/0.47 tff(1028,plain,
% 0.18/0.47 ((~(iT = iplus6)) <=> (~(iplus6 = iplus3))),
% 0.18/0.47 inference(monotonicity,[status(thm)],[1027])).
% 0.18/0.47 tff(1029,plain,
% 0.18/0.47 (~(iplus6 = iplus3)),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[710, 1028])).
% 0.18/0.47 tff(1030,plain,
% 0.18/0.47 ($false),
% 0.18/0.47 inference(unit_resolution,[status(thm)],[803, 1029, 1013])).
% 0.18/0.47 % SZS output end Proof
% 0.18/0.48 % E exiting
%------------------------------------------------------------------------------