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