%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL002-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 : n006.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:20 PM UTC 2026
% Result : Unsatisfiable 188.13s 54.02s
% Output : CNFRefutation 188.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 111
% Number of leaves : 3
% Syntax : Number of formulae : 234 ( 146 unt; 0 def)
% Number of atoms : 332 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 201 ( 103 ~; 98 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 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 : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 891 ( 0 sgn 891 !; 0 ?; 884 :)
% 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(or(not(b),c)),or(not(or(a,b)),or(a,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_1) ).
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(not(b),c)),or(not(or(a,b)),or(a,c)))),
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_573,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(not(X1),or(X4,X1)),X2)))),
inference(superposition,[status(thm)],[c_295,c_160]) ).
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_661,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(not(X4),or(X5,X4)),X1))))),
inference(superposition,[status(thm)],[c_573,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_829,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(not(X4),or(X5,X4)),X2),X1)))),
inference(superposition,[status(thm)],[c_661,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_11349,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_11576,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_11622,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_11576,c_160]) ).
tcf(c_11684,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_11622,c_11349]) ).
tcf(c_11881,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_11684,c_160]) ).
tcf(c_11909,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_11881,c_52]) ).
tcf(c_11910,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_11881,c_160]) ).
tcf(c_12128,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_11910,c_52]) ).
tcf(c_12268,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_11881,c_12128]) ).
tcf(c_12296,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_11910,c_572]) ).
tcf(c_12304,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_12268,c_52]) ).
tcf(c_12388,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_12296,c_52]) ).
tcf(c_12427,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_11881,c_12304]) ).
tcf(c_12503,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_11881,c_12388]) ).
tcf(c_12536,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_12427,c_52]) ).
tcf(c_12577,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_12503,c_52]) ).
tcf(c_12578,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_12503,c_160]) ).
tcf(c_12581,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_12503,c_11349]) ).
tcf(c_12627,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_12578,c_160]) ).
tcf(c_12752,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_11881,c_12536]) ).
tcf(c_12818,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_12581,c_52]) ).
tcf(c_13045,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_11910,c_12818]) ).
tcf(c_13118,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_12627,c_52]) ).
tcf(c_13122,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(X3,or(not(or(X1,X2)),or(X1,X2))))),
inference(superposition,[status(thm)],[c_12627,c_11349]) ).
tcf(c_13125,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_12627,c_12128]) ).
tcf(c_13163,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_13045,c_52]) ).
tcf(c_13189,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_13118,c_52]) ).
tcf(c_13194,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_13118,c_11349]) ).
tcf(c_13222,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( is_a_theorem(or(X2,or(or(not(X3),X4),or(or(or(not(X5),or(X6,X5)),X3),X1))))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_829,c_13189]) ).
tcf(c_13225,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_12578,c_13189]) ).
tcf(c_13357,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_12752,c_13163]) ).
tcf(c_13462,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_13357,c_160]) ).
tcf(c_13468,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_13357,c_12128]) ).
tcf(c_13535,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_13468,c_52]) ).
tcf(c_13738,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(X1,or(X2,not(X2))))),
inference(superposition,[status(thm)],[c_12752,c_13535]) ).
tcf(c_13833,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_13738,c_52]) ).
tcf(c_13904,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,or(X1,not(X1)))),
inference(superposition,[status(thm)],[c_13738,c_13833]) ).
tcf(c_13916,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X1,not(X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13904,c_52]) ).
tcf(c_13984,plain,
! [X0: $i] : is_a_theorem(or(X0,not(X0))),
inference(superposition,[status(thm)],[c_13738,c_13916]) ).
tcf(c_13989,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(not(not(X0))),or(X1,not(not(X0))))),
inference(superposition,[status(thm)],[c_13984,c_12577]) ).
tcf(c_14505,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_11910,c_13225]) ).
tcf(c_14661,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_13125,c_52]) ).
tcf(c_14985,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_13989,c_14661]) ).
tcf(c_15076,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X3,or(not(or(X1,X2)),or(X1,X2))))
| ~ is_a_theorem(or(not(X0),or(X1,X2))) ),
inference(superposition,[status(thm)],[c_13122,c_52]) ).
tcf(c_15163,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_12578,c_13194]) ).
tcf(c_15614,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_15163,c_52]) ).
tcf(c_15952,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_13462,c_15614]) ).
tcf(c_16085,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_15952,c_52]) ).
tcf(c_16317,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X1,X2)))),
inference(superposition,[status(thm)],[c_14505,c_16085]) ).
tcf(c_16340,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_16317,c_52]) ).
tcf(c_16441,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,X1))),
inference(superposition,[status(thm)],[c_14985,c_16340]) ).
tcf(c_16452,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(or(X1,not(X1)),or(X2,X3)))),
inference(superposition,[status(thm)],[c_16441,c_11909]) ).
tcf(c_16473,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(or(X1,X2)),or(X1,X2)))),
inference(superposition,[status(thm)],[c_16441,c_15076]) ).
tcf(c_17604,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(not(or(X1,X2)),or(X1,X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_16473,c_52]) ).
tcf(c_18176,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(or(X0,X1)),or(X0,X1))),
inference(superposition,[status(thm)],[c_16452,c_17604]) ).
tcf(c_19014,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : is_a_theorem(or(X0,or(or(not(X1),X2),or(or(or(not(X3),or(X4,X3)),X1),or(X5,X6))))),
inference(superposition,[status(thm)],[c_18176,c_13222]) ).
tcf(c_27948,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(or(X2,X1),or(not(X1),or(X3,X4))))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_7369,c_52]) ).
tcf(c_27955,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : is_a_theorem(or(or(X0,or(X1,or(not(X2),or(X3,X4)))),or(not(or(X1,or(not(X2),or(X3,X4)))),or(X5,X6)))),
inference(superposition,[status(thm)],[c_7352,c_27948]) ).
tcf(c_27979,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( is_a_theorem(or(or(not(X1),X2),or(or(or(not(X3),or(X4,X3)),X1),or(X5,X6))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_19014,c_52]) ).
tcf(c_28012,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(or(not(X0),X1),or(or(or(not(X2),or(X3,X2)),X0),or(X4,X5)))),
inference(superposition,[status(thm)],[c_27955,c_27979]) ).
tcf(c_28203,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_28353,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_28369,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_28353,c_160]) ).
tcf(c_28396,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_28369,c_28203]) ).
tcf(c_28540,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_28396,c_52]) ).
tcf(c_28541,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_28396,c_160]) ).
tcf(c_28560,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_28541,c_160]) ).
tcf(c_28792,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_28560,c_52]) ).
tcf(c_28798,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_28560,c_572]) ).
tcf(c_28901,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_28798,c_52]) ).
tcf(c_28944,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_28541,c_28901]) ).
tcf(c_28995,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_28944,c_160]) ).
tcf(c_29045,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_28995,c_160]) ).
tcf(c_29048,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_28995,c_28203]) ).
tcf(c_29051,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_28995,c_28792]) ).
tcf(c_29156,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_29045,c_28792]) ).
tcf(c_29323,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_29051,c_52]) ).
tcf(c_29363,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(X1,or(X2,or(not(X3),or(X4,not(not(X3)))))))),
inference(superposition,[status(thm)],[c_29156,c_28792]) ).
tcf(c_29438,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_28012,c_29323]) ).
tcf(c_29458,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_29438,c_52]) ).
tcf(c_29514,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,not(not(X1))))),
inference(superposition,[status(thm)],[c_29438,c_29458]) ).
tcf(c_29762,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_29514,c_28540]) ).
tcf(c_29904,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_29762,c_52]) ).
tcf(c_29916,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(X2,or(not(X3),not(not(X3))))))),
inference(superposition,[status(thm)],[c_29762,c_28792]) ).
tcf(c_30067,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,or(not(X1),not(not(X1))))),
inference(superposition,[status(thm)],[c_29363,c_29904]) ).
tcf(c_30238,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(not(X1),not(not(X1))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_30067,c_52]) ).
tcf(c_30341,plain,
! [X0: $i] : is_a_theorem(or(not(X0),not(not(X0)))),
inference(superposition,[status(thm)],[c_30067,c_30238]) ).
tcf(c_30365,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_30341,c_28792]) ).
tcf(c_30629,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_29048,c_52]) ).
tcf(c_30631,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(not(X0)),X1)),or(X2,or(or(X0,X3),X1)))),
inference(superposition,[status(thm)],[c_29048,c_160]) ).
tcf(c_30706,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_30365,c_52]) ).
tcf(c_30899,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,not(not(or(X1,not(X1)))))),
inference(superposition,[status(thm)],[c_30067,c_30706]) ).
tcf(c_30926,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_28560,c_30629]) ).
tcf(c_31129,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X2,or(or(X0,X3),X1)))
| ~ is_a_theorem(or(not(not(X0)),X1)) ),
inference(superposition,[status(thm)],[c_30631,c_52]) ).
tcf(c_31224,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(not(not(or(X1,not(X1)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_30899,c_52]) ).
tcf(c_31313,plain,
! [X0: $i] : is_a_theorem(not(not(or(X0,not(X0))))),
inference(superposition,[status(thm)],[c_30067,c_31224]) ).
tcf(c_31334,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_30926,c_52]) ).
tcf(c_31433,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(X0),or(X0,or(X1,X2)))),
inference(superposition,[status(thm)],[c_30067,c_31334]) ).
tcf(c_31454,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X0,or(X1,X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_31433,c_52]) ).
tcf(c_31500,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_31454,c_30629]) ).
tcf(c_31543,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(or(X0,X3),X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(or(not(not(X0)),X1)) ),
inference(superposition,[status(thm)],[c_31129,c_52]) ).
tcf(c_31607,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(or(X1,X2),not(not(not(X1)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_30341,c_31543]) ).
tcf(c_31841,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(or(X0,X1),not(not(not(X0))))),
inference(superposition,[status(thm)],[c_30067,c_31607]) ).
tcf(c_32781,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X1,X2)))),
inference(superposition,[status(thm)],[c_31313,c_31500]) ).
tcf(c_32801,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_32781,c_52]) ).
tcf(c_32914,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X0,X1))),
inference(superposition,[status(thm)],[c_29916,c_32801]) ).
tcf(c_33208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(or(not(X2),X3),X2)))),
inference(superposition,[status(thm)],[c_32914,c_537]) ).
tcf(c_33659,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(or(not(X1),X2)),or(or(not(X2),X3),X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_33208,c_52]) ).
tcf(c_34605,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X1),X2),X1))),
inference(superposition,[status(thm)],[c_31841,c_33659]) ).
tcf(c_311845,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(or(not(or(not(X0),X1)),or(not(X1),or(X2,X1))))
| ~ is_a_theorem(or(not(or(not(or(not(X0),X1)),or(not(X1),or(X2,X1)))),X3)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_318881,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(or(not(X0),X1)),or(not(X1),or(X2,X1))))
| ~ is_a_theorem(or(not(or(not(or(not(X0),X1)),or(not(X1),or(X2,X1)))),or(X3,or(not(or(not(X4),X1)),or(not(X1),or(X2,X1)))))) ),
inference(instantiation,[status(thm)],[c_311845]) ).
tcf(c_318882,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(or(not(X0),X1)),or(not(X1),or(X2,X1)))),or(X3,or(not(or(not(X4),X1)),or(not(X1),or(X2,X1)))))),
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_320918,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X1),X2),X1)))
| ~ is_a_theorem(or(not(or(not(or(not(X0),X1)),or(or(not(X1),X2),X1))),X3)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_336787,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(or(not(X0),X1)),or(or(not(X1),X2),X1)))
| ~ is_a_theorem(or(not(or(not(or(not(X0),X1)),or(or(not(X1),X2),X1))),or(X3,or(not(or(not(X4),X1)),or(or(not(X1),X2),X1))))) ),
inference(instantiation,[status(thm)],[c_320918]) ).
tcf(c_336788,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(or(not(or(not(X0),X1)),or(or(not(X1),X2),X1))),or(X3,or(not(or(not(X4),X1)),or(or(not(X1),X2),X1))))),
inference(instantiation,[status(thm)],[c_294]) ).
tcf(c_342349,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(or(or(X2,X1),or(not(X1),or(X3,X4))))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_7369,c_52]) ).
tcf(c_342358,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : is_a_theorem(or(or(X0,or(X1,or(not(X2),or(X3,X4)))),or(not(or(X1,or(not(X2),or(X3,X4)))),or(X5,X6)))),
inference(superposition,[status(thm)],[c_7352,c_342349]) ).
tcf(c_342372,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( is_a_theorem(or(or(not(X1),X2),or(or(or(not(X3),or(X4,X3)),X1),or(X5,X6))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_19014,c_52]) ).
tcf(c_342411,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(or(not(X0),X1),or(or(or(not(X2),or(X3,X2)),X0),or(X4,X5)))),
inference(superposition,[status(thm)],[c_342358,c_342372]) ).
tcf(c_342622,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_342830,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_343024,plain,
! [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)))),
inference(global_subsumption_just,[status(thm)],[c_537,c_34605,c_336787,c_336788]) ).
tcf(c_343025,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(or(not(X2),X3),X2)))),
inference(renaming,[status(thm)],[c_343024]) ).
tcf(c_343034,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(or(not(X1),X2)),or(or(not(X2),X3),X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_343025,c_52]) ).
tcf(c_343082,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X1),X2),X1))),
inference(superposition,[status(thm)],[c_342411,c_343034]) ).
tcf(c_343163,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(or(not(X1),X3),X1)))),
inference(superposition,[status(thm)],[c_343082,c_342622]) ).
tcf(c_343209,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(or(not(X0),X1)),X2)),or(X3,or(X0,X2)))),
inference(superposition,[status(thm)],[c_343163,c_160]) ).
tcf(c_343253,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X3,or(X0,X2)))
| ~ is_a_theorem(or(not(or(not(X0),X1)),X2)) ),
inference(superposition,[status(thm)],[c_343209,c_52]) ).
tcf(c_343254,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(X0),or(not(X0),X1))),or(X2,or(X3,or(not(X0),X1))))),
inference(superposition,[status(thm)],[c_343209,c_160]) ).
tcf(c_343275,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : is_a_theorem(or(X0,or(not(X1),or(or(X2,X1),or(or(X3,X4),X5))))),
inference(superposition,[status(thm)],[c_342830,c_343253]) ).
tcf(c_343372,plain,
! [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))))),
inference(global_subsumption_just,[status(thm)],[c_572,c_6118,c_318881,c_318882]) ).
tcf(c_343373,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(renaming,[status(thm)],[c_343372]) ).
tcf(c_343384,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_343373,c_52]) ).
tcf(c_343422,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_342411,c_343384]) ).
tcf(c_343841,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X2,or(X3,or(not(X0),X1))))
| ~ is_a_theorem(or(not(X0),or(not(X0),X1))) ),
inference(superposition,[status(thm)],[c_343254,c_52]) ).
tcf(c_343845,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(X0,or(X1,or(X2,or(X3,or(not(X1),X4)))))),
inference(superposition,[status(thm)],[c_343254,c_343253]) ).
tcf(c_344266,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(X1,or(not(X2),or(X3,X2))))),
inference(superposition,[status(thm)],[c_343422,c_343253]) ).
tcf(c_344277,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X1,or(not(X2),or(X3,X2))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_344266,c_52]) ).
tcf(c_344280,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(or(not(not(X0)),X1)),or(X2,or(or(X3,X0),X1)))),
inference(superposition,[status(thm)],[c_344266,c_160]) ).
tcf(c_344334,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(not(X1),or(X2,X1)))),
inference(superposition,[status(thm)],[c_343254,c_344277]) ).
tcf(c_344362,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_344334,c_52]) ).
tcf(c_344419,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(not(X0),or(X1,X0))),
inference(superposition,[status(thm)],[c_343254,c_344362]) ).
tcf(c_344450,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_344419,c_160]) ).
tcf(c_344489,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(X0,or(X1,or(not(X2),X2)))),
inference(superposition,[status(thm)],[c_344419,c_343841]) ).
tcf(c_344547,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_344489,c_52]) ).
tcf(c_344550,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(or(not(not(X0)),X1)),or(X2,or(X0,X1)))),
inference(superposition,[status(thm)],[c_344489,c_160]) ).
tcf(c_344602,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,or(not(X1),X1))),
inference(superposition,[status(thm)],[c_343254,c_344547]) ).
tcf(c_344629,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(not(X1),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_344602,c_52]) ).
tcf(c_344632,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_344602,c_160]) ).
tcf(c_344685,plain,
! [X0: $i] : is_a_theorem(or(not(X0),X0)),
inference(superposition,[status(thm)],[c_343254,c_344629]) ).
tcf(c_346558,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(X0,or(not(X1),or(X2,or(X3,X1))))),
inference(superposition,[status(thm)],[c_344450,c_343253]) ).
tcf(c_346562,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(X1),or(X2,or(X3,X1))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_346558,c_52]) ).
tcf(c_346653,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(or(not(X0),or(X1,or(X2,X0)))),
inference(superposition,[status(thm)],[c_343845,c_346562]) ).
tcf(c_346765,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X2,or(X0,X1)))
| ~ is_a_theorem(or(not(not(X0)),X1)) ),
inference(superposition,[status(thm)],[c_344550,c_52]) ).
tcf(c_346894,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(X0,or(X1,not(X1)))),
inference(superposition,[status(thm)],[c_344685,c_346765]) ).
tcf(c_346965,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(or(X1,not(X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_346894,c_52]) ).
tcf(c_347062,plain,
! [X0: $i] : is_a_theorem(or(X0,not(X0))),
inference(superposition,[status(thm)],[c_346653,c_346965]) ).
tcf(c_347080,plain,
! [X0: $i] :
( is_a_theorem(not(not(X0)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_347062,c_52]) ).
tcf(c_357052,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( is_a_theorem(or(not(X1),or(or(X2,X1),or(or(X3,X4),X5))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_343275,c_52]) ).
tcf(c_357637,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : is_a_theorem(or(not(X0),or(or(X1,X0),or(or(X2,X3),X4)))),
inference(superposition,[status(thm)],[c_343275,c_357052]) ).
tcf(c_358039,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(X2,or(or(X3,X0),X1)))
| ~ is_a_theorem(or(not(not(X0)),X1)) ),
inference(superposition,[status(thm)],[c_344280,c_52]) ).
tcf(c_358343,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(or(X3,X0),X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(or(not(not(X0)),X1)) ),
inference(superposition,[status(thm)],[c_358039,c_52]) ).
tcf(c_358389,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(or(X1,X2),not(not(not(X2)))))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_347062,c_358343]) ).
tcf(c_361815,plain,
! [X0: $i,X1: $i] : is_a_theorem(or(or(X0,X1),not(not(not(X1))))),
inference(superposition,[status(thm)],[c_357637,c_358389]) ).
tcf(c_370717,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_344632,c_52]) ).
tcf(c_370740,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(or(X2,X1))
| ~ is_a_theorem(or(X0,X2))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(superposition,[status(thm)],[c_370717,c_52]) ).
tcf(c_370762,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( is_a_theorem(or(X5,or(not(or(not(X3),X0)),or(X2,or(X4,X0)))))
| ~ is_a_theorem(or(or(not(or(not(X0),X1)),or(X2,or(X3,X4))),X5)) ),
inference(superposition,[status(thm)],[c_53,c_370740]) ).
tcf(c_371183,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(or(not(not(not(or(X0,or(X1,X2))))),or(not(or(not(X1),X3)),or(X0,or(X2,X3))))),
inference(superposition,[status(thm)],[c_361815,c_370762]) ).
tcf(c_371580,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(or(not(or(not(X1),X3)),or(X0,or(X2,X3))))
| ~ is_a_theorem(not(not(or(X0,or(X1,X2))))) ),
inference(superposition,[status(thm)],[c_371183,c_52]) ).
tcf(c_372125,plain,
~ is_a_theorem(not(not(or(not(or(a,b)),or(b,a))))),
inference(superposition,[status(thm)],[c_371580,c_54]) ).
tcf(c_372143,plain,
~ is_a_theorem(or(not(or(a,b)),or(b,a))),
inference(superposition,[status(thm)],[c_347080,c_372125]) ).
tcf(c_372212,plain,
~ is_a_theorem(or(not(a),a)),
inference(superposition,[status(thm)],[c_370717,c_372143]) ).
tcf(c_372213,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_372212,c_344685]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/25.41 % Computer : n006.cluster.edu
% 0.12/25.41 % Model : x86_64 x86_64
% 0.12/25.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/25.41 % Memory : 8046.5625MB
% 0.12/25.41 % OS : Linux 6.8.0-71-generic
% 0.12/25.41 % CPULimit : 300
% 0.12/25.41 % WCLimit : 300
% 0.12/25.41 % DateTime : Wed Sep 23 21:34:30 UTC 2026
% 0.12/25.41 % CPUTime :
% 0.12/25.41 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/25.45 Running first-order theorem proving
% 0.12/25.45 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.12/25.46
% 0.12/25.46 % ======== iProver multi-core TPTP/SMT =========
% 0.12/25.46
% 0.12/25.46 % Detected problem language: tptp
% 0.12/25.48 % Proving...
% 188.13/54.02 % SZS status Started for theBenchmark.p
% 188.13/54.02 % SZS status Unsatisfiable for theBenchmark.p
% 188.13/54.02
% 188.13/54.02 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 188.13/54.02
% 188.13/54.02 % ------ iProver source info
% 188.13/54.02
% 188.13/54.02 % git: date: 2026-07-19 20:42:38 +0200
% 188.13/54.02 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 188.13/54.02 % git: non_committed_changes: false
% 188.13/54.02
% 188.13/54.02 % ------ Parsing...% successful
% 188.13/54.02
% 188.13/54.02
% 188.13/54.02 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 188.13/54.02
% 188.13/54.02 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 188.13/54.02
% 188.13/54.02 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 188.13/54.02 % ------ Proving...
% 188.13/54.02 % ------ Problem Properties
% 188.13/54.02
% 188.13/54.02 %
% 188.13/54.02 % clauses 3
% 188.13/54.02 % conjectures 1
% 188.13/54.02 % EPR 0
% 188.13/54.02 % Horn 3
% 188.13/54.02 % unary 2
% 188.13/54.02 % binary 0
% 188.13/54.02 % lits 5
% 188.13/54.02 % lits eq 0
% 188.13/54.02 % fd_pure 0
% 188.13/54.02 % fd_pseudo 0
% 188.13/54.02 % fd_cond 0
% 188.13/54.02 % fd_pseudo_cond 0
% 188.13/54.02 % AC symbols 0
% 188.13/54.02
% 188.13/54.02 % ------ Input Options Time Limit: Unbounded
% 188.13/54.02
% 188.13/54.02
% 188.13/54.02 % ------
% 188.13/54.02 % Current options:
% 188.13/54.02 % ------
% 188.13/54.02
% 188.13/54.02
% 188.13/54.02 %
% 188.13/54.02
% 188.13/54.02 % ------ Proving...
% 188.13/54.02 %
% 188.13/54.02
% 188.13/54.02 % SZS status Unsatisfiable for theBenchmark.p
% 188.13/54.02
% 188.13/54.02 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 188.13/54.03
%------------------------------------------------------------------------------