%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL516+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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:49 PM UTC 2026
% Result : Theorem 112.56s 16.63s
% Output : CNFRefutation 112.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 16
% Syntax : Number of formulae : 177 ( 76 unt; 0 def)
% Number of atoms : 306 ( 18 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 245 ( 116 ~; 112 |; 2 &)
% ( 5 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 9 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 283 ( 0 sgn 281 !; 2 ?; 225 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( modus_ponens
<=> ! [X0,X1] :
( ( is_a_theorem(implies(X0,X1))
& is_a_theorem(X0) )
=> is_a_theorem(X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax',modus_ponens) ).
fof(f16,axiom,
( kn1
<=> ! [X0] : is_a_theorem(implies(X0,and(X0,X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax',kn1) ).
fof(f17,axiom,
( kn2
<=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax',kn2) ).
fof(f18,axiom,
( kn3
<=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax',kn3) ).
fof(f20,axiom,
( cn2
<=> ! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax',cn2) ).
fof(f27,axiom,
( op_or
=> ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+1.ax',op_or) ).
fof(f29,axiom,
( op_implies_and
=> ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+1.ax',op_implies_and) ).
fof(f31,axiom,
( op_equiv
=> ! [X0,X1] : equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+1.ax',op_equiv) ).
fof(f33,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+5.ax',rosser_op_implies_and) ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+5.ax',rosser_modus_ponens) ).
fof(f36,axiom,
kn1,
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+5.ax',rosser_kn1) ).
fof(f37,axiom,
kn2,
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+5.ax',rosser_kn2) ).
fof(f38,axiom,
kn3,
file('/export/starexec/sandbox/benchmark/Axioms/LCL006+5.ax',rosser_kn3) ).
fof(f40,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',luka_op_or) ).
fof(f42,axiom,
op_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',luka_op_equiv) ).
fof(f43,conjecture,
cn2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',luka_cn2) ).
fof(f44,negated_conjecture,
~ cn2,
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f45,plain,
~ cn2,
inference(flattening,[],[f44]) ).
fof(f46,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1)))
=> cn2 ),
inference(unused_predicate_definition_removal,[],[f20]) ).
fof(f47,plain,
( kn3
=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
inference(unused_predicate_definition_removal,[],[f18]) ).
fof(f48,plain,
( kn2
=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) ),
inference(unused_predicate_definition_removal,[],[f17]) ).
fof(f49,plain,
( kn1
=> ! [X0] : is_a_theorem(implies(X0,and(X0,X0))) ),
inference(unused_predicate_definition_removal,[],[f16]) ).
fof(f51,plain,
( modus_ponens
=> ! [X0,X1] :
( ( is_a_theorem(implies(X0,X1))
& is_a_theorem(X0) )
=> is_a_theorem(X1) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f55,plain,
( ~ modus_ponens
| ! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f56,plain,
( ~ modus_ponens
| ! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ) ),
inference(flattening,[],[f55]) ).
fof(f58,plain,
( ~ kn1
| ! [X0] : is_a_theorem(implies(X0,and(X0,X0))) ),
inference(ennf_transformation,[],[f49]) ).
fof(f59,plain,
( ~ kn2
| ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) ),
inference(ennf_transformation,[],[f48]) ).
fof(f60,plain,
( ~ kn3
| ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
inference(ennf_transformation,[],[f47]) ).
fof(f61,plain,
( ? [X0,X1] : ~ is_a_theorem(implies(X0,implies(not(X0),X1)))
| cn2 ),
inference(ennf_transformation,[],[f46]) ).
fof(f62,plain,
( ~ op_or
| ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(ennf_transformation,[],[f27]) ).
fof(f63,plain,
( ~ op_implies_and
| ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))) ),
inference(ennf_transformation,[],[f29]) ).
fof(f64,plain,
( ~ op_equiv
| ! [X0,X1] : equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
inference(ennf_transformation,[],[f31]) ).
fof(f65,plain,
( ~ is_a_theorem(implies(sK0,implies(not(sK0),sK1)))
| cn2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f61]) ).
fof(f66,plain,
! [X0,X1] :
( ~ modus_ponens
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
inference(cnf_transformation,[],[f56]) ).
fof(f68,plain,
! [X0] :
( ~ kn1
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(cnf_transformation,[],[f58]) ).
fof(f69,plain,
! [X0,X1] :
( ~ kn2
| is_a_theorem(implies(and(X0,X1),X0)) ),
inference(cnf_transformation,[],[f59]) ).
fof(f70,plain,
! [X2,X0,X1] :
( ~ kn3
| is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
inference(cnf_transformation,[],[f60]) ).
fof(f71,plain,
( ~ is_a_theorem(implies(sK0,implies(not(sK0),sK1)))
| cn2 ),
inference(cnf_transformation,[],[f65]) ).
fof(f72,plain,
! [X0,X1] :
( ~ op_or
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(cnf_transformation,[],[f62]) ).
fof(f73,plain,
! [X0,X1] :
( ~ op_implies_and
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(cnf_transformation,[],[f63]) ).
fof(f74,plain,
! [X0,X1] :
( ~ op_equiv
| equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
inference(cnf_transformation,[],[f64]) ).
fof(f76,plain,
op_implies_and,
inference(cnf_transformation,[],[f33]) ).
fof(f78,plain,
modus_ponens,
inference(cnf_transformation,[],[f35]) ).
fof(f79,plain,
kn1,
inference(cnf_transformation,[],[f36]) ).
fof(f80,plain,
kn2,
inference(cnf_transformation,[],[f37]) ).
fof(f81,plain,
kn3,
inference(cnf_transformation,[],[f38]) ).
fof(f83,plain,
op_or,
inference(cnf_transformation,[],[f40]) ).
fof(f84,plain,
op_equiv,
inference(cnf_transformation,[],[f42]) ).
fof(f85,plain,
~ cn2,
inference(cnf_transformation,[],[f45]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ modus_ponens
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_51,plain,
! [X0: $i] :
( is_a_theorem(implies(X0,and(X0,X0)))
| ~ kn1 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(implies(and(X0,X1),X0))
| ~ kn2 ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
| ~ kn3 ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_54,plain,
( cn2
| ~ is_a_theorem(implies(sK0,implies(not(sK0),sK1))) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( ( not(and(not(X0),not(X1))) = or(X0,X1) )
| ~ op_or ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( ( not(and(X0,not(X1))) = implies(X0,X1) )
| ~ op_implies_and ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( ( and(implies(X0,X1),implies(X1,X0)) = equiv(X0,X1) )
| ~ op_equiv ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_59,plain,
op_implies_and,
inference(cnf_transformation,[],[f76]) ).
tcf(c_61,plain,
modus_ponens,
inference(cnf_transformation,[],[f78]) ).
tcf(c_62,plain,
kn1,
inference(cnf_transformation,[],[f79]) ).
tcf(c_63,plain,
kn2,
inference(cnf_transformation,[],[f80]) ).
tcf(c_64,plain,
kn3,
inference(cnf_transformation,[],[f81]) ).
tcf(c_66,plain,
op_or,
inference(cnf_transformation,[],[f83]) ).
tcf(c_67,plain,
op_equiv,
inference(cnf_transformation,[],[f84]) ).
tcf(c_68,negated_conjecture,
~ cn2,
inference(cnf_transformation,[],[f85]) ).
tcf(c_69,plain,
( is_a_theorem(implies(and(sK0,sK0),sK0))
| ~ kn2 ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(and(X0,X1),X0)),
inference(global_subsumption_just,[status(thm)],[c_52,c_63,c_52]) ).
tcf(c_79,plain,
! [X0: $i] : is_a_theorem(implies(X0,and(X0,X0))),
inference(global_subsumption_just,[status(thm)],[c_51,c_62,c_51]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] : not(and(X0,not(X1))) = implies(X0,X1),
inference(global_subsumption_just,[status(thm)],[c_56,c_59,c_56]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_49,c_61,c_49]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(renaming,[status(thm)],[c_90]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] : not(and(not(X0),not(X1))) = or(X0,X1),
inference(global_subsumption_just,[status(thm)],[c_55,c_66,c_55]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i] : and(implies(X0,X1),implies(X1,X0)) = equiv(X0,X1),
inference(global_subsumption_just,[status(thm)],[c_57,c_67,c_57]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))),
inference(global_subsumption_just,[status(thm)],[c_53,c_64,c_53]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i] : implies(not(X0),X1) = or(X0,X1),
inference(demodulation,[status(thm)],[c_92,c_87]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(implies(X0,X1),or(and(X1,X2),not(and(X2,X0))))),
inference(demodulation,[status(thm)],[c_98,c_143]) ).
tcf(c_430,plain,
! [X0: $i] : is_a_theorem(or(X0,and(not(X0),not(X0)))),
inference(superposition,[status(thm)],[c_143,c_79]) ).
tcf(c_443,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(and(X0,not(X1)),and(implies(X0,X1),implies(X0,X1)))),
inference(superposition,[status(thm)],[c_87,c_430]) ).
tcf(c_444,plain,
! [X0: $i,X1: $i,X2: $i] : or(and(X0,not(X1)),X2) = implies(implies(X0,X1),X2),
inference(superposition,[status(thm)],[c_87,c_143]) ).
tcf(c_467,plain,
! [X0: $i,X1: $i] : and(implies(X0,not(X1)),or(X1,X0)) = equiv(X0,not(X1)),
inference(superposition,[status(thm)],[c_143,c_95]) ).
tcf(c_468,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,X0),equiv(X0,X0))),
inference(superposition,[status(thm)],[c_95,c_79]) ).
tcf(c_469,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(equiv(X0,X1),implies(X0,X1))),
inference(superposition,[status(thm)],[c_95,c_76]) ).
tcf(c_511,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(implies(not(X0),X1),or(and(X1,X2),implies(X2,X0)))),
inference(superposition,[status(thm)],[c_87,c_144]) ).
tcf(c_577,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(equiv(not(X0),X1),or(X0,X1))),
inference(superposition,[status(thm)],[c_143,c_469]) ).
tcf(c_641,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(implies(X0,X1),and(implies(X0,X1),implies(X0,X1)))),
inference(superposition,[status(thm)],[c_444,c_443]) ).
tcf(c_704,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(or(X0,X1),or(and(X1,X2),implies(X2,X0)))),
inference(superposition,[status(thm)],[c_143,c_511]) ).
tcf(c_971,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(and(X1,X2),not(and(X2,X0))))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(superposition,[status(thm)],[c_144,c_91]) ).
tcf(c_973,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(equiv(X0,X1)) ),
inference(superposition,[status(thm)],[c_469,c_91]) ).
tcf(c_976,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(and(implies(X0,X1),implies(X0,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(superposition,[status(thm)],[c_641,c_91]) ).
tcf(c_1190,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(or(X0,X1),or(and(X1,not(X2)),or(X2,X0)))),
inference(superposition,[status(thm)],[c_143,c_704]) ).
tcf(c_1191,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(and(X1,X2),implies(X2,X0)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_704,c_91]) ).
tcf(c_1459,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(and(X0,X1)) ),
inference(superposition,[status(thm)],[c_76,c_91]) ).
tcf(c_1540,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(and(or(X0,X1),or(X0,X1)))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_143,c_976]) ).
tcf(c_1545,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(or(X0,X1),implies(implies(X1,X2),or(X2,X0)))),
inference(superposition,[status(thm)],[c_444,c_1190]) ).
tcf(c_1633,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(implies(X1,X2),implies(not(X2),X0)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_444,c_1191]) ).
tcf(c_1735,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(or(X0,not(X1)),implies(or(X1,X2),or(X2,X0)))),
inference(superposition,[status(thm)],[c_143,c_1545]) ).
tcf(c_1737,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(implies(X1,X2),or(X2,X0)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_1545,c_91]) ).
tcf(c_1900,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(and(X1,X2),implies(X2,X0)))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_511,c_91]) ).
tcf(c_1906,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(or(X1,X2),or(X2,X0)))
| ~ is_a_theorem(or(X0,not(X1))) ),
inference(superposition,[status(thm)],[c_1735,c_91]) ).
tcf(c_2187,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(implies(X0,not(X1)))
| ~ is_a_theorem(equiv(X0,not(X1))) ),
inference(superposition,[status(thm)],[c_467,c_1459]) ).
tcf(c_2693,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(implies(X1,X2),not(and(not(X2),X0))))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(superposition,[status(thm)],[c_444,c_971]) ).
tcf(c_2826,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(and(X0,X1)) ),
inference(superposition,[status(thm)],[c_76,c_91]) ).
tcf(c_2831,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X1,X2))
| ~ is_a_theorem(or(X2,X0))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(superposition,[status(thm)],[c_1737,c_91]) ).
tcf(c_2833,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(not(X0))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_143,c_91]) ).
tcf(c_2912,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X0,X1))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_1540,c_2826]) ).
tcf(c_2957,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(and(X0,not(X1)),X2))
| ~ is_a_theorem(implies(implies(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_87,c_2912]) ).
tcf(c_3322,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(not(X1),X2))
| ~ is_a_theorem(or(X2,X0))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(superposition,[status(thm)],[c_1633,c_91]) ).
tcf(c_3575,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(and(X1,not(X2)),or(X2,X0)))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_143,c_1900]) ).
tcf(c_3576,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(X2,X0))
| ~ is_a_theorem(not(and(X1,X2)))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_1900,c_2833]) ).
tcf(c_3626,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X2,X0))
| ~ is_a_theorem(or(X1,X2))
| ~ is_a_theorem(or(X0,not(X1))) ),
inference(superposition,[status(thm)],[c_1906,c_91]) ).
tcf(c_4374,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(not(and(not(X2),X0)))
| ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(superposition,[status(thm)],[c_2693,c_91]) ).
tcf(c_5526,plain,
! [X0: $i] : is_a_theorem(or(X0,and(not(X0),not(X0)))),
inference(superposition,[status(thm)],[c_143,c_79]) ).
tcf(c_5551,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X1,X0))
| ~ is_a_theorem(or(X0,and(X1,X2))) ),
inference(superposition,[status(thm)],[c_76,c_2831]) ).
tcf(c_5571,plain,
! [X0: $i] :
( is_a_theorem(equiv(X0,X0))
| ~ is_a_theorem(implies(X0,X0)) ),
inference(superposition,[status(thm)],[c_468,c_91]) ).
tcf(c_5575,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(not(X0))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_143,c_91]) ).
tcf(c_5596,plain,
! [X0: $i] : is_a_theorem(or(not(X0),X0)),
inference(superposition,[status(thm)],[c_5526,c_5551]) ).
tcf(c_5749,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(implies(X0,X1),and(X0,not(X1)))),
inference(superposition,[status(thm)],[c_87,c_5596]) ).
tcf(c_5751,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,not(and(X0,X1)))),
inference(superposition,[status(thm)],[c_5596,c_5551]) ).
tcf(c_5855,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,implies(X0,X1))),
inference(superposition,[status(thm)],[c_87,c_5751]) ).
tcf(c_6026,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(not(X0)) ),
inference(superposition,[status(thm)],[c_5855,c_5575]) ).
tcf(c_6293,plain,
! [X0: $i] :
( is_a_theorem(equiv(X0,X0))
| ~ is_a_theorem(not(X0)) ),
inference(superposition,[status(thm)],[c_6026,c_5571]) ).
tcf(c_7148,plain,
! [X0: $i] :
( is_a_theorem(implies(X0,X0))
| ~ is_a_theorem(not(X0)) ),
inference(superposition,[status(thm)],[c_6293,c_973]) ).
tcf(c_7177,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X1,X0))
| ~ is_a_theorem(not(X1))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_7148,c_2831]) ).
tcf(c_7324,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(not(X1),X0))
| ~ is_a_theorem(or(X0,and(X1,X2))) ),
inference(superposition,[status(thm)],[c_76,c_3322]) ).
tcf(c_7685,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X1,not(not(X0))))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_5596,c_3626]) ).
tcf(c_7686,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X2,X0))
| ~ is_a_theorem(or(and(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_5751,c_3626]) ).
tcf(c_8260,plain,
! [X0: $i] :
( is_a_theorem(implies(not(X0),not(X0)))
| ~ is_a_theorem(not(not(X0))) ),
inference(superposition,[status(thm)],[c_6293,c_2187]) ).
tcf(c_8272,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(and(not(and(X0,X1)),not(and(X0,X1))),X0)),
inference(superposition,[status(thm)],[c_5526,c_7686]) ).
tcf(c_8275,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X2,X0))
| ~ is_a_theorem(implies(implies(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_2957,c_7686]) ).
tcf(c_8276,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(or(X2,X0),X1))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_3575,c_7686]) ).
tcf(c_8282,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(not(X0)),X1))
| ~ is_a_theorem(or(X0,and(X1,X2))) ),
inference(superposition,[status(thm)],[c_7685,c_7686]) ).
tcf(c_10562,plain,
! [X0: $i] :
( is_a_theorem(equiv(not(X0),not(X0)))
| ~ is_a_theorem(not(not(X0))) ),
inference(superposition,[status(thm)],[c_8260,c_5571]) ).
tcf(c_10983,plain,
! [X0: $i] : is_a_theorem(implies(not(not(X0)),X0)),
inference(superposition,[status(thm)],[c_5526,c_7324]) ).
tcf(c_10988,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(not(X0),implies(X0,X1))),
inference(superposition,[status(thm)],[c_5749,c_7324]) ).
tcf(c_11799,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(implies(not(X1),X0))
| ~ is_a_theorem(or(X0,not(not(X1)))) ),
inference(superposition,[status(thm)],[c_10983,c_3322]) ).
tcf(c_11808,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(not(implies(X1,X2)),X0))
| ~ is_a_theorem(or(X0,not(X1))) ),
inference(superposition,[status(thm)],[c_10988,c_3322]) ).
tcf(c_12001,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X2,not(X0)))
| ~ is_a_theorem(implies(or(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_143,c_8275]) ).
tcf(c_13182,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(implies(X1,not(X0)))
| ~ is_a_theorem(not(and(X0,X1))) ),
inference(superposition,[status(thm)],[c_10983,c_3576]) ).
tcf(c_14047,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(not(and(not(X1),X0)))
| ~ is_a_theorem(implies(and(X0,X0),X1)) ),
inference(superposition,[status(thm)],[c_79,c_4374]) ).
tcf(c_14084,plain,
( is_a_theorem(not(and(not(sK0),sK0)))
| ~ is_a_theorem(implies(and(sK0,sK0),sK0)) ),
inference(instantiation,[status(thm)],[c_14047]) ).
tcf(c_14716,plain,
! [X0: $i] : is_a_theorem(or(X0,and(not(X0),not(X0)))),
inference(superposition,[status(thm)],[c_143,c_79]) ).
tcf(c_14741,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X0,X1))
| ~ is_a_theorem(equiv(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_577,c_91]) ).
tcf(c_14781,plain,
! [X0: $i] :
( is_a_theorem(or(X0,not(X0)))
| ~ is_a_theorem(not(not(X0))) ),
inference(superposition,[status(thm)],[c_10562,c_14741]) ).
tcf(c_26915,plain,
! [X0: $i] :
( is_a_theorem(or(not(X0),X0))
| ~ is_a_theorem(not(not(X0))) ),
inference(superposition,[status(thm)],[c_14781,c_7177]) ).
tcf(c_32136,plain,
! [X0: $i] : is_a_theorem(or(not(not(X0)),not(X0))),
inference(superposition,[status(thm)],[c_14716,c_8282]) ).
tcf(c_32164,plain,
is_a_theorem(or(not(not(sK0)),not(sK0))),
inference(instantiation,[status(thm)],[c_32136]) ).
tcf(c_40415,plain,
! [X0: $i] :
( is_a_theorem(implies(sK0,implies(not(sK0),sK1)))
| ~ is_a_theorem(not(and(X0,sK0)))
| ~ is_a_theorem(implies(not(implies(not(sK0),sK1)),X0)) ),
inference(instantiation,[status(thm)],[c_3576]) ).
tcf(c_41335,plain,
! [X0: $i] :
( is_a_theorem(implies(sK0,implies(not(sK0),sK1)))
| ~ is_a_theorem(not(and(not(X0),sK0)))
| ~ is_a_theorem(implies(not(implies(not(sK0),sK1)),not(X0))) ),
inference(instantiation,[status(thm)],[c_40415]) ).
tcf(c_41336,plain,
( is_a_theorem(implies(sK0,implies(not(sK0),sK1)))
| ~ is_a_theorem(not(and(not(sK0),sK0)))
| ~ is_a_theorem(implies(not(implies(not(sK0),sK1)),not(sK0))) ),
inference(instantiation,[status(thm)],[c_41335]) ).
tcf(c_45719,plain,
! [X0: $i] :
( is_a_theorem(implies(not(implies(not(sK0),sK1)),not(X0)))
| ~ is_a_theorem(or(not(X0),not(not(sK0)))) ),
inference(instantiation,[status(thm)],[c_11808]) ).
tcf(c_45720,plain,
( is_a_theorem(implies(not(implies(not(sK0),sK1)),not(sK0)))
| ~ is_a_theorem(or(not(sK0),not(not(sK0)))) ),
inference(instantiation,[status(thm)],[c_45719]) ).
tcf(c_47428,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(not(sK0),not(X0)))
| ~ is_a_theorem(or(X1,not(sK0)))
| ~ is_a_theorem(or(not(X0),not(X1))) ),
inference(instantiation,[status(thm)],[c_3626]) ).
tcf(c_92303,plain,
! [X0: $i] : is_a_theorem(or(not(X0),X0)),
inference(global_subsumption_just,[status(thm)],[c_26915,c_5596]) ).
tcf(c_92655,plain,
! [X0: $i] : is_a_theorem(implies(not(X0),not(not(not(X0))))),
inference(superposition,[status(thm)],[c_92303,c_11799]) ).
tcf(c_92721,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(implies(X0,X1),not(not(implies(X0,X1))))),
inference(superposition,[status(thm)],[c_87,c_92655]) ).
tcf(c_92730,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(or(X0,X1),not(not(or(X0,X1))))),
inference(superposition,[status(thm)],[c_143,c_92721]) ).
tcf(c_92733,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(not(not(or(X0,X1))))
| ~ is_a_theorem(or(X0,X1)) ),
inference(superposition,[status(thm)],[c_92730,c_91]) ).
tcf(c_93078,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(implies(not(and(X0,X1)),and(X0,X1)),X0)),
inference(superposition,[status(thm)],[c_444,c_8272]) ).
tcf(c_93268,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(or(and(X0,X1),and(X0,X1)),X0)),
inference(superposition,[status(thm)],[c_143,c_93078]) ).
tcf(c_93277,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,not(and(X0,X1)))),
inference(superposition,[status(thm)],[c_93268,c_12001]) ).
tcf(c_93279,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,implies(X0,X1))),
inference(superposition,[status(thm)],[c_87,c_93277]) ).
tcf(c_93283,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,X1))),
inference(superposition,[status(thm)],[c_143,c_93279]) ).
tcf(c_93627,plain,
! [X0: $i] : is_a_theorem(not(and(not(X0),X0))),
inference(superposition,[status(thm)],[c_76,c_14047]) ).
tcf(c_93633,plain,
! [X0: $i,X1: $i] : is_a_theorem(not(and(implies(X0,X1),and(X0,not(X1))))),
inference(superposition,[status(thm)],[c_87,c_93627]) ).
tcf(c_93639,plain,
! [X0: $i,X1: $i] : is_a_theorem(not(and(or(X0,X1),and(not(X0),not(X1))))),
inference(superposition,[status(thm)],[c_143,c_93633]) ).
tcf(c_93724,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(and(not(X0),not(X1)),not(or(X0,X1)))),
inference(superposition,[status(thm)],[c_93639,c_13182]) ).
tcf(c_93752,plain,
! [X0: $i] : is_a_theorem(not(and(not(not(or(X0,X0))),not(X0)))),
inference(superposition,[status(thm)],[c_93724,c_14047]) ).
tcf(c_94351,plain,
! [X0: $i] : is_a_theorem(implies(not(not(or(X0,X0))),X0)),
inference(superposition,[status(thm)],[c_87,c_93752]) ).
tcf(c_94367,plain,
! [X0: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(not(not(or(X0,X0)))) ),
inference(superposition,[status(thm)],[c_94351,c_91]) ).
tcf(c_94443,plain,
! [X0: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(or(X0,X0)) ),
inference(superposition,[status(thm)],[c_92733,c_94367]) ).
tcf(c_94462,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X1,X0))
| ~ is_a_theorem(implies(not(X0),or(X1,X0))) ),
inference(superposition,[status(thm)],[c_8276,c_94443]) ).
tcf(c_96133,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X1,X0))
| ~ is_a_theorem(or(X0,or(X1,X0))) ),
inference(superposition,[status(thm)],[c_143,c_94462]) ).
tcf(c_96268,plain,
! [X0: $i] : is_a_theorem(or(X0,not(X0))),
inference(superposition,[status(thm)],[c_93283,c_96133]) ).
tcf(c_96303,plain,
is_a_theorem(or(sK0,not(sK0))),
inference(instantiation,[status(thm)],[c_96268]) ).
tcf(c_138295,plain,
! [X0: $i] :
( is_a_theorem(or(not(sK0),not(not(X0))))
| ~ is_a_theorem(or(X0,not(sK0)))
| ~ is_a_theorem(or(not(not(X0)),not(X0))) ),
inference(instantiation,[status(thm)],[c_47428]) ).
tcf(c_138296,plain,
( is_a_theorem(or(not(sK0),not(not(sK0))))
| ~ is_a_theorem(or(sK0,not(sK0)))
| ~ is_a_theorem(or(not(not(sK0)),not(sK0))) ),
inference(instantiation,[status(thm)],[c_138295]) ).
tcf(c_138297,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_138296,c_96303,c_45720,c_41336,c_32164,c_14084,c_54,c_69,c_68,c_63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL516+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Wed Sep 23 23:37:28 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.32 Running first-order theorem proving
% 0.04/0.32 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.33
% 0.04/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.04/0.33
% 0.04/0.33 % Detected problem language: tptp
% 0.07/0.33 % Proving...
% 112.56/16.63 % SZS status Started for theBenchmark.p
% 112.56/16.63 % SZS status Theorem for theBenchmark.p
% 112.56/16.63
% 112.56/16.63 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 112.56/16.63
% 112.56/16.63 % ------ iProver source info
% 112.56/16.63
% 112.56/16.63 % git: date: 2026-07-19 20:42:38 +0200
% 112.56/16.63 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 112.56/16.63 % git: non_committed_changes: false
% 112.56/16.63
% 112.56/16.63 % ------ Parsing...
% 112.56/16.63 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 112.56/16.63
% 112.56/16.63 % ------ Preprocessing... sup_sim: 2 sf_s rm: 10 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 112.56/16.63
% 112.56/16.63 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 112.56/16.63
% 112.56/16.63 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 112.56/16.63 % ------ Proving...
% 112.56/16.63 % ------ Problem Properties
% 112.56/16.63
% 112.56/16.63 %
% 112.56/16.63 % clauses 9
% 112.56/16.63 % conjectures 0
% 112.56/16.63 % EPR 0
% 112.56/16.63 % Horn 9
% 112.56/16.63 % unary 7
% 112.56/16.63 % binary 1
% 112.56/16.63 % lits 12
% 112.56/16.63 % lits eq 4
% 112.56/16.63 % fd_pure 0
% 112.56/16.63 % fd_pseudo 0
% 112.56/16.63 % fd_cond 0
% 112.56/16.63 % fd_pseudo_cond 1
% 112.56/16.63 % AC symbols 0
% 112.56/16.63
% 112.56/16.63 % ------ Input Options Time Limit: Unbounded
% 112.56/16.63
% 112.56/16.63
% 112.56/16.63 % ------
% 112.56/16.63 % Current options:
% 112.56/16.63 % ------
% 112.56/16.63
% 112.56/16.63
% 112.56/16.63 %
% 112.56/16.63
% 112.56/16.63 % ------ Proving...
% 112.56/16.63 %
% 112.56/16.63
% 112.56/16.63 % SZS status Theorem for theBenchmark.p
% 112.56/16.63
% 112.56/16.63 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 112.56/16.64
% 112.56/16.64
%------------------------------------------------------------------------------