%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN445-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:40:15 PM UTC 2026
% Result : Unsatisfiable 3.65s 1.11s
% Output : CNFRefutation 3.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 70
% Syntax : Number of formulae : 266 ( 2 unt; 0 def)
% Number of atoms : 1197 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 1535 ( 604 ~; 931 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 40 ( 39 usr; 36 prp; 0-1 aty)
% Number of functors : 13 ( 13 usr; 13 con; 0-0 aty)
% Number of variables : 222 ( 0 sgn 222 !; 0 ?; 171 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp16
| hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f21,negated_conjecture,
( ndr1_0
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
fof(f24,negated_conjecture,
( ndr1_0
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
fof(f30,negated_conjecture,
( ndr1_0
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
fof(f31,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
fof(f33,negated_conjecture,
( hskp10
| hskp1
| hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
fof(f36,negated_conjecture,
( hskp12
| hskp11
| hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
fof(f47,negated_conjecture,
( c0_1(a349)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f51,negated_conjecture,
( c3_1(a336)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( c1_1(a333)
| ~ hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f58,negated_conjecture,
( c2_1(a321)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( c3_1(a321)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
fof(f61,negated_conjecture,
( c1_1(a315)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( c2_1(a315)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f65,negated_conjecture,
( c3_1(a310)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( c1_1(a309)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( c3_1(a309)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( c1_1(a308)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( c3_1(a308)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f76,negated_conjecture,
( c0_1(a299)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( c3_1(a299)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f79,negated_conjecture,
( c0_1(a295)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( c2_1(a295)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp26
| ~ c2_1(a349) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp26
| ~ c3_1(a349) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f89,negated_conjecture,
( ~ hskp22
| ~ c1_1(a338) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ hskp22
| ~ c2_1(a338) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ hskp22
| ~ c3_1(a338) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp21
| ~ c0_1(a336) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ hskp21
| ~ c1_1(a336) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ hskp20
| ~ c2_1(a333) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ hskp20
| ~ c3_1(a333) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f100,negated_conjecture,
( ~ hskp16
| ~ c1_1(a321) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f103,negated_conjecture,
( ~ hskp14
| ~ c0_1(a315) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f105,negated_conjecture,
( ~ hskp12
| ~ c0_1(a310) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ hskp12
| ~ c2_1(a310) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ hskp11
| ~ c2_1(a309) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ hskp10
| ~ c0_1(a308) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f118,negated_conjecture,
( ~ hskp4
| ~ c0_1(a300) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ hskp4
| ~ c1_1(a300) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ hskp4
| ~ c2_1(a300) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ hskp3
| ~ c2_1(a299) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f124,negated_conjecture,
( ~ hskp1
| ~ c1_1(a295) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ hskp0
| ~ c0_1(a294) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ hskp0
| ~ c2_1(a294) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ hskp0
| ~ c3_1(a294) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
! [X0] :
( hskp16
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
! [X0] :
( hskp21
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
! [X0] :
( hskp22
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f134,negated_conjecture,
! [X0] :
( hskp11
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause134) ).
fof(f140,negated_conjecture,
! [X0] :
( hskp20
| hskp11
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f149,negated_conjecture,
! [X0,X1] :
( hskp0
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f154,negated_conjecture,
! [X0,X1] :
( hskp1
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( hskp0
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f159,negated_conjecture,
! [X0,X1] :
( hskp9
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( hskp12
| c3_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( hskp3
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
! [X0,X1] :
( hskp14
| c2_1(X1)
| c1_1(X1)
| c2_1(X0)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
! [X0,X1] :
( hskp7
| c2_1(X1)
| c1_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause165) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( hskp4
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause167) ).
fof(f169,negated_conjecture,
! [X0,X1] :
( c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( hskp11
| c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f172,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c1_1(X2)
| c0_1(X2)
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause172) ).
fof(f174,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X2)
| c1_1(X2)
| c0_1(X2)
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X2)
| c1_1(X2)
| c0_1(X2)
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X2)
| c2_1(X2)
| c0_1(X2)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X2)
| c0_1(X2)
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| ~ c2_1(X2)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c0_1(X2)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c1_1(X2)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c1_1(X2)
| c0_1(X2)
| c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X2)
| c2_1(X2)
| c2_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
tcf(c_229,negated_conjecture,
( hskp16
| hskp26 ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_249,negated_conjecture,
( ndr1_0
| ~ hskp10 ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_252,negated_conjecture,
( ndr1_0
| ~ hskp7 ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_258,negated_conjecture,
( ndr1_0
| ~ hskp1 ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_259,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_261,negated_conjecture,
( hskp1
| hskp7
| hskp10 ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_264,negated_conjecture,
( hskp11
| hskp12
| hskp26 ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_275,negated_conjecture,
( c0_1(a349)
| ~ hskp26 ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_279,negated_conjecture,
( c3_1(a336)
| ~ hskp21 ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_280,negated_conjecture,
( c1_1(a333)
| ~ hskp20 ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_286,negated_conjecture,
( c2_1(a321)
| ~ hskp16 ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_287,negated_conjecture,
( c3_1(a321)
| ~ hskp16 ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_289,negated_conjecture,
( c1_1(a315)
| ~ hskp14 ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_290,negated_conjecture,
( c2_1(a315)
| ~ hskp14 ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_293,negated_conjecture,
( c3_1(a310)
| ~ hskp12 ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_294,negated_conjecture,
( c1_1(a309)
| ~ hskp11 ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_295,negated_conjecture,
( c3_1(a309)
| ~ hskp11 ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_296,negated_conjecture,
( c1_1(a308)
| ~ hskp10 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_297,negated_conjecture,
( c3_1(a308)
| ~ hskp10 ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_304,negated_conjecture,
( c0_1(a299)
| ~ hskp3 ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_305,negated_conjecture,
( c3_1(a299)
| ~ hskp3 ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_307,negated_conjecture,
( c0_1(a295)
| ~ hskp1 ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_308,negated_conjecture,
( c2_1(a295)
| ~ hskp1 ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_309,negated_conjecture,
( ~ hskp26
| ~ c2_1(a349) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_310,negated_conjecture,
( ~ hskp26
| ~ c3_1(a349) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_317,negated_conjecture,
( ~ hskp22
| ~ c1_1(a338) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_318,negated_conjecture,
( ~ hskp22
| ~ c2_1(a338) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_319,negated_conjecture,
( ~ hskp22
| ~ c3_1(a338) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_320,negated_conjecture,
( ~ hskp21
| ~ c0_1(a336) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_321,negated_conjecture,
( ~ hskp21
| ~ c1_1(a336) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_322,negated_conjecture,
( ~ hskp20
| ~ c2_1(a333) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_323,negated_conjecture,
( ~ hskp20
| ~ c3_1(a333) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_328,negated_conjecture,
( ~ hskp16
| ~ c1_1(a321) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_331,negated_conjecture,
( ~ hskp14
| ~ c0_1(a315) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_333,negated_conjecture,
( ~ hskp12
| ~ c0_1(a310) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_334,negated_conjecture,
( ~ hskp12
| ~ c2_1(a310) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_335,negated_conjecture,
( ~ hskp11
| ~ c2_1(a309) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_336,negated_conjecture,
( ~ hskp10
| ~ c0_1(a308) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_346,negated_conjecture,
( ~ hskp4
| ~ c0_1(a300) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_347,negated_conjecture,
( ~ hskp4
| ~ c1_1(a300) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_348,negated_conjecture,
( ~ hskp4
| ~ c2_1(a300) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_349,negated_conjecture,
( ~ hskp3
| ~ c2_1(a299) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_352,negated_conjecture,
( ~ hskp1
| ~ c1_1(a295) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_353,negated_conjecture,
( ~ hskp0
| ~ c0_1(a294) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_354,negated_conjecture,
( ~ hskp0
| ~ c2_1(a294) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_355,negated_conjecture,
( ~ hskp0
| ~ c3_1(a294) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_356,negated_conjecture,
! [X0: $i] :
( hskp16
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_357,negated_conjecture,
! [X0: $i] :
( hskp21
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_358,negated_conjecture,
! [X0: $i] :
( hskp22
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_362,negated_conjecture,
! [X0: $i] :
( hskp10
| hskp11
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_368,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp20
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_377,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_382,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_383,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_387,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp9
| c3_1(X0)
| c2_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_388,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp12
| c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_391,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp3
| c3_1(X0)
| c2_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_392,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp14
| c2_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_393,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp7
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_395,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp4
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_397,negated_conjecture,
! [X0: $i,X1: $i] :
( c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_398,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp11
| c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_400,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X1)
| c2_1(X2)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f172]) ).
tcf(c_402,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X1)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_403,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X0)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_404,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c0_1(X2)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_405,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X2)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_406,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X1)
| c2_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X2)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_407,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| c0_1(X2)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_408,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c2_1(X2)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X2)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_435,negated_conjecture,
ndr1_0,
inference(global_subsumption_just,[status(thm)],[c_259,c_261,c_258,c_252,c_249]) ).
tcf(c_495,negated_conjecture,
! [X0: $i] :
( hskp22
| c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_358,c_261,c_258,c_252,c_249,c_358]) ).
tcf(c_498,negated_conjecture,
! [X0: $i] :
( hskp21
| c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_357,c_261,c_258,c_252,c_249,c_357]) ).
tcf(c_501,negated_conjecture,
! [X0: $i] :
( hskp16
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_356,c_261,c_258,c_252,c_249,c_356]) ).
tcf(c_510,negated_conjecture,
! [X0: $i] :
( hskp10
| hskp11
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_362,c_261,c_258,c_252,c_249,c_362]) ).
tcf(c_537,plain,
! [X0: $i] :
( hskp11
| hskp20
| c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_368,c_261,c_258,c_252,c_249,c_368]) ).
tcf(c_538,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp20
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_537]) ).
tcf(c_568,plain,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_377,c_261,c_258,c_252,c_249,c_377]) ).
tcf(c_569,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_568]) ).
tcf(c_570,plain,
! [X0: $i,X1: $i] :
( hskp7
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_393,c_261,c_258,c_252,c_249,c_393]) ).
tcf(c_571,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp7
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_570]) ).
tcf(c_572,plain,
! [X0: $i,X1: $i] :
( hskp14
| c2_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_392,c_261,c_258,c_252,c_249,c_392]) ).
tcf(c_573,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp14
| c2_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_572]) ).
tcf(c_574,plain,
! [X0: $i,X1: $i] :
( hskp3
| c3_1(X0)
| c2_1(X0)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_391,c_261,c_258,c_252,c_249,c_391]) ).
tcf(c_575,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp3
| c3_1(X0)
| c2_1(X0)
| c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_574]) ).
tcf(c_581,plain,
! [X0: $i,X1: $i] :
( hskp12
| c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_388,c_261,c_258,c_252,c_249,c_388]) ).
tcf(c_582,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp12
| c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_581]) ).
tcf(c_583,plain,
! [X0: $i,X1: $i] :
( hskp9
| c3_1(X0)
| c2_1(X1)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_387,c_261,c_258,c_252,c_249,c_387]) ).
tcf(c_584,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp9
| c3_1(X0)
| c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_583]) ).
tcf(c_591,plain,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_383,c_261,c_258,c_252,c_249,c_383]) ).
tcf(c_592,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_591]) ).
tcf(c_593,plain,
! [X0: $i,X1: $i] :
( hskp1
| c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_382,c_261,c_258,c_252,c_249,c_382]) ).
tcf(c_594,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_593]) ).
tcf(c_596,plain,
! [X0: $i,X1: $i] :
( c2_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_397,c_261,c_258,c_252,c_249,c_397]) ).
tcf(c_597,negated_conjecture,
! [X0: $i,X1: $i] :
( c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_596]) ).
tcf(c_600,plain,
! [X0: $i,X1: $i] :
( hskp4
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_395,c_261,c_258,c_252,c_249,c_395]) ).
tcf(c_601,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp4
| c1_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_600]) ).
tcf(c_607,plain,
! [X0: $i,X1: $i] :
( hskp11
| c3_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_398,c_261,c_258,c_252,c_249,c_398]) ).
tcf(c_608,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp11
| c3_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_607]) ).
tcf(c_609,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X1)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_402,c_261,c_258,c_252,c_249,c_402]) ).
tcf(c_610,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X1)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_609]) ).
tcf(c_613,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X1)
| c2_1(X2)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_400,c_261,c_258,c_252,c_249,c_400]) ).
tcf(c_614,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X1)
| c2_1(X2)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_613]) ).
tcf(c_615,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c0_1(X2)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_404,c_404,c_435]) ).
tcf(c_616,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c0_1(X2)
| c0_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_615]) ).
tcf(c_617,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X0)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_403,c_261,c_258,c_252,c_249,c_403]) ).
tcf(c_618,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X0)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_617]) ).
tcf(c_619,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X1)
| c2_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_406,c_261,c_258,c_252,c_249,c_406]) ).
tcf(c_620,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X1)
| c2_1(X2)
| c0_1(X2)
| c0_1(X1)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X2)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_619]) ).
tcf(c_621,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_405,c_261,c_258,c_252,c_249,c_405]) ).
tcf(c_622,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c2_1(X1)
| c1_1(X2)
| c0_1(X2)
| c0_1(X1)
| ~ c2_1(X2)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_621]) ).
tcf(c_623,plain,
! [X0: $i,X1: $i,X2: $i] :
( c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| c0_1(X2)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_407,c_261,c_258,c_252,c_249,c_407]) ).
tcf(c_624,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| c0_1(X2)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_623]) ).
tcf(c_625,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c2_1(X2)
| c2_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_408,c_261,c_258,c_252,c_249,c_408]) ).
tcf(c_626,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c2_1(X2)
| c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X2)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_625]) ).
tcf(c_1806,plain,
! [X0: $i] :
( c3_1(X0)
| c2_1(X0)
| ~ c3_1(a338)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[c_495,c_319]) ).
tcf(c_1807,plain,
( c3_1(a294)
| c2_1(a294)
| ~ c3_1(a338)
| ~ c1_1(a294) ),
inference(instantiation,[status(thm)],[c_1806]) ).
tcf(c_1820,plain,
! [X0: $i] :
( c3_1(X0)
| c2_1(X0)
| ~ c2_1(a338)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[c_495,c_318]) ).
tcf(c_1821,plain,
( c3_1(a294)
| c2_1(a294)
| ~ c2_1(a338)
| ~ c1_1(a294) ),
inference(instantiation,[status(thm)],[c_1820]) ).
tcf(c_1834,plain,
! [X0: $i] :
( c3_1(X0)
| c2_1(X0)
| ~ c1_1(a338)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[c_495,c_317]) ).
tcf(c_1835,plain,
( c3_1(a294)
| c2_1(a294)
| ~ c1_1(a294)
| ~ c1_1(a338) ),
inference(instantiation,[status(thm)],[c_1834]) ).
tcf(c_2661,plain,
( hskp16
| ~ c3_1(a349) ),
inference(resolution,[status(thm)],[c_229,c_310]) ).
tcf(c_2668,plain,
( hskp16
| ~ c2_1(a349) ),
inference(resolution,[status(thm)],[c_229,c_309]) ).
tcf(c_2675,plain,
( hskp16
| c0_1(a349) ),
inference(resolution,[status(thm)],[c_229,c_275]) ).
tcf(c_5775,plain,
( hskp11
| hskp26
| ~ c2_1(a310) ),
inference(resolution,[status(thm)],[c_264,c_334]) ).
tcf(c_5785,plain,
( hskp11
| hskp26
| ~ c0_1(a310) ),
inference(resolution,[status(thm)],[c_264,c_333]) ).
tcf(c_5795,plain,
( hskp11
| hskp26
| c3_1(a310) ),
inference(resolution,[status(thm)],[c_264,c_293]) ).
tcf(c_13228,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_626]) ).
tcf(c_13229,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ~ c1_1(X0)
| c2_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_626]) ).
tcf(c_13232,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ~ c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_624]) ).
tcf(c_13233,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| c0_1(X0)
| c1_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_624]) ).
tcf(c_13235,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_622]) ).
tcf(c_13236,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_622]) ).
tcf(c_13239,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| c0_1(X0)
| ~ c1_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_620]) ).
tcf(c_13240,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_620]) ).
tcf(c_13241,negated_conjecture,
( iPr_def_19
| iPr_def_18
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_620]) ).
tcf(c_13242,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| c0_1(X0)
| c1_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_618]) ).
tcf(c_13245,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_616]) ).
tcf(c_13246,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| c0_1(X0)
| c2_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_616]) ).
tcf(c_13247,negated_conjecture,
( iPr_def_23
| iPr_def_22
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_616]) ).
tcf(c_13248,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_24
| c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_614]) ).
tcf(c_13249,negated_conjecture,
( iPr_def_24
| iPr_def_23
| iPr_def_14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_614]) ).
tcf(c_13252,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_26
| c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_26])],[c_610]) ).
tcf(c_13253,negated_conjecture,
( iPr_def_26
| iPr_def_23
| iPr_def_20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_610]) ).
tcf(c_13254,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_27
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_608]) ).
tcf(c_13260,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_30
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_601]) ).
tcf(c_13261,negated_conjecture,
( iPr_def_30
| iPr_def_13
| hskp4 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_601]) ).
tcf(c_13263,negated_conjecture,
( iPr_def_27
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_597]) ).
tcf(c_13264,negated_conjecture,
( iPr_def_22
| iPr_def_15
| hskp1 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_594]) ).
tcf(c_13265,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_31
| c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_31])],[c_592]) ).
tcf(c_13266,negated_conjecture,
( iPr_def_31
| iPr_def_10
| hskp0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_592]) ).
tcf(c_13270,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_32
| c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_32])],[c_584]) ).
tcf(c_13272,negated_conjecture,
( iPr_def_18
| iPr_def_10
| hskp12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_582]) ).
tcf(c_13277,negated_conjecture,
( iPr_def_26
| iPr_def_11
| hskp3 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_575]) ).
tcf(c_13278,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_35
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_35])],[c_573]) ).
tcf(c_13279,negated_conjecture,
( iPr_def_35
| iPr_def_10
| hskp14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_573]) ).
tcf(c_13281,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_37
| ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_37])],[c_571]) ).
tcf(c_13283,negated_conjecture,
( iPr_def_37
| iPr_def_14
| hskp0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_569]) ).
tcf(c_13297,negated_conjecture,
( iPr_def_13
| hskp11
| hskp20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_538]) ).
tcf(c_13305,negated_conjecture,
( iPr_def_32
| hskp10
| hskp11 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_510]) ).
tcf(c_13309,plain,
( c3_1(a294)
| c1_1(a294)
| c0_1(a294)
| ~ iPr_def_20 ),
inference(instantiation,[status(thm)],[c_13242]) ).
tcf(c_13310,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| ~ iPr_def_23 ),
inference(instantiation,[status(thm)],[c_13246]) ).
tcf(c_13314,plain,
( c2_1(a294)
| c0_1(a294)
| ~ iPr_def_16
| ~ c1_1(a294) ),
inference(instantiation,[status(thm)],[c_13236]) ).
tcf(c_13315,plain,
( c3_1(a294)
| c0_1(a294)
| ~ iPr_def_18
| ~ c1_1(a294) ),
inference(instantiation,[status(thm)],[c_13239]) ).
tcf(c_13363,plain,
( c2_1(a309)
| ~ iPr_def_10
| ~ c3_1(a309)
| ~ c1_1(a309) ),
inference(instantiation,[status(thm)],[c_13228]) ).
tcf(c_13364,plain,
( c2_1(a308)
| ~ iPr_def_10
| ~ c3_1(a308)
| ~ c1_1(a308) ),
inference(instantiation,[status(thm)],[c_13228]) ).
tcf(c_13365,plain,
( c2_1(a299)
| ~ iPr_def_10
| ~ c3_1(a299)
| ~ c1_1(a299) ),
inference(instantiation,[status(thm)],[c_13228]) ).
tcf(c_13366,plain,
( c2_1(a310)
| c1_1(a310)
| c0_1(a310)
| ~ iPr_def_14 ),
inference(instantiation,[status(thm)],[c_13233]) ).
tcf(c_13370,plain,
( c2_1(a300)
| c1_1(a300)
| c0_1(a300)
| ~ iPr_def_14 ),
inference(instantiation,[status(thm)],[c_13233]) ).
tcf(c_13412,plain,
( c2_1(a333)
| c0_1(a333)
| ~ iPr_def_16
| ~ c1_1(a333) ),
inference(instantiation,[status(thm)],[c_13236]) ).
tcf(c_13415,plain,
( hskp21
| c3_1(a349)
| c2_1(a349)
| ~ c0_1(a349) ),
inference(instantiation,[status(thm)],[c_498]) ).
tcf(c_13427,plain,
( c1_1(a295)
| ~ iPr_def_13
| ~ c2_1(a295)
| ~ c0_1(a295) ),
inference(instantiation,[status(thm)],[c_13232]) ).
tcf(c_13460,plain,
( c3_1(a333)
| c2_1(a333)
| ~ iPr_def_11
| ~ c1_1(a333) ),
inference(instantiation,[status(thm)],[c_13229]) ).
tcf(c_13470,plain,
( c2_1(a333)
| ~ iPr_def_37
| ~ c1_1(a333)
| ~ c0_1(a333) ),
inference(instantiation,[status(thm)],[c_13281]) ).
tcf(c_13495,plain,
( c3_1(a338)
| c1_1(a338)
| c0_1(a338)
| ~ iPr_def_20 ),
inference(instantiation,[status(thm)],[c_13242]) ).
tcf(c_13527,plain,
( c1_1(a321)
| ~ iPr_def_13
| ~ c2_1(a321)
| ~ c0_1(a321) ),
inference(instantiation,[status(thm)],[c_13232]) ).
tcf(c_13539,plain,
( c1_1(a336)
| ~ iPr_def_22
| ~ c3_1(a336)
| ~ c2_1(a336) ),
inference(instantiation,[status(thm)],[c_13245]) ).
tcf(c_13540,plain,
( c1_1(a321)
| ~ iPr_def_22
| ~ c3_1(a321)
| ~ c2_1(a321) ),
inference(instantiation,[status(thm)],[c_13245]) ).
tcf(c_13551,plain,
( ~ iPr_def_27
| ~ c3_1(a321)
| ~ c2_1(a321)
| ~ c0_1(a321) ),
inference(instantiation,[status(thm)],[c_13254]) ).
tcf(c_13597,plain,
( c0_1(a315)
| ~ iPr_def_24
| ~ c2_1(a315)
| ~ c1_1(a315) ),
inference(instantiation,[status(thm)],[c_13248]) ).
tcf(c_13599,plain,
( c0_1(a308)
| ~ iPr_def_24
| ~ c2_1(a308)
| ~ c1_1(a308) ),
inference(instantiation,[status(thm)],[c_13248]) ).
tcf(c_13631,plain,
( c1_1(a321)
| ~ iPr_def_30
| ~ c3_1(a321)
| ~ c0_1(a321) ),
inference(instantiation,[status(thm)],[c_13260]) ).
tcf(c_13636,plain,
( c1_1(a299)
| ~ iPr_def_30
| ~ c3_1(a299)
| ~ c0_1(a299) ),
inference(instantiation,[status(thm)],[c_13260]) ).
tcf(c_13648,plain,
( c1_1(a336)
| c0_1(a336)
| ~ iPr_def_15
| ~ c2_1(a336) ),
inference(instantiation,[status(thm)],[c_13235]) ).
tcf(c_13659,plain,
( c0_1(a310)
| ~ iPr_def_19
| ~ c3_1(a310)
| ~ c1_1(a310) ),
inference(instantiation,[status(thm)],[c_13240]) ).
tcf(c_13678,plain,
( c2_1(a336)
| c0_1(a336)
| ~ iPr_def_32
| ~ c3_1(a336) ),
inference(instantiation,[status(thm)],[c_13270]) ).
tcf(c_13681,plain,
( c2_1(a310)
| c0_1(a310)
| ~ iPr_def_32
| ~ c3_1(a310) ),
inference(instantiation,[status(thm)],[c_13270]) ).
tcf(c_13735,plain,
( c1_1(a321)
| c0_1(a321)
| ~ iPr_def_15
| ~ c2_1(a321) ),
inference(instantiation,[status(thm)],[c_13235]) ).
tcf(c_13848,plain,
( c0_1(a336)
| ~ iPr_def_26
| ~ c3_1(a336)
| ~ c2_1(a336) ),
inference(instantiation,[status(thm)],[c_13252]) ).
tcf(c_13849,plain,
( c0_1(a321)
| ~ iPr_def_26
| ~ c3_1(a321)
| ~ c2_1(a321) ),
inference(instantiation,[status(thm)],[c_13252]) ).
tcf(c_13976,plain,
( hskp16
| c2_1(a336)
| c1_1(a336)
| ~ c3_1(a336) ),
inference(instantiation,[status(thm)],[c_501]) ).
tcf(c_13998,plain,
( c1_1(a336)
| c0_1(a336)
| ~ iPr_def_31
| ~ c3_1(a336) ),
inference(instantiation,[status(thm)],[c_13265]) ).
tcf(c_13999,plain,
( c1_1(a321)
| c0_1(a321)
| ~ iPr_def_31
| ~ c3_1(a321) ),
inference(instantiation,[status(thm)],[c_13265]) ).
tcf(c_14006,plain,
( c2_1(a338)
| c1_1(a338)
| ~ iPr_def_35
| ~ c0_1(a338) ),
inference(instantiation,[status(thm)],[c_13278]) ).
tcf(c_14145,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| ~ iPr_def_23 ),
inference(instantiation,[status(thm)],[c_13246]) ).
tcf(c_14276,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_14145,c_14006,c_13999,c_13998,c_13976,c_13849,c_13848,c_13735,c_13681,c_13678,c_13659,c_13648,c_13636,c_13631,c_13599,c_13597,c_13551,c_13540,c_13539,c_13527,c_13495,c_13470,c_13460,c_13427,c_13415,c_13412,c_13370,c_13366,c_13365,c_13364,c_13363,c_13315,c_13314,c_13310,c_13309,c_13305,c_13297,c_13283,c_13279,c_13277,c_13272,c_13266,c_13264,c_13261,c_13253,c_13249,c_13247,c_13241,c_13263,c_5795,c_5785,c_5775,c_2675,c_2668,c_2661,c_1835,c_1821,c_1807,c_309,c_310,c_320,c_321,c_322,c_323,c_328,c_331,c_333,c_334,c_335,c_336,c_346,c_347,c_348,c_349,c_352,c_353,c_354,c_355,c_275,c_279,c_280,c_286,c_287,c_289,c_290,c_293,c_294,c_295,c_296,c_297,c_304,c_305,c_307,c_308]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN445-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.34 % Computer : n008.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 25 01:13:54 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.38 Running EPR theorem proving
% 0.12/0.38 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.39
% 0.12/0.39 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.39
% 0.12/0.39 % Detected problem language: tptp
% 0.12/0.40 % Proving...
% 3.65/1.11 % SZS status Started for theBenchmark.p
% 3.65/1.11 % SZS status Unsatisfiable for theBenchmark.p
% 3.65/1.11
% 3.65/1.11 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.65/1.11
% 3.65/1.11 % ------ iProver source info
% 3.65/1.11
% 3.65/1.11 % git: date: 2026-07-19 20:42:38 +0200
% 3.65/1.11 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.65/1.11 % git: non_committed_changes: false
% 3.65/1.11
% 3.65/1.11 % ------ Parsing...% successful
% 3.65/1.11
% 3.65/1.11
% 3.65/1.11 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 3.65/1.11 %
% 3.65/1.11
% 3.65/1.11 % ------ Preprocessing... sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 3.65/1.11
% 3.65/1.11 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 3.65/1.11 gs_s sp: 90 0s gs_e snvd_s sp: 0 0s snvd_e
% 3.65/1.11 % ------ Proving...
% 3.65/1.11 % ------ Problem Properties
% 3.65/1.11
% 3.65/1.11 %
% 3.65/1.11 % clauses 180
% 3.65/1.11 % conjectures 177
% 3.65/1.11 % EPR 180
% 3.65/1.11 % Horn 103
% 3.65/1.11 % unary 0
% 3.65/1.11 % binary 89
% 3.65/1.11 % lits 486
% 3.65/1.11 % lits eq 0
% 3.65/1.11 % fd_pure 0
% 3.65/1.11 % fd_pseudo 0
% 3.65/1.11 % fd_cond 0
% 3.65/1.11 % fd_pseudo_cond 0
% 3.65/1.11 % AC symbols 0
% 3.65/1.11
% 3.65/1.11 % ------ Schedule EPR non Horn non eq is on
% 3.65/1.11
% 3.65/1.11 % ------ no equalities: superposition off
% 3.65/1.11
% 3.65/1.11 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 3.65/1.11
% 3.65/1.11
% 3.65/1.11 % ------
% 3.65/1.11 % Current options:
% 3.65/1.11 % ------
% 3.65/1.11
% 3.65/1.11
% 3.65/1.11 %
% 3.65/1.11
% 3.65/1.11 % ------ Proving...
% 3.65/1.11 %
% 3.65/1.11
% 3.65/1.11 % SZS status Unsatisfiable for theBenchmark.p
% 3.65/1.11
% 3.65/1.11 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.65/1.12
% 3.65/1.12
%------------------------------------------------------------------------------