%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL004-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n003.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:05:24 PM UTC 2026
% Result : Unsatisfiable 32.55s 8.62s
% Output : CNFRefutation 32.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 3
% Syntax : Number of formulae : 119 ( 77 unt; 0 def)
% Number of atoms : 164 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 92 ( 47 ~; 45 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 6 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 459 ( 0 sgn 459 !; 0 ?; 452 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(or(not(X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4] : is_a_theorem(or(not(or(not(or(not(X0),X1)),or(X2,or(X3,X4)))),or(not(or(not(X3),X0)),or(X2,or(X4,X0))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_CAMeredith) ).
fof(f3,negated_conjecture,
~ is_a_theorem(or(not(a),or(b,a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_3) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(or(not(X0),X1)),or(X2,or(X3,X4)))),or(not(or(not(X3),X0)),or(X2,or(X4,X0))))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_54,negated_conjecture,
~ is_a_theorem(or(not(a),or(b,a))),
inference(cnf_transformation,[],[f3]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X3),X0)),or(X2,or(X4,X0))))
| ~ is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(X3,X4)))) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),or(not(X1),X2))),or(not(or(not(X3),X1)),or(or(X4,X1),or(not(X1),X2))))),
inference(superposition,[status(thm)],[c_53,c_72]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X3),X1)),or(or(X4,X1),or(not(X1),X2))))
| ~ is_a_theorem(or(not(X0),or(not(X1),X2))) ),
inference(superposition,[status(thm)],[c_75,c_52]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(or(X0,X1)),X2)),or(not(or(not(X3),X1)),or(or(not(X1),X4),X2)))),
inference(superposition,[status(thm)],[c_75,c_72]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X3),X0)),or(X2,or(X4,X0))))
| ~ is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(X3,X4)))) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(or(not(X0),X1)),or(X2,X0))),or(not(or(not(X3),X0)),or(X4,or(X2,X0))))),
inference(superposition,[status(thm)],[c_86,c_160]) ).
tcf(c_290,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X3),X0)),or(X4,or(X2,X0))))
| ~ is_a_theorem(or(not(or(not(X0),X1)),or(X2,X0))) ),
inference(superposition,[status(thm)],[c_211,c_52]) ).
tcf(c_294,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),or(or(not(X1),X2),X1))),or(X3,or(not(or(not(X4),X1)),or(or(not(X1),X2),X1))))),
inference(superposition,[status(thm)],[c_86,c_290]) ).
tcf(c_295,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),or(not(X1),or(X2,X1)))),or(X3,or(not(or(not(X4),X1)),or(not(X1),or(X2,X1)))))),
inference(superposition,[status(thm)],[c_211,c_290]) ).
tcf(c_474,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X3),X1)),or(or(not(X1),X4),X2)))
| ~ is_a_theorem(or(not(or(X0,X1)),X2)) ),
inference(superposition,[status(thm)],[c_86,c_52]) ).
tcf(c_537,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(X3,or(not(or(not(X4),X1)),or(or(not(X1),X2),X1))))
| ~ is_a_theorem(or(not(X0),or(or(not(X1),X2),X1))) ),
inference(superposition,[status(thm)],[c_294,c_52]) ).
tcf(c_538,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(not(or(not(X0),X1))),X2)),or(X3,or(or(or(not(X1),X4),X1),X2)))),
inference(superposition,[status(thm)],[c_294,c_160]) ).
tcf(c_572,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(X3,or(not(or(not(X4),X1)),or(not(X1),or(X2,X1)))))
| ~ is_a_theorem(or(not(X0),or(not(X1),or(X2,X1)))) ),
inference(superposition,[status(thm)],[c_295,c_52]) ).
tcf(c_638,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(X2,X1),or(not(X1),or(or(or(not(X3),X4),X3),X5))))),
inference(superposition,[status(thm)],[c_538,c_85]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X1),X2),or(X3,or(or(or(not(X4),X5),X4),X1))))),
inference(superposition,[status(thm)],[c_538,c_474]) ).
tcf(c_712,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(not(X0)),X1)),or(or(X2,X0),or(or(or(or(not(X3),X4),X3),X5),X1)))),
inference(superposition,[status(thm)],[c_638,c_160]) ).
tcf(c_737,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X2),X3),or(or(or(or(not(X4),X5),X4),X2),X1)))),
inference(superposition,[status(thm)],[c_639,c_160]) ).
tcf(c_1912,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X3),X0)),or(X4,or(X2,X0))))
| ~ is_a_theorem(or(not(or(not(X0),X1)),or(X2,X0))) ),
inference(superposition,[status(thm)],[c_211,c_52]) ).
tcf(c_1982,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(or(or(or(not(X0),X1),X0),X2)),not(X3))),or(or(X4,X3),or(X5,not(X3))))),
inference(superposition,[status(thm)],[c_712,c_160]) ).
tcf(c_1983,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(or(or(or(not(X0),X1),X0),X2)),X3)),or(or(not(X2),X4),or(X5,X3)))),
inference(superposition,[status(thm)],[c_737,c_160]) ).
tcf(c_2153,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(not(or(not(X1),or(X2,X3))),or(or(not(or(X2,X3)),X4),or(X2,X3))))),
inference(superposition,[status(thm)],[c_1983,c_537]) ).
tcf(c_2187,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X1),or(X2,X3))),or(or(not(or(X2,X3)),X4),or(X2,X3))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_2153,c_52]) ).
tcf(c_2249,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(or(not(or(X1,X2)),X3),or(X1,X2)))),
inference(superposition,[status(thm)],[c_1982,c_2187]) ).
tcf(c_2273,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(not(or(X0,X2)),X3),or(X2,X1)))),
inference(superposition,[status(thm)],[c_2249,c_160]) ).
tcf(c_2276,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(X3,or(or(not(or(X1,X2)),X4),or(X1,X2))))),
inference(superposition,[status(thm)],[c_2249,c_1912]) ).
tcf(c_2291,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(not(or(X1,X0)),X2),or(X3,X1)))),
inference(superposition,[status(thm)],[c_2273,c_160]) ).
tcf(c_2310,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(not(or(X2,X1)),X3),or(X2,X1)))),
inference(superposition,[status(thm)],[c_2291,c_160]) ).
tcf(c_2533,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(or(not(or(X0,X1)),X2)),X3)),or(X4,or(or(X0,X1),X3)))),
inference(superposition,[status(thm)],[c_2276,c_160]) ).
tcf(c_2651,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(not(X2),or(or(X3,X4),X2))))),
inference(superposition,[status(thm)],[c_2533,c_572]) ).
tcf(c_2679,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X1),X2)),or(not(X2),or(or(X3,X4),X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_2651,c_52]) ).
tcf(c_2731,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X1),or(or(X2,X3),X1)))),
inference(superposition,[status(thm)],[c_2310,c_2679]) ).
tcf(c_2746,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(X1),or(or(X2,X3),X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_2731,c_52]) ).
tcf(c_2782,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(X0,or(or(X1,X2),X3))),or(or(X4,X5),or(X0,or(or(X1,X2),X3))))),
inference(superposition,[status(thm)],[c_2533,c_2746]) ).
tcf(c_5220,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(not(or(not(X0),X1))),X2)),or(X3,or(or(or(not(X1),X4),X1),X2)))),
inference(superposition,[status(thm)],[c_294,c_160]) ).
tcf(c_5226,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(not(X0)),X0)),or(or(X1,X2),or(or(or(X3,X4),X5),X0)))),
inference(superposition,[status(thm)],[c_2782,c_160]) ).
tcf(c_5368,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(not(X2),or(or(or(not(X3),X4),X3),X2))))),
inference(superposition,[status(thm)],[c_5220,c_572]) ).
tcf(c_5385,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X1),X2)),or(not(X2),or(or(or(not(X3),X4),X3),X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_5368,c_52]) ).
tcf(c_5474,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X1),or(or(or(not(X2),X3),X2),X1)))),
inference(superposition,[status(thm)],[c_5226,c_5385]) ).
tcf(c_5589,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(or(or(not(X0),X1),X0)),X2)),or(not(X3),or(X3,X2)))),
inference(superposition,[status(thm)],[c_5474,c_160]) ).
tcf(c_5661,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(not(X2),or(X2,X2))))),
inference(superposition,[status(thm)],[c_5589,c_572]) ).
tcf(c_5676,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(or(not(X1),X2)),or(not(X2),or(X2,X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_5661,c_52]) ).
tcf(c_5723,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X1),or(X1,X1)))),
inference(superposition,[status(thm)],[c_5226,c_5676]) ).
tcf(c_5740,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X0),or(X0,X1)))),
inference(superposition,[status(thm)],[c_5723,c_160]) ).
tcf(c_5864,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(or(not(X0),X0)),or(not(X0),or(X1,X0)))),
inference(superposition,[status(thm)],[c_5740,c_160]) ).
tcf(c_5911,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(not(X2),or(X3,X2))))),
inference(superposition,[status(thm)],[c_5864,c_572]) ).
tcf(c_6017,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(or(not(X1),X2)),or(not(X2),or(X3,X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_5911,c_52]) ).
tcf(c_6073,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X1),or(X2,X1)))),
inference(superposition,[status(thm)],[c_5226,c_6017]) ).
tcf(c_6166,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(X2,X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_6073,c_52]) ).
tcf(c_6167,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X2),or(X2,X1)))),
inference(superposition,[status(thm)],[c_6073,c_160]) ).
tcf(c_6227,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X0),or(X2,X1)))),
inference(superposition,[status(thm)],[c_6167,c_160]) ).
tcf(c_7196,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(X3,or(not(X0),or(X1,X2))))),
inference(superposition,[status(thm)],[c_6227,c_6166]) ).
tcf(c_11233,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X3),X0)),or(X4,or(X2,X0))))
| ~ is_a_theorem(or(not(or(not(X0),X1)),or(X2,X0))) ),
inference(superposition,[status(thm)],[c_211,c_52]) ).
tcf(c_11466,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(not(X0)),X0)),or(X1,or(or(X2,X3),X0)))),
inference(superposition,[status(thm)],[c_7196,c_160]) ).
tcf(c_11512,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(or(X0,X1)),not(X2))),or(X3,or(X2,not(X2))))),
inference(superposition,[status(thm)],[c_11466,c_160]) ).
tcf(c_11574,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),or(X1,not(X1)))),or(X2,or(X3,or(X1,not(X1)))))),
inference(superposition,[status(thm)],[c_11512,c_11233]) ).
tcf(c_11774,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(or(X3,not(X3)),X1)))),
inference(superposition,[status(thm)],[c_11574,c_160]) ).
tcf(c_11802,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X2,or(or(X3,not(X3)),X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_11774,c_52]) ).
tcf(c_11803,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(or(X0,not(X0))),X1)),or(X2,or(X3,X1)))),
inference(superposition,[status(thm)],[c_11774,c_160]) ).
tcf(c_12021,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X2,or(X3,X1)))
| ~ is_a_theorem(or(not(or(X0,not(X0))),X1)) ),
inference(superposition,[status(thm)],[c_11803,c_52]) ).
tcf(c_12161,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(X1,or(X2,or(or(X3,not(X3)),not(not(X4))))))),
inference(superposition,[status(thm)],[c_11774,c_12021]) ).
tcf(c_12189,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(not(X2),or(X3,X2))))),
inference(superposition,[status(thm)],[c_11803,c_572]) ).
tcf(c_12197,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(X1,or(X2,or(or(X3,not(X3)),not(not(X4))))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_12161,c_52]) ).
tcf(c_12281,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(or(not(X1),X2)),or(not(X2),or(X3,X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_12189,c_52]) ).
tcf(c_12320,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(or(X2,not(X2)),not(not(X3)))))),
inference(superposition,[status(thm)],[c_11774,c_12197]) ).
tcf(c_12396,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X1),or(X2,X1)))),
inference(superposition,[status(thm)],[c_11774,c_12281]) ).
tcf(c_12429,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(or(X2,not(X2)),not(not(X3)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_12320,c_52]) ).
tcf(c_12470,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(X2,X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_12396,c_52]) ).
tcf(c_12471,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X2),or(X2,X1)))),
inference(superposition,[status(thm)],[c_12396,c_160]) ).
tcf(c_12474,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(X3,or(not(X2),or(X1,X2))))),
inference(superposition,[status(thm)],[c_12396,c_11233]) ).
tcf(c_12520,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X0),or(X2,X1)))),
inference(superposition,[status(thm)],[c_12471,c_160]) ).
tcf(c_12525,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(not(X2),or(X2,not(not(X3))))))),
inference(superposition,[status(thm)],[c_12471,c_12021]) ).
tcf(c_12644,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(or(X1,not(X1)),not(not(X2))))),
inference(superposition,[status(thm)],[c_11774,c_12429]) ).
tcf(c_12734,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X3,or(not(X2),or(X1,X2))))
| ~ is_a_theorem(or(not(X0),or(X1,X2))) ),
inference(superposition,[status(thm)],[c_12474,c_52]) ).
tcf(c_12964,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(not(or(X1,X2)),or(X3,or(X1,X2))))),
inference(superposition,[status(thm)],[c_11803,c_12734]) ).
tcf(c_13057,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X0),or(X2,X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_12520,c_52]) ).
tcf(c_13064,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(not(X2),or(X3,not(not(X2))))))),
inference(superposition,[status(thm)],[c_12520,c_12021]) ).
tcf(c_13074,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(not(X2),or(X2,not(not(X3))))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_12525,c_52]) ).
tcf(c_13102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(or(X1,X2)),or(X3,or(X1,X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_12964,c_52]) ).
tcf(c_13128,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_13057,c_52]) ).
tcf(c_13133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(not(or(not(X2),X0)),or(X3,or(X4,X0))))
| ~ is_a_theorem(or(not(or(not(X0),X1)),X0)) ),
inference(superposition,[status(thm)],[c_13057,c_11233]) ).
tcf(c_13156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(not(X2),or(X3,not(not(X2))))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13064,c_52]) ).
tcf(c_13182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X2,or(not(X3),or(X3,X1))))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_12471,c_13128]) ).
tcf(c_13261,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X1,not(not(X2)))))),
inference(superposition,[status(thm)],[c_12644,c_13074]) ).
tcf(c_13314,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(X0,X1)),or(X2,or(X0,X1)))),
inference(superposition,[status(thm)],[c_12644,c_13102]) ).
tcf(c_13367,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X2,not(not(X1)))))),
inference(superposition,[status(thm)],[c_12644,c_13156]) ).
tcf(c_13446,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(X1,not(not(X2)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13261,c_52]) ).
tcf(c_13473,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(not(X0)),X0)),or(X1,or(X2,X0)))),
inference(superposition,[status(thm)],[c_13314,c_160]) ).
tcf(c_13479,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(X2,or(X3,not(X3)))))),
inference(superposition,[status(thm)],[c_13314,c_12021]) ).
tcf(c_13495,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(X2,not(not(X1)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13367,c_52]) ).
tcf(c_13570,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(X2,or(X3,not(X3)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13479,c_52]) ).
tcf(c_13632,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,not(not(X1))))),
inference(superposition,[status(thm)],[c_12644,c_13446]) ).
tcf(c_13646,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(or(X1,not(X1)),or(X2,not(not(X3)))))),
inference(superposition,[status(thm)],[c_13632,c_11802]) ).
tcf(c_13764,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X1,not(not(X0))))),
inference(superposition,[status(thm)],[c_12644,c_13495]) ).
tcf(c_13821,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(X1,or(X2,not(X2))))),
inference(superposition,[status(thm)],[c_12644,c_13570]) ).
tcf(c_13869,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X1,or(X2,not(X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13821,c_52]) ).
tcf(c_13976,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,or(X1,not(X1)))),
inference(superposition,[status(thm)],[c_13764,c_13869]) ).
tcf(c_13990,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X1,not(X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13976,c_52]) ).
tcf(c_14062,plain,
! [X0: $i] : is_a_theorem(or(X0,not(X0))),
inference(superposition,[status(thm)],[c_13976,c_13990]) ).
tcf(c_14066,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(not(not(X0))),or(X1,not(not(X0))))),
inference(superposition,[status(thm)],[c_14062,c_12470]) ).
tcf(c_14519,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(not(X1),or(X1,or(X2,or(X3,X4)))))),
inference(superposition,[status(thm)],[c_11803,c_13182]) ).
tcf(c_14803,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(or(X1,not(X1)),or(X2,not(not(X3)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13646,c_52]) ).
tcf(c_14965,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(or(X0,not(X0)),or(X1,not(not(X2))))),
inference(superposition,[status(thm)],[c_14066,c_14803]) ).
tcf(c_15071,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),or(not(X1),or(X1,X2)))),or(X3,or(X4,or(not(X1),or(X1,X2)))))),
inference(superposition,[status(thm)],[c_12471,c_13133]) ).
tcf(c_15146,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(X3,or(X4,or(not(X1),or(X1,X2)))))
| ~ is_a_theorem(or(not(X0),or(not(X1),or(X1,X2)))) ),
inference(superposition,[status(thm)],[c_15071,c_52]) ).
tcf(c_15453,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(not(X2),or(X2,X3))))),
inference(superposition,[status(thm)],[c_13473,c_15146]) ).
tcf(c_15738,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(not(X2),or(X2,X3))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_15453,c_52]) ).
tcf(c_15841,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X1,X2)))),
inference(superposition,[status(thm)],[c_14519,c_15738]) ).
tcf(c_15861,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(X1,X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_15841,c_52]) ).
tcf(c_15962,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,X1))),
inference(superposition,[status(thm)],[c_14965,c_15861]) ).
tcf(c_15992,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X2,X1)))),
inference(superposition,[status(thm)],[c_15962,c_12734]) ).
tcf(c_16376,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(X2,X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_15992,c_52]) ).
tcf(c_16466,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X1,X0))),
inference(superposition,[status(thm)],[c_14965,c_16376]) ).
tcf(c_16469,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_54,c_16466]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL004-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.19/0.44 % Computer : n003.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Wed Sep 23 21:37:19 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.45 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.27/0.51 Running first-order theorem proving
% 0.27/0.51 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.27/0.53
% 0.27/0.53 % ======== iProver multi-core TPTP/SMT =========
% 0.27/0.53
% 0.27/0.53 % Detected problem language: tptp
% 0.27/0.55 % Proving...
% 32.55/8.62 % SZS status Started for theBenchmark.p
% 32.55/8.62 % SZS status Unsatisfiable for theBenchmark.p
% 32.55/8.62
% 32.55/8.62 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 32.55/8.62
% 32.55/8.62 % ------ iProver source info
% 32.55/8.62
% 32.55/8.62 % git: date: 2026-07-19 20:42:38 +0200
% 32.55/8.62 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 32.55/8.62 % git: non_committed_changes: false
% 32.55/8.62
% 32.55/8.62 % ------ Parsing...% successful
% 32.55/8.62
% 32.55/8.62
% 32.55/8.62 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 32.55/8.62
% 32.55/8.62 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 32.55/8.62
% 32.55/8.62 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 32.55/8.62 % ------ Proving...
% 32.55/8.62 % ------ Problem Properties
% 32.55/8.62
% 32.55/8.62 %
% 32.55/8.62 % clauses 3
% 32.55/8.62 % conjectures 1
% 32.55/8.62 % EPR 0
% 32.55/8.62 % Horn 3
% 32.55/8.62 % unary 2
% 32.55/8.62 % binary 0
% 32.55/8.62 % lits 5
% 32.55/8.62 % lits eq 0
% 32.55/8.62 % fd_pure 0
% 32.55/8.62 % fd_pseudo 0
% 32.55/8.62 % fd_cond 0
% 32.55/8.62 % fd_pseudo_cond 0
% 32.55/8.62 % AC symbols 0
% 32.55/8.62
% 32.55/8.62 % ------ Input Options Time Limit: Unbounded
% 32.55/8.62
% 32.55/8.62
% 32.55/8.62 % ------
% 32.55/8.62 % Current options:
% 32.55/8.62 % ------
% 32.55/8.62
% 32.55/8.62
% 32.55/8.62 %
% 32.55/8.62
% 32.55/8.62 % ------ Proving...
% 32.55/8.62 %
% 32.55/8.62
% 32.55/8.62 % SZS status Unsatisfiable for theBenchmark.p
% 32.55/8.62
% 32.55/8.62 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 32.55/8.62
% 32.55/8.62
%------------------------------------------------------------------------------