%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL003-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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 67.57s 11.37s
% Output : CNFRefutation 67.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 3
% Syntax : Number of formulae : 149 ( 98 unt; 0 def)
% Number of atoms : 202 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 109 ( 56 ~; 53 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 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 : 557 ( 0 sgn 557 !; 0 ?; 550 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(or(not(X0),X1)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',an_CAMeredith) ).
fof(f3,negated_conjecture,
~ is_a_theorem(or(not(or(a,b)),or(b,a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',an_2) ).
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(or(a,b)),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_6018,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_6118,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_6018]) ).
tcf(c_6192,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_6118,c_52]) ).
tcf(c_6193,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_6118,c_160]) ).
tcf(c_6255,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_6193,c_160]) ).
tcf(c_7352,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_6255,c_6192]) ).
tcf(c_7369,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(X2,X1),or(not(X1),or(X3,X4))))),
inference(superposition,[status(thm)],[c_6255,c_85]) ).
tcf(c_27577,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_27759,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_7352,c_160]) ).
tcf(c_27760,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(not(X0)),X1)),or(or(X2,X0),or(or(X3,X4),X1)))),
inference(superposition,[status(thm)],[c_7369,c_160]) ).
tcf(c_27798,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_27759,c_160]) ).
tcf(c_27851,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_27798,c_27577]) ).
tcf(c_28058,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(or(X0,X1)),not(X2))),or(or(X3,X2),or(X4,not(X2))))),
inference(superposition,[status(thm)],[c_27760,c_160]) ).
tcf(c_28114,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X2,or(X3,or(X1,not(X1)))))
| ~ is_a_theorem(or(not(X0),or(X1,not(X1)))) ),
inference(superposition,[status(thm)],[c_27851,c_52]) ).
tcf(c_28115,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_27851,c_160]) ).
tcf(c_28311,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_28115,c_160]) ).
tcf(c_28315,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),or(or(X1,not(X1)),X2))),or(X3,or(X4,or(or(X1,not(X1)),X2))))),
inference(superposition,[status(thm)],[c_28115,c_27577]) ).
tcf(c_28380,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_28311,c_52]) ).
tcf(c_28515,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_28115,c_28380]) ).
tcf(c_28516,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(X1,or(X2,or(X3,not(not(or(X4,not(X4))))))))),
inference(superposition,[status(thm)],[c_28311,c_28380]) ).
tcf(c_28568,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_28515,c_52]) ).
tcf(c_28587,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(X1,or(X2,or(X3,not(not(or(X4,not(X4))))))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_28516,c_52]) ).
tcf(c_28706,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_28115,c_28568]) ).
tcf(c_28747,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(X2,not(not(or(X3,not(X3)))))))),
inference(superposition,[status(thm)],[c_28115,c_28587]) ).
tcf(c_28885,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_28706,c_52]) ).
tcf(c_28905,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(X2,not(not(or(X3,not(X3)))))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_28747,c_52]) ).
tcf(c_28942,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_28115,c_28885]) ).
tcf(c_29053,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(X1,not(not(or(X2,not(X2))))))),
inference(superposition,[status(thm)],[c_28115,c_28905]) ).
tcf(c_29153,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X1,not(not(or(X2,not(X2))))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_29053,c_52]) ).
tcf(c_29192,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,not(not(or(X1,not(X1)))))),
inference(superposition,[status(thm)],[c_28115,c_29153]) ).
tcf(c_29225,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(not(not(or(X1,not(X1)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_29192,c_52]) ).
tcf(c_29260,plain,
! [X0: $i] : is_a_theorem(not(not(or(X0,not(X0))))),
inference(superposition,[status(thm)],[c_28115,c_29225]) ).
tcf(c_29353,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_28311,c_572]) ).
tcf(c_29373,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(or(or(X3,not(X3)),X4),X1)))),
inference(superposition,[status(thm)],[c_28315,c_160]) ).
tcf(c_29377,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(not(or(not(X0),or(X1,or(or(X2,not(X2)),X3)))),or(X4,or(X5,or(X1,or(or(X2,not(X2)),X3)))))),
inference(superposition,[status(thm)],[c_28315,c_27577]) ).
tcf(c_29407,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(X2,or(or(or(X3,not(X3)),X4),X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_29373,c_52]) ).
tcf(c_29428,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_29353,c_52]) ).
tcf(c_29467,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_28058,c_29428]) ).
tcf(c_29505,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_29467,c_52]) ).
tcf(c_29506,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_29467,c_160]) ).
tcf(c_29567,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_29506,c_160]) ).
tcf(c_29571,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(X3,or(not(X1),or(X1,X2))))),
inference(superposition,[status(thm)],[c_29506,c_27577]) ).
tcf(c_29573,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_29506,c_28380]) ).
tcf(c_29831,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X3,or(not(X1),or(X1,X2))))
| ~ is_a_theorem(or(not(X0),or(X1,X2))) ),
inference(superposition,[status(thm)],[c_29571,c_52]) ).
tcf(c_29858,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_29567,c_28380]) ).
tcf(c_29870,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_29573,c_52]) ).
tcf(c_29955,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_29858,c_52]) ).
tcf(c_30080,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_28942,c_29870]) ).
tcf(c_30209,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_28942,c_29955]) ).
tcf(c_30338,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_30080,c_52]) ).
tcf(c_30388,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(X2),or(not(not(X2)),X1)))),
inference(superposition,[status(thm)],[c_30209,c_160]) ).
tcf(c_30452,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,not(not(X1))))),
inference(superposition,[status(thm)],[c_28942,c_30338]) ).
tcf(c_30492,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(X1,or(not(X2),not(not(X2)))))),
inference(superposition,[status(thm)],[c_30452,c_28114]) ).
tcf(c_30882,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X1,or(not(X2),not(not(X2)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_30492,c_52]) ).
tcf(c_31004,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,or(not(X1),not(not(X1))))),
inference(superposition,[status(thm)],[c_29377,c_30882]) ).
tcf(c_31123,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(not(X1),or(X1,or(X2,X3))))),
inference(superposition,[status(thm)],[c_28311,c_29831]) ).
tcf(c_31305,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(not(X1),not(not(X1))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_31004,c_52]) ).
tcf(c_31405,plain,
! [X0: $i] : is_a_theorem(or(not(X0),not(not(X0)))),
inference(superposition,[status(thm)],[c_31004,c_31305]) ).
tcf(c_31409,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(or(or(X1,not(X1)),X2),not(not(X3))))),
inference(superposition,[status(thm)],[c_31405,c_29407]) ).
tcf(c_31447,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(X1),or(X1,or(X2,X3))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_31123,c_52]) ).
tcf(c_31595,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(X0),or(X0,or(X1,X2)))),
inference(superposition,[status(thm)],[c_31004,c_31447]) ).
tcf(c_31806,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X0,or(X1,X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_31595,c_52]) ).
tcf(c_31849,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(not(X2),or(X2,X3))))
| ~ is_a_theorem(not(X0)) ),
inference(superposition,[status(thm)],[c_31806,c_29831]) ).
tcf(c_33197,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X1,X2)))),
inference(superposition,[status(thm)],[c_29260,c_31849]) ).
tcf(c_33213,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_33197,c_52]) ).
tcf(c_33225,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_33197,c_28380]) ).
tcf(c_33325,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,X1))),
inference(superposition,[status(thm)],[c_31409,c_33213]) ).
tcf(c_33333,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_33325,c_29505]) ).
tcf(c_33342,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X0,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_33325,c_52]) ).
tcf(c_33370,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(X2,X1)))
| ~ is_a_theorem(not(X0)) ),
inference(superposition,[status(thm)],[c_33342,c_29505]) ).
tcf(c_33571,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(X1,or(X2,or(not(X3),or(X3,X4)))))),
inference(superposition,[status(thm)],[c_33225,c_28380]) ).
tcf(c_33588,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_33333,c_160]) ).
tcf(c_33620,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X1,X0))),
inference(superposition,[status(thm)],[c_29260,c_33370]) ).
tcf(c_35114,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(or(not(X3),or(X3,X4)),X1)))),
inference(superposition,[status(thm)],[c_33571,c_160]) ).
tcf(c_35137,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X1,or(X2,X0)))
| ~ is_a_theorem(or(not(not(X0)),X0)) ),
inference(superposition,[status(thm)],[c_33588,c_52]) ).
tcf(c_37456,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X2),or(not(not(X2)),X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_30388,c_52]) ).
tcf(c_37826,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(X1),or(not(not(X1)),X2)))
| ~ is_a_theorem(not(X0)) ),
inference(superposition,[status(thm)],[c_33342,c_37456]) ).
tcf(c_37827,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(X0),or(not(not(X0)),or(X1,X2)))),
inference(superposition,[status(thm)],[c_33620,c_37456]) ).
tcf(c_37945,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(not(or(not(X1),X2))),or(X3,X1)))),
inference(superposition,[status(thm)],[c_37827,c_160]) ).
tcf(c_38050,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(not(not(X0)),X1))),
inference(superposition,[status(thm)],[c_29260,c_37826]) ).
tcf(c_38078,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(not(not(or(X2,not(X2)))),X3)))),
inference(superposition,[status(thm)],[c_38050,c_28380]) ).
tcf(c_38487,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(not(not(or(X2,not(X2)))),X3)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_38078,c_52]) ).
tcf(c_38688,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(not(or(X1,not(X1)))),X2))),
inference(superposition,[status(thm)],[c_38050,c_38487]) ).
tcf(c_38701,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(not(or(X1,not(X1)))),X2))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_38688,c_52]) ).
tcf(c_38870,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(not(or(X0,not(X0)))),X1)),
inference(superposition,[status(thm)],[c_38050,c_38701]) ).
tcf(c_50502,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(X2,or(or(not(X3),or(X3,X4)),X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_35114,c_52]) ).
tcf(c_52302,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(or(not(X1),or(X1,X2)),X3))),
inference(superposition,[status(thm)],[c_38870,c_50502]) ).
tcf(c_58214,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(not(or(not(X1),X2))),or(X3,X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_37945,c_52]) ).
tcf(c_58911,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(not(or(not(X0),X1))),or(X2,X0))),
inference(superposition,[status(thm)],[c_38870,c_58214]) ).
tcf(c_59018,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(X1,or(not(X2),X2)))),
inference(superposition,[status(thm)],[c_58911,c_35137]) ).
tcf(c_59028,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X1,or(not(X2),X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_59018,c_52]) ).
tcf(c_59319,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,or(not(X1),X1))),
inference(superposition,[status(thm)],[c_52302,c_59028]) ).
tcf(c_59484,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(not(X1),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_59319,c_52]) ).
tcf(c_59498,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(not(or(X0,X2)),or(X2,X1)))),
inference(superposition,[status(thm)],[c_59319,c_160]) ).
tcf(c_59846,plain,
! [X0: $i] : is_a_theorem(or(not(X0),X0)),
inference(superposition,[status(thm)],[c_52302,c_59484]) ).
tcf(c_61044,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(or(X0,X2)),or(X2,X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_59498,c_52]) ).
tcf(c_63913,plain,
~ is_a_theorem(or(not(a),a)),
inference(superposition,[status(thm)],[c_61044,c_54]) ).
tcf(c_63928,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_63913,c_59846]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL003-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 21:38:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/0.41 Running first-order theorem proving
% 0.15/0.41 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...
% 67.57/11.37 % SZS status Started for theBenchmark.p
% 67.57/11.37 % SZS status Unsatisfiable for theBenchmark.p
% 67.57/11.37
% 67.57/11.37 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 67.57/11.37
% 67.57/11.37 % ------ iProver source info
% 67.57/11.37
% 67.57/11.37 % git: date: 2026-07-19 20:42:38 +0200
% 67.57/11.37 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 67.57/11.37 % git: non_committed_changes: false
% 67.57/11.37
% 67.57/11.37 % ------ Parsing...% successful
% 67.57/11.37
% 67.57/11.37
% 67.57/11.37 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 67.57/11.37
% 67.57/11.37 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 67.57/11.37
% 67.57/11.37 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 67.57/11.37 % ------ Proving...
% 67.57/11.37 % ------ Problem Properties
% 67.57/11.37
% 67.57/11.37 %
% 67.57/11.37 % clauses 3
% 67.57/11.37 % conjectures 1
% 67.57/11.37 % EPR 0
% 67.57/11.37 % Horn 3
% 67.57/11.37 % unary 2
% 67.57/11.37 % binary 0
% 67.57/11.37 % lits 5
% 67.57/11.37 % lits eq 0
% 67.57/11.37 % fd_pure 0
% 67.57/11.37 % fd_pseudo 0
% 67.57/11.37 % fd_cond 0
% 67.57/11.37 % fd_pseudo_cond 0
% 67.57/11.37 % AC symbols 0
% 67.57/11.37
% 67.57/11.37 % ------ Input Options Time Limit: Unbounded
% 67.57/11.37
% 67.57/11.37
% 67.57/11.37 % ------
% 67.57/11.37 % Current options:
% 67.57/11.37 % ------
% 67.57/11.37
% 67.57/11.37
% 67.57/11.37 %
% 67.57/11.37
% 67.57/11.37 % ------ Proving...
% 67.57/11.37 %
% 67.57/11.37
% 67.57/11.37 % SZS status Unsatisfiable for theBenchmark.p
% 67.57/11.37
% 67.57/11.37 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 67.57/11.38
% 67.57/11.38
%------------------------------------------------------------------------------