%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LCL243-3 : TPTP v9.2.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:39:52 PM UTC 2026
% Result : Unsatisfiable 162.03s 86.94s
% Output : CNFRefutation 162.63s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_11)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
~ theorem(implies(implies(p,implies(q,r)),implies(and(p,q),r))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
cnf(implies_definition,axiom,
implies(X1,X2) = or(not(X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',implies_definition) ).
cnf(and_defn,axiom,
and(X1,X2) = not(or(not(X1),not(X2))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-1.ax',and_defn) ).
cnf(axiom_1_6,axiom,
axiom(implies(implies(X1,X2),implies(or(X3,X1),or(X3,X2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_6) ).
cnf(axiom_1_5,axiom,
axiom(implies(or(X1,or(X2,X3)),or(X2,or(X1,X3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_5) ).
cnf(axiom_1_4,axiom,
axiom(implies(or(X1,X2),or(X2,X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_4) ).
cnf(axiom_1_2,axiom,
axiom(implies(or(X1,X1),X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_2) ).
cnf(axiom_1_3,axiom,
axiom(implies(X1,or(X2,X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_3) ).
cnf(rule_2,axiom,
( theorem(X1)
| ~ theorem(implies(X2,X1))
| ~ theorem(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',rule_2) ).
cnf(rule_1,axiom,
( theorem(X1)
| ~ axiom(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',rule_1) ).
cnf(i_0_10,negated_conjecture,
~ theorem(implies(implies(p,implies(q,r)),implies(and(p,q),r))),
prove_this ).
cnf(i_0_11,axiom,
implies(X1,X2) = or(not(X1),X2),
implies_definition ).
cnf(i_0_12,axiom,
and(X1,X2) = not(or(not(X1),not(X2))),
and_defn ).
cnf(i_0_13,axiom,
axiom(implies(implies(X1,X2),implies(or(X3,X1),or(X3,X2)))),
axiom_1_6 ).
cnf(i_0_14,axiom,
axiom(implies(or(X1,or(X2,X3)),or(X2,or(X1,X3)))),
axiom_1_5 ).
cnf(i_0_15,axiom,
axiom(implies(or(X1,X2),or(X2,X1))),
axiom_1_4 ).
cnf(i_0_16,axiom,
axiom(implies(or(X1,X1),X1)),
axiom_1_2 ).
cnf(i_0_17,axiom,
axiom(implies(X1,or(X2,X1))),
axiom_1_3 ).
cnf(i_0_18,axiom,
( theorem(X1)
| ~ theorem(implies(X2,X1))
| ~ theorem(X2) ),
rule_2 ).
cnf(i_0_19,negated_conjecture,
~ theorem(or(not(or(not(p),or(not(q),r))),or(not(not(or(not(p),not(q)))),r))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_10,c_0_11]),c_0_11]),c_0_11]),c_0_11]),c_0_12]),
[final] ).
cnf(i_0_20,plain,
axiom(or(not(or(not(X1),X2)),or(not(or(X3,X1)),or(X3,X2)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_13,c_0_11]),c_0_11]),c_0_11]),
[final] ).
cnf(i_0_21,plain,
axiom(or(not(or(X1,or(X2,X3))),or(X2,or(X1,X3)))),
inference(rw,[status(thm)],[i_0_14,c_0_11]),
[final] ).
cnf(i_0_22,plain,
axiom(or(not(or(X1,X2)),or(X2,X1))),
inference(rw,[status(thm)],[i_0_15,c_0_11]),
[final] ).
cnf(i_0_23,plain,
axiom(or(not(or(X1,X1)),X1)),
inference(rw,[status(thm)],[i_0_16,c_0_11]),
[final] ).
cnf(i_0_24,plain,
axiom(or(not(X1),or(X2,X1))),
inference(rw,[status(thm)],[i_0_17,c_0_11]),
[final] ).
cnf(i_0_25,plain,
( theorem(X1)
| ~ theorem(X2)
| ~ theorem(or(not(X2),X1)) ),
inference(rw,[status(thm)],[i_0_18,c_0_11]),
[final] ).
cnf(i_0_26,axiom,
( theorem(X1)
| ~ axiom(X1) ),
rule_1,
[final] ).
cnf(i_0_839,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X5))))),or(or(X2,or(X3,or(X5,X4))),X1))),
inference(scs_inference,[],[i_0_35,i_0_129,i_0_25]) ).
cnf(i_0_840,plain,
theorem(or(not(or(not(X1),X2)),or(not(or(X3,or(X4,X1))),or(or(X4,X2),X3)))),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_872,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(or(or(X4,X3),not(or(X4,X2))),X1))),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_881,plain,
theorem(or(or(X1,or(or(X2,X3),X4)),not(or(X1,or(X4,or(X3,X2)))))),
inference(scs_inference,[],[i_0_35,i_0_875,i_0_25]) ).
cnf(i_0_882,plain,
theorem(or(not(or(not(X1),or(X2,X3))),or(or(X4,or(X3,X2)),not(or(X4,X1))))),
inference(rename_variables,[],[i_0_875]) ).
cnf(i_0_884,plain,
theorem(or(or(X1,or(X2,or(X3,or(X4,X5)))),not(or(X1,or(X2,or(X3,or(X5,X4))))))),
inference(scs_inference,[],[i_0_35,i_0_167,i_0_25]) ).
cnf(i_0_885,plain,
theorem(or(not(or(not(X1),X2)),or(or(X3,or(X4,X2)),not(or(X3,or(X4,X1)))))),
inference(rename_variables,[],[i_0_167]) ).
cnf(i_0_905,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(or(not(or(X4,X2)),or(X4,X3)),X1))),
inference(rename_variables,[],[i_0_121]) ).
cnf(i_0_923,plain,
theorem(or(or(X1,or(or(X2,or(X3,X4)),X5)),not(or(X1,or(X5,or(X2,or(X4,X3))))))),
inference(scs_inference,[],[i_0_38,i_0_875,i_0_25]) ).
cnf(i_0_924,plain,
theorem(or(not(or(not(X1),or(X2,X3))),or(or(X4,or(X3,X2)),not(or(X4,X1))))),
inference(rename_variables,[],[i_0_875]) ).
cnf(i_0_1018,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(or(or(X4,X3),X2),X1))),
inference(rename_variables,[],[i_0_916]) ).
cnf(i_0_1143,plain,
theorem(or(not(or(X1,or(or(X2,X3),not(X4)))),or(X1,or(not(or(X5,X4)),or(X5,or(X3,X2)))))),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_79,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X2,or(X5,or(X6,or(X4,X3))))))),
inference(scs_inference,[],[i_0_76,i_0_29]) ).
cnf(i_0_92,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X4))))),or(X1,or(X2,or(X3,X4))))),
inference(scs_inference,[],[i_0_87,i_0_29]) ).
cnf(i_0_94,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X4))))),or(X1,or(or(X3,X4),X2)))),
inference(scs_inference,[],[i_0_87,i_0_42,i_0_29,i_0_25]) ).
cnf(i_0_99,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X5))))),or(X1,or(X2,or(X4,or(X3,X5)))))),
inference(scs_inference,[],[i_0_97,i_0_29]) ).
cnf(i_0_101,plain,
theorem(or(not(or(not(X1),X2)),or(X3,or(not(or(X3,X1)),X2)))),
inference(scs_inference,[],[i_0_27,i_0_97,i_0_25]) ).
cnf(i_0_102,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X3,or(X2,X4))))),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_104,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(X1,or(X4,or(not(or(X4,X2)),X3))))),
inference(scs_inference,[],[i_0_27,i_0_97,i_0_25,i_0_29]) ).
cnf(i_0_111,plain,
theorem(or(not(or(not(X1),X2)),or(X3,or(X4,or(or(X5,X2),not(or(X5,X1))))))),
inference(scs_inference,[],[i_0_27,i_0_76,i_0_25]) ).
cnf(i_0_112,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X4,or(X5,or(X3,X2)))))),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_148,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(X4,or(X1,or(not(or(X5,X2)),or(X5,X3)))))),
inference(scs_inference,[],[i_0_27,i_0_143,i_0_25]) ).
cnf(i_0_149,plain,
theorem(or(not(or(not(X1),X2)),or(not(or(X3,X1)),or(X4,or(X3,X2))))),
inference(rename_variables,[],[i_0_143]) ).
cnf(i_0_156,plain,
theorem(or(X1,or(or(X2,or(not(or(X3,X4)),or(X3,X5))),not(or(X2,or(not(X4),X5)))))),
inference(scs_inference,[],[i_0_27,i_0_151,i_0_25]) ).
cnf(i_0_157,plain,
theorem(or(not(or(not(X1),X2)),or(X3,or(or(X4,X2),not(or(X4,X1)))))),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_178,plain,
theorem(or(not(or(or(X1,or(X2,X2)),X3)),or(or(X2,X1),X3))),
inference(scs_inference,[],[i_0_33,i_0_89,i_0_25]) ).
cnf(i_0_179,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X4))))),or(X1,or(or(X4,X3),X2)))),
inference(rename_variables,[],[i_0_89]) ).
cnf(i_0_182,plain,
theorem(or(not(or(X1,or(or(X2,or(X3,X3)),X4))),or(X1,or(or(X3,X2),X4)))),
inference(scs_inference,[],[i_0_33,i_0_89,i_0_25,i_0_29]) ).
cnf(i_0_253,plain,
theorem(or(not(or(X1,not(X2))),or(not(or(X3,or(X4,X2))),or(or(X4,X1),X3)))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_265,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X1,or(X4,X2))))),
inference(scs_inference,[],[i_0_33,i_0_74,i_0_25]) ).
cnf(i_0_266,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X2,or(X3,or(X5,X4)))))),
inference(rename_variables,[],[i_0_74]) ).
cnf(i_0_269,plain,
theorem(or(not(or(X1,or(or(X2,X3),X4))),or(X1,or(X4,or(X2,or(X5,X3)))))),
inference(scs_inference,[],[i_0_33,i_0_74,i_0_25,i_0_29]) ).
cnf(i_0_271,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X4,or(X2,X1))))),
inference(scs_inference,[],[i_0_33,i_0_81,i_0_25]) ).
cnf(i_0_272,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X2,or(X5,or(X4,X3)))))),
inference(rename_variables,[],[i_0_81]) ).
cnf(i_0_275,plain,
theorem(or(not(or(X1,or(or(X2,X3),X4))),or(X1,or(X4,or(X5,or(X3,X2)))))),
inference(scs_inference,[],[i_0_33,i_0_81,i_0_25,i_0_29]) ).
cnf(i_0_277,plain,
theorem(or(not(or(X1,not(X2))),or(not(or(X3,X2)),or(X4,or(X3,X1))))),
inference(scs_inference,[],[i_0_33,i_0_146,i_0_25]) ).
cnf(i_0_278,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(X1,or(not(or(X4,X2)),or(X5,or(X4,X3)))))),
inference(rename_variables,[],[i_0_146]) ).
cnf(i_0_281,plain,
theorem(or(not(or(X1,or(X2,not(X3)))),or(X1,or(not(or(X4,X3)),or(X5,or(X4,X2)))))),
inference(scs_inference,[],[i_0_33,i_0_146,i_0_25,i_0_29]) ).
cnf(i_0_310,plain,
theorem(or(or(not(or(X1,or(X2,X3))),or(X1,or(X2,X4))),not(or(not(X3),X4)))),
inference(rename_variables,[],[i_0_126]) ).
cnf(i_0_365,plain,
theorem(or(not(or(not(X1),X2)),or(not(or(X3,X1)),or(X4,or(X3,X2))))),
inference(rename_variables,[],[i_0_143]) ).
cnf(i_0_472,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X1,or(X3,X2)))),
inference(scs_inference,[],[i_0_33,i_0_97,i_0_25]) ).
cnf(i_0_473,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X3,or(X2,X4))))),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_476,plain,
theorem(or(not(or(X1,or(or(X2,X3),X4))),or(X1,or(X2,or(X4,X3))))),
inference(scs_inference,[],[i_0_33,i_0_97,i_0_25,i_0_29]) ).
cnf(i_0_551,plain,
theorem(or(not(or(X1,X2)),or(X3,or(X4,or(X1,X2))))),
inference(scs_inference,[],[i_0_33,i_0_76,i_0_25]) ).
cnf(i_0_552,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X4,or(X5,or(X3,X2)))))),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_554,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X4,or(X5,or(X2,X3)))))),
inference(scs_inference,[],[i_0_33,i_0_76,i_0_25,i_0_29]) ).
cnf(i_0_599,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,or(X4,X2))))),
inference(scs_inference,[],[i_0_596,i_0_29]) ).
cnf(i_0_601,plain,
~ theorem(or(r,not(or(not(p),or(not(q),r))))),
inference(scs_inference,[],[i_0_596,i_0_19,i_0_29,i_0_25]) ).
cnf(i_0_602,plain,
theorem(or(not(or(X1,X2)),or(X2,or(X3,X1)))),
inference(rename_variables,[],[i_0_596]) ).
cnf(i_0_730,plain,
theorem(or(not(or(X1,or(or(X2,X2),X3))),or(or(X2,X3),X1))),
inference(scs_inference,[],[i_0_35,i_0_89,i_0_25]) ).
cnf(i_0_731,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X4))))),or(X1,or(or(X4,X3),X2)))),
inference(rename_variables,[],[i_0_89]) ).
cnf(i_0_734,plain,
theorem(or(not(or(X1,or(X2,or(or(X3,X3),X4)))),or(X1,or(or(X3,X4),X2)))),
inference(scs_inference,[],[i_0_35,i_0_89,i_0_25,i_0_29]) ).
cnf(i_0_836,plain,
theorem(or(X1,or(or(X2,or(X3,or(X4,X5))),not(or(X2,or(X3,or(X5,X4))))))),
inference(scs_inference,[],[i_0_35,i_0_151,i_0_25]) ).
cnf(i_0_837,plain,
theorem(or(not(or(not(X1),X2)),or(X3,or(or(X4,X2),not(or(X4,X1)))))),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_855,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X5,or(X1,or(X2,or(X4,X3)))))),
inference(scs_inference,[],[i_0_35,i_0_143,i_0_25]) ).
cnf(i_0_856,plain,
theorem(or(not(or(not(X1),X2)),or(not(or(X3,X1)),or(X4,or(X3,X2))))),
inference(rename_variables,[],[i_0_143]) ).
cnf(i_0_897,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X3,or(X1,X2)))),
inference(scs_inference,[],[i_0_35,i_0_97,i_0_25]) ).
cnf(i_0_898,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X3,or(X2,X4))))),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_900,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X4,or(X2,X3))))),
inference(scs_inference,[],[i_0_35,i_0_97,i_0_25,i_0_29]) ).
cnf(i_0_908,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X4,or(X5,or(or(X3,X2),X1))))),
inference(scs_inference,[],[i_0_35,i_0_76,i_0_25]) ).
cnf(i_0_909,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X4,or(X5,or(X3,X2)))))),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_911,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X5,or(X6,or(or(X4,X3),X2)))))),
inference(scs_inference,[],[i_0_35,i_0_76,i_0_25,i_0_29]) ).
cnf(i_0_106,plain,
theorem(or(X1,or(not(or(X1,or(not(X2),X3))),or(not(or(X4,X2)),or(X4,X3))))),
inference(scs_inference,[],[i_0_27,i_0_101,i_0_25]) ).
cnf(i_0_107,plain,
theorem(or(not(or(not(X1),X2)),or(X3,or(not(or(X3,X1)),X2)))),
inference(rename_variables,[],[i_0_101]) ).
cnf(i_0_109,plain,
theorem(or(not(or(X1,X2)),or(X1,or(not(or(not(X2),or(not(X3),X4))),or(not(or(X5,X3)),or(X5,X4)))))),
inference(scs_inference,[],[i_0_27,i_0_101,i_0_25,i_0_29]) ).
cnf(i_0_184,plain,
theorem(or(not(or(or(X1,or(X2,X2)),X3)),or(X3,or(X1,X2)))),
inference(scs_inference,[],[i_0_33,i_0_92,i_0_25]) ).
cnf(i_0_185,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X4))))),or(X1,or(X2,or(X3,X4))))),
inference(rename_variables,[],[i_0_92]) ).
cnf(i_0_188,plain,
theorem(or(not(or(X1,or(or(X2,or(X3,X3)),X4))),or(X1,or(X4,or(X2,X3))))),
inference(scs_inference,[],[i_0_33,i_0_92,i_0_25,i_0_29]) ).
cnf(i_0_190,plain,
theorem(or(not(or(or(X1,or(X2,X2)),X3)),or(or(X1,X2),X3))),
inference(scs_inference,[],[i_0_33,i_0_94,i_0_25]) ).
cnf(i_0_191,plain,
theorem(or(not(or(X1,or(X2,or(X3,or(X4,X4))))),or(X1,or(or(X3,X4),X2)))),
inference(rename_variables,[],[i_0_94]) ).
cnf(i_0_194,plain,
theorem(or(not(or(X1,or(or(X2,or(X3,X3)),X4))),or(X1,or(or(X2,X3),X4)))),
inference(scs_inference,[],[i_0_33,i_0_94,i_0_25,i_0_29]) ).
cnf(i_0_196,plain,
theorem(or(not(or(X1,or(X2,or(X3,X3)))),or(or(X3,X2),X1))),
inference(scs_inference,[],[i_0_33,i_0_182,i_0_25]) ).
cnf(i_0_197,plain,
theorem(or(not(or(X1,or(or(X2,or(X3,X3)),X4))),or(X1,or(or(X3,X2),X4)))),
inference(rename_variables,[],[i_0_182]) ).
cnf(i_0_205,plain,
theorem(or(not(or(or(X1,or(X2,X2)),X3)),or(or(X2,X1),X3))),
inference(rename_variables,[],[i_0_178]) ).
cnf(i_0_283,plain,
theorem(or(X1,or(not(or(X2,not(X3))),or(not(or(X4,X3)),or(X4,X2))))),
inference(scs_inference,[],[i_0_33,i_0_148,i_0_25]) ).
cnf(i_0_284,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(X4,or(X1,or(not(or(X5,X2)),or(X5,X3)))))),
inference(rename_variables,[],[i_0_148]) ).
cnf(i_0_287,plain,
theorem(or(not(or(X1,X2)),or(X1,or(not(or(X3,not(X4))),or(not(or(X5,X4)),or(X5,X3)))))),
inference(scs_inference,[],[i_0_33,i_0_148,i_0_25,i_0_29]) ).
cnf(i_0_297,plain,
theorem(or(X1,or(or(X2,or(not(or(X3,X4)),or(X3,X5))),not(or(X2,or(not(X4),X5)))))),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_299,plain,
theorem(or(X1,or(X2,or(or(X3,or(X4,X5)),not(or(X3,or(X5,X4))))))),
inference(scs_inference,[],[i_0_33,i_0_111,i_0_25]) ).
cnf(i_0_300,plain,
theorem(or(not(or(not(X1),X2)),or(X3,or(X4,or(or(X5,X2),not(or(X5,X1))))))),
inference(rename_variables,[],[i_0_111]) ).
cnf(i_0_308,plain,
theorem(or(or(or(X1,X2),not(or(or(X1,X2),or(X1,X3)))),not(or(not(X3),X2)))),
inference(scs_inference,[],[i_0_126,i_0_178,i_0_25]) ).
cnf(i_0_309,plain,
theorem(or(not(or(or(X1,or(X2,X2)),X3)),or(or(X2,X1),X3))),
inference(rename_variables,[],[i_0_178]) ).
cnf(i_0_320,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X1,or(X4,X2))))),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_403,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X4,or(X2,X1))))),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_408,plain,
theorem(or(not(or(X1,not(X2))),or(not(or(X3,X2)),or(X4,or(X3,X1))))),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_437,plain,
theorem(or(X1,or(not(or(X1,or(X2,X3))),or(X3,X2)))),
inference(scs_inference,[],[i_0_33,i_0_101,i_0_25]) ).
cnf(i_0_438,plain,
theorem(or(not(or(not(X1),X2)),or(X3,or(not(or(X3,X1)),X2)))),
inference(rename_variables,[],[i_0_101]) ).
cnf(i_0_440,plain,
theorem(or(not(or(X1,X2)),or(X1,or(not(or(not(X2),or(X3,X4))),or(X4,X3))))),
inference(scs_inference,[],[i_0_33,i_0_101,i_0_25,i_0_29]) ).
cnf(i_0_478,plain,
theorem(or(not(or(X1,or(X2,or(or(X3,X4),X5)))),or(X1,or(X2,or(X3,or(X5,X4)))))),
inference(scs_inference,[],[i_0_476,i_0_29]) ).
cnf(i_0_480,plain,
theorem(or(not(or(X1,not(X2))),or(not(or(X3,X2)),or(X1,X3)))),
inference(scs_inference,[],[i_0_33,i_0_476,i_0_117,i_0_29,i_0_25]) ).
cnf(i_0_493,plain,
theorem(or(not(or(or(X1,or(X2,X2)),X3)),or(or(X2,X1),X3))),
inference(rename_variables,[],[i_0_178]) ).
cnf(i_0_513,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X1,or(X4,X2))))),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_517,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X4,or(X2,X1))))),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_536,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X1,or(X4,X2))))),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_546,plain,
theorem(or(not(or(or(X1,X2),X3)),or(X3,or(X4,or(X2,X1))))),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_556,plain,
theorem(or(not(or(X1,or(X2,or(X3,X4)))),or(X1,or(X2,or(X5,or(X6,or(X3,X4))))))),
inference(scs_inference,[],[i_0_554,i_0_29]) ).
cnf(c_0_916,axiom,
( theorem(X1)
| ~ axiom(X1) ),
i_0_26 ).
cnf(c_0_917,plain,
axiom(or(not(or(X1,X1)),X1)),
i_0_23 ).
cnf(c_0_918,plain,
( theorem(X1)
| ~ theorem(X2)
| ~ theorem(or(not(X2),X1)) ),
i_0_25 ).
cnf(c_0_919,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(spm,[status(thm)],[c_0_916,c_0_917]) ).
cnf(c_0_920,plain,
theorem(or(not(or(X1,X2)),or(X2,or(X3,X1)))),
i_0_602 ).
cnf(c_0_921,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X3,or(X1,X2)))),
i_0_897 ).
cnf(c_0_922,plain,
axiom(or(not(X1),or(X2,X1))),
i_0_24 ).
cnf(c_0_923,plain,
theorem(or(not(or(X1,not(X2))),or(not(or(X3,X2)),or(X1,X3)))),
i_0_480 ).
cnf(c_0_924,plain,
( theorem(X1)
| ~ theorem(or(X1,X1)) ),
inference(spm,[status(thm)],[c_0_918,c_0_919]) ).
cnf(c_0_925,plain,
( theorem(or(X1,or(X2,X3)))
| ~ theorem(or(X3,X1)) ),
inference(spm,[status(thm)],[c_0_918,c_0_920]) ).
cnf(c_0_926,plain,
( theorem(or(X1,or(X2,X3)))
| ~ theorem(or(X2,or(X3,X1))) ),
inference(spm,[status(thm)],[c_0_918,c_0_921]) ).
cnf(c_0_927,plain,
theorem(or(not(X1),or(X2,X1))),
inference(spm,[status(thm)],[c_0_916,c_0_922]) ).
cnf(c_0_928,plain,
( theorem(or(not(or(X1,X2)),or(X3,X1)))
| ~ theorem(or(X3,not(X2))) ),
inference(spm,[status(thm)],[c_0_918,c_0_923]) ).
cnf(c_0_929,plain,
( theorem(or(X1,X2))
| ~ theorem(or(X2,or(X1,X2))) ),
inference(spm,[status(thm)],[c_0_924,c_0_925]) ).
cnf(c_0_930,plain,
theorem(or(X1,or(not(X1),X2))),
inference(spm,[status(thm)],[c_0_926,c_0_927]) ).
cnf(c_0_931,plain,
( theorem(or(X1,X2))
| ~ theorem(or(X1,not(X3)))
| ~ theorem(or(X2,X3)) ),
inference(spm,[status(thm)],[c_0_918,c_0_928]) ).
cnf(c_0_932,plain,
theorem(or(not(X1),X1)),
inference(spm,[status(thm)],[c_0_929,c_0_930]) ).
cnf(c_0_933,plain,
theorem(or(X1,or(not(or(X1,or(X2,X3))),or(X3,X2)))),
i_0_437 ).
cnf(c_0_934,plain,
( theorem(or(not(not(X1)),X2))
| ~ theorem(or(X2,X1)) ),
inference(spm,[status(thm)],[c_0_931,c_0_932]) ).
cnf(c_0_935,plain,
( theorem(or(not(or(not(X1),or(X2,X3))),or(X3,X2)))
| ~ theorem(X1) ),
inference(spm,[status(thm)],[c_0_918,c_0_933]) ).
cnf(c_0_936,negated_conjecture,
~ theorem(or(not(or(not(p),or(not(q),r))),or(not(not(or(not(p),not(q)))),r))),
i_0_19 ).
cnf(c_0_937,plain,
( theorem(or(X1,or(not(not(X2)),X3)))
| ~ theorem(or(or(X3,X1),X2)) ),
inference(spm,[status(thm)],[c_0_926,c_0_934]) ).
cnf(c_0_938,plain,
( theorem(or(X1,X2))
| ~ theorem(or(not(X3),or(X2,X1)))
| ~ theorem(X3) ),
inference(spm,[status(thm)],[c_0_918,c_0_935]) ).
cnf(c_0_939,negated_conjecture,
~ theorem(or(or(r,not(or(not(p),or(not(q),r)))),or(not(p),not(q)))),
inference(spm,[status(thm)],[c_0_936,c_0_937]) ).
cnf(c_0_940,plain,
( theorem(or(or(X1,X2),X3))
| ~ theorem(or(X1,or(X2,X3))) ),
inference(spm,[status(thm)],[c_0_938,c_0_921]) ).
cnf(c_0_941,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(or(not(or(X4,X2)),or(X4,X3)),X1))),
i_0_905 ).
cnf(c_0_942,plain,
~ theorem(or(r,or(not(or(not(p),or(not(q),r))),or(not(p),not(q))))),
inference(spm,[status(thm)],[c_0_939,c_0_940]) ).
cnf(c_0_943,plain,
( theorem(or(X1,or(not(or(X2,X3)),or(X2,X4))))
| ~ theorem(or(X1,or(not(X3),X4))) ),
inference(spm,[status(thm)],[c_0_938,c_0_941]) ).
cnf(c_0_944,plain,
theorem(or(X1,or(not(or(X2,X1)),X2))),
inference(spm,[status(thm)],[c_0_926,c_0_932]) ).
cnf(c_0_945,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_942,c_0_943]),c_0_944])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL243-3 : TPTP v9.2.1. Released v2.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n028.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 22:15:30 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 162.03/86.94 % Version : CSE_E---1.7
% 162.03/86.94 % Problem : theBenchmark.p
% 162.03/86.94 % SZS status Unsatisfiable for theBenchmark.p
% 162.03/86.94 % SZS output start CNFRefutation
% See solution above
% 162.63/87.54 % Total time : 86.022s
%------------------------------------------------------------------------------