%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN036-3 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:37:59 AM UTC 2025
% Result : Unsatisfiable 0.23s 0.52s
% Output : Proof 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SYN036-3 : TPTP v9.0.0. Released v1.0.0.
% 0.09/0.14 % Command : run_E %s %d THM
% 0.14/0.36 % Computer : n013.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri Jun 20 12:26:38 EDT 2025
% 0.14/0.36 % CPUTime :
% 0.23/0.52 % SZS status Unsatisfiable
% 0.23/0.52 % SZS output start Proof
% 0.23/0.52 tff(p_type, type, (
% 0.23/0.52 p: $i > $o)).
% 0.23/0.52 tff(s7_type, type, (
% 0.23/0.52 s7: $i)).
% 0.23/0.52 tff(n7_type, type, (
% 0.23/0.52 n7: $o)).
% 0.23/0.52 tff(n10_type, type, (
% 0.23/0.52 n10: $o)).
% 0.23/0.52 tff(q_type, type, (
% 0.23/0.52 q: $i > $o)).
% 0.23/0.52 tff(s5_type, type, (
% 0.23/0.52 s5: $i > $i)).
% 0.23/0.52 tff(s4_type, type, (
% 0.23/0.52 s4: $i)).
% 0.23/0.52 tff(n5_type, type, (
% 0.23/0.52 n5: $i > $o)).
% 0.23/0.52 tff(n6_type, type, (
% 0.23/0.52 n6: $o)).
% 0.23/0.52 tff(n9_type, type, (
% 0.23/0.52 n9: $o)).
% 0.23/0.52 tff(n4_type, type, (
% 0.23/0.52 n4: $o)).
% 0.23/0.52 tff(n3_type, type, (
% 0.23/0.52 n3: $o)).
% 0.23/0.52 tff(n8_type, type, (
% 0.23/0.52 n8: $o)).
% 0.23/0.52 tff(s2_type, type, (
% 0.23/0.52 s2: $i)).
% 0.23/0.52 tff(n1_type, type, (
% 0.23/0.52 n1: $i > $o)).
% 0.23/0.52 tff(n2_type, type, (
% 0.23/0.52 n2: $o)).
% 0.23/0.52 tff(s1_type, type, (
% 0.23/0.52 s1: $i > $i)).
% 0.23/0.52 tff(s8_type, type, (
% 0.23/0.52 s8: $i)).
% 0.23/0.52 tff(s6_type, type, (
% 0.23/0.52 s6: $i)).
% 0.23/0.52 tff(s3_type, type, (
% 0.23/0.52 s3: $i)).
% 0.23/0.52 tff(1,assumption,(n10), introduced(assumption)).
% 0.23/0.52 tff(2,assumption,(~q(s4)), introduced(assumption)).
% 0.23/0.52 tff(3,plain,
% 0.23/0.52 (^[X4: $i] : refl(((~n4) | q(X4)) <=> ((~n4) | q(X4)))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(4,plain,
% 0.23/0.52 (![X4: $i] : ((~n4) | q(X4)) <=> ![X4: $i] : ((~n4) | q(X4))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[3])).
% 0.23/0.52 tff(5,plain,
% 0.23/0.52 (![X4: $i] : ((~n4) | q(X4)) <=> ![X4: $i] : ((~n4) | q(X4))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(6,axiom,(![X4: $i] : ((~n4) | q(X4))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_20')).
% 0.23/0.52 tff(7,plain,
% 0.23/0.52 (![X4: $i] : ((~n4) | q(X4))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.23/0.52 tff(8,plain,(
% 0.23/0.52 ![X4: $i] : ((~n4) | q(X4))),
% 0.23/0.52 inference(skolemize,[status(sab)],[7])).
% 0.23/0.52 tff(9,plain,
% 0.23/0.52 (![X4: $i] : ((~n4) | q(X4))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[8, 4])).
% 0.23/0.52 tff(10,assumption,(n4), introduced(assumption)).
% 0.23/0.52 tff(11,plain,
% 0.23/0.52 (((~![X4: $i] : ((~n4) | q(X4))) | ((~n4) | q(s4))) <=> ((~![X4: $i] : ((~n4) | q(X4))) | (~n4) | q(s4))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(12,plain,
% 0.23/0.52 ((~![X4: $i] : ((~n4) | q(X4))) | ((~n4) | q(s4))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(13,plain,
% 0.23/0.52 ((~![X4: $i] : ((~n4) | q(X4))) | (~n4) | q(s4)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.23/0.52 tff(14,plain,
% 0.23/0.52 ($false),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[13, 2, 10, 9])).
% 0.23/0.52 tff(15,plain,(q(s4) | (~n4)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.52 tff(16,plain,
% 0.23/0.52 (~n4),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[15, 2])).
% 0.23/0.52 tff(17,plain,
% 0.23/0.52 (^[X8: $i] : refl(((~n8) | p(X8)) <=> ((~n8) | p(X8)))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(18,plain,
% 0.23/0.52 (![X8: $i] : ((~n8) | p(X8)) <=> ![X8: $i] : ((~n8) | p(X8))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[17])).
% 0.23/0.52 tff(19,plain,
% 0.23/0.52 (![X8: $i] : ((~n8) | p(X8)) <=> ![X8: $i] : ((~n8) | p(X8))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(20,axiom,(![X8: $i] : ((~n8) | p(X8))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_10')).
% 0.23/0.52 tff(21,plain,
% 0.23/0.52 (![X8: $i] : ((~n8) | p(X8))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[20, 19])).
% 0.23/0.52 tff(22,plain,(
% 0.23/0.52 ![X8: $i] : ((~n8) | p(X8))),
% 0.23/0.52 inference(skolemize,[status(sab)],[21])).
% 0.23/0.52 tff(23,plain,
% 0.23/0.52 (![X8: $i] : ((~n8) | p(X8))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[22, 18])).
% 0.23/0.52 tff(24,assumption,(~n3), introduced(assumption)).
% 0.23/0.52 tff(25,plain,
% 0.23/0.52 (^[X3: $i] : refl(((~q(X3)) | n3) <=> ((~q(X3)) | n3))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(26,plain,
% 0.23/0.52 (![X3: $i] : ((~q(X3)) | n3) <=> ![X3: $i] : ((~q(X3)) | n3)),
% 0.23/0.52 inference(quant_intro,[status(thm)],[25])).
% 0.23/0.52 tff(27,plain,
% 0.23/0.52 (![X3: $i] : ((~q(X3)) | n3) <=> ![X3: $i] : ((~q(X3)) | n3)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(28,axiom,(![X3: $i] : ((~q(X3)) | n3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_21')).
% 0.23/0.52 tff(29,plain,
% 0.23/0.52 (![X3: $i] : ((~q(X3)) | n3)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.23/0.52 tff(30,plain,(
% 0.23/0.52 ![X3: $i] : ((~q(X3)) | n3)),
% 0.23/0.52 inference(skolemize,[status(sab)],[29])).
% 0.23/0.52 tff(31,plain,
% 0.23/0.52 (![X3: $i] : ((~q(X3)) | n3)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[30, 26])).
% 0.23/0.52 tff(32,assumption,(q(s4)), introduced(assumption)).
% 0.23/0.52 tff(33,plain,
% 0.23/0.52 (((~![X3: $i] : ((~q(X3)) | n3)) | ((~q(s4)) | n3)) <=> ((~![X3: $i] : ((~q(X3)) | n3)) | (~q(s4)) | n3)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(34,plain,
% 0.23/0.52 ((~![X3: $i] : ((~q(X3)) | n3)) | ((~q(s4)) | n3)),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(35,plain,
% 0.23/0.52 ((~![X3: $i] : ((~q(X3)) | n3)) | (~q(s4)) | n3),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.23/0.52 tff(36,plain,
% 0.23/0.52 ($false),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[35, 32, 31, 24])).
% 0.23/0.52 tff(37,plain,((~q(s4)) | n3), inference(lemma,lemma(discharge,[]))).
% 0.23/0.52 tff(38,plain,
% 0.23/0.52 (~q(s4)),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[37, 24])).
% 0.23/0.52 tff(39,plain,
% 0.23/0.52 (~n4),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[13, 38, 9])).
% 0.23/0.52 tff(40,plain,
% 0.23/0.52 ((n9 | n4 | n3) <=> (n9 | n4 | n3)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(41,plain,
% 0.23/0.52 (((n3 | n4) | n9) <=> (n9 | n4 | n3)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(42,axiom,((n3 | n4) | n9), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_30')).
% 0.23/0.52 tff(43,plain,
% 0.23/0.52 (n9 | n4 | n3),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[42, 41])).
% 0.23/0.52 tff(44,plain,
% 0.23/0.52 (n9 | n4 | n3),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[43, 40])).
% 0.23/0.52 tff(45,plain,
% 0.23/0.52 (n9 | n4 | n3),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[44, 40])).
% 0.23/0.52 tff(46,plain,
% 0.23/0.52 (n9 | n4 | n3),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[45, 40])).
% 0.23/0.52 tff(47,plain,
% 0.23/0.52 (n9 | n4 | n3),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[46, 40])).
% 0.23/0.52 tff(48,plain,
% 0.23/0.52 (n9),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[47, 39, 24])).
% 0.23/0.52 tff(49,assumption,(q(s5(s4))), introduced(assumption)).
% 0.23/0.52 tff(50,plain,
% 0.23/0.52 (((~![X3: $i] : ((~q(X3)) | n3)) | (n3 | (~q(s5(s4))))) <=> ((~![X3: $i] : ((~q(X3)) | n3)) | n3 | (~q(s5(s4))))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(51,plain,
% 0.23/0.52 (((~q(s5(s4))) | n3) <=> (n3 | (~q(s5(s4))))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(52,plain,
% 0.23/0.52 (((~![X3: $i] : ((~q(X3)) | n3)) | ((~q(s5(s4))) | n3)) <=> ((~![X3: $i] : ((~q(X3)) | n3)) | (n3 | (~q(s5(s4)))))),
% 0.23/0.52 inference(monotonicity,[status(thm)],[51])).
% 0.23/0.52 tff(53,plain,
% 0.23/0.52 (((~![X3: $i] : ((~q(X3)) | n3)) | ((~q(s5(s4))) | n3)) <=> ((~![X3: $i] : ((~q(X3)) | n3)) | n3 | (~q(s5(s4))))),
% 0.23/0.52 inference(transitivity,[status(thm)],[52, 50])).
% 0.23/0.52 tff(54,plain,
% 0.23/0.52 ((~![X3: $i] : ((~q(X3)) | n3)) | ((~q(s5(s4))) | n3)),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(55,plain,
% 0.23/0.52 ((~![X3: $i] : ((~q(X3)) | n3)) | n3 | (~q(s5(s4)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[54, 53])).
% 0.23/0.52 tff(56,plain,
% 0.23/0.52 ($false),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[55, 31, 24, 49])).
% 0.23/0.52 tff(57,plain,((~q(s5(s4))) | n3), inference(lemma,lemma(discharge,[]))).
% 0.23/0.52 tff(58,plain,
% 0.23/0.52 (~q(s5(s4))),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[57, 24])).
% 0.23/0.52 tff(59,plain,
% 0.23/0.52 (^[X: $i] : refl((n5(X) | q(s5(X)) | q(X)) <=> (n5(X) | q(s5(X)) | q(X)))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(60,plain,
% 0.23/0.52 (![X: $i] : (n5(X) | q(s5(X)) | q(X)) <=> ![X: $i] : (n5(X) | q(s5(X)) | q(X))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[59])).
% 0.23/0.52 tff(61,plain,
% 0.23/0.52 (![X: $i] : (n5(X) | q(s5(X)) | q(X)) <=> ![X: $i] : (n5(X) | q(s5(X)) | q(X))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(62,plain,
% 0.23/0.52 (^[X: $i] : rewrite(((q(X) | q(s5(X))) | n5(X)) <=> (n5(X) | q(s5(X)) | q(X)))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(63,plain,
% 0.23/0.52 (![X: $i] : ((q(X) | q(s5(X))) | n5(X)) <=> ![X: $i] : (n5(X) | q(s5(X)) | q(X))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[62])).
% 0.23/0.52 tff(64,axiom,(![X: $i] : ((q(X) | q(s5(X))) | n5(X))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_16')).
% 0.23/0.52 tff(65,plain,
% 0.23/0.52 (![X: $i] : (n5(X) | q(s5(X)) | q(X))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.23/0.52 tff(66,plain,
% 0.23/0.52 (![X: $i] : (n5(X) | q(s5(X)) | q(X))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[65, 61])).
% 0.23/0.52 tff(67,plain,(
% 0.23/0.52 ![X: $i] : (n5(X) | q(s5(X)) | q(X))),
% 0.23/0.52 inference(skolemize,[status(sab)],[66])).
% 0.23/0.52 tff(68,plain,
% 0.23/0.52 (![X: $i] : (n5(X) | q(s5(X)) | q(X))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[67, 60])).
% 0.23/0.52 tff(69,plain,
% 0.23/0.52 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (q(s4) | n5(s4) | q(s5(s4)))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s4) | n5(s4) | q(s5(s4)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(70,plain,
% 0.23/0.52 ((n5(s4) | q(s5(s4)) | q(s4)) <=> (q(s4) | n5(s4) | q(s5(s4)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(71,plain,
% 0.23/0.52 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s4) | q(s5(s4)) | q(s4))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (q(s4) | n5(s4) | q(s5(s4))))),
% 0.23/0.52 inference(monotonicity,[status(thm)],[70])).
% 0.23/0.52 tff(72,plain,
% 0.23/0.52 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s4) | q(s5(s4)) | q(s4))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s4) | n5(s4) | q(s5(s4)))),
% 0.23/0.52 inference(transitivity,[status(thm)],[71, 69])).
% 0.23/0.52 tff(73,plain,
% 0.23/0.52 ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s4) | q(s5(s4)) | q(s4))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(74,plain,
% 0.23/0.52 ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s4) | n5(s4) | q(s5(s4))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.23/0.52 tff(75,plain,
% 0.23/0.52 (q(s4) | n5(s4) | q(s5(s4))),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[74, 68])).
% 0.23/0.52 tff(76,plain,
% 0.23/0.52 (n5(s4)),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[75, 38, 58])).
% 0.23/0.52 tff(77,assumption,(n5(s4)), introduced(assumption)).
% 0.23/0.52 tff(78,plain,
% 0.23/0.52 (^[X6: $i] : refl((n6 | (~n5(X6))) <=> (n6 | (~n5(X6))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(79,plain,
% 0.23/0.52 (![X6: $i] : (n6 | (~n5(X6))) <=> ![X6: $i] : (n6 | (~n5(X6)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[78])).
% 0.23/0.52 tff(80,plain,
% 0.23/0.52 (![X6: $i] : (n6 | (~n5(X6))) <=> ![X6: $i] : (n6 | (~n5(X6)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(81,plain,
% 0.23/0.52 (^[X6: $i] : rewrite(((~n5(X6)) | n6) <=> (n6 | (~n5(X6))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(82,plain,
% 0.23/0.52 (![X6: $i] : ((~n5(X6)) | n6) <=> ![X6: $i] : (n6 | (~n5(X6)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[81])).
% 0.23/0.52 tff(83,axiom,(![X6: $i] : ((~n5(X6)) | n6)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_13')).
% 0.23/0.52 tff(84,plain,
% 0.23/0.52 (![X6: $i] : (n6 | (~n5(X6)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.23/0.52 tff(85,plain,
% 0.23/0.52 (![X6: $i] : (n6 | (~n5(X6)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[84, 80])).
% 0.23/0.52 tff(86,plain,(
% 0.23/0.52 ![X6: $i] : (n6 | (~n5(X6)))),
% 0.23/0.52 inference(skolemize,[status(sab)],[85])).
% 0.23/0.52 tff(87,plain,
% 0.23/0.52 (![X6: $i] : (n6 | (~n5(X6)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[86, 79])).
% 0.23/0.52 tff(88,assumption,(~n6), introduced(assumption)).
% 0.23/0.52 tff(89,plain,
% 0.23/0.52 (((~![X6: $i] : (n6 | (~n5(X6)))) | (n6 | (~n5(s4)))) <=> ((~![X6: $i] : (n6 | (~n5(X6)))) | n6 | (~n5(s4)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(90,plain,
% 0.23/0.52 ((~![X6: $i] : (n6 | (~n5(X6)))) | (n6 | (~n5(s4)))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(91,plain,
% 0.23/0.52 ((~![X6: $i] : (n6 | (~n5(X6)))) | n6 | (~n5(s4))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.23/0.52 tff(92,plain,
% 0.23/0.52 ($false),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[91, 88, 87, 77])).
% 0.23/0.52 tff(93,plain,((~n5(s4)) | n6), inference(lemma,lemma(discharge,[]))).
% 0.23/0.52 tff(94,plain,
% 0.23/0.52 (n6),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[93, 76])).
% 0.23/0.52 tff(95,assumption,(n9), introduced(assumption)).
% 0.23/0.52 tff(96,assumption,(n6), introduced(assumption)).
% 0.23/0.52 tff(97,assumption,(~n10), introduced(assumption)).
% 0.23/0.52 tff(98,plain,
% 0.23/0.52 ((n2 | (~n9) | (~n6) | n10) <=> (n2 | (~n9) | (~n6) | n10)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(99,plain,
% 0.23/0.52 (((n2 | (~n9) | (~n6)) | n10) <=> (n2 | (~n9) | (~n6) | n10)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(100,plain,
% 0.23/0.52 (((n2 | (~n9)) | (~n6)) <=> (n2 | (~n9) | (~n6))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(101,plain,
% 0.23/0.52 ((((n2 | (~n9)) | (~n6)) | n10) <=> ((n2 | (~n9) | (~n6)) | n10)),
% 0.23/0.52 inference(monotonicity,[status(thm)],[100])).
% 0.23/0.52 tff(102,plain,
% 0.23/0.52 ((((n2 | (~n9)) | (~n6)) | n10) <=> (n2 | (~n9) | (~n6) | n10)),
% 0.23/0.52 inference(transitivity,[status(thm)],[101, 99])).
% 0.23/0.52 tff(103,axiom,(((n2 | (~n9)) | (~n6)) | n10), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_7')).
% 0.23/0.52 tff(104,plain,
% 0.23/0.52 (n2 | (~n9) | (~n6) | n10),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.23/0.52 tff(105,plain,
% 0.23/0.52 (n2 | (~n9) | (~n6) | n10),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[104, 98])).
% 0.23/0.52 tff(106,plain,
% 0.23/0.52 (n2 | (~n9) | (~n6) | n10),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[105, 98])).
% 0.23/0.52 tff(107,plain,
% 0.23/0.52 (n2 | (~n9) | (~n6) | n10),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[106, 98])).
% 0.23/0.52 tff(108,plain,
% 0.23/0.52 (n2 | (~n9) | (~n6) | n10),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[107, 98])).
% 0.23/0.52 tff(109,plain,
% 0.23/0.52 (n2),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[108, 97, 96, 95])).
% 0.23/0.52 tff(110,plain,
% 0.23/0.52 (((~n2) | n1(s2)) <=> ((~n2) | n1(s2))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(111,axiom,((~n2) | n1(s2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_24')).
% 0.23/0.52 tff(112,plain,
% 0.23/0.52 ((~n2) | n1(s2)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.23/0.52 tff(113,plain,
% 0.23/0.52 ((~n2) | n1(s2)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[112, 110])).
% 0.23/0.52 tff(114,plain,
% 0.23/0.52 ((~n2) | n1(s2)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[113, 110])).
% 0.23/0.52 tff(115,plain,
% 0.23/0.52 ((~n2) | n1(s2)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[114, 110])).
% 0.23/0.52 tff(116,plain,
% 0.23/0.52 ((~n2) | n1(s2)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[115, 110])).
% 0.23/0.52 tff(117,plain,
% 0.23/0.52 (n1(s2)),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[116, 109])).
% 0.23/0.52 tff(118,assumption,(~n7), introduced(assumption)).
% 0.23/0.52 tff(119,assumption,(p(s1(s8))), introduced(assumption)).
% 0.23/0.52 tff(120,plain,
% 0.23/0.52 (^[X7: $i] : refl((n7 | (~p(X7))) <=> (n7 | (~p(X7))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(121,plain,
% 0.23/0.52 (![X7: $i] : (n7 | (~p(X7))) <=> ![X7: $i] : (n7 | (~p(X7)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[120])).
% 0.23/0.52 tff(122,plain,
% 0.23/0.52 (![X7: $i] : (n7 | (~p(X7))) <=> ![X7: $i] : (n7 | (~p(X7)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(123,plain,
% 0.23/0.52 (^[X7: $i] : rewrite(((~p(X7)) | n7) <=> (n7 | (~p(X7))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(124,plain,
% 0.23/0.52 (![X7: $i] : ((~p(X7)) | n7) <=> ![X7: $i] : (n7 | (~p(X7)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[123])).
% 0.23/0.52 tff(125,axiom,(![X7: $i] : ((~p(X7)) | n7)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_11')).
% 0.23/0.52 tff(126,plain,
% 0.23/0.52 (![X7: $i] : (n7 | (~p(X7)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[125, 124])).
% 0.23/0.52 tff(127,plain,
% 0.23/0.52 (![X7: $i] : (n7 | (~p(X7)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[126, 122])).
% 0.23/0.52 tff(128,plain,(
% 0.23/0.52 ![X7: $i] : (n7 | (~p(X7)))),
% 0.23/0.52 inference(skolemize,[status(sab)],[127])).
% 0.23/0.52 tff(129,plain,
% 0.23/0.52 (![X7: $i] : (n7 | (~p(X7)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[128, 121])).
% 0.23/0.52 tff(130,plain,
% 0.23/0.52 (((~![X7: $i] : (n7 | (~p(X7)))) | (n7 | (~p(s1(s8))))) <=> ((~![X7: $i] : (n7 | (~p(X7)))) | n7 | (~p(s1(s8))))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(131,plain,
% 0.23/0.52 ((~![X7: $i] : (n7 | (~p(X7)))) | (n7 | (~p(s1(s8))))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(132,plain,
% 0.23/0.52 ((~![X7: $i] : (n7 | (~p(X7)))) | n7 | (~p(s1(s8)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.23/0.52 tff(133,plain,
% 0.23/0.52 ($false),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[132, 129, 118, 119])).
% 0.23/0.52 tff(134,plain,((~p(s1(s8))) | n7), inference(lemma,lemma(discharge,[]))).
% 0.23/0.52 tff(135,plain,
% 0.23/0.52 (~p(s1(s8))),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[134, 118])).
% 0.23/0.52 tff(136,plain,
% 0.23/0.52 ((n10 | n8 | n7) <=> (n10 | n8 | n7)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(137,plain,
% 0.23/0.52 (((n7 | n8) | n10) <=> (n10 | n8 | n7)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(138,axiom,((n7 | n8) | n10), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_34')).
% 0.23/0.52 tff(139,plain,
% 0.23/0.52 (n10 | n8 | n7),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[138, 137])).
% 0.23/0.52 tff(140,plain,
% 0.23/0.52 (n10 | n8 | n7),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[139, 136])).
% 0.23/0.52 tff(141,plain,
% 0.23/0.52 (n10 | n8 | n7),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[140, 136])).
% 0.23/0.52 tff(142,plain,
% 0.23/0.52 (n10 | n8 | n7),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[141, 136])).
% 0.23/0.52 tff(143,plain,
% 0.23/0.52 (n10 | n8 | n7),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[142, 136])).
% 0.23/0.52 tff(144,plain,
% 0.23/0.52 (n8),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[143, 118, 97])).
% 0.23/0.52 tff(145,plain,
% 0.23/0.52 (((~![X8: $i] : ((~n8) | p(X8))) | ((~n8) | p(s1(s8)))) <=> ((~![X8: $i] : ((~n8) | p(X8))) | (~n8) | p(s1(s8)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(146,plain,
% 0.23/0.52 ((~![X8: $i] : ((~n8) | p(X8))) | ((~n8) | p(s1(s8)))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(147,plain,
% 0.23/0.52 ((~![X8: $i] : ((~n8) | p(X8))) | (~n8) | p(s1(s8))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.23/0.52 tff(148,plain,
% 0.23/0.52 ($false),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[147, 144, 23, 135])).
% 0.23/0.52 tff(149,plain,(n7 | n10), inference(lemma,lemma(discharge,[]))).
% 0.23/0.52 tff(150,plain,
% 0.23/0.52 (n7),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[149, 97])).
% 0.23/0.52 tff(151,plain,
% 0.23/0.52 ((n10 | (~n7) | (~n8)) <=> (n10 | (~n7) | (~n8))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(152,plain,
% 0.23/0.52 ((((~n7) | (~n8)) | n10) <=> (n10 | (~n7) | (~n8))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(153,axiom,(((~n7) | (~n8)) | n10), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_33')).
% 0.23/0.52 tff(154,plain,
% 0.23/0.52 (n10 | (~n7) | (~n8)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.23/0.52 tff(155,plain,
% 0.23/0.52 (n10 | (~n7) | (~n8)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[154, 151])).
% 0.23/0.52 tff(156,plain,
% 0.23/0.52 (~n8),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[155, 150, 97])).
% 0.23/0.52 tff(157,plain,
% 0.23/0.52 (((~p(s8)) | n8) <=> ((~p(s8)) | n8)),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(158,axiom,((~p(s8)) | n8), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_9')).
% 0.23/0.52 tff(159,plain,
% 0.23/0.52 ((~p(s8)) | n8),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[158, 157])).
% 0.23/0.52 tff(160,plain,
% 0.23/0.52 ((~p(s8)) | n8),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[159, 157])).
% 0.23/0.52 tff(161,plain,
% 0.23/0.52 ((~p(s8)) | n8),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[160, 157])).
% 0.23/0.52 tff(162,plain,
% 0.23/0.52 ((~p(s8)) | n8),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[161, 157])).
% 0.23/0.52 tff(163,plain,
% 0.23/0.52 ((~p(s8)) | n8),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[162, 157])).
% 0.23/0.52 tff(164,plain,
% 0.23/0.52 (~p(s8)),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[163, 156])).
% 0.23/0.52 tff(165,plain,
% 0.23/0.52 (^[X: $i, X1: $i] : refl(((~p(X1)) | p(X) | (~n1(X))) <=> ((~p(X1)) | p(X) | (~n1(X))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(166,plain,
% 0.23/0.52 (![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X))) <=> ![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[165])).
% 0.23/0.52 tff(167,plain,
% 0.23/0.52 (![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X))) <=> ![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(168,plain,
% 0.23/0.52 (^[X: $i, X1: $i] : trans(monotonicity(rewrite(((~n1(X)) | p(X)) <=> (p(X) | (~n1(X)))), ((((~n1(X)) | p(X)) | (~p(X1))) <=> ((p(X) | (~n1(X))) | (~p(X1))))), rewrite(((p(X) | (~n1(X))) | (~p(X1))) <=> ((~p(X1)) | p(X) | (~n1(X)))), ((((~n1(X)) | p(X)) | (~p(X1))) <=> ((~p(X1)) | p(X) | (~n1(X)))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(169,plain,
% 0.23/0.52 (![X: $i, X1: $i] : (((~n1(X)) | p(X)) | (~p(X1))) <=> ![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[168])).
% 0.23/0.52 tff(170,axiom,(![X: $i, X1: $i] : (((~n1(X)) | p(X)) | (~p(X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_28')).
% 0.23/0.52 tff(171,plain,
% 0.23/0.52 (![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[170, 169])).
% 0.23/0.52 tff(172,plain,
% 0.23/0.52 (![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[171, 167])).
% 0.23/0.52 tff(173,plain,(
% 0.23/0.52 ![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))),
% 0.23/0.52 inference(skolemize,[status(sab)],[172])).
% 0.23/0.52 tff(174,plain,
% 0.23/0.52 (![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[173, 166])).
% 0.23/0.52 tff(175,plain,
% 0.23/0.52 (((~n7) | p(s7)) <=> ((~n7) | p(s7))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(176,axiom,((~n7) | p(s7)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_12')).
% 0.23/0.52 tff(177,plain,
% 0.23/0.52 ((~n7) | p(s7)),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[176, 175])).
% 0.23/0.52 tff(178,plain,
% 0.23/0.52 (p(s7)),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[177, 150])).
% 0.23/0.52 tff(179,plain,
% 0.23/0.52 (((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | (p(s8) | (~p(s7)) | (~n1(s8)))) <=> ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | p(s8) | (~p(s7)) | (~n1(s8)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(180,plain,
% 0.23/0.52 (((~p(s7)) | p(s8) | (~n1(s8))) <=> (p(s8) | (~p(s7)) | (~n1(s8)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(181,plain,
% 0.23/0.52 (((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | ((~p(s7)) | p(s8) | (~n1(s8)))) <=> ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | (p(s8) | (~p(s7)) | (~n1(s8))))),
% 0.23/0.52 inference(monotonicity,[status(thm)],[180])).
% 0.23/0.52 tff(182,plain,
% 0.23/0.52 (((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | ((~p(s7)) | p(s8) | (~n1(s8)))) <=> ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | p(s8) | (~p(s7)) | (~n1(s8)))),
% 0.23/0.52 inference(transitivity,[status(thm)],[181, 179])).
% 0.23/0.52 tff(183,plain,
% 0.23/0.52 ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | ((~p(s7)) | p(s8) | (~n1(s8)))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(184,plain,
% 0.23/0.52 ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | p(s8) | (~p(s7)) | (~n1(s8))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[183, 182])).
% 0.23/0.52 tff(185,plain,
% 0.23/0.52 (~n1(s8)),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[184, 164, 178, 174])).
% 0.23/0.52 tff(186,plain,
% 0.23/0.52 (^[X: $i] : refl((p(X) | n1(X) | p(s1(X))) <=> (p(X) | n1(X) | p(s1(X))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(187,plain,
% 0.23/0.52 (![X: $i] : (p(X) | n1(X) | p(s1(X))) <=> ![X: $i] : (p(X) | n1(X) | p(s1(X)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[186])).
% 0.23/0.52 tff(188,plain,
% 0.23/0.52 (![X: $i] : (p(X) | n1(X) | p(s1(X))) <=> ![X: $i] : (p(X) | n1(X) | p(s1(X)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(189,plain,
% 0.23/0.52 (^[X: $i] : rewrite(((p(X) | p(s1(X))) | n1(X)) <=> (p(X) | n1(X) | p(s1(X))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(190,plain,
% 0.23/0.52 (![X: $i] : ((p(X) | p(s1(X))) | n1(X)) <=> ![X: $i] : (p(X) | n1(X) | p(s1(X)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[189])).
% 0.23/0.52 tff(191,axiom,(![X: $i] : ((p(X) | p(s1(X))) | n1(X))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_26')).
% 0.23/0.52 tff(192,plain,
% 0.23/0.52 (![X: $i] : (p(X) | n1(X) | p(s1(X)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[191, 190])).
% 0.23/0.52 tff(193,plain,
% 0.23/0.52 (![X: $i] : (p(X) | n1(X) | p(s1(X)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[192, 188])).
% 0.23/0.52 tff(194,plain,(
% 0.23/0.52 ![X: $i] : (p(X) | n1(X) | p(s1(X)))),
% 0.23/0.52 inference(skolemize,[status(sab)],[193])).
% 0.23/0.52 tff(195,plain,
% 0.23/0.52 (![X: $i] : (p(X) | n1(X) | p(s1(X)))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[194, 187])).
% 0.23/0.52 tff(196,plain,
% 0.23/0.52 (((~![X: $i] : (p(X) | n1(X) | p(s1(X)))) | (p(s8) | n1(s8) | p(s1(s8)))) <=> ((~![X: $i] : (p(X) | n1(X) | p(s1(X)))) | p(s8) | n1(s8) | p(s1(s8)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(197,plain,
% 0.23/0.52 ((~![X: $i] : (p(X) | n1(X) | p(s1(X)))) | (p(s8) | n1(s8) | p(s1(s8)))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(198,plain,
% 0.23/0.52 ((~![X: $i] : (p(X) | n1(X) | p(s1(X)))) | p(s8) | n1(s8) | p(s1(s8))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[197, 196])).
% 0.23/0.52 tff(199,plain,
% 0.23/0.52 (p(s8) | n1(s8) | p(s1(s8))),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[198, 195])).
% 0.23/0.52 tff(200,plain,
% 0.23/0.52 (p(s1(s8))),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[199, 185, 164])).
% 0.23/0.52 tff(201,plain,
% 0.23/0.52 (((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | ((~p(s1(s8))) | p(s2) | (~n1(s2)))) <=> ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | (~p(s1(s8))) | p(s2) | (~n1(s2)))),
% 0.23/0.52 inference(rewrite,[status(thm)],[])).
% 0.23/0.52 tff(202,plain,
% 0.23/0.52 ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | ((~p(s1(s8))) | p(s2) | (~n1(s2)))),
% 0.23/0.52 inference(quant_inst,[status(thm)],[])).
% 0.23/0.52 tff(203,plain,
% 0.23/0.52 ((~![X: $i, X1: $i] : ((~p(X1)) | p(X) | (~n1(X)))) | (~p(s1(s8))) | p(s2) | (~n1(s2))),
% 0.23/0.52 inference(modus_ponens,[status(thm)],[202, 201])).
% 0.23/0.52 tff(204,plain,
% 0.23/0.52 ((~p(s1(s8))) | p(s2) | (~n1(s2))),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[203, 174])).
% 0.23/0.52 tff(205,plain,
% 0.23/0.52 (p(s2)),
% 0.23/0.52 inference(unit_resolution,[status(thm)],[204, 200, 117])).
% 0.23/0.52 tff(206,plain,
% 0.23/0.52 (^[X: $i, X1: $i] : refl((p(X1) | (~p(X)) | (~n1(X))) <=> (p(X1) | (~p(X)) | (~n1(X))))),
% 0.23/0.52 inference(bind,[status(th)],[])).
% 0.23/0.52 tff(207,plain,
% 0.23/0.52 (![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X))) <=> ![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))),
% 0.23/0.52 inference(quant_intro,[status(thm)],[206])).
% 0.23/0.53 tff(208,plain,
% 0.23/0.53 (![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X))) <=> ![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(209,plain,
% 0.23/0.53 (^[X: $i, X1: $i] : rewrite((((~n1(X)) | (~p(X))) | p(X1)) <=> (p(X1) | (~p(X)) | (~n1(X))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(210,plain,
% 0.23/0.53 (![X: $i, X1: $i] : (((~n1(X)) | (~p(X))) | p(X1)) <=> ![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[209])).
% 0.23/0.53 tff(211,axiom,(![X: $i, X1: $i] : (((~n1(X)) | (~p(X))) | p(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_27')).
% 0.23/0.53 tff(212,plain,
% 0.23/0.53 (![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[211, 210])).
% 0.23/0.53 tff(213,plain,
% 0.23/0.53 (![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[212, 208])).
% 0.23/0.53 tff(214,plain,(
% 0.23/0.53 ![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))),
% 0.23/0.53 inference(skolemize,[status(sab)],[213])).
% 0.23/0.53 tff(215,plain,
% 0.23/0.53 (![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[214, 207])).
% 0.23/0.53 tff(216,plain,
% 0.23/0.53 (((~![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))) | (p(s8) | (~p(s2)) | (~n1(s2)))) <=> ((~![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))) | p(s8) | (~p(s2)) | (~n1(s2)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(217,plain,
% 0.23/0.53 ((~![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))) | (p(s8) | (~p(s2)) | (~n1(s2)))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(218,plain,
% 0.23/0.53 ((~![X: $i, X1: $i] : (p(X1) | (~p(X)) | (~n1(X)))) | p(s8) | (~p(s2)) | (~n1(s2))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[217, 216])).
% 0.23/0.53 tff(219,plain,
% 0.23/0.53 ($false),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[218, 164, 117, 215, 205])).
% 0.23/0.53 tff(220,plain,(n10 | (~n6) | (~n9)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.53 tff(221,plain,
% 0.23/0.53 (n10),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[220, 94, 48])).
% 0.23/0.53 tff(222,plain,
% 0.23/0.53 (((~n2) | (~n9) | (~n6) | (~n10)) <=> ((~n2) | (~n9) | (~n6) | (~n10))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(223,plain,
% 0.23/0.53 ((((~n2) | (~n9) | (~n6)) | (~n10)) <=> ((~n2) | (~n9) | (~n6) | (~n10))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(224,plain,
% 0.23/0.53 ((((~n2) | (~n9)) | (~n6)) <=> ((~n2) | (~n9) | (~n6))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(225,plain,
% 0.23/0.53 (((((~n2) | (~n9)) | (~n6)) | (~n10)) <=> (((~n2) | (~n9) | (~n6)) | (~n10))),
% 0.23/0.53 inference(monotonicity,[status(thm)],[224])).
% 0.23/0.53 tff(226,plain,
% 0.23/0.53 (((((~n2) | (~n9)) | (~n6)) | (~n10)) <=> ((~n2) | (~n9) | (~n6) | (~n10))),
% 0.23/0.53 inference(transitivity,[status(thm)],[225, 223])).
% 0.23/0.53 tff(227,axiom,((((~n2) | (~n9)) | (~n6)) | (~n10)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_1')).
% 0.23/0.53 tff(228,plain,
% 0.23/0.53 ((~n2) | (~n9) | (~n6) | (~n10)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[227, 226])).
% 0.23/0.53 tff(229,plain,
% 0.23/0.53 ((~n2) | (~n9) | (~n6) | (~n10)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[228, 222])).
% 0.23/0.53 tff(230,plain,
% 0.23/0.53 ((~n2) | (~n9) | (~n6) | (~n10)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[229, 222])).
% 0.23/0.53 tff(231,plain,
% 0.23/0.53 ((~n2) | (~n9) | (~n6) | (~n10)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[230, 222])).
% 0.23/0.53 tff(232,plain,
% 0.23/0.53 ((~n2) | (~n9) | (~n6) | (~n10)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[231, 222])).
% 0.23/0.53 tff(233,plain,
% 0.23/0.53 (~n2),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[232, 221, 94, 48])).
% 0.23/0.53 tff(234,assumption,(n1(s8)), introduced(assumption)).
% 0.23/0.53 tff(235,plain,
% 0.23/0.53 (^[X2: $i] : refl((n2 | (~n1(X2))) <=> (n2 | (~n1(X2))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(236,plain,
% 0.23/0.53 (![X2: $i] : (n2 | (~n1(X2))) <=> ![X2: $i] : (n2 | (~n1(X2)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[235])).
% 0.23/0.53 tff(237,plain,
% 0.23/0.53 (![X2: $i] : (n2 | (~n1(X2))) <=> ![X2: $i] : (n2 | (~n1(X2)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(238,plain,
% 0.23/0.53 (^[X2: $i] : rewrite(((~n1(X2)) | n2) <=> (n2 | (~n1(X2))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(239,plain,
% 0.23/0.53 (![X2: $i] : ((~n1(X2)) | n2) <=> ![X2: $i] : (n2 | (~n1(X2)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[238])).
% 0.23/0.53 tff(240,axiom,(![X2: $i] : ((~n1(X2)) | n2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_23')).
% 0.23/0.53 tff(241,plain,
% 0.23/0.53 (![X2: $i] : (n2 | (~n1(X2)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[240, 239])).
% 0.23/0.53 tff(242,plain,
% 0.23/0.53 (![X2: $i] : (n2 | (~n1(X2)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[241, 237])).
% 0.23/0.53 tff(243,plain,(
% 0.23/0.53 ![X2: $i] : (n2 | (~n1(X2)))),
% 0.23/0.53 inference(skolemize,[status(sab)],[242])).
% 0.23/0.53 tff(244,plain,
% 0.23/0.53 (![X2: $i] : (n2 | (~n1(X2)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[243, 236])).
% 0.23/0.53 tff(245,assumption,(~n2), introduced(assumption)).
% 0.23/0.53 tff(246,plain,
% 0.23/0.53 (((~![X2: $i] : (n2 | (~n1(X2)))) | (n2 | (~n1(s8)))) <=> ((~![X2: $i] : (n2 | (~n1(X2)))) | n2 | (~n1(s8)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(247,plain,
% 0.23/0.53 ((~![X2: $i] : (n2 | (~n1(X2)))) | (n2 | (~n1(s8)))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(248,plain,
% 0.23/0.53 ((~![X2: $i] : (n2 | (~n1(X2)))) | n2 | (~n1(s8))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[247, 246])).
% 0.23/0.53 tff(249,plain,
% 0.23/0.53 ($false),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[248, 245, 244, 234])).
% 0.23/0.53 tff(250,plain,((~n1(s8)) | n2), inference(lemma,lemma(discharge,[]))).
% 0.23/0.53 tff(251,plain,
% 0.23/0.53 (~n1(s8)),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[250, 233])).
% 0.23/0.53 tff(252,plain,
% 0.23/0.53 (((~n10) | (~n8) | n7) <=> ((~n10) | (~n8) | n7)),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(253,plain,
% 0.23/0.53 (((n7 | (~n8)) | (~n10)) <=> ((~n10) | (~n8) | n7)),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(254,axiom,((n7 | (~n8)) | (~n10)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_36')).
% 0.23/0.53 tff(255,plain,
% 0.23/0.53 ((~n10) | (~n8) | n7),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[254, 253])).
% 0.23/0.53 tff(256,plain,
% 0.23/0.53 ((~n10) | (~n8) | n7),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[255, 252])).
% 0.23/0.53 tff(257,plain,
% 0.23/0.53 ((~n10) | (~n8) | n7),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[256, 252])).
% 0.23/0.53 tff(258,plain,
% 0.23/0.53 ((~n10) | (~n8) | n7),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[257, 252])).
% 0.23/0.53 tff(259,plain,
% 0.23/0.53 ((~n10) | (~n8) | n7),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[258, 252])).
% 0.23/0.53 tff(260,plain,
% 0.23/0.53 (~n8),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[259, 118, 1])).
% 0.23/0.53 tff(261,assumption,(~n1(s8)), introduced(assumption)).
% 0.23/0.53 tff(262,plain,
% 0.23/0.53 (p(s8)),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[199, 135, 261])).
% 0.23/0.53 tff(263,plain,
% 0.23/0.53 ($false),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[163, 262, 260])).
% 0.23/0.53 tff(264,plain,(n7 | n1(s8) | (~n10)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.53 tff(265,plain,
% 0.23/0.53 (n7),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[264, 251, 221])).
% 0.23/0.53 tff(266,plain,
% 0.23/0.53 (((~n10) | n8 | (~n7)) <=> ((~n10) | n8 | (~n7))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(267,plain,
% 0.23/0.53 (((n8 | (~n7)) | (~n10)) <=> ((~n10) | n8 | (~n7))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(268,plain,
% 0.23/0.53 (((~n7) | n8) <=> (n8 | (~n7))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(269,plain,
% 0.23/0.53 ((((~n7) | n8) | (~n10)) <=> ((n8 | (~n7)) | (~n10))),
% 0.23/0.53 inference(monotonicity,[status(thm)],[268])).
% 0.23/0.53 tff(270,plain,
% 0.23/0.53 ((((~n7) | n8) | (~n10)) <=> ((~n10) | n8 | (~n7))),
% 0.23/0.53 inference(transitivity,[status(thm)],[269, 267])).
% 0.23/0.53 tff(271,axiom,(((~n7) | n8) | (~n10)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_35')).
% 0.23/0.53 tff(272,plain,
% 0.23/0.53 ((~n10) | n8 | (~n7)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[271, 270])).
% 0.23/0.53 tff(273,plain,
% 0.23/0.53 ((~n10) | n8 | (~n7)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[272, 266])).
% 0.23/0.53 tff(274,plain,
% 0.23/0.53 ((~n10) | n8 | (~n7)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[273, 266])).
% 0.23/0.53 tff(275,plain,
% 0.23/0.53 ((~n10) | n8 | (~n7)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[274, 266])).
% 0.23/0.53 tff(276,plain,
% 0.23/0.53 ((~n10) | n8 | (~n7)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[275, 266])).
% 0.23/0.53 tff(277,plain,
% 0.23/0.53 (n8),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[276, 265, 221])).
% 0.23/0.53 tff(278,assumption,(~p(s1(s8))), introduced(assumption)).
% 0.23/0.53 tff(279,assumption,(n8), introduced(assumption)).
% 0.23/0.53 tff(280,plain,
% 0.23/0.53 ($false),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[147, 279, 23, 278])).
% 0.23/0.53 tff(281,plain,(p(s1(s8)) | (~n8)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.53 tff(282,plain,
% 0.23/0.53 (p(s1(s8))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[281, 277])).
% 0.23/0.53 tff(283,plain,
% 0.23/0.53 (^[X: $i] : refl(((~p(X)) | n1(X) | (~p(s1(X)))) <=> ((~p(X)) | n1(X) | (~p(s1(X)))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(284,plain,
% 0.23/0.53 (![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X)))) <=> ![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[283])).
% 0.23/0.53 tff(285,plain,
% 0.23/0.53 (![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X)))) <=> ![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(286,plain,
% 0.23/0.53 (^[X: $i] : rewrite((((~p(X)) | (~p(s1(X)))) | n1(X)) <=> ((~p(X)) | n1(X) | (~p(s1(X)))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(287,plain,
% 0.23/0.53 (![X: $i] : (((~p(X)) | (~p(s1(X)))) | n1(X)) <=> ![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[286])).
% 0.23/0.53 tff(288,axiom,(![X: $i] : (((~p(X)) | (~p(s1(X)))) | n1(X))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_25')).
% 0.23/0.53 tff(289,plain,
% 0.23/0.53 (![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[288, 287])).
% 0.23/0.53 tff(290,plain,
% 0.23/0.53 (![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[289, 285])).
% 0.23/0.53 tff(291,plain,(
% 0.23/0.53 ![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))),
% 0.23/0.53 inference(skolemize,[status(sab)],[290])).
% 0.23/0.53 tff(292,plain,
% 0.23/0.53 (![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[291, 284])).
% 0.23/0.53 tff(293,plain,
% 0.23/0.53 (((~![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))) | ((~p(s8)) | n1(s8) | (~p(s1(s8))))) <=> ((~![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))) | (~p(s8)) | n1(s8) | (~p(s1(s8))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(294,plain,
% 0.23/0.53 ((~![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))) | ((~p(s8)) | n1(s8) | (~p(s1(s8))))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(295,plain,
% 0.23/0.53 ((~![X: $i] : ((~p(X)) | n1(X) | (~p(s1(X))))) | (~p(s8)) | n1(s8) | (~p(s1(s8)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[294, 293])).
% 0.23/0.53 tff(296,plain,
% 0.23/0.53 ((~p(s8)) | (~p(s1(s8)))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[295, 292, 251])).
% 0.23/0.53 tff(297,plain,
% 0.23/0.53 (~p(s8)),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[296, 282])).
% 0.23/0.53 tff(298,plain,
% 0.23/0.53 (((~![X8: $i] : ((~n8) | p(X8))) | ((~n8) | p(s8))) <=> ((~![X8: $i] : ((~n8) | p(X8))) | (~n8) | p(s8))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(299,plain,
% 0.23/0.53 ((~![X8: $i] : ((~n8) | p(X8))) | ((~n8) | p(s8))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(300,plain,
% 0.23/0.53 ((~![X8: $i] : ((~n8) | p(X8))) | (~n8) | p(s8)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[299, 298])).
% 0.23/0.53 tff(301,plain,
% 0.23/0.53 ($false),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[300, 297, 277, 23])).
% 0.23/0.53 tff(302,plain,(n3), inference(lemma,lemma(discharge,[]))).
% 0.23/0.53 tff(303,plain,
% 0.23/0.53 (((~n9) | n4 | (~n3)) <=> ((~n9) | n4 | (~n3))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(304,plain,
% 0.23/0.53 (((n4 | (~n3)) | (~n9)) <=> ((~n9) | n4 | (~n3))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(305,plain,
% 0.23/0.53 (((~n3) | n4) <=> (n4 | (~n3))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(306,plain,
% 0.23/0.53 ((((~n3) | n4) | (~n9)) <=> ((n4 | (~n3)) | (~n9))),
% 0.23/0.53 inference(monotonicity,[status(thm)],[305])).
% 0.23/0.53 tff(307,plain,
% 0.23/0.53 ((((~n3) | n4) | (~n9)) <=> ((~n9) | n4 | (~n3))),
% 0.23/0.53 inference(transitivity,[status(thm)],[306, 304])).
% 0.23/0.53 tff(308,axiom,(((~n3) | n4) | (~n9)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_31')).
% 0.23/0.53 tff(309,plain,
% 0.23/0.53 ((~n9) | n4 | (~n3)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[308, 307])).
% 0.23/0.53 tff(310,plain,
% 0.23/0.53 ((~n9) | n4 | (~n3)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[309, 303])).
% 0.23/0.53 tff(311,plain,
% 0.23/0.53 ((~n9) | n4 | (~n3)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[310, 303])).
% 0.23/0.53 tff(312,plain,
% 0.23/0.53 ((~n9) | n4 | (~n3)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[311, 303])).
% 0.23/0.53 tff(313,plain,
% 0.23/0.53 ((~n9) | n4 | (~n3)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[312, 303])).
% 0.23/0.53 tff(314,plain,
% 0.23/0.53 ((~n9) | n4),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[313, 302])).
% 0.23/0.53 tff(315,plain,
% 0.23/0.53 (~n9),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[314, 16])).
% 0.23/0.53 tff(316,assumption,(n5(s5(s5(s5(s4))))), introduced(assumption)).
% 0.23/0.53 tff(317,plain,
% 0.23/0.53 (((~n3) | q(s3)) <=> ((~n3) | q(s3))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(318,axiom,((~n3) | q(s3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_22')).
% 0.23/0.53 tff(319,plain,
% 0.23/0.53 ((~n3) | q(s3)),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[318, 317])).
% 0.23/0.53 tff(320,plain,
% 0.23/0.53 (q(s3)),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[319, 302])).
% 0.23/0.53 tff(321,plain,
% 0.23/0.53 (^[X: $i, X5: $i] : refl(((~q(X5)) | q(X) | (~n5(X))) <=> ((~q(X5)) | q(X) | (~n5(X))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(322,plain,
% 0.23/0.53 (![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X))) <=> ![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[321])).
% 0.23/0.53 tff(323,plain,
% 0.23/0.53 (![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X))) <=> ![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(324,plain,
% 0.23/0.53 (^[X: $i, X5: $i] : trans(monotonicity(rewrite(((~n5(X)) | q(X)) <=> (q(X) | (~n5(X)))), ((((~n5(X)) | q(X)) | (~q(X5))) <=> ((q(X) | (~n5(X))) | (~q(X5))))), rewrite(((q(X) | (~n5(X))) | (~q(X5))) <=> ((~q(X5)) | q(X) | (~n5(X)))), ((((~n5(X)) | q(X)) | (~q(X5))) <=> ((~q(X5)) | q(X) | (~n5(X)))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(325,plain,
% 0.23/0.53 (![X: $i, X5: $i] : (((~n5(X)) | q(X)) | (~q(X5))) <=> ![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[324])).
% 0.23/0.53 tff(326,axiom,(![X: $i, X5: $i] : (((~n5(X)) | q(X)) | (~q(X5)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_18')).
% 0.23/0.53 tff(327,plain,
% 0.23/0.53 (![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[326, 325])).
% 0.23/0.53 tff(328,plain,
% 0.23/0.53 (![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[327, 323])).
% 0.23/0.53 tff(329,plain,(
% 0.23/0.53 ![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))),
% 0.23/0.53 inference(skolemize,[status(sab)],[328])).
% 0.23/0.53 tff(330,plain,
% 0.23/0.53 (![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[329, 322])).
% 0.23/0.53 tff(331,plain,
% 0.23/0.53 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (q(s4) | (~n5(s4)) | (~q(s3)))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | q(s4) | (~n5(s4)) | (~q(s3)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(332,plain,
% 0.23/0.53 (((~q(s3)) | q(s4) | (~n5(s4))) <=> (q(s4) | (~n5(s4)) | (~q(s3)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(333,plain,
% 0.23/0.53 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s3)) | q(s4) | (~n5(s4)))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (q(s4) | (~n5(s4)) | (~q(s3))))),
% 0.23/0.53 inference(monotonicity,[status(thm)],[332])).
% 0.23/0.53 tff(334,plain,
% 0.23/0.53 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s3)) | q(s4) | (~n5(s4)))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | q(s4) | (~n5(s4)) | (~q(s3)))),
% 0.23/0.53 inference(transitivity,[status(thm)],[333, 331])).
% 0.23/0.53 tff(335,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s3)) | q(s4) | (~n5(s4)))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(336,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | q(s4) | (~n5(s4)) | (~q(s3))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[335, 334])).
% 0.23/0.53 tff(337,plain,
% 0.23/0.53 (~n5(s4)),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[336, 330, 2, 320])).
% 0.23/0.53 tff(338,plain,
% 0.23/0.53 (q(s5(s4))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[75, 337, 2])).
% 0.23/0.53 tff(339,plain,
% 0.23/0.53 (^[X: $i, X5: $i] : refl((q(X5) | (~q(X)) | (~n5(X))) <=> (q(X5) | (~q(X)) | (~n5(X))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(340,plain,
% 0.23/0.53 (![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X))) <=> ![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[339])).
% 0.23/0.53 tff(341,plain,
% 0.23/0.53 (![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X))) <=> ![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(342,plain,
% 0.23/0.53 (^[X: $i, X5: $i] : rewrite((((~n5(X)) | (~q(X))) | q(X5)) <=> (q(X5) | (~q(X)) | (~n5(X))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(343,plain,
% 0.23/0.53 (![X: $i, X5: $i] : (((~n5(X)) | (~q(X))) | q(X5)) <=> ![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[342])).
% 0.23/0.53 tff(344,axiom,(![X: $i, X5: $i] : (((~n5(X)) | (~q(X))) | q(X5))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_17')).
% 0.23/0.53 tff(345,plain,
% 0.23/0.53 (![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[344, 343])).
% 0.23/0.53 tff(346,plain,
% 0.23/0.53 (![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[345, 341])).
% 0.23/0.53 tff(347,plain,(
% 0.23/0.53 ![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))),
% 0.23/0.53 inference(skolemize,[status(sab)],[346])).
% 0.23/0.53 tff(348,plain,
% 0.23/0.53 (![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[347, 340])).
% 0.23/0.53 tff(349,plain,
% 0.23/0.53 (((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | (q(s4) | (~q(s5(s4))) | (~n5(s5(s4))))) <=> ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | q(s4) | (~q(s5(s4))) | (~n5(s5(s4))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(350,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | (q(s4) | (~q(s5(s4))) | (~n5(s5(s4))))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(351,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | q(s4) | (~q(s5(s4))) | (~n5(s5(s4)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[350, 349])).
% 0.23/0.53 tff(352,plain,
% 0.23/0.53 (~n5(s5(s4))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[351, 348, 2, 338])).
% 0.23/0.53 tff(353,plain,
% 0.23/0.53 (^[X: $i] : refl((n5(X) | (~q(s5(X))) | (~q(X))) <=> (n5(X) | (~q(s5(X))) | (~q(X))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(354,plain,
% 0.23/0.53 (![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X))) <=> ![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[353])).
% 0.23/0.53 tff(355,plain,
% 0.23/0.53 (![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X))) <=> ![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(356,plain,
% 0.23/0.53 (^[X: $i] : rewrite((((~q(X)) | (~q(s5(X)))) | n5(X)) <=> (n5(X) | (~q(s5(X))) | (~q(X))))),
% 0.23/0.53 inference(bind,[status(th)],[])).
% 0.23/0.53 tff(357,plain,
% 0.23/0.53 (![X: $i] : (((~q(X)) | (~q(s5(X)))) | n5(X)) <=> ![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))),
% 0.23/0.53 inference(quant_intro,[status(thm)],[356])).
% 0.23/0.53 tff(358,axiom,(![X: $i] : (((~q(X)) | (~q(s5(X)))) | n5(X))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_15')).
% 0.23/0.53 tff(359,plain,
% 0.23/0.53 (![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[358, 357])).
% 0.23/0.53 tff(360,plain,
% 0.23/0.53 (![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[359, 355])).
% 0.23/0.53 tff(361,plain,(
% 0.23/0.53 ![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))),
% 0.23/0.53 inference(skolemize,[status(sab)],[360])).
% 0.23/0.53 tff(362,plain,
% 0.23/0.53 (![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[361, 354])).
% 0.23/0.53 tff(363,plain,
% 0.23/0.53 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | ((~q(s5(s4))) | (~q(s5(s5(s4)))) | n5(s5(s4)))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s5(s4))) | (~q(s5(s5(s4)))) | n5(s5(s4)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(364,plain,
% 0.23/0.53 ((n5(s5(s4)) | (~q(s5(s5(s4)))) | (~q(s5(s4)))) <=> ((~q(s5(s4))) | (~q(s5(s5(s4)))) | n5(s5(s4)))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(365,plain,
% 0.23/0.53 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s5(s4)) | (~q(s5(s5(s4)))) | (~q(s5(s4))))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | ((~q(s5(s4))) | (~q(s5(s5(s4)))) | n5(s5(s4))))),
% 0.23/0.53 inference(monotonicity,[status(thm)],[364])).
% 0.23/0.53 tff(366,plain,
% 0.23/0.53 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s5(s4)) | (~q(s5(s5(s4)))) | (~q(s5(s4))))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s5(s4))) | (~q(s5(s5(s4)))) | n5(s5(s4)))),
% 0.23/0.53 inference(transitivity,[status(thm)],[365, 363])).
% 0.23/0.53 tff(367,plain,
% 0.23/0.53 ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s5(s4)) | (~q(s5(s5(s4)))) | (~q(s5(s4))))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(368,plain,
% 0.23/0.53 ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s5(s4))) | (~q(s5(s5(s4)))) | n5(s5(s4))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[367, 366])).
% 0.23/0.53 tff(369,plain,
% 0.23/0.53 (~q(s5(s5(s4)))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[368, 362, 338, 352])).
% 0.23/0.53 tff(370,assumption,(~q(s5(s5(s5(s4))))), introduced(assumption)).
% 0.23/0.53 tff(371,assumption,(~q(s5(s5(s4)))), introduced(assumption)).
% 0.23/0.53 tff(372,plain,
% 0.23/0.53 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s3)) | q(s5(s5(s4))) | (~n5(s5(s5(s4)))))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (~q(s3)) | q(s5(s5(s4))) | (~n5(s5(s5(s4)))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(373,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s3)) | q(s5(s5(s4))) | (~n5(s5(s5(s4)))))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(374,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (~q(s3)) | q(s5(s5(s4))) | (~n5(s5(s5(s4))))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[373, 372])).
% 0.23/0.53 tff(375,plain,
% 0.23/0.53 (~n5(s5(s5(s4)))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[374, 330, 320, 371])).
% 0.23/0.53 tff(376,plain,
% 0.23/0.53 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (q(s5(s5(s5(s4)))) | q(s5(s5(s4))) | n5(s5(s5(s4))))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s5(s5(s5(s4)))) | q(s5(s5(s4))) | n5(s5(s5(s4))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(377,plain,
% 0.23/0.53 ((n5(s5(s5(s4))) | q(s5(s5(s5(s4)))) | q(s5(s5(s4)))) <=> (q(s5(s5(s5(s4)))) | q(s5(s5(s4))) | n5(s5(s5(s4))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(378,plain,
% 0.23/0.53 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s5(s5(s4))) | q(s5(s5(s5(s4)))) | q(s5(s5(s4))))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (q(s5(s5(s5(s4)))) | q(s5(s5(s4))) | n5(s5(s5(s4)))))),
% 0.23/0.53 inference(monotonicity,[status(thm)],[377])).
% 0.23/0.53 tff(379,plain,
% 0.23/0.53 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s5(s5(s4))) | q(s5(s5(s5(s4)))) | q(s5(s5(s4))))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s5(s5(s5(s4)))) | q(s5(s5(s4))) | n5(s5(s5(s4))))),
% 0.23/0.53 inference(transitivity,[status(thm)],[378, 376])).
% 0.23/0.53 tff(380,plain,
% 0.23/0.53 ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s5(s5(s4))) | q(s5(s5(s5(s4)))) | q(s5(s5(s4))))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(381,plain,
% 0.23/0.53 ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s5(s5(s5(s4)))) | q(s5(s5(s4))) | n5(s5(s5(s4)))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[380, 379])).
% 0.23/0.53 tff(382,plain,
% 0.23/0.53 ($false),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[381, 68, 371, 375, 370])).
% 0.23/0.53 tff(383,plain,(q(s5(s5(s5(s4)))) | q(s5(s5(s4)))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.53 tff(384,plain,
% 0.23/0.53 (q(s5(s5(s5(s4))))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[383, 369])).
% 0.23/0.53 tff(385,plain,
% 0.23/0.53 (((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | (q(s4) | (~q(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s4))))))) <=> ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | q(s4) | (~q(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s4))))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(386,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | (q(s4) | (~q(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s4))))))),
% 0.23/0.53 inference(quant_inst,[status(thm)],[])).
% 0.23/0.53 tff(387,plain,
% 0.23/0.53 ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | q(s4) | (~q(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s4)))))),
% 0.23/0.53 inference(modus_ponens,[status(thm)],[386, 385])).
% 0.23/0.53 tff(388,plain,
% 0.23/0.53 ($false),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[387, 348, 2, 384, 316])).
% 0.23/0.53 tff(389,plain,((~n5(s5(s5(s5(s4))))) | q(s4)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.53 tff(390,plain,
% 0.23/0.53 (~n5(s5(s5(s5(s4))))),
% 0.23/0.53 inference(unit_resolution,[status(thm)],[389, 2])).
% 0.23/0.53 tff(391,assumption,(q(s5(s5(s5(s5(s4)))))), introduced(assumption)).
% 0.23/0.53 tff(392,assumption,(~n5(s5(s5(s5(s4))))), introduced(assumption)).
% 0.23/0.53 tff(393,assumption,(q(s5(s5(s5(s4))))), introduced(assumption)).
% 0.23/0.53 tff(394,plain,
% 0.23/0.53 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | ((~q(s5(s5(s5(s4))))) | (~q(s5(s5(s5(s5(s4)))))) | n5(s5(s5(s5(s4)))))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s5(s5(s5(s4))))) | (~q(s5(s5(s5(s5(s4)))))) | n5(s5(s5(s5(s4)))))),
% 0.23/0.53 inference(rewrite,[status(thm)],[])).
% 0.23/0.53 tff(395,plain,
% 0.23/0.53 ((n5(s5(s5(s5(s4)))) | (~q(s5(s5(s5(s5(s4)))))) | (~q(s5(s5(s5(s4)))))) <=> ((~q(s5(s5(s5(s4))))) | (~q(s5(s5(s5(s5(s4)))))) | n5(s5(s5(s5(s4)))))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(396,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s5(s5(s5(s4)))) | (~q(s5(s5(s5(s5(s4)))))) | (~q(s5(s5(s5(s4))))))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | ((~q(s5(s5(s5(s4))))) | (~q(s5(s5(s5(s5(s4)))))) | n5(s5(s5(s5(s4))))))),
% 0.23/0.54 inference(monotonicity,[status(thm)],[395])).
% 0.23/0.54 tff(397,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s5(s5(s5(s4)))) | (~q(s5(s5(s5(s5(s4)))))) | (~q(s5(s5(s5(s4))))))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s5(s5(s5(s4))))) | (~q(s5(s5(s5(s5(s4)))))) | n5(s5(s5(s5(s4)))))),
% 0.23/0.54 inference(transitivity,[status(thm)],[396, 394])).
% 0.23/0.54 tff(398,plain,
% 0.23/0.54 ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s5(s5(s5(s4)))) | (~q(s5(s5(s5(s5(s4)))))) | (~q(s5(s5(s5(s4))))))),
% 0.23/0.54 inference(quant_inst,[status(thm)],[])).
% 0.23/0.54 tff(399,plain,
% 0.23/0.54 ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s5(s5(s5(s4))))) | (~q(s5(s5(s5(s5(s4)))))) | n5(s5(s5(s5(s4))))),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[398, 397])).
% 0.23/0.54 tff(400,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[399, 362, 393, 392, 391])).
% 0.23/0.54 tff(401,plain,((~q(s5(s5(s5(s5(s4)))))) | (~q(s5(s5(s5(s4))))) | n5(s5(s5(s5(s4))))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(402,plain,
% 0.23/0.54 (~q(s5(s5(s5(s5(s4)))))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[401, 384, 390])).
% 0.23/0.54 tff(403,assumption,(~q(s5(s5(s5(s5(s4)))))), introduced(assumption)).
% 0.23/0.54 tff(404,assumption,(n5(s5(s5(s5(s5(s4)))))), introduced(assumption)).
% 0.23/0.54 tff(405,plain,
% 0.23/0.54 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s3)) | q(s5(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s5(s4)))))))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (~q(s3)) | q(s5(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s5(s4)))))))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(406,plain,
% 0.23/0.54 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s3)) | q(s5(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s5(s4)))))))),
% 0.23/0.54 inference(quant_inst,[status(thm)],[])).
% 0.23/0.54 tff(407,plain,
% 0.23/0.54 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (~q(s3)) | q(s5(s5(s5(s5(s4))))) | (~n5(s5(s5(s5(s5(s4))))))),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[406, 405])).
% 0.23/0.54 tff(408,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[407, 330, 320, 403, 404])).
% 0.23/0.54 tff(409,plain,((~n5(s5(s5(s5(s5(s4)))))) | q(s5(s5(s5(s5(s4)))))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(410,plain,
% 0.23/0.54 (~n5(s5(s5(s5(s5(s4)))))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[409, 403])).
% 0.23/0.54 tff(411,assumption,(~q(s5(s5(s5(s5(s5(s4))))))), introduced(assumption)).
% 0.23/0.54 tff(412,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (q(s5(s5(s5(s5(s4))))) | n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s5(s5(s5(s5(s4))))) | n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(413,plain,
% 0.23/0.54 ((n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))) | q(s5(s5(s5(s5(s4)))))) <=> (q(s5(s5(s5(s5(s4))))) | n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(414,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))) | q(s5(s5(s5(s5(s4))))))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (q(s5(s5(s5(s5(s4))))) | n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4))))))))),
% 0.23/0.54 inference(monotonicity,[status(thm)],[413])).
% 0.23/0.54 tff(415,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))) | q(s5(s5(s5(s5(s4))))))) <=> ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s5(s5(s5(s5(s4))))) | n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))))),
% 0.23/0.54 inference(transitivity,[status(thm)],[414, 412])).
% 0.23/0.54 tff(416,plain,
% 0.23/0.54 ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | (n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4)))))) | q(s5(s5(s5(s5(s4))))))),
% 0.23/0.54 inference(quant_inst,[status(thm)],[])).
% 0.23/0.54 tff(417,plain,
% 0.23/0.54 ((~![X: $i] : (n5(X) | q(s5(X)) | q(X))) | q(s5(s5(s5(s5(s4))))) | n5(s5(s5(s5(s5(s4))))) | q(s5(s5(s5(s5(s5(s4))))))),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[416, 415])).
% 0.23/0.54 tff(418,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[417, 68, 411, 403, 410])).
% 0.23/0.54 tff(419,plain,(q(s5(s5(s5(s5(s5(s4)))))) | q(s5(s5(s5(s5(s4)))))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(420,plain,
% 0.23/0.54 (q(s5(s5(s5(s5(s5(s4))))))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[419, 402])).
% 0.23/0.54 tff(421,assumption,(n5(s6)), introduced(assumption)).
% 0.23/0.54 tff(422,plain,
% 0.23/0.54 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (q(s6) | (~q(s5(s5(s5(s5(s5(s4))))))) | (~n5(s6)))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | q(s6) | (~q(s5(s5(s5(s5(s5(s4))))))) | (~n5(s6)))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(423,plain,
% 0.23/0.54 (((~q(s5(s5(s5(s5(s5(s4))))))) | q(s6) | (~n5(s6))) <=> (q(s6) | (~q(s5(s5(s5(s5(s5(s4))))))) | (~n5(s6)))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(424,plain,
% 0.23/0.54 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s5(s5(s5(s5(s5(s4))))))) | q(s6) | (~n5(s6)))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | (q(s6) | (~q(s5(s5(s5(s5(s5(s4))))))) | (~n5(s6))))),
% 0.23/0.54 inference(monotonicity,[status(thm)],[423])).
% 0.23/0.54 tff(425,plain,
% 0.23/0.54 (((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s5(s5(s5(s5(s5(s4))))))) | q(s6) | (~n5(s6)))) <=> ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | q(s6) | (~q(s5(s5(s5(s5(s5(s4))))))) | (~n5(s6)))),
% 0.23/0.54 inference(transitivity,[status(thm)],[424, 422])).
% 0.23/0.54 tff(426,plain,
% 0.23/0.54 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | ((~q(s5(s5(s5(s5(s5(s4))))))) | q(s6) | (~n5(s6)))),
% 0.23/0.54 inference(quant_inst,[status(thm)],[])).
% 0.23/0.54 tff(427,plain,
% 0.23/0.54 ((~![X: $i, X5: $i] : ((~q(X5)) | q(X) | (~n5(X)))) | q(s6) | (~q(s5(s5(s5(s5(s5(s4))))))) | (~n5(s6))),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[426, 425])).
% 0.23/0.54 tff(428,plain,
% 0.23/0.54 (q(s6) | (~q(s5(s5(s5(s5(s5(s4))))))) | (~n5(s6))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[427, 330])).
% 0.23/0.54 tff(429,plain,
% 0.23/0.54 (q(s6)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[428, 421, 420])).
% 0.23/0.54 tff(430,plain,
% 0.23/0.54 (((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | (q(s4) | (~q(s6)) | (~n5(s6)))) <=> ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | q(s4) | (~q(s6)) | (~n5(s6)))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(431,plain,
% 0.23/0.54 ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | (q(s4) | (~q(s6)) | (~n5(s6)))),
% 0.23/0.54 inference(quant_inst,[status(thm)],[])).
% 0.23/0.54 tff(432,plain,
% 0.23/0.54 ((~![X: $i, X5: $i] : (q(X5) | (~q(X)) | (~n5(X)))) | q(s4) | (~q(s6)) | (~n5(s6))),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[431, 430])).
% 0.23/0.54 tff(433,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[432, 421, 348, 2, 429])).
% 0.23/0.54 tff(434,plain,((~n5(s6)) | q(s4)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(435,plain,
% 0.23/0.54 (~n5(s6)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[434, 2])).
% 0.23/0.54 tff(436,plain,
% 0.23/0.54 (((~n6) | n5(s6)) <=> ((~n6) | n5(s6))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(437,axiom,((~n6) | n5(s6)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_14')).
% 0.23/0.54 tff(438,plain,
% 0.23/0.54 ((~n6) | n5(s6)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[437, 436])).
% 0.23/0.54 tff(439,plain,
% 0.23/0.54 ((~n6) | n5(s6)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[438, 436])).
% 0.23/0.54 tff(440,plain,
% 0.23/0.54 ((~n6) | n5(s6)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[439, 436])).
% 0.23/0.54 tff(441,plain,
% 0.23/0.54 ((~n6) | n5(s6)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[440, 436])).
% 0.23/0.54 tff(442,plain,
% 0.23/0.54 ((~n6) | n5(s6)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[441, 436])).
% 0.23/0.54 tff(443,plain,
% 0.23/0.54 (~n6),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[442, 435])).
% 0.23/0.54 tff(444,plain,
% 0.23/0.54 ((n2 | n9 | n6 | n10) <=> (n2 | n9 | n6 | n10)),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(445,plain,
% 0.23/0.54 (((n2 | n9 | n6) | n10) <=> (n2 | n9 | n6 | n10)),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(446,plain,
% 0.23/0.54 (((n2 | n9) | n6) <=> (n2 | n9 | n6)),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(447,plain,
% 0.23/0.54 ((((n2 | n9) | n6) | n10) <=> ((n2 | n9 | n6) | n10)),
% 0.23/0.54 inference(monotonicity,[status(thm)],[446])).
% 0.23/0.54 tff(448,plain,
% 0.23/0.54 ((((n2 | n9) | n6) | n10) <=> (n2 | n9 | n6 | n10)),
% 0.23/0.54 inference(transitivity,[status(thm)],[447, 445])).
% 0.23/0.54 tff(449,axiom,(((n2 | n9) | n6) | n10), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_4')).
% 0.23/0.54 tff(450,plain,
% 0.23/0.54 (n2 | n9 | n6 | n10),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[449, 448])).
% 0.23/0.54 tff(451,plain,
% 0.23/0.54 (n2 | n9 | n6 | n10),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[450, 444])).
% 0.23/0.54 tff(452,plain,
% 0.23/0.54 (n2 | n9 | n6 | n10),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[451, 444])).
% 0.23/0.54 tff(453,plain,
% 0.23/0.54 (n2 | n9 | n6 | n10),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[452, 444])).
% 0.23/0.54 tff(454,plain,
% 0.23/0.54 (n2 | n9 | n6 | n10),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[453, 444])).
% 0.23/0.54 tff(455,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[454, 443, 315, 97, 245])).
% 0.23/0.54 tff(456,plain,(q(s4) | n10 | n2), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(457,plain,
% 0.23/0.54 (q(s4)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[456, 97, 245])).
% 0.23/0.54 tff(458,plain,
% 0.23/0.54 (((~q(s4)) | n4) <=> ((~q(s4)) | n4)),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(459,axiom,((~q(s4)) | n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_19')).
% 0.23/0.54 tff(460,plain,
% 0.23/0.54 ((~q(s4)) | n4),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[459, 458])).
% 0.23/0.54 tff(461,plain,
% 0.23/0.54 ((~q(s4)) | n4),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[460, 458])).
% 0.23/0.54 tff(462,plain,
% 0.23/0.54 ((~q(s4)) | n4),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[461, 458])).
% 0.23/0.54 tff(463,plain,
% 0.23/0.54 ((~q(s4)) | n4),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[462, 458])).
% 0.23/0.54 tff(464,plain,
% 0.23/0.54 ((~q(s4)) | n4),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[463, 458])).
% 0.23/0.54 tff(465,plain,
% 0.23/0.54 (n4),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[464, 457])).
% 0.23/0.54 tff(466,plain,
% 0.23/0.54 ((n9 | (~n4) | (~n3)) <=> (n9 | (~n4) | (~n3))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(467,plain,
% 0.23/0.54 ((((~n3) | (~n4)) | n9) <=> (n9 | (~n4) | (~n3))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(468,axiom,(((~n3) | (~n4)) | n9), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_29')).
% 0.23/0.54 tff(469,plain,
% 0.23/0.54 (n9 | (~n4) | (~n3)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[468, 467])).
% 0.23/0.54 tff(470,plain,
% 0.23/0.54 (n9 | (~n4) | (~n3)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[469, 466])).
% 0.23/0.54 tff(471,plain,
% 0.23/0.54 (n9 | (~n4) | (~n3)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[470, 466])).
% 0.23/0.54 tff(472,plain,
% 0.23/0.54 (n9 | (~n4) | (~n3)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[471, 466])).
% 0.23/0.54 tff(473,plain,
% 0.23/0.54 (n9 | (~n4) | (~n3)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[472, 466])).
% 0.23/0.54 tff(474,plain,
% 0.23/0.54 (n9 | (~n4)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[473, 302])).
% 0.23/0.54 tff(475,plain,
% 0.23/0.54 (n9),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[474, 465])).
% 0.23/0.54 tff(476,plain,
% 0.23/0.54 (~n6),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[220, 475, 97])).
% 0.23/0.54 tff(477,plain,
% 0.23/0.54 (~n5(s4)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[93, 476])).
% 0.23/0.54 tff(478,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | ((~q(s4)) | n5(s4) | (~q(s5(s4))))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s4)) | n5(s4) | (~q(s5(s4))))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(479,plain,
% 0.23/0.54 ((n5(s4) | (~q(s5(s4))) | (~q(s4))) <=> ((~q(s4)) | n5(s4) | (~q(s5(s4))))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(480,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s4) | (~q(s5(s4))) | (~q(s4)))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | ((~q(s4)) | n5(s4) | (~q(s5(s4)))))),
% 0.23/0.54 inference(monotonicity,[status(thm)],[479])).
% 0.23/0.54 tff(481,plain,
% 0.23/0.54 (((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s4) | (~q(s5(s4))) | (~q(s4)))) <=> ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s4)) | n5(s4) | (~q(s5(s4))))),
% 0.23/0.54 inference(transitivity,[status(thm)],[480, 478])).
% 0.23/0.54 tff(482,plain,
% 0.23/0.54 ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (n5(s4) | (~q(s5(s4))) | (~q(s4)))),
% 0.23/0.54 inference(quant_inst,[status(thm)],[])).
% 0.23/0.54 tff(483,plain,
% 0.23/0.54 ((~![X: $i] : (n5(X) | (~q(s5(X))) | (~q(X)))) | (~q(s4)) | n5(s4) | (~q(s5(s4)))),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[482, 481])).
% 0.23/0.54 tff(484,plain,
% 0.23/0.54 (~q(s5(s4))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[483, 362, 457, 477])).
% 0.23/0.54 tff(485,plain,
% 0.23/0.54 (((~![X4: $i] : ((~n4) | q(X4))) | ((~n4) | q(s5(s4)))) <=> ((~![X4: $i] : ((~n4) | q(X4))) | (~n4) | q(s5(s4)))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(486,plain,
% 0.23/0.54 ((~![X4: $i] : ((~n4) | q(X4))) | ((~n4) | q(s5(s4)))),
% 0.23/0.54 inference(quant_inst,[status(thm)],[])).
% 0.23/0.54 tff(487,plain,
% 0.23/0.54 ((~![X4: $i] : ((~n4) | q(X4))) | (~n4) | q(s5(s4))),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[486, 485])).
% 0.23/0.54 tff(488,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[487, 465, 9, 484])).
% 0.23/0.54 tff(489,plain,(n10 | n2), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(490,plain,
% 0.23/0.54 (n10),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[489, 245])).
% 0.23/0.54 tff(491,plain,
% 0.23/0.54 (~n1(s8)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[250, 245])).
% 0.23/0.54 tff(492,plain,
% 0.23/0.54 (n7),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[264, 490, 491])).
% 0.23/0.54 tff(493,plain,
% 0.23/0.54 (n8),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[276, 492, 490])).
% 0.23/0.54 tff(494,plain,
% 0.23/0.54 (p(s1(s8))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[281, 493])).
% 0.23/0.54 tff(495,plain,
% 0.23/0.54 (~p(s8)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[295, 292, 491, 494])).
% 0.23/0.54 tff(496,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[300, 495, 493, 23])).
% 0.23/0.54 tff(497,plain,(n2), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(498,plain,
% 0.23/0.54 (((~n2) | n9 | n6 | (~n10)) <=> ((~n2) | n9 | n6 | (~n10))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(499,plain,
% 0.23/0.54 ((((~n2) | n9 | n6) | (~n10)) <=> ((~n2) | n9 | n6 | (~n10))),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(500,plain,
% 0.23/0.54 ((((~n2) | n9) | n6) <=> ((~n2) | n9 | n6)),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(501,plain,
% 0.23/0.54 (((~n2) | n9) <=> ((~n2) | n9)),
% 0.23/0.54 inference(rewrite,[status(thm)],[])).
% 0.23/0.54 tff(502,plain,
% 0.23/0.54 ((((~n2) | n9) | n6) <=> (((~n2) | n9) | n6)),
% 0.23/0.54 inference(monotonicity,[status(thm)],[501])).
% 0.23/0.54 tff(503,plain,
% 0.23/0.54 ((((~n2) | n9) | n6) <=> ((~n2) | n9 | n6)),
% 0.23/0.54 inference(transitivity,[status(thm)],[502, 500])).
% 0.23/0.54 tff(504,plain,
% 0.23/0.54 (((((~n2) | n9) | n6) | (~n10)) <=> (((~n2) | n9 | n6) | (~n10))),
% 0.23/0.54 inference(monotonicity,[status(thm)],[503])).
% 0.23/0.54 tff(505,plain,
% 0.23/0.54 (((((~n2) | n9) | n6) | (~n10)) <=> ((~n2) | n9 | n6 | (~n10))),
% 0.23/0.54 inference(transitivity,[status(thm)],[504, 499])).
% 0.23/0.54 tff(506,axiom,((((~n2) | n9) | n6) | (~n10)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','clause_6')).
% 0.23/0.54 tff(507,plain,
% 0.23/0.54 ((~n2) | n9 | n6 | (~n10)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[506, 505])).
% 0.23/0.54 tff(508,plain,
% 0.23/0.54 ((~n2) | n9 | n6 | (~n10)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[507, 498])).
% 0.23/0.54 tff(509,plain,
% 0.23/0.54 ((~n2) | n9 | n6 | (~n10)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[508, 498])).
% 0.23/0.54 tff(510,plain,
% 0.23/0.54 ((~n2) | n9 | n6 | (~n10)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[509, 498])).
% 0.23/0.54 tff(511,plain,
% 0.23/0.54 ((~n2) | n9 | n6 | (~n10)),
% 0.23/0.54 inference(modus_ponens,[status(thm)],[510, 498])).
% 0.23/0.54 tff(512,plain,
% 0.23/0.54 (n9 | n6 | (~n10)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[511, 497])).
% 0.23/0.54 tff(513,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[512, 443, 315, 1])).
% 0.23/0.54 tff(514,plain,(q(s4) | (~n10)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(515,plain,
% 0.23/0.54 (q(s4)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[514, 1])).
% 0.23/0.54 tff(516,plain,
% 0.23/0.54 (n4),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[464, 515])).
% 0.23/0.54 tff(517,plain,
% 0.23/0.54 (n9),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[474, 516])).
% 0.23/0.54 tff(518,plain,
% 0.23/0.54 ((~n9) | (~n6) | (~n10)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[232, 497])).
% 0.23/0.54 tff(519,plain,
% 0.23/0.54 (~n6),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[518, 517, 1])).
% 0.23/0.54 tff(520,plain,
% 0.23/0.54 (~n5(s4)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[93, 519])).
% 0.23/0.54 tff(521,plain,
% 0.23/0.54 (~q(s5(s4))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[483, 362, 515, 520])).
% 0.23/0.54 tff(522,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[487, 516, 9, 521])).
% 0.23/0.54 tff(523,plain,(~n10), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(524,plain,
% 0.23/0.54 (n7),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[149, 523])).
% 0.23/0.54 tff(525,plain,
% 0.23/0.54 (p(s7)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[177, 524])).
% 0.23/0.54 tff(526,plain,
% 0.23/0.54 (~n8),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[155, 523, 524])).
% 0.23/0.54 tff(527,plain,
% 0.23/0.54 (~p(s8)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[163, 526])).
% 0.23/0.54 tff(528,assumption,(~p(s8)), introduced(assumption)).
% 0.23/0.54 tff(529,plain,
% 0.23/0.54 (n1(s2)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[116, 497])).
% 0.23/0.54 tff(530,assumption,(n1(s2)), introduced(assumption)).
% 0.23/0.54 tff(531,plain,
% 0.23/0.54 (p(s2)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[204, 530, 119])).
% 0.23/0.54 tff(532,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[218, 528, 530, 215, 531])).
% 0.23/0.54 tff(533,plain,((~n1(s2)) | p(s8) | (~p(s1(s8)))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(534,plain,
% 0.23/0.54 (p(s8) | (~p(s1(s8)))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[533, 529])).
% 0.23/0.54 tff(535,plain,
% 0.23/0.54 (~p(s1(s8))),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[534, 528])).
% 0.23/0.54 tff(536,plain,
% 0.23/0.54 (n1(s8)),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[199, 535, 528])).
% 0.23/0.54 tff(537,assumption,(p(s7)), introduced(assumption)).
% 0.23/0.54 tff(538,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[184, 528, 537, 174, 536])).
% 0.23/0.54 tff(539,plain,((~p(s7)) | p(s8)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.54 tff(540,plain,
% 0.23/0.54 ($false),
% 0.23/0.54 inference(unit_resolution,[status(thm)],[539, 527, 525])).
% 0.23/0.54 % SZS output end Proof
% 0.23/0.54 % E exiting
%------------------------------------------------------------------------------