%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL304-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:06:18 PM UTC 2026
% Result : Unsatisfiable 174.10s 28.03s
% Output : CNFRefutation 174.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 30
% Syntax : Number of formulae : 156 ( 109 unt; 19 def)
% Number of atoms : 480 ( 23 equ)
% Maximal formula atoms : 3 ( 3 avg)
% Number of connectives : 126 ( 66 ~; 60 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 21 usr; 20 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 136 ( 0 sgn 136 !; 0 ?; 101 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_2) ).
fof(f2,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_3) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_4) ).
fof(f4,axiom,
! [X2,X0,X1] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_5) ).
fof(f5,axiom,
! [X2,X0,X1] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',axiom_1_6) ).
fof(f6,axiom,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',implies_definition) ).
fof(f7,axiom,
! [X0] :
( ~ axiom(X0)
| theorem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',rule_1) ).
fof(f8,axiom,
! [X0,X1] :
( ~ theorem(X1)
| ~ theorem(implies(X1,X0))
| theorem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-0.ax',rule_2) ).
fof(f9,axiom,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-1.ax',and_defn) ).
fof(f10,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL004-2.ax',equivalent_defn) ).
fof(f11,negated_conjecture,
~ theorem(equivalent(implies(p,q),equivalent(q,or(p,q)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f12,plain,
! [X0,X1] : equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0)))),
inference(definition_unfolding,[],[f10,f9,f6,f6]) ).
fof(f13,plain,
! [X0] : axiom(or(not(or(X0,X0)),X0)),
inference(definition_unfolding,[],[f1,f6]) ).
fof(f14,plain,
! [X0,X1] : axiom(or(not(X0),or(X1,X0))),
inference(definition_unfolding,[],[f2,f6]) ).
fof(f15,plain,
! [X0,X1] : axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(definition_unfolding,[],[f3,f6]) ).
fof(f16,plain,
! [X2,X0,X1] : axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(definition_unfolding,[],[f4,f6]) ).
fof(f17,plain,
! [X2,X0,X1] : axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(definition_unfolding,[],[f5,f6,f6,f6]) ).
fof(f18,plain,
! [X0,X1] :
( ~ theorem(X1)
| ~ theorem(or(not(X1),X0))
| theorem(X0) ),
inference(definition_unfolding,[],[f8,f6]) ).
fof(f19,plain,
~ theorem(not(or(not(or(not(or(not(p),q)),not(or(not(or(not(q),or(p,q))),not(or(not(or(p,q)),q)))))),not(or(not(not(or(not(or(not(q),or(p,q))),not(or(not(or(p,q)),q))))),or(not(p),q)))))),
inference(definition_unfolding,[],[f11,f12,f6,f12]) ).
tcf(c_60,plain,
! [X0: $i] : axiom(or(not(or(X0,X0)),X0)),
inference(cnf_transformation,[],[f13]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : axiom(or(not(X0),or(X1,X0))),
inference(cnf_transformation,[],[f14]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(cnf_transformation,[],[f15]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] : axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(cnf_transformation,[],[f16]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] : axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(cnf_transformation,[],[f17]) ).
tcf(c_65,plain,
! [X0: $i] :
( theorem(X0)
| ~ axiom(X0) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( theorem(X1)
| ~ theorem(X0)
| ~ theorem(or(not(X0),X1)) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_67,negated_conjecture,
~ theorem(not(or(not(or(not(or(not(p),q)),not(or(not(or(not(q),or(p,q))),not(or(not(or(p,q)),q)))))),not(or(not(not(or(not(or(not(q),or(p,q))),not(or(not(or(p,q)),q))))),or(not(p),q)))))),
inference(cnf_transformation,[],[f19]) ).
tcf(c_96,plain,
! [X0: $i] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[status(thm)],[c_65,c_60]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[status(thm)],[c_65,c_61]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[status(thm)],[c_65,c_62]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[status(thm)],[c_65,c_63]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[status(thm)],[c_65,c_64]) ).
tcf(c_144,definition,
iPr_def_10 = not(p),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_145,definition,
iPr_def_11 = or(iPr_def_10,q),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_146,definition,
iPr_def_12 = not(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_147,definition,
iPr_def_13 = not(q),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_148,definition,
iPr_def_14 = or(p,q),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_149,definition,
iPr_def_15 = or(iPr_def_13,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_150,definition,
iPr_def_16 = not(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_151,definition,
iPr_def_17 = not(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_152,definition,
iPr_def_18 = or(iPr_def_17,q),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_153,definition,
iPr_def_19 = not(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_154,definition,
iPr_def_20 = or(iPr_def_16,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_155,definition,
iPr_def_21 = not(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_156,definition,
iPr_def_22 = or(iPr_def_12,iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_157,definition,
iPr_def_23 = not(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_158,definition,
iPr_def_24 = not(iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_159,definition,
iPr_def_25 = or(iPr_def_24,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_160,definition,
iPr_def_26 = not(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_161,definition,
iPr_def_27 = or(iPr_def_23,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_162,definition,
iPr_def_28 = not(iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_163,negated_conjecture,
~ theorem(iPr_def_28),
inference(demodulation,[status(thm)],[c_67,c_158,c_159,c_160,c_151,c_152,c_153,c_148,c_147,c_149,c_150,c_154,c_155,c_144,c_145,c_146,c_156,c_157,c_161,c_162]) ).
tcf(c_340,plain,
! [X0: $i] : theorem(or(iPr_def_17,or(X0,iPr_def_14))),
inference(superposition,[status(thm)],[c_151,c_101]) ).
tcf(c_341,plain,
! [X0: $i] : theorem(or(iPr_def_19,or(X0,iPr_def_18))),
inference(superposition,[status(thm)],[c_153,c_101]) ).
tcf(c_342,plain,
! [X0: $i] : theorem(or(iPr_def_21,or(X0,iPr_def_20))),
inference(superposition,[status(thm)],[c_155,c_101]) ).
tcf(c_344,plain,
! [X0: $i] : theorem(or(iPr_def_24,or(X0,iPr_def_21))),
inference(superposition,[status(thm)],[c_158,c_101]) ).
tcf(c_347,plain,
theorem(or(not(q),iPr_def_14)),
inference(superposition,[status(thm)],[c_148,c_101]) ).
tcf(c_350,plain,
theorem(or(not(q),iPr_def_18)),
inference(superposition,[status(thm)],[c_152,c_101]) ).
tcf(c_357,plain,
theorem(or(iPr_def_13,iPr_def_18)),
inference(light_normalisation,[status(thm)],[c_350,c_147]) ).
tcf(c_360,plain,
theorem(iPr_def_15),
inference(light_normalisation,[status(thm)],[c_347,c_147,c_149]) ).
tcf(c_379,plain,
theorem(or(not(iPr_def_27),or(iPr_def_26,iPr_def_23))),
inference(superposition,[status(thm)],[c_161,c_106]) ).
tcf(c_388,plain,
theorem(or(iPr_def_28,or(iPr_def_26,iPr_def_23))),
inference(light_normalisation,[status(thm)],[c_379,c_162]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i] :
( theorem(or(X1,X0))
| ~ theorem(X0) ),
inference(superposition,[status(thm)],[c_101,c_66]) ).
tcf(c_413,plain,
! [X0: $i,X1: $i] :
( theorem(or(X1,X0))
| ~ theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_106,c_66]) ).
tcf(c_417,plain,
! [X0: $i] :
( theorem(X0)
| ~ theorem(iPr_def_15)
| ~ theorem(or(iPr_def_16,X0)) ),
inference(superposition,[status(thm)],[c_150,c_66]) ).
tcf(c_421,plain,
! [X0: $i] :
( theorem(X0)
| ~ theorem(iPr_def_22)
| ~ theorem(or(iPr_def_23,X0)) ),
inference(superposition,[status(thm)],[c_157,c_66]) ).
tcf(c_423,plain,
! [X0: $i] :
( theorem(X0)
| ~ theorem(iPr_def_25)
| ~ theorem(or(iPr_def_26,X0)) ),
inference(superposition,[status(thm)],[c_160,c_66]) ).
tcf(c_452,plain,
! [X0: $i] :
( theorem(X0)
| ~ theorem(or(iPr_def_16,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_417,c_360]) ).
tcf(c_520,plain,
! [X0: $i] : theorem(or(not(or(X0,iPr_def_14)),or(p,or(X0,q)))),
inference(superposition,[status(thm)],[c_148,c_111]) ).
tcf(c_521,plain,
! [X0: $i] : theorem(or(not(or(X0,iPr_def_11)),or(iPr_def_10,or(X0,q)))),
inference(superposition,[status(thm)],[c_145,c_111]) ).
tcf(c_524,plain,
! [X0: $i] : theorem(or(not(or(X0,iPr_def_20)),or(iPr_def_16,or(X0,iPr_def_19)))),
inference(superposition,[status(thm)],[c_154,c_111]) ).
tcf(c_532,plain,
! [X0: $i] : theorem(or(not(or(iPr_def_16,or(X0,iPr_def_19))),or(X0,iPr_def_20))),
inference(superposition,[status(thm)],[c_154,c_111]) ).
tcf(c_533,plain,
! [X0: $i] : theorem(or(not(or(iPr_def_12,or(X0,iPr_def_21))),or(X0,iPr_def_22))),
inference(superposition,[status(thm)],[c_156,c_111]) ).
tcf(c_536,plain,
! [X0: $i,X1: $i,X2: $i] :
( theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,or(X1,X2))) ),
inference(superposition,[status(thm)],[c_111,c_66]) ).
tcf(c_599,plain,
! [X0: $i,X1: $i] : theorem(or(not(or(iPr_def_10,X0)),or(not(or(X1,p)),or(X1,X0)))),
inference(superposition,[status(thm)],[c_144,c_116]) ).
tcf(c_603,plain,
! [X0: $i,X1: $i] : theorem(or(not(or(iPr_def_17,X0)),or(not(or(X1,iPr_def_14)),or(X1,X0)))),
inference(superposition,[status(thm)],[c_151,c_116]) ).
tcf(c_604,plain,
! [X0: $i,X1: $i] : theorem(or(not(or(iPr_def_19,X0)),or(not(or(X1,iPr_def_18)),or(X1,X0)))),
inference(superposition,[status(thm)],[c_153,c_116]) ).
tcf(c_605,plain,
! [X0: $i,X1: $i] : theorem(or(not(or(iPr_def_21,X0)),or(not(or(X1,iPr_def_20)),or(X1,X0)))),
inference(superposition,[status(thm)],[c_155,c_116]) ).
tcf(c_611,plain,
! [X0: $i] : theorem(or(not(or(not(q),X0)),or(not(iPr_def_11),or(iPr_def_10,X0)))),
inference(superposition,[status(thm)],[c_145,c_116]) ).
tcf(c_633,plain,
! [X0: $i] : theorem(or(not(or(iPr_def_13,X0)),or(iPr_def_12,or(iPr_def_10,X0)))),
inference(light_normalisation,[status(thm)],[c_611,c_146,c_147]) ).
tcf(c_1815,plain,
theorem(or(not(or(iPr_def_17,iPr_def_14)),or(p,iPr_def_18))),
inference(superposition,[status(thm)],[c_152,c_520]) ).
tcf(c_1864,plain,
( theorem(or(p,iPr_def_18))
| ~ theorem(or(iPr_def_17,iPr_def_14)) ),
inference(superposition,[status(thm)],[c_1815,c_66]) ).
tcf(c_1906,plain,
theorem(or(not(or(p,iPr_def_11)),or(iPr_def_10,iPr_def_14))),
inference(superposition,[status(thm)],[c_148,c_521]) ).
tcf(c_1986,plain,
( theorem(or(iPr_def_10,iPr_def_14))
| ~ theorem(or(p,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_1906,c_66]) ).
tcf(c_2265,plain,
! [X0: $i] :
( theorem(or(iPr_def_16,or(X0,iPr_def_19)))
| ~ theorem(or(X0,iPr_def_20)) ),
inference(superposition,[status(thm)],[c_524,c_66]) ).
tcf(c_2646,plain,
! [X0: $i] :
( theorem(or(X0,iPr_def_20))
| ~ theorem(or(iPr_def_16,or(X0,iPr_def_19))) ),
inference(superposition,[status(thm)],[c_532,c_66]) ).
tcf(c_2690,plain,
! [X0: $i] :
( theorem(or(X0,iPr_def_22))
| ~ theorem(or(iPr_def_12,or(X0,iPr_def_21))) ),
inference(superposition,[status(thm)],[c_533,c_66]) ).
tcf(c_2811,plain,
! [X0: $i,X1: $i] : theorem(or(X0,or(not(or(or(X0,X1),or(X0,X1))),X1))),
inference(superposition,[status(thm)],[c_96,c_536]) ).
tcf(c_2820,plain,
! [X0: $i] : theorem(or(X0,or(iPr_def_17,iPr_def_14))),
inference(superposition,[status(thm)],[c_340,c_536]) ).
tcf(c_2821,plain,
! [X0: $i] : theorem(or(X0,or(iPr_def_19,iPr_def_18))),
inference(superposition,[status(thm)],[c_341,c_536]) ).
tcf(c_2822,plain,
! [X0: $i] : theorem(or(X0,or(iPr_def_21,iPr_def_20))),
inference(superposition,[status(thm)],[c_342,c_536]) ).
tcf(c_2824,plain,
! [X0: $i] : theorem(or(X0,or(iPr_def_24,iPr_def_21))),
inference(superposition,[status(thm)],[c_344,c_536]) ).
tcf(c_2827,plain,
theorem(or(iPr_def_26,or(iPr_def_28,iPr_def_23))),
inference(superposition,[status(thm)],[c_388,c_536]) ).
tcf(c_2850,plain,
! [X0: $i] : theorem(or(X0,or(not(or(iPr_def_12,or(X0,iPr_def_21))),iPr_def_22))),
inference(superposition,[status(thm)],[c_533,c_536]) ).
tcf(c_3188,plain,
! [X0: $i,X1: $i] :
( theorem(or(not(or(X1,p)),or(X1,X0)))
| ~ theorem(or(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_599,c_66]) ).
tcf(c_3277,plain,
theorem(or(iPr_def_17,iPr_def_14)),
inference(superposition,[status(thm)],[c_2820,c_452]) ).
tcf(c_3286,plain,
theorem(or(p,iPr_def_18)),
inference(backward_subsumption_resolution,[status(thm)],[c_1864,c_3277]) ).
tcf(c_3290,plain,
theorem(or(iPr_def_18,p)),
inference(superposition,[status(thm)],[c_3286,c_413]) ).
tcf(c_3299,plain,
theorem(or(iPr_def_19,iPr_def_18)),
inference(superposition,[status(thm)],[c_2821,c_452]) ).
tcf(c_3309,plain,
theorem(or(iPr_def_18,iPr_def_19)),
inference(superposition,[status(thm)],[c_3299,c_413]) ).
tcf(c_3318,plain,
theorem(or(iPr_def_21,iPr_def_20)),
inference(superposition,[status(thm)],[c_2822,c_452]) ).
tcf(c_3391,plain,
! [X0: $i] :
( theorem(or(iPr_def_12,or(iPr_def_10,X0)))
| ~ theorem(or(iPr_def_13,X0)) ),
inference(superposition,[status(thm)],[c_633,c_66]) ).
tcf(c_3428,plain,
theorem(or(iPr_def_24,iPr_def_21)),
inference(superposition,[status(thm)],[c_2824,c_452]) ).
tcf(c_3438,plain,
theorem(or(iPr_def_21,iPr_def_24)),
inference(superposition,[status(thm)],[c_3428,c_413]) ).
tcf(c_3484,plain,
( theorem(or(iPr_def_28,iPr_def_23))
| ~ theorem(iPr_def_25) ),
inference(superposition,[status(thm)],[c_2827,c_423]) ).
tcf(c_3765,plain,
! [X0: $i] :
( theorem(or(X0,iPr_def_19))
| ~ theorem(or(X0,iPr_def_20)) ),
inference(superposition,[status(thm)],[c_2265,c_452]) ).
tcf(c_3940,plain,
theorem(or(not(or(iPr_def_17,q)),or(not(or(iPr_def_10,iPr_def_14)),iPr_def_11))),
inference(superposition,[status(thm)],[c_145,c_603]) ).
tcf(c_3952,plain,
theorem(or(iPr_def_19,or(not(or(iPr_def_10,iPr_def_14)),iPr_def_11))),
inference(light_normalisation,[status(thm)],[c_3940,c_152,c_153]) ).
tcf(c_3964,plain,
theorem(or(not(or(iPr_def_10,iPr_def_14)),or(iPr_def_19,iPr_def_11))),
inference(superposition,[status(thm)],[c_3952,c_536]) ).
tcf(c_4108,plain,
theorem(or(not(or(iPr_def_19,iPr_def_11)),or(not(or(iPr_def_24,iPr_def_18)),iPr_def_25))),
inference(superposition,[status(thm)],[c_159,c_604]) ).
tcf(c_4110,plain,
! [X0: $i,X1: $i] :
( theorem(or(not(or(X1,iPr_def_18)),or(X1,X0)))
| ~ theorem(or(iPr_def_19,X0)) ),
inference(superposition,[status(thm)],[c_604,c_66]) ).
tcf(c_4196,plain,
! [X0: $i] :
( theorem(or(X0,iPr_def_20))
| ~ theorem(or(X0,iPr_def_19)) ),
inference(superposition,[status(thm)],[c_412,c_2646]) ).
tcf(c_4380,plain,
! [X0: $i,X1: $i] :
( theorem(or(not(or(X1,iPr_def_20)),or(X1,X0)))
| ~ theorem(or(iPr_def_21,X0)) ),
inference(superposition,[status(thm)],[c_605,c_66]) ).
tcf(c_4426,plain,
! [X0: $i] :
( theorem(or(X0,iPr_def_22))
| ~ theorem(or(X0,iPr_def_21)) ),
inference(superposition,[status(thm)],[c_412,c_2690]) ).
tcf(c_4487,plain,
( theorem(or(iPr_def_23,iPr_def_28))
| ~ theorem(iPr_def_25) ),
inference(superposition,[status(thm)],[c_3484,c_413]) ).
tcf(c_4952,plain,
( theorem(iPr_def_28)
| ~ theorem(iPr_def_25)
| ~ theorem(iPr_def_22) ),
inference(superposition,[status(thm)],[c_4487,c_421]) ).
tcf(c_4953,plain,
( ~ theorem(iPr_def_25)
| ~ theorem(iPr_def_22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4952,c_163]) ).
tcf(c_5100,plain,
( theorem(or(iPr_def_10,iPr_def_22))
| ~ theorem(or(iPr_def_13,iPr_def_21)) ),
inference(superposition,[status(thm)],[c_3391,c_2690]) ).
tcf(c_8022,plain,
theorem(or(iPr_def_21,iPr_def_19)),
inference(superposition,[status(thm)],[c_3318,c_3765]) ).
tcf(c_8070,plain,
theorem(or(iPr_def_19,iPr_def_21)),
inference(superposition,[status(thm)],[c_8022,c_413]) ).
tcf(c_8428,plain,
( theorem(or(iPr_def_19,iPr_def_11))
| ~ theorem(or(iPr_def_10,iPr_def_14)) ),
inference(superposition,[status(thm)],[c_3964,c_66]) ).
tcf(c_9143,plain,
( theorem(or(not(or(iPr_def_24,iPr_def_18)),iPr_def_25))
| ~ theorem(or(iPr_def_19,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_4108,c_66]) ).
tcf(c_10319,plain,
theorem(or(iPr_def_18,iPr_def_20)),
inference(superposition,[status(thm)],[c_3309,c_4196]) ).
tcf(c_12591,plain,
theorem(or(iPr_def_19,iPr_def_22)),
inference(superposition,[status(thm)],[c_8070,c_4426]) ).
tcf(c_13842,plain,
( theorem(iPr_def_25)
| ~ theorem(or(iPr_def_24,iPr_def_18))
| ~ theorem(or(iPr_def_19,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_9143,c_66]) ).
tcf(c_14861,plain,
theorem(or(iPr_def_12,or(not(or(iPr_def_22,iPr_def_22)),iPr_def_21))),
inference(superposition,[status(thm)],[c_156,c_2811]) ).
tcf(c_19347,plain,
! [X0: $i] :
( theorem(or(not(or(iPr_def_12,or(not(X0),iPr_def_21))),iPr_def_22))
| ~ theorem(X0) ),
inference(superposition,[status(thm)],[c_2850,c_66]) ).
tcf(c_22488,plain,
! [X0: $i] :
( theorem(iPr_def_22)
| ~ theorem(X0)
| ~ theorem(or(iPr_def_12,or(not(X0),iPr_def_21))) ),
inference(superposition,[status(thm)],[c_19347,c_66]) ).
tcf(c_22838,plain,
! [X0: $i,X1: $i] :
( theorem(or(X0,X1))
| ~ theorem(or(iPr_def_10,X1))
| ~ theorem(or(X0,p)) ),
inference(superposition,[status(thm)],[c_3188,c_66]) ).
tcf(c_26118,plain,
( theorem(iPr_def_22)
| ~ theorem(or(iPr_def_22,iPr_def_22)) ),
inference(superposition,[status(thm)],[c_14861,c_22488]) ).
tcf(c_30055,plain,
! [X0: $i,X1: $i] :
( theorem(or(X0,X1))
| ~ theorem(or(iPr_def_19,X1))
| ~ theorem(or(X0,iPr_def_18)) ),
inference(superposition,[status(thm)],[c_4110,c_66]) ).
tcf(c_30103,plain,
! [X0: $i,X1: $i] :
( theorem(or(X0,X1))
| ~ theorem(or(iPr_def_21,X1))
| ~ theorem(or(X0,iPr_def_20)) ),
inference(superposition,[status(thm)],[c_4380,c_66]) ).
tcf(c_30609,plain,
! [X0: $i] :
( theorem(or(iPr_def_18,X0))
| ~ theorem(or(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_3290,c_22838]) ).
tcf(c_35487,plain,
! [X0: $i] :
( theorem(or(iPr_def_13,X0))
| ~ theorem(or(iPr_def_19,X0)) ),
inference(superposition,[status(thm)],[c_357,c_30055]) ).
tcf(c_36100,plain,
! [X0: $i] :
( theorem(or(iPr_def_18,X0))
| ~ theorem(or(iPr_def_21,X0)) ),
inference(superposition,[status(thm)],[c_10319,c_30103]) ).
tcf(c_54929,plain,
theorem(or(iPr_def_13,iPr_def_21)),
inference(superposition,[status(thm)],[c_8070,c_35487]) ).
tcf(c_55015,plain,
theorem(or(iPr_def_10,iPr_def_22)),
inference(backward_subsumption_resolution,[status(thm)],[c_5100,c_54929]) ).
tcf(c_55191,plain,
theorem(or(iPr_def_18,iPr_def_22)),
inference(superposition,[status(thm)],[c_55015,c_30609]) ).
tcf(c_55200,plain,
theorem(or(iPr_def_22,iPr_def_18)),
inference(superposition,[status(thm)],[c_55191,c_413]) ).
tcf(c_55206,plain,
! [X0: $i] :
( theorem(or(iPr_def_22,X0))
| ~ theorem(or(iPr_def_19,X0)) ),
inference(superposition,[status(thm)],[c_55200,c_30055]) ).
tcf(c_59026,plain,
theorem(or(iPr_def_18,iPr_def_24)),
inference(superposition,[status(thm)],[c_3438,c_36100]) ).
tcf(c_59143,plain,
theorem(or(iPr_def_24,iPr_def_18)),
inference(superposition,[status(thm)],[c_59026,c_413]) ).
tcf(c_92347,plain,
theorem(or(iPr_def_22,iPr_def_22)),
inference(superposition,[status(thm)],[c_12591,c_55206]) ).
tcf(c_372425,plain,
! [X0: $i] : theorem(or(iPr_def_10,or(X0,p))),
inference(superposition,[status(thm)],[c_144,c_101]) ).
tcf(c_372483,plain,
! [X0: $i] : theorem(or(not(or(X0,iPr_def_11)),or(iPr_def_10,or(X0,q)))),
inference(superposition,[status(thm)],[c_145,c_111]) ).
tcf(c_372491,plain,
! [X0: $i] : theorem(or(not(or(iPr_def_10,or(X0,q))),or(X0,iPr_def_11))),
inference(superposition,[status(thm)],[c_145,c_111]) ).
tcf(c_372542,plain,
! [X0: $i,X1: $i,X2: $i] :
( theorem(or(not(or(X2,X0)),or(X2,X1)))
| ~ theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_116,c_66]) ).
tcf(c_372889,plain,
theorem(or(not(or(p,iPr_def_11)),or(iPr_def_10,iPr_def_14))),
inference(superposition,[status(thm)],[c_148,c_372483]) ).
tcf(c_373035,plain,
! [X0: $i] :
( theorem(or(X0,iPr_def_11))
| ~ theorem(or(iPr_def_10,or(X0,q))) ),
inference(superposition,[status(thm)],[c_372491,c_66]) ).
tcf(c_373844,plain,
! [X0: $i,X1: $i,X2: $i] :
( theorem(or(X2,X1))
| ~ theorem(or(X2,X0))
| ~ theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_372542,c_66]) ).
tcf(c_374079,plain,
( theorem(or(iPr_def_10,iPr_def_14))
| ~ theorem(or(p,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_372889,c_66]) ).
tcf(c_376035,plain,
! [X0: $i,X1: $i,X2: $i] :
( theorem(or(X0,or(X2,X1)))
| ~ theorem(or(X0,or(X1,X2))) ),
inference(superposition,[status(thm)],[c_106,c_373844]) ).
tcf(c_377147,plain,
~ theorem(or(p,iPr_def_11)),
inference(global_subsumption_just,[status(thm)],[c_374079,c_1986,c_4953,c_8428,c_13842,c_26118,c_59143,c_92347]) ).
tcf(c_393078,plain,
! [X0: $i] : theorem(or(iPr_def_10,or(p,X0))),
inference(superposition,[status(thm)],[c_372425,c_376035]) ).
tcf(c_396551,plain,
theorem(or(p,iPr_def_11)),
inference(superposition,[status(thm)],[c_393078,c_373035]) ).
tcf(c_396554,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_396551,c_377147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL304-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 22:48:09 UTC 2026
% 0.15/0.36 % CPUTime :
% 0.15/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/0.40 Running first-order theorem proving
% 0.15/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42
% 0.15/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.42
% 0.15/0.42 % Detected problem language: tptp
% 0.15/0.43 % Proving...
% 174.10/28.03 % SZS status Started for theBenchmark.p
% 174.10/28.03 % SZS status Unsatisfiable for theBenchmark.p
% 174.10/28.03
% 174.10/28.03 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 174.10/28.03
% 174.10/28.03 % ------ iProver source info
% 174.10/28.03
% 174.10/28.03 % git: date: 2026-07-19 20:42:38 +0200
% 174.10/28.03 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 174.10/28.03 % git: non_committed_changes: false
% 174.10/28.03
% 174.10/28.03 % ------ Parsing...% successful
% 174.10/28.03
% 174.10/28.03
% 174.10/28.03 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 174.10/28.03
% 174.10/28.03 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 174.10/28.03
% 174.10/28.03 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 174.10/28.03
% 174.10/28.03 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 174.10/28.03 % ------ Proving...
% 174.10/28.03 % ------ Problem Properties
% 174.10/28.03
% 174.10/28.03 %
% 174.10/28.03 % clauses 26
% 174.10/28.03 % conjectures 1
% 174.10/28.03 % EPR 1
% 174.10/28.03 % Horn 26
% 174.10/28.03 % unary 25
% 174.10/28.03 % binary 0
% 174.10/28.03 % lits 28
% 174.10/28.03 % lits eq 19
% 174.10/28.03 % fd_pure 0
% 174.10/28.03 % fd_pseudo 0
% 174.10/28.03 % fd_cond 0
% 174.10/28.03 % fd_pseudo_cond 0
% 174.10/28.03 % AC symbols 0
% 174.10/28.03
% 174.10/28.03 % ------ Schedule dynamic 5 is on
% 174.10/28.03
% 174.10/28.03 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 174.10/28.03
% 174.10/28.03
% 174.10/28.03 % ------
% 174.10/28.03 % Current options:
% 174.10/28.03 % ------
% 174.10/28.03
% 174.10/28.03
% 174.10/28.03 %
% 174.10/28.03
% 174.10/28.03 % ------ Proving...
% 174.10/28.03 % Proof_search_loop: time out after: 9339 full_loop iterations
% 174.10/28.03
% 174.10/28.03 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 174.10/28.03
% 174.10/28.03
% 174.10/28.03 % ------
% 174.10/28.03 % Current options:
% 174.10/28.03 % ------
% 174.10/28.03
% 174.10/28.03
% 174.10/28.03 %
% 174.10/28.03
% 174.10/28.03 % ------ Proving...
% 174.10/28.03 % Proof_search_loop: time out after: 13032 full_loop iterations
% 174.10/28.03
% 174.10/28.03 % ------ Option_1: Negative Selections Time Limit: 35.
% 174.10/28.03
% 174.10/28.03
% 174.10/28.03 % ------
% 174.10/28.03 % Current options:
% 174.10/28.03 % ------
% 174.10/28.03
% 174.10/28.03
% 174.10/28.03 %
% 174.10/28.03
% 174.10/28.03 % ------ Proving...
% 174.10/28.03 %
% 174.10/28.03
% 174.10/28.03 % SZS status Unsatisfiable for theBenchmark.p
% 174.10/28.03
% 174.10/28.03 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 174.10/28.03
% 174.10/28.03
%------------------------------------------------------------------------------