%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LCL191-3 : TPTP v9.2.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n005.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:39 PM UTC 2026
% Result : Unsatisfiable 114.24s 80.48s
% Output : CNFRefutation 115.23s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_10)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
~ theorem(implies(or(p,or(q,r)),or(or(p,q),r))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
cnf(implies_definition,axiom,
implies(X1,X2) = or(not(X1),X2),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',implies_definition) ).
cnf(axiom_1_6,axiom,
axiom(implies(implies(X1,X2),implies(or(X3,X1),or(X3,X2)))),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_5) ).
cnf(axiom_1_4,axiom,
axiom(implies(or(X1,X2),or(X2,X1))),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_4) ).
cnf(axiom_1_2,axiom,
axiom(implies(or(X1,X1),X1)),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_2) ).
cnf(axiom_1_3,axiom,
axiom(implies(X1,or(X2,X1))),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_3) ).
cnf(rule_2,axiom,
( theorem(X1)
| ~ theorem(implies(X2,X1))
| ~ theorem(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',rule_2) ).
cnf(rule_1,axiom,
( theorem(X1)
| ~ axiom(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',rule_1) ).
cnf(i_0_9,negated_conjecture,
~ theorem(implies(or(p,or(q,r)),or(or(p,q),r))),
prove_this ).
cnf(i_0_10,axiom,
implies(X1,X2) = or(not(X1),X2),
implies_definition ).
cnf(i_0_11,axiom,
axiom(implies(implies(X1,X2),implies(or(X3,X1),or(X3,X2)))),
axiom_1_6 ).
cnf(i_0_12,axiom,
axiom(implies(or(X1,or(X2,X3)),or(X2,or(X1,X3)))),
axiom_1_5 ).
cnf(i_0_13,axiom,
axiom(implies(or(X1,X2),or(X2,X1))),
axiom_1_4 ).
cnf(i_0_14,axiom,
axiom(implies(or(X1,X1),X1)),
axiom_1_2 ).
cnf(i_0_15,axiom,
axiom(implies(X1,or(X2,X1))),
axiom_1_3 ).
cnf(i_0_16,axiom,
( theorem(X1)
| ~ theorem(implies(X2,X1))
| ~ theorem(X2) ),
rule_2 ).
cnf(i_0_17,negated_conjecture,
~ theorem(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(rw,[status(thm)],[i_0_9,c_0_10]),
[final] ).
cnf(i_0_18,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_11,c_0_10]),c_0_10]),c_0_10]),
[final] ).
cnf(i_0_19,plain,
axiom(or(not(or(X1,or(X2,X3))),or(X2,or(X1,X3)))),
inference(rw,[status(thm)],[i_0_12,c_0_10]),
[final] ).
cnf(i_0_20,plain,
axiom(or(not(or(X1,X2)),or(X2,X1))),
inference(rw,[status(thm)],[i_0_13,c_0_10]),
[final] ).
cnf(i_0_21,plain,
axiom(or(not(or(X1,X1)),X1)),
inference(rw,[status(thm)],[i_0_14,c_0_10]),
[final] ).
cnf(i_0_22,plain,
axiom(or(not(X1),or(X2,X1))),
inference(rw,[status(thm)],[i_0_15,c_0_10]),
[final] ).
cnf(i_0_23,plain,
( theorem(X1)
| ~ theorem(X2)
| ~ theorem(or(not(X2),X1)) ),
inference(rw,[status(thm)],[i_0_16,c_0_10]),
[final] ).
cnf(i_0_24,axiom,
( theorem(X1)
| ~ axiom(X1) ),
rule_1,
[final] ).
cnf(i_0_25,plain,
theorem(or(not(or(not(X1),X2)),or(not(or(X3,X1)),or(X3,X2)))),
inference(scs_inference,[],[i_0_18,i_0_24]) ).
cnf(i_0_29,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(scs_inference,[],[i_0_20,i_0_24]) ).
cnf(i_0_34,plain,
theorem(or(not(X1),or(X2,X1))),
inference(scs_inference,[],[i_0_22,i_0_24]) ).
cnf(i_0_36,plain,
~ theorem(or(or(p,q),r)),
inference(scs_inference,[],[i_0_17,i_0_22,i_0_24,i_0_23]) ).
cnf(i_0_831,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_837,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_839,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_841,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_843,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_847,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_849,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_851,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_853,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_859,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_861,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_863,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_865,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_869,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_871,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_873,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_875,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_881,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_883,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_885,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_887,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_893,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_895,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_897,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_899,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_905,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_907,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_909,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_911,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_915,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_917,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_919,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_921,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_923,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_925,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_927,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_929,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_931,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_933,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_935,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_937,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_939,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_941,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_943,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_945,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_947,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_949,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_951,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_953,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_955,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_957,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_959,plain,
~ axiom(or(not(or(p,or(q,r))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_24]) ).
cnf(i_0_31,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(scs_inference,[],[i_0_25,i_0_20,i_0_24,i_0_23]) ).
cnf(i_0_32,plain,
theorem(or(not(or(not(X1),X2)),or(not(or(X3,X1)),or(X3,X2)))),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_38,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(scs_inference,[],[i_0_34,i_0_27]) ).
cnf(i_0_40,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(scs_inference,[],[i_0_34,i_0_21,i_0_27,i_0_24]) ).
cnf(i_0_42,plain,
~ theorem(or(not(or(p,or(q,r))),r)),
inference(scs_inference,[],[i_0_17,i_0_34,i_0_21,i_0_27,i_0_24,i_0_23]) ).
cnf(i_0_51,plain,
~ theorem(or(r,or(p,q))),
inference(scs_inference,[],[i_0_36,i_0_29,i_0_23]) ).
cnf(i_0_52,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_54,plain,
~ theorem(r),
inference(scs_inference,[],[i_0_36,i_0_34,i_0_23]) ).
cnf(i_0_55,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_61,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_70,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_73,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_91,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_106,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_112,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_118,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_160,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_166,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_175,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_181,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_187,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_193,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_202,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_232,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_268,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_277,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_289,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_298,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_319,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_346,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_352,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_358,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_364,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_367,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_397,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_403,plain,
theorem(or(not(X1),or(X2,X1))),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_409,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_457,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_466,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_490,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_517,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_535,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_541,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_547,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_553,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_562,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_568,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_577,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_583,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_592,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_604,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_619,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_643,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_649,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_676,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_708,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(X1,or(not(or(X4,X2)),or(X4,X3))))),
inference(scs_inference,[],[i_0_25,i_0_27]) ).
cnf(i_0_833,plain,
~ theorem(or(not(or(not(X1),or(X2,X1))),or(not(or(p,or(q,r))),or(or(p,q),r)))),
inference(scs_inference,[],[i_0_17,i_0_34,i_0_24,i_0_23]) ).
cnf(i_0_835,plain,
~ theorem(or(not(or(X1,or(p,or(q,r)))),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_34,i_0_24,i_0_23,i_0_27]) ).
cnf(i_0_889,plain,
~ theorem(or(not(or(not(or(X1,X2)),or(X2,X1))),or(not(or(p,or(q,r))),or(or(p,q),r)))),
inference(scs_inference,[],[i_0_17,i_0_29,i_0_24,i_0_23]) ).
cnf(i_0_891,plain,
~ theorem(or(not(or(or(q,r),p)),or(or(p,q),r))),
inference(scs_inference,[],[i_0_17,i_0_29,i_0_24,i_0_23,i_0_27]) ).
cnf(i_0_1175,plain,
~ axiom(or(or(p,q),r)),
inference(scs_inference,[],[i_0_36,i_0_24]) ).
cnf(i_0_1234,plain,
theorem(or(not(or(not(X1),X2)),or(not(or(X3,X1)),or(X3,X2)))),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_44,plain,
theorem(or(not(or(X1,or(X2,X2))),or(X1,X2))),
inference(scs_inference,[],[i_0_40,i_0_27]) ).
cnf(i_0_46,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X2,or(X1,X3)))),
inference(scs_inference,[],[i_0_40,i_0_19,i_0_27,i_0_24]) ).
cnf(i_0_57,plain,
~ theorem(or(or(or(p,q),r),or(or(p,q),r))),
inference(scs_inference,[],[i_0_36,i_0_40,i_0_23]) ).
cnf(i_0_58,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_60,plain,
~ theorem(or(r,not(or(p,or(q,r))))),
inference(scs_inference,[],[i_0_42,i_0_29,i_0_23]) ).
cnf(i_0_76,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_78,plain,
~ theorem(or(r,or(q,p))),
inference(scs_inference,[],[i_0_51,i_0_31,i_0_23]) ).
cnf(i_0_79,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_81,plain,
~ theorem(or(r,q)),
inference(scs_inference,[],[i_0_51,i_0_38,i_0_23]) ).
cnf(i_0_82,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_90,plain,
~ theorem(or(p,q)),
inference(scs_inference,[],[i_0_51,i_0_34,i_0_23]) ).
cnf(i_0_93,plain,
~ theorem(or(or(r,or(p,q)),or(r,or(p,q)))),
inference(scs_inference,[],[i_0_51,i_0_40,i_0_23]) ).
cnf(i_0_94,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_97,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_100,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_121,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_127,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_130,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_136,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_145,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_148,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_154,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_163,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_178,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_196,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_205,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_211,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_214,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_220,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_229,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_235,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_238,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_247,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_253,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_259,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_274,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_280,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_286,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_304,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_307,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_313,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_325,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_328,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_337,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_343,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_355,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_373,plain,
theorem(or(not(or(X1,X1)),X1)),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_376,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_379,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
inference(rename_variables,[],[i_0_38]) ).
cnf(c_0_841,plain,
( theorem(X1)
| ~ theorem(X2)
| ~ theorem(or(not(X2),X1)) ),
i_0_23 ).
cnf(c_0_842,plain,
theorem(or(not(or(X1,X2)),or(X1,or(X3,X2)))),
i_0_38 ).
cnf(c_0_843,plain,
( theorem(or(X1,or(X2,X3)))
| ~ theorem(or(X1,X3)) ),
inference(spm,[status(thm)],[c_0_841,c_0_842]) ).
cnf(c_0_844,plain,
( theorem(or(X1,X2))
| ~ theorem(or(not(X3),X2))
| ~ theorem(X3) ),
inference(spm,[status(thm)],[c_0_841,c_0_843]) ).
cnf(c_0_845,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X1,or(X3,X2)))),
i_0_31 ).
cnf(c_0_846,plain,
theorem(or(not(or(X1,or(X2,X3))),or(X2,or(X1,X3)))),
i_0_46 ).
cnf(c_0_847,plain,
theorem(or(not(or(X1,or(not(X2),X3))),or(X1,or(not(or(X4,X2)),or(X4,X3))))),
i_0_708 ).
cnf(c_0_848,plain,
~ theorem(or(not(or(not(X1),or(X2,X1))),or(not(or(p,or(q,r))),or(or(p,q),r)))),
i_0_833 ).
cnf(c_0_849,plain,
( theorem(or(X1,or(X2,or(X3,X4))))
| ~ theorem(or(X2,or(X4,X3))) ),
inference(spm,[status(thm)],[c_0_844,c_0_845]) ).
cnf(c_0_850,plain,
( theorem(or(X1,or(X2,X3)))
| ~ theorem(or(X2,or(X1,X3))) ),
inference(spm,[status(thm)],[c_0_841,c_0_846]) ).
cnf(c_0_851,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_841,c_0_847]) ).
cnf(c_0_852,plain,
theorem(or(not(or(X1,X2)),or(X2,X1))),
i_0_29 ).
cnf(c_0_853,plain,
~ theorem(or(not(or(p,or(q,r))),or(r,or(p,q)))),
inference(spm,[status(thm)],[c_0_848,c_0_849]) ).
cnf(c_0_854,plain,
( theorem(or(not(or(X1,X2)),or(X3,or(X1,X4))))
| ~ theorem(or(X3,or(not(X2),X4))) ),
inference(spm,[status(thm)],[c_0_850,c_0_851]) ).
cnf(c_0_855,plain,
theorem(or(X1,or(not(or(X2,X1)),X2))),
inference(spm,[status(thm)],[c_0_850,c_0_852]) ).
cnf(c_0_856,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_853,c_0_854]),c_0_855])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL191-3 : TPTP v9.2.1. Released v2.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32 % Computer : n005.cluster.edu
% 0.16/0.32 % Model : x86_64 x86_64
% 0.16/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.32 % Memory : 8042.1875MB
% 0.16/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.32 % CPULimit : 300
% 0.16/0.32 % WCLimit : 300
% 0.16/0.32 % DateTime : Mon May 4 22:07:45 EDT 2026
% 0.16/0.32 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 114.24/80.48 % Version : CSE_E---1.7
% 114.24/80.48 % Problem : theBenchmark.p
% 114.24/80.48 % SZS status Unsatisfiable for theBenchmark.p
% 114.24/80.48 % SZS output start CNFRefutation
% See solution above
% 115.23/81.40 % Total time : 80.106s
%------------------------------------------------------------------------------