%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN439-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 : n020.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:12 PM UTC 2026
% Result : Unsatisfiable 6.72s 11.61s
% Output : CNFRefutation 6.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 155
% Syntax : Number of formulae : 588 ( 2 unt; 0 def)
% Number of atoms : 2259 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2910 (1239 ~;1671 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 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 : 74 ( 73 usr; 70 prp; 0-1 aty)
% Number of functors : 38 ( 38 usr; 38 con; 0-0 aty)
% Number of variables : 285 ( 0 sgn 285 !; 0 ?; 219 :)
% Comments :
%------------------------------------------------------------------------------
fof(f17,negated_conjecture,
( ndr1_0
| ~ hskp36 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
fof(f19,negated_conjecture,
( ndr1_0
| ~ hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
fof(f50,negated_conjecture,
( ndr1_0
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
fof(f53,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( hskp3
| hskp34
| hskp36 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( hskp18
| hskp17
| hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( hskp4
| hskp27
| hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
fof(f60,negated_conjecture,
( c0_1(a583)
| ~ hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( c3_1(a583)
| ~ hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( c0_1(a574)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( c1_1(a574)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( c2_1(a568)
| ~ hskp49 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f66,negated_conjecture,
( c0_1(a564)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( c1_1(a564)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( c1_1(a562)
| ~ hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f70,negated_conjecture,
( c0_1(a559)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( c2_1(a559)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f76,negated_conjecture,
( c3_1(a555)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( c0_1(a555)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( c3_1(a551)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( c2_1(a551)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( c3_1(a549)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( c2_1(a549)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( c1_1(a549)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( c2_1(a547)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( c1_1(a547)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( c0_1(a547)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( c1_1(a544)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f90,negated_conjecture,
( c2_1(a538)
| ~ hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( c1_1(a538)
| ~ hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( c3_1(a538)
| ~ hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( c0_1(a537)
| ~ hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( c3_1(a537)
| ~ hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( c1_1(a536)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( c2_1(a536)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( c0_1(a536)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( c0_1(a596)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( c1_1(a591)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( c2_1(a589)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( c3_1(a589)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( c1_1(a586)
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( c0_1(a584)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( c1_1(a584)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( c2_1(a581)
| ~ hskp24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( c3_1(a578)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( c1_1(a577)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f109,negated_conjecture,
( c0_1(a572)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( c0_1(a571)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( c3_1(a571)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( c3_1(a570)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( c1_1(a570)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f118,negated_conjecture,
( c1_1(a560)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f120,negated_conjecture,
( c0_1(a550)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( c3_1(a550)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( c3_1(a548)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( c2_1(a546)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( c1_1(a545)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f127,negated_conjecture,
( c1_1(a535)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( c0_1(a535)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f130,negated_conjecture,
( ~ hskp51
| ~ c2_1(a583) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( ~ hskp50
| ~ c3_1(a574) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ hskp49
| ~ c0_1(a568) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( ~ hskp49
| ~ c1_1(a568) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f136,negated_conjecture,
( ~ hskp47
| ~ c2_1(a564) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( ~ hskp46
| ~ c3_1(a562) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
( ~ hskp46
| ~ c0_1(a562) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause138) ).
fof(f141,negated_conjecture,
( ~ hskp44
| ~ c3_1(a559) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause141) ).
fof(f144,negated_conjecture,
( ~ hskp41
| ~ c2_1(a555) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
( ~ hskp40
| ~ c0_1(a551) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
( ~ hskp37
| ~ c2_1(a544) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
( ~ hskp37
| ~ c3_1(a544) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
( ~ hskp34
| ~ c1_1(a537) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
( ~ hskp32
| ~ c3_1(a596) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
( ~ hskp32
| ~ c2_1(a596) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause150) ).
fof(f154,negated_conjecture,
( ~ hskp30
| ~ c2_1(a591) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( ~ hskp30
| ~ c0_1(a591) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
( ~ hskp29
| ~ c3_1(a590) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
( ~ hskp29
| ~ c0_1(a590) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
( ~ hskp29
| ~ c1_1(a590) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
( ~ hskp28
| ~ c0_1(a589) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( ~ hskp27
| ~ c0_1(a586) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( ~ hskp27
| ~ c3_1(a586) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
( ~ hskp26
| ~ c3_1(a584) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
( ~ hskp25
| ~ c3_1(a582) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
( ~ hskp25
| ~ c2_1(a582) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
( ~ hskp25
| ~ c1_1(a582) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause165) ).
fof(f166,negated_conjecture,
( ~ hskp24
| ~ c1_1(a581) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
( ~ hskp24
| ~ c3_1(a581) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
( ~ hskp23
| ~ c0_1(a578) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( ~ hskp23
| ~ c1_1(a578) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
( ~ hskp22
| ~ c3_1(a577) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
( ~ hskp22
| ~ c0_1(a577) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause171) ).
fof(f177,negated_conjecture,
( ~ hskp19
| ~ c2_1(a573) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
( ~ hskp19
| ~ c0_1(a573) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
( ~ hskp19
| ~ c1_1(a573) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
( ~ hskp18
| ~ c3_1(a572) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
( ~ hskp18
| ~ c1_1(a572) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( ~ hskp17
| ~ c2_1(a571) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
( ~ hskp16
| ~ c0_1(a570) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
( ~ hskp15
| ~ c0_1(a569) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
( ~ hskp15
| ~ c1_1(a569) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
( ~ hskp15
| ~ c2_1(a569) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause186) ).
fof(f192,negated_conjecture,
( ~ hskp11
| ~ c3_1(a560) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
( ~ hskp11
| ~ c0_1(a560) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
( ~ hskp10
| ~ c1_1(a558) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
( ~ hskp10
| ~ c0_1(a558) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
( ~ hskp9
| ~ c0_1(a554) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause196) ).
fof(f197,negated_conjecture,
( ~ hskp9
| ~ c2_1(a554) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause197) ).
fof(f198,negated_conjecture,
( ~ hskp9
| ~ c1_1(a554) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause198) ).
fof(f199,negated_conjecture,
( ~ hskp8
| ~ c3_1(a552) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
( ~ hskp8
| ~ c1_1(a552) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
( ~ hskp8
| ~ c2_1(a552) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ hskp7
| ~ c1_1(a550) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ hskp6
| ~ c2_1(a548) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
( ~ hskp6
| ~ c0_1(a548) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
( ~ hskp5
| ~ c3_1(a546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
( ~ hskp5
| ~ c1_1(a546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ hskp4
| ~ c2_1(a545) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ hskp4
| ~ c0_1(a545) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause208) ).
fof(f216,negated_conjecture,
( ~ hskp0
| ~ c2_1(a535) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause216) ).
fof(f217,negated_conjecture,
! [X0] :
( c2_1(X0)
| c0_1(X0)
| c1_1(X0)
| hskp28
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
! [X0] :
( hskp11
| hskp44
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
fof(f220,negated_conjecture,
! [X0] :
( hskp50
| hskp19
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause220) ).
fof(f221,negated_conjecture,
! [X0] :
( hskp24
| hskp39
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause221) ).
fof(f222,negated_conjecture,
! [X0] :
( hskp30
| hskp29
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause222) ).
fof(f223,negated_conjecture,
! [X0] :
( hskp40
| hskp7
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause223) ).
fof(f224,negated_conjecture,
! [X0] :
( hskp41
| hskp9
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause224) ).
fof(f226,negated_conjecture,
! [X0] :
( hskp23
| hskp22
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause226) ).
fof(f228,negated_conjecture,
! [X0,X1] :
( hskp38
| c2_1(X1)
| c1_1(X1)
| c3_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause228) ).
fof(f230,negated_conjecture,
! [X0,X1] :
( hskp33
| c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause230) ).
fof(f231,negated_conjecture,
! [X0,X1] :
( hskp6
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause231) ).
fof(f234,negated_conjecture,
! [X0,X1] :
( hskp51
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause234) ).
fof(f235,negated_conjecture,
! [X0,X1] :
( hskp26
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c0_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause235) ).
fof(f236,negated_conjecture,
! [X0,X1] :
( hskp0
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause236) ).
fof(f237,negated_conjecture,
! [X0,X1] :
( hskp34
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause237) ).
fof(f238,negated_conjecture,
! [X0,X1] :
( hskp35
| c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause238) ).
fof(f239,negated_conjecture,
! [X0,X1] :
( hskp37
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause239) ).
fof(f240,negated_conjecture,
! [X0,X1] :
( hskp5
| c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause240) ).
fof(f241,negated_conjecture,
! [X0,X1] :
( hskp39
| c0_1(X1)
| c3_1(X1)
| c2_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause241) ).
fof(f242,negated_conjecture,
! [X0,X1] :
( hskp8
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause242) ).
fof(f244,negated_conjecture,
! [X0,X1] :
( hskp49
| c2_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
! [X0,X1] :
( hskp15
| c1_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
! [X0,X1] :
( hskp46
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
! [X0,X1] :
( hskp4
| c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause247) ).
fof(f248,negated_conjecture,
! [X0,X1] :
( hskp46
| c0_1(X1)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause248) ).
fof(f249,negated_conjecture,
! [X0,X1] :
( hskp47
| c0_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause249) ).
fof(f250,negated_conjecture,
! [X0,X1] :
( hskp34
| c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause250) ).
fof(f252,negated_conjecture,
! [X0,X1] :
( hskp32
| c3_1(X1)
| c3_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause252) ).
fof(f253,negated_conjecture,
! [X0,X1] :
( hskp38
| c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause253) ).
fof(f255,negated_conjecture,
! [X0,X1] :
( hskp10
| c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause255) ).
fof(f256,negated_conjecture,
! [X0,X1] :
( hskp25
| c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause256) ).
fof(f257,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c0_1(X0)
| ~ c0_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause257) ).
fof(f258,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X1)
| c1_1(X2)
| c3_1(X2)
| c2_1(X2)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause258) ).
fof(f259,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X2)
| c3_1(X1)
| c1_1(X1)
| c2_1(X0)
| ~ c3_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause259) ).
fof(f260,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c1_1(X1)
| c2_1(X1)
| ~ c0_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause260) ).
tcf(c_325,negated_conjecture,
( ndr1_0
| ~ hskp36 ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_327,negated_conjecture,
( ndr1_0
| ~ hskp34 ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_358,negated_conjecture,
( ndr1_0
| ~ hskp3 ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_361,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_362,negated_conjecture,
( hskp3
| hskp34
| hskp36 ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_363,negated_conjecture,
( hskp16
| hskp17
| hskp18 ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_364,negated_conjecture,
( hskp4
| hskp6
| hskp27 ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_368,negated_conjecture,
( c0_1(a583)
| ~ hskp51 ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_369,negated_conjecture,
( c3_1(a583)
| ~ hskp51 ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_370,negated_conjecture,
( c0_1(a574)
| ~ hskp50 ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_371,negated_conjecture,
( c1_1(a574)
| ~ hskp50 ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_372,negated_conjecture,
( c2_1(a568)
| ~ hskp49 ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_374,negated_conjecture,
( c0_1(a564)
| ~ hskp47 ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_375,negated_conjecture,
( c1_1(a564)
| ~ hskp47 ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_376,negated_conjecture,
( c1_1(a562)
| ~ hskp46 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_378,negated_conjecture,
( c0_1(a559)
| ~ hskp44 ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_379,negated_conjecture,
( c2_1(a559)
| ~ hskp44 ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_384,negated_conjecture,
( c3_1(a555)
| ~ hskp41 ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_385,negated_conjecture,
( c0_1(a555)
| ~ hskp41 ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_386,negated_conjecture,
( c3_1(a551)
| ~ hskp40 ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_387,negated_conjecture,
( c2_1(a551)
| ~ hskp40 ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_388,negated_conjecture,
( c3_1(a549)
| ~ hskp39 ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_389,negated_conjecture,
( c2_1(a549)
| ~ hskp39 ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_390,negated_conjecture,
( c1_1(a549)
| ~ hskp39 ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_391,negated_conjecture,
( c2_1(a547)
| ~ hskp38 ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_392,negated_conjecture,
( c1_1(a547)
| ~ hskp38 ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_393,negated_conjecture,
( c0_1(a547)
| ~ hskp38 ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_394,negated_conjecture,
( c1_1(a544)
| ~ hskp37 ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_398,negated_conjecture,
( c2_1(a538)
| ~ hskp35 ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_399,negated_conjecture,
( c1_1(a538)
| ~ hskp35 ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_400,negated_conjecture,
( c3_1(a538)
| ~ hskp35 ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_401,negated_conjecture,
( c0_1(a537)
| ~ hskp34 ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_402,negated_conjecture,
( c3_1(a537)
| ~ hskp34 ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_403,negated_conjecture,
( c1_1(a536)
| ~ hskp33 ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_404,negated_conjecture,
( c2_1(a536)
| ~ hskp33 ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_405,negated_conjecture,
( c0_1(a536)
| ~ hskp33 ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_406,negated_conjecture,
( c0_1(a596)
| ~ hskp32 ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_407,negated_conjecture,
( c1_1(a591)
| ~ hskp30 ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_408,negated_conjecture,
( c2_1(a589)
| ~ hskp28 ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_409,negated_conjecture,
( c3_1(a589)
| ~ hskp28 ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_410,negated_conjecture,
( c1_1(a586)
| ~ hskp27 ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_411,negated_conjecture,
( c0_1(a584)
| ~ hskp26 ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_412,negated_conjecture,
( c1_1(a584)
| ~ hskp26 ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_413,negated_conjecture,
( c2_1(a581)
| ~ hskp24 ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_414,negated_conjecture,
( c3_1(a578)
| ~ hskp23 ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_415,negated_conjecture,
( c1_1(a577)
| ~ hskp22 ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_417,negated_conjecture,
( c0_1(a572)
| ~ hskp18 ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_418,negated_conjecture,
( c0_1(a571)
| ~ hskp17 ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_419,negated_conjecture,
( c3_1(a571)
| ~ hskp17 ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_420,negated_conjecture,
( c3_1(a570)
| ~ hskp16 ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_421,negated_conjecture,
( c1_1(a570)
| ~ hskp16 ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_426,negated_conjecture,
( c1_1(a560)
| ~ hskp11 ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_428,negated_conjecture,
( c0_1(a550)
| ~ hskp7 ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_429,negated_conjecture,
( c3_1(a550)
| ~ hskp7 ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_430,negated_conjecture,
( c3_1(a548)
| ~ hskp6 ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_431,negated_conjecture,
( c2_1(a546)
| ~ hskp5 ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_432,negated_conjecture,
( c1_1(a545)
| ~ hskp4 ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_435,negated_conjecture,
( c1_1(a535)
| ~ hskp0 ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_436,negated_conjecture,
( c0_1(a535)
| ~ hskp0 ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_438,negated_conjecture,
( ~ hskp51
| ~ c2_1(a583) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_439,negated_conjecture,
( ~ hskp50
| ~ c3_1(a574) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_440,negated_conjecture,
( ~ hskp49
| ~ c0_1(a568) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_441,negated_conjecture,
( ~ hskp49
| ~ c1_1(a568) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_444,negated_conjecture,
( ~ hskp47
| ~ c2_1(a564) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_445,negated_conjecture,
( ~ hskp46
| ~ c3_1(a562) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_446,negated_conjecture,
( ~ hskp46
| ~ c0_1(a562) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_449,negated_conjecture,
( ~ hskp44
| ~ c3_1(a559) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_452,negated_conjecture,
( ~ hskp41
| ~ c2_1(a555) ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_453,negated_conjecture,
( ~ hskp40
| ~ c0_1(a551) ),
inference(cnf_transformation,[],[f145]) ).
tcf(c_454,negated_conjecture,
( ~ hskp37
| ~ c2_1(a544) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_455,negated_conjecture,
( ~ hskp37
| ~ c3_1(a544) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_456,negated_conjecture,
( ~ hskp34
| ~ c1_1(a537) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_457,negated_conjecture,
( ~ hskp32
| ~ c3_1(a596) ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_458,negated_conjecture,
( ~ hskp32
| ~ c2_1(a596) ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_462,negated_conjecture,
( ~ hskp30
| ~ c2_1(a591) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_463,negated_conjecture,
( ~ hskp30
| ~ c0_1(a591) ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_464,negated_conjecture,
( ~ hskp29
| ~ c3_1(a590) ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_465,negated_conjecture,
( ~ hskp29
| ~ c0_1(a590) ),
inference(cnf_transformation,[],[f157]) ).
tcf(c_466,negated_conjecture,
( ~ hskp29
| ~ c1_1(a590) ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_467,negated_conjecture,
( ~ hskp28
| ~ c0_1(a589) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_468,negated_conjecture,
( ~ hskp27
| ~ c0_1(a586) ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_469,negated_conjecture,
( ~ hskp27
| ~ c3_1(a586) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_470,negated_conjecture,
( ~ hskp26
| ~ c3_1(a584) ),
inference(cnf_transformation,[],[f162]) ).
tcf(c_471,negated_conjecture,
( ~ hskp25
| ~ c3_1(a582) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_472,negated_conjecture,
( ~ hskp25
| ~ c2_1(a582) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_473,negated_conjecture,
( ~ hskp25
| ~ c1_1(a582) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_474,negated_conjecture,
( ~ hskp24
| ~ c1_1(a581) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_475,negated_conjecture,
( ~ hskp24
| ~ c3_1(a581) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_476,negated_conjecture,
( ~ hskp23
| ~ c0_1(a578) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_477,negated_conjecture,
( ~ hskp23
| ~ c1_1(a578) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_478,negated_conjecture,
( ~ hskp22
| ~ c3_1(a577) ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_479,negated_conjecture,
( ~ hskp22
| ~ c0_1(a577) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_485,negated_conjecture,
( ~ hskp19
| ~ c2_1(a573) ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_486,negated_conjecture,
( ~ hskp19
| ~ c0_1(a573) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_487,negated_conjecture,
( ~ hskp19
| ~ c1_1(a573) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_488,negated_conjecture,
( ~ hskp18
| ~ c3_1(a572) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_489,negated_conjecture,
( ~ hskp18
| ~ c1_1(a572) ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_490,negated_conjecture,
( ~ hskp17
| ~ c2_1(a571) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_491,negated_conjecture,
( ~ hskp16
| ~ c0_1(a570) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_492,negated_conjecture,
( ~ hskp15
| ~ c0_1(a569) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_493,negated_conjecture,
( ~ hskp15
| ~ c1_1(a569) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_494,negated_conjecture,
( ~ hskp15
| ~ c2_1(a569) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_500,negated_conjecture,
( ~ hskp11
| ~ c3_1(a560) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_501,negated_conjecture,
( ~ hskp11
| ~ c0_1(a560) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_502,negated_conjecture,
( ~ hskp10
| ~ c1_1(a558) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_503,negated_conjecture,
( ~ hskp10
| ~ c0_1(a558) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_504,negated_conjecture,
( ~ hskp9
| ~ c0_1(a554) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_505,negated_conjecture,
( ~ hskp9
| ~ c2_1(a554) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_506,negated_conjecture,
( ~ hskp9
| ~ c1_1(a554) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_507,negated_conjecture,
( ~ hskp8
| ~ c3_1(a552) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_508,negated_conjecture,
( ~ hskp8
| ~ c1_1(a552) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_509,negated_conjecture,
( ~ hskp8
| ~ c2_1(a552) ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_510,negated_conjecture,
( ~ hskp7
| ~ c1_1(a550) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_511,negated_conjecture,
( ~ hskp6
| ~ c2_1(a548) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_512,negated_conjecture,
( ~ hskp6
| ~ c0_1(a548) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_513,negated_conjecture,
( ~ hskp5
| ~ c3_1(a546) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_514,negated_conjecture,
( ~ hskp5
| ~ c1_1(a546) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_515,negated_conjecture,
( ~ hskp4
| ~ c2_1(a545) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_516,negated_conjecture,
( ~ hskp4
| ~ c0_1(a545) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_524,negated_conjecture,
( ~ hskp0
| ~ c2_1(a535) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_525,negated_conjecture,
! [X0: $i] :
( hskp28
| c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_526,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp44
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_528,negated_conjecture,
! [X0: $i] :
( hskp19
| hskp50
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_529,negated_conjecture,
! [X0: $i] :
( hskp24
| hskp39
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_530,negated_conjecture,
! [X0: $i] :
( hskp29
| hskp30
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_531,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp40
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_532,negated_conjecture,
! [X0: $i] :
( hskp9
| hskp41
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_534,negated_conjecture,
! [X0: $i] :
( hskp22
| hskp23
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_536,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c3_1(X1)
| c0_1(X0)
| c1_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_538,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp33
| c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_539,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp6
| c0_1(X1)
| c0_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_542,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp51
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_543,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp26
| c3_1(X0)
| c0_1(X1)
| c0_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_544,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_545,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_546,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_547,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp37
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_548,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp5
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_549,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp39
| c3_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_550,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp8
| c0_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f242]) ).
tcf(c_552,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp49
| c3_1(X0)
| c2_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_553,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp15
| c3_1(X1)
| c1_1(X0)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_554,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_555,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp4
| c3_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_556,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c0_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_557,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp47
| c3_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_558,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c3_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_560,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp32
| c3_1(X1)
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f252]) ).
tcf(c_561,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_563,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp10
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_564,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp25
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_565,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c0_1(X2)
| c0_1(X0)
| c1_1(X2)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X2)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_566,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c1_1(X2)
| c1_1(X0)
| c2_1(X2)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_567,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c1_1(X2)
| c1_1(X0)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_568,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c2_1(X2)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X2)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_583,negated_conjecture,
ndr1_0,
inference(global_subsumption_just,[status(thm)],[c_361,c_362,c_358,c_327,c_325]) ).
tcf(c_689,negated_conjecture,
! [X0: $i] :
( hskp28
| c0_1(X0)
| c1_1(X0)
| c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_525,c_362,c_358,c_327,c_325,c_525]) ).
tcf(c_692,negated_conjecture,
! [X0: $i] :
( hskp29
| hskp30
| c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_530,c_362,c_358,c_327,c_325,c_530]) ).
tcf(c_695,negated_conjecture,
! [X0: $i] :
( hskp24
| hskp39
| c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_529,c_362,c_358,c_327,c_325,c_529]) ).
tcf(c_698,negated_conjecture,
! [X0: $i] :
( hskp19
| hskp50
| c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_528,c_362,c_358,c_327,c_325,c_528]) ).
tcf(c_704,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp44
| c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_526,c_362,c_358,c_327,c_325,c_526]) ).
tcf(c_707,plain,
! [X0: $i] :
( hskp22
| hskp23
| c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_534,c_362,c_358,c_327,c_325,c_534]) ).
tcf(c_708,negated_conjecture,
! [X0: $i] :
( hskp22
| hskp23
| c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_707]) ).
tcf(c_713,plain,
! [X0: $i] :
( hskp9
| hskp41
| c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_532,c_362,c_358,c_327,c_325,c_532]) ).
tcf(c_714,negated_conjecture,
! [X0: $i] :
( hskp9
| hskp41
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_713]) ).
tcf(c_716,plain,
! [X0: $i] :
( hskp7
| hskp40
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_531,c_362,c_358,c_327,c_325,c_531]) ).
tcf(c_717,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp40
| c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_716]) ).
tcf(c_724,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c3_1(X1)
| c0_1(X0)
| c1_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_536,c_362,c_358,c_327,c_325,c_536]) ).
tcf(c_726,plain,
! [X0: $i,X1: $i] :
( hskp26
| c3_1(X0)
| c0_1(X1)
| c0_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_543,c_362,c_358,c_327,c_325,c_543]) ).
tcf(c_727,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp26
| c3_1(X0)
| c0_1(X1)
| c0_1(X0)
| c1_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_726]) ).
tcf(c_728,plain,
! [X0: $i,X1: $i] :
( hskp51
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| c2_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_542,c_362,c_358,c_327,c_325,c_542]) ).
tcf(c_729,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp51
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_728]) ).
tcf(c_734,plain,
! [X0: $i,X1: $i] :
( hskp6
| c0_1(X1)
| c0_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_539,c_362,c_358,c_327,c_325,c_539]) ).
tcf(c_735,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp6
| c0_1(X1)
| c0_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_734]) ).
tcf(c_736,plain,
! [X0: $i,X1: $i] :
( hskp33
| c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_538,c_362,c_358,c_327,c_325,c_538]) ).
tcf(c_737,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp33
| c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_736]) ).
tcf(c_738,plain,
! [X0: $i,X1: $i] :
( hskp46
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_554,c_362,c_358,c_327,c_325,c_554]) ).
tcf(c_739,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_738]) ).
tcf(c_741,plain,
! [X0: $i,X1: $i] :
( hskp15
| c3_1(X1)
| c1_1(X0)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_553,c_362,c_358,c_327,c_325,c_553]) ).
tcf(c_742,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp15
| c3_1(X1)
| c1_1(X0)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_741]) ).
tcf(c_743,plain,
! [X0: $i,X1: $i] :
( hskp49
| c3_1(X0)
| c2_1(X1)
| c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_552,c_362,c_358,c_327,c_325,c_552]) ).
tcf(c_744,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp49
| c3_1(X0)
| c2_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_743]) ).
tcf(c_747,plain,
! [X0: $i,X1: $i] :
( hskp8
| c0_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_550,c_362,c_358,c_327,c_325,c_550]) ).
tcf(c_748,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp8
| c0_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_747]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i] :
( hskp39
| c3_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_549,c_362,c_358,c_327,c_325,c_549]) ).
tcf(c_750,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp39
| c3_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_749]) ).
tcf(c_751,plain,
! [X0: $i,X1: $i] :
( hskp5
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_548,c_362,c_358,c_327,c_325,c_548]) ).
tcf(c_752,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp5
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_751]) ).
tcf(c_753,plain,
! [X0: $i,X1: $i] :
( hskp37
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_547,c_362,c_358,c_327,c_325,c_547]) ).
tcf(c_754,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp37
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_753]) ).
tcf(c_756,plain,
! [X0: $i,X1: $i] :
( hskp35
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_546,c_362,c_358,c_327,c_325,c_546]) ).
tcf(c_757,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_756]) ).
tcf(c_758,plain,
! [X0: $i,X1: $i] :
( hskp34
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_545,c_362,c_358,c_327,c_325,c_545]) ).
tcf(c_759,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_758]) ).
tcf(c_760,plain,
! [X0: $i,X1: $i] :
( hskp0
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_544,c_362,c_358,c_327,c_325,c_544]) ).
tcf(c_761,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_760]) ).
tcf(c_762,plain,
! [X0: $i,X1: $i] :
( hskp32
| c3_1(X1)
| c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_560,c_362,c_358,c_327,c_325,c_560]) ).
tcf(c_763,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp32
| c3_1(X1)
| c3_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_762]) ).
tcf(c_767,plain,
! [X0: $i,X1: $i] :
( hskp34
| c3_1(X1)
| c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_558,c_362,c_358,c_327,c_325,c_558]) ).
tcf(c_768,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c3_1(X1)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_767]) ).
tcf(c_769,plain,
! [X0: $i,X1: $i] :
( hskp47
| c3_1(X0)
| c0_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_557,c_362,c_358,c_327,c_325,c_557]) ).
tcf(c_770,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp47
| c3_1(X0)
| c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_769]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i] :
( hskp46
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_556,c_362,c_358,c_327,c_325,c_556]) ).
tcf(c_772,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c0_1(X1)
| c1_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_771]) ).
tcf(c_773,plain,
! [X0: $i,X1: $i] :
( hskp4
| c3_1(X1)
| c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_555,c_362,c_358,c_327,c_325,c_555]) ).
tcf(c_774,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp4
| c3_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_773]) ).
tcf(c_775,plain,
! [X0: $i,X1: $i] :
( hskp25
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_564,c_362,c_358,c_327,c_325,c_564]) ).
tcf(c_776,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp25
| c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_775]) ).
tcf(c_777,plain,
! [X0: $i,X1: $i] :
( hskp10
| c0_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_563,c_563,c_583]) ).
tcf(c_778,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp10
| c0_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_777]) ).
tcf(c_781,plain,
! [X0: $i,X1: $i] :
( hskp38
| c1_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_561,c_362,c_358,c_327,c_325,c_561]) ).
tcf(c_782,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c1_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_781]) ).
tcf(c_783,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c1_1(X2)
| c1_1(X0)
| c2_1(X2)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_566,c_362,c_358,c_327,c_325,c_566]) ).
tcf(c_784,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c1_1(X2)
| c1_1(X0)
| c2_1(X2)
| c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_783]) ).
tcf(c_785,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c0_1(X2)
| c0_1(X0)
| c1_1(X2)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_565,c_362,c_358,c_327,c_325,c_565]) ).
tcf(c_786,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c0_1(X2)
| c0_1(X0)
| c1_1(X2)
| c2_1(X1)
| ~ c3_1(X2)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_785]) ).
tcf(c_787,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c1_1(X2)
| c1_1(X0)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X2)
| ~ c3_1(X1)
| ~ c3_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_567,c_362,c_358,c_327,c_325,c_567]) ).
tcf(c_788,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X0)
| c1_1(X2)
| c1_1(X0)
| c2_1(X1)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_787]) ).
tcf(c_789,plain,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c2_1(X2)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_568,c_362,c_358,c_327,c_325,c_568]) ).
tcf(c_790,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c2_1(X2)
| c2_1(X1)
| ~ c3_1(X2)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_789]) ).
tcf(c_2117,plain,
( hskp4
| hskp6
| ~ c3_1(a586) ),
inference(resolution,[status(thm)],[c_364,c_469]) ).
tcf(c_2127,plain,
( hskp4
| hskp6
| ~ c0_1(a586) ),
inference(resolution,[status(thm)],[c_364,c_468]) ).
tcf(c_2137,plain,
( hskp4
| hskp6
| c1_1(a586) ),
inference(resolution,[status(thm)],[c_364,c_410]) ).
tcf(c_2156,plain,
( hskp16
| hskp17
| ~ c1_1(a572) ),
inference(resolution,[status(thm)],[c_363,c_489]) ).
tcf(c_2166,plain,
( hskp16
| hskp17
| ~ c3_1(a572) ),
inference(resolution,[status(thm)],[c_363,c_488]) ).
tcf(c_2176,plain,
( hskp16
| hskp17
| c0_1(a572) ),
inference(resolution,[status(thm)],[c_363,c_417]) ).
tcf(c_5330,plain,
( hskp17
| c0_1(a572)
| ~ c0_1(a570) ),
inference(resolution,[status(thm)],[c_2176,c_491]) ).
tcf(c_5340,plain,
( hskp17
| c0_1(a572)
| c1_1(a570) ),
inference(resolution,[status(thm)],[c_2176,c_421]) ).
tcf(c_5350,plain,
( hskp17
| c3_1(a570)
| c0_1(a572) ),
inference(resolution,[status(thm)],[c_2176,c_420]) ).
tcf(c_5360,plain,
( hskp17
| ~ c3_1(a572)
| ~ c0_1(a570) ),
inference(resolution,[status(thm)],[c_2166,c_491]) ).
tcf(c_5370,plain,
( hskp17
| c1_1(a570)
| ~ c3_1(a572) ),
inference(resolution,[status(thm)],[c_2166,c_421]) ).
tcf(c_5380,plain,
( hskp17
| c3_1(a570)
| ~ c3_1(a572) ),
inference(resolution,[status(thm)],[c_2166,c_420]) ).
tcf(c_5390,plain,
( hskp17
| ~ c0_1(a570)
| ~ c1_1(a572) ),
inference(resolution,[status(thm)],[c_2156,c_491]) ).
tcf(c_5400,plain,
( hskp17
| c1_1(a570)
| ~ c1_1(a572) ),
inference(resolution,[status(thm)],[c_2156,c_421]) ).
tcf(c_5410,plain,
( hskp17
| c3_1(a570)
| ~ c1_1(a572) ),
inference(resolution,[status(thm)],[c_2156,c_420]) ).
tcf(c_6278,plain,
( hskp6
| c1_1(a586)
| ~ c0_1(a545) ),
inference(resolution,[status(thm)],[c_2137,c_516]) ).
tcf(c_6288,plain,
( hskp6
| c1_1(a586)
| ~ c2_1(a545) ),
inference(resolution,[status(thm)],[c_2137,c_515]) ).
tcf(c_6298,plain,
( hskp6
| c1_1(a545)
| c1_1(a586) ),
inference(resolution,[status(thm)],[c_2137,c_432]) ).
tcf(c_6308,plain,
( hskp6
| ~ c0_1(a545)
| ~ c0_1(a586) ),
inference(resolution,[status(thm)],[c_2127,c_516]) ).
tcf(c_6318,plain,
( hskp6
| ~ c0_1(a586)
| ~ c2_1(a545) ),
inference(resolution,[status(thm)],[c_2127,c_515]) ).
tcf(c_6328,plain,
( hskp6
| c1_1(a545)
| ~ c0_1(a586) ),
inference(resolution,[status(thm)],[c_2127,c_432]) ).
tcf(c_6338,plain,
( hskp6
| ~ c3_1(a586)
| ~ c0_1(a545) ),
inference(resolution,[status(thm)],[c_2117,c_516]) ).
tcf(c_6348,plain,
( hskp6
| ~ c3_1(a586)
| ~ c2_1(a545) ),
inference(resolution,[status(thm)],[c_2117,c_515]) ).
tcf(c_6358,plain,
( hskp6
| c1_1(a545)
| ~ c3_1(a586) ),
inference(resolution,[status(thm)],[c_2117,c_432]) ).
tcf(c_13053,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_790]) ).
tcf(c_13054,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_790]) ).
tcf(c_13055,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_790]) ).
tcf(c_13056,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_790]) ).
tcf(c_13057,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_788]) ).
tcf(c_13058,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_788]) ).
tcf(c_13059,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_788]) ).
tcf(c_13060,negated_conjecture,
( iPr_def_15
| iPr_def_14
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_788]) ).
tcf(c_13061,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_786]) ).
tcf(c_13062,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| ~ c2_1(X0)
| c0_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_786]) ).
tcf(c_13063,negated_conjecture,
( iPr_def_17
| iPr_def_16
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_786]) ).
tcf(c_13064,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_784]) ).
tcf(c_13065,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| c2_1(X0)
| c1_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_784]) ).
tcf(c_13066,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_784]) ).
tcf(c_13067,negated_conjecture,
( iPr_def_20
| iPr_def_19
| iPr_def_18 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_784]) ).
tcf(c_13068,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_21
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_782]) ).
tcf(c_13071,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_778]) ).
tcf(c_13072,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_778]) ).
tcf(c_13073,negated_conjecture,
( iPr_def_23
| iPr_def_22
| hskp10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_778]) ).
tcf(c_13074,negated_conjecture,
( iPr_def_21
| iPr_def_18
| hskp25 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_776]) ).
tcf(c_13075,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_24
| ~ c1_1(X0)
| c0_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_774]) ).
tcf(c_13076,negated_conjecture,
( iPr_def_24
| iPr_def_21
| hskp4 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_774]) ).
tcf(c_13077,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_25
| ~ c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_25])],[c_772]) ).
tcf(c_13079,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_26
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_26])],[c_770]) ).
tcf(c_13080,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_27
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_770]) ).
tcf(c_13081,negated_conjecture,
( iPr_def_27
| iPr_def_26
| hskp47 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_770]) ).
tcf(c_13082,negated_conjecture,
( iPr_def_24
| iPr_def_12
| hskp34 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_768]) ).
tcf(c_13084,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_28
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_763]) ).
tcf(c_13085,negated_conjecture,
( iPr_def_28
| iPr_def_27
| hskp32 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_763]) ).
tcf(c_13086,negated_conjecture,
( iPr_def_19
| iPr_def_12
| hskp0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_761]) ).
tcf(c_13087,negated_conjecture,
( iPr_def_21
| iPr_def_19
| hskp34 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_759]) ).
tcf(c_13088,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_29
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_757]) ).
tcf(c_13089,negated_conjecture,
( iPr_def_29
| iPr_def_27
| hskp35 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_757]) ).
tcf(c_13090,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_30
| c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_754]) ).
tcf(c_13091,negated_conjecture,
( iPr_def_30
| iPr_def_25
| hskp37 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_754]) ).
tcf(c_13092,negated_conjecture,
( iPr_def_27
| iPr_def_11
| hskp5 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_752]) ).
tcf(c_13093,negated_conjecture,
( iPr_def_24
| iPr_def_18
| hskp39 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_750]) ).
tcf(c_13094,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_31
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_31])],[c_748]) ).
tcf(c_13095,negated_conjecture,
( iPr_def_31
| iPr_def_14
| hskp8 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_748]) ).
tcf(c_13097,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_32
| c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_32])],[c_744]) ).
tcf(c_13098,negated_conjecture,
( iPr_def_32
| iPr_def_13
| hskp49 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_744]) ).
tcf(c_13099,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_33
| c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_33])],[c_742]) ).
tcf(c_13100,negated_conjecture,
( iPr_def_33
| iPr_def_20
| hskp15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_742]) ).
tcf(c_13101,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_34
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_34])],[c_739]) ).
tcf(c_13102,negated_conjecture,
( iPr_def_34
| iPr_def_18
| hskp46 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_739]) ).
tcf(c_13103,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_35
| c2_1(X0)
| c0_1(X0)
| c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_35])],[c_737]) ).
tcf(c_13104,negated_conjecture,
( iPr_def_35
| iPr_def_28
| hskp33 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_737]) ).
tcf(c_13105,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_36
| c2_1(X0)
| c1_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_36])],[c_735]) ).
tcf(c_13106,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_37
| ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_37])],[c_735]) ).
tcf(c_13107,negated_conjecture,
( iPr_def_37
| iPr_def_36
| hskp6 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_735]) ).
tcf(c_13110,negated_conjecture,
( iPr_def_19
| iPr_def_14
| hskp51 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_729]) ).
tcf(c_13111,negated_conjecture,
( iPr_def_24
| iPr_def_16
| hskp26 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_727]) ).
tcf(c_13112,negated_conjecture,
( iPr_def_34
| iPr_def_19
| hskp38 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_724]) ).
tcf(c_13117,negated_conjecture,
( iPr_def_25
| hskp7
| hskp40 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_717]) ).
tcf(c_13118,negated_conjecture,
( iPr_def_37
| hskp9
| hskp41 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_714]) ).
tcf(c_13120,negated_conjecture,
( iPr_def_28
| hskp22
| hskp23 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_708]) ).
tcf(c_13121,negated_conjecture,
( iPr_def_34
| hskp11
| hskp44 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_704]) ).
tcf(c_13123,negated_conjecture,
( iPr_def_29
| hskp19
| hskp50 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_698]) ).
tcf(c_13124,negated_conjecture,
( iPr_def_32
| hskp24
| hskp39 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_695]) ).
tcf(c_13125,negated_conjecture,
( iPr_def_11
| hskp29
| hskp30 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_692]) ).
tcf(c_13141,plain,
( c2_1(a535)
| ~ iPr_def_10
| ~ c0_1(a535)
| ~ c1_1(a535) ),
inference(instantiation,[status(thm)],[c_13053]) ).
tcf(c_13157,plain,
( c2_1(a564)
| ~ iPr_def_10
| ~ c0_1(a564)
| ~ c1_1(a564) ),
inference(instantiation,[status(thm)],[c_13053]) ).
tcf(c_13164,plain,
( c2_1(a584)
| ~ iPr_def_10
| ~ c0_1(a584)
| ~ c1_1(a584) ),
inference(instantiation,[status(thm)],[c_13053]) ).
tcf(c_13171,plain,
( ~ iPr_def_12
| ~ c0_1(a547)
| ~ c1_1(a547)
| ~ c2_1(a547) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_13173,plain,
( ~ iPr_def_12
| ~ c0_1(a536)
| ~ c1_1(a536)
| ~ c2_1(a536) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_13175,plain,
( ~ iPr_def_12
| ~ c0_1(a584)
| ~ c1_1(a584)
| ~ c2_1(a584) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_13177,plain,
( ~ iPr_def_12
| ~ c0_1(a550)
| ~ c1_1(a550)
| ~ c2_1(a550) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_13178,plain,
( c2_1(a583)
| ~ iPr_def_13
| ~ c3_1(a583)
| ~ c0_1(a583) ),
inference(instantiation,[status(thm)],[c_13057]) ).
tcf(c_13181,plain,
( c2_1(a555)
| ~ iPr_def_13
| ~ c3_1(a555)
| ~ c0_1(a555) ),
inference(instantiation,[status(thm)],[c_13057]) ).
tcf(c_13183,plain,
( c2_1(a537)
| ~ iPr_def_13
| ~ c3_1(a537)
| ~ c0_1(a537) ),
inference(instantiation,[status(thm)],[c_13057]) ).
tcf(c_13189,plain,
( c2_1(a583)
| ~ iPr_def_18
| ~ c3_1(a583)
| ~ c1_1(a583) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_13191,plain,
( c2_1(a555)
| ~ iPr_def_18
| ~ c3_1(a555)
| ~ c1_1(a555) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_13195,plain,
( c2_1(a570)
| ~ iPr_def_18
| ~ c3_1(a570)
| ~ c1_1(a570) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_13199,plain,
( c2_1(a548)
| ~ iPr_def_18
| ~ c3_1(a548)
| ~ c1_1(a548) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_13205,plain,
( c0_1(a589)
| ~ iPr_def_26
| ~ c3_1(a589)
| ~ c2_1(a589) ),
inference(instantiation,[status(thm)],[c_13079]) ).
tcf(c_13216,plain,
( c0_1(a589)
| c1_1(a589)
| ~ iPr_def_16
| ~ c3_1(a589) ),
inference(instantiation,[status(thm)],[c_13061]) ).
tcf(c_13217,plain,
( c0_1(a570)
| c1_1(a570)
| ~ iPr_def_16
| ~ c3_1(a570) ),
inference(instantiation,[status(thm)],[c_13061]) ).
tcf(c_13221,plain,
( c0_1(a548)
| c1_1(a548)
| ~ iPr_def_16
| ~ c3_1(a548) ),
inference(instantiation,[status(thm)],[c_13061]) ).
tcf(c_13226,plain,
( c3_1(a573)
| c1_1(a573)
| c2_1(a573)
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_13065]) ).
tcf(c_13227,plain,
( c3_1(a569)
| c1_1(a569)
| c2_1(a569)
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_13065]) ).
tcf(c_13230,plain,
( c3_1(a545)
| c1_1(a545)
| c2_1(a545)
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_13065]) ).
tcf(c_13234,plain,
( c1_1(a555)
| ~ iPr_def_14
| ~ c3_1(a555)
| ~ c0_1(a555) ),
inference(instantiation,[status(thm)],[c_13058]) ).
tcf(c_13236,plain,
( c1_1(a537)
| ~ iPr_def_14
| ~ c3_1(a537)
| ~ c0_1(a537) ),
inference(instantiation,[status(thm)],[c_13058]) ).
tcf(c_13241,plain,
( c1_1(a550)
| ~ iPr_def_14
| ~ c3_1(a550)
| ~ c0_1(a550) ),
inference(instantiation,[status(thm)],[c_13058]) ).
tcf(c_13253,plain,
( ~ iPr_def_12
| ~ c0_1(a538)
| ~ c1_1(a538)
| ~ c2_1(a538) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_13261,plain,
( c3_1(a584)
| ~ iPr_def_27
| ~ c1_1(a584)
| ~ c2_1(a584) ),
inference(instantiation,[status(thm)],[c_13080]) ).
tcf(c_13263,plain,
( c3_1(a577)
| ~ iPr_def_27
| ~ c1_1(a577)
| ~ c2_1(a577) ),
inference(instantiation,[status(thm)],[c_13080]) ).
tcf(c_13271,plain,
( c3_1(a582)
| c1_1(a582)
| c2_1(a582)
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_13065]) ).
tcf(c_13274,plain,
( c3_1(a562)
| c0_1(a562)
| ~ iPr_def_24
| ~ c1_1(a562) ),
inference(instantiation,[status(thm)],[c_13075]) ).
tcf(c_13275,plain,
( c3_1(a544)
| c0_1(a544)
| ~ iPr_def_24
| ~ c1_1(a544) ),
inference(instantiation,[status(thm)],[c_13075]) ).
tcf(c_13285,plain,
( c3_1(a560)
| c0_1(a560)
| ~ iPr_def_24
| ~ c1_1(a560) ),
inference(instantiation,[status(thm)],[c_13075]) ).
tcf(c_13291,plain,
( c1_1(a537)
| c2_1(a537)
| ~ iPr_def_29
| ~ c0_1(a537) ),
inference(instantiation,[status(thm)],[c_13088]) ).
tcf(c_13295,plain,
( c1_1(a550)
| c2_1(a550)
| ~ iPr_def_29
| ~ c0_1(a550) ),
inference(instantiation,[status(thm)],[c_13088]) ).
tcf(c_13303,plain,
( c3_1(a590)
| c0_1(a590)
| ~ iPr_def_17
| ~ c2_1(a590) ),
inference(instantiation,[status(thm)],[c_13062]) ).
tcf(c_13306,plain,
( c3_1(a577)
| c0_1(a577)
| ~ iPr_def_17
| ~ c2_1(a577) ),
inference(instantiation,[status(thm)],[c_13062]) ).
tcf(c_13315,plain,
( ~ iPr_def_12
| ~ c0_1(a559)
| ~ c1_1(a559)
| ~ c2_1(a559) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_13319,plain,
( c3_1(a559)
| ~ iPr_def_27
| ~ c1_1(a559)
| ~ c2_1(a559) ),
inference(instantiation,[status(thm)],[c_13080]) ).
tcf(c_13330,plain,
( c2_1(a545)
| ~ iPr_def_18
| ~ c3_1(a545)
| ~ c1_1(a545) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_13333,plain,
( c1_1(a559)
| ~ iPr_def_25
| ~ c0_1(a559)
| ~ c2_1(a559) ),
inference(instantiation,[status(thm)],[c_13077]) ).
tcf(c_13335,plain,
( c1_1(a537)
| ~ iPr_def_25
| ~ c0_1(a537)
| ~ c2_1(a537) ),
inference(instantiation,[status(thm)],[c_13077]) ).
tcf(c_13338,plain,
( c1_1(a550)
| ~ iPr_def_25
| ~ c0_1(a550)
| ~ c2_1(a550) ),
inference(instantiation,[status(thm)],[c_13077]) ).
tcf(c_13352,plain,
( c2_1(a544)
| ~ iPr_def_10
| ~ c0_1(a544)
| ~ c1_1(a544) ),
inference(instantiation,[status(thm)],[c_13053]) ).
tcf(c_13410,plain,
( c1_1(a555)
| c2_1(a555)
| ~ iPr_def_11
| ~ c3_1(a555) ),
inference(instantiation,[status(thm)],[c_13054]) ).
tcf(c_13413,plain,
( c1_1(a569)
| c2_1(a569)
| ~ iPr_def_11
| ~ c3_1(a569) ),
inference(instantiation,[status(thm)],[c_13054]) ).
tcf(c_13416,plain,
( c1_1(a548)
| c2_1(a548)
| ~ iPr_def_11
| ~ c3_1(a548) ),
inference(instantiation,[status(thm)],[c_13054]) ).
tcf(c_13422,plain,
( c1_1(a555)
| c2_1(a555)
| ~ iPr_def_29
| ~ c0_1(a555) ),
inference(instantiation,[status(thm)],[c_13088]) ).
tcf(c_13433,plain,
( c3_1(a559)
| c1_1(a559)
| ~ iPr_def_30
| ~ c0_1(a559) ),
inference(instantiation,[status(thm)],[c_13090]) ).
tcf(c_13451,plain,
( c0_1(a570)
| ~ iPr_def_22
| ~ c1_1(a570)
| ~ c2_1(a570) ),
inference(instantiation,[status(thm)],[c_13071]) ).
tcf(c_13490,plain,
( c3_1(a544)
| ~ iPr_def_28
| ~ c0_1(a544)
| ~ c1_1(a544) ),
inference(instantiation,[status(thm)],[c_13084]) ).
tcf(c_13492,plain,
( c3_1(a584)
| ~ iPr_def_28
| ~ c0_1(a584)
| ~ c1_1(a584) ),
inference(instantiation,[status(thm)],[c_13084]) ).
tcf(c_13526,plain,
( c1_1(a570)
| c2_1(a570)
| ~ iPr_def_29
| ~ c0_1(a570) ),
inference(instantiation,[status(thm)],[c_13088]) ).
tcf(c_13534,plain,
( c3_1(a572)
| c1_1(a572)
| ~ iPr_def_30
| ~ c0_1(a572) ),
inference(instantiation,[status(thm)],[c_13090]) ).
tcf(c_13538,plain,
( hskp28
| c0_1(a558)
| c1_1(a558)
| c2_1(a558) ),
inference(instantiation,[status(thm)],[c_689]) ).
tcf(c_13575,plain,
( c3_1(a545)
| c0_1(a545)
| ~ iPr_def_24
| ~ c1_1(a545) ),
inference(instantiation,[status(thm)],[c_13075]) ).
tcf(c_13594,plain,
( c0_1(a568)
| c1_1(a568)
| ~ iPr_def_31
| ~ c2_1(a568) ),
inference(instantiation,[status(thm)],[c_13094]) ).
tcf(c_13596,plain,
( c0_1(a589)
| c1_1(a589)
| ~ iPr_def_31
| ~ c2_1(a589) ),
inference(instantiation,[status(thm)],[c_13094]) ).
tcf(c_13603,plain,
( c0_1(a558)
| c1_1(a558)
| ~ iPr_def_31
| ~ c2_1(a558) ),
inference(instantiation,[status(thm)],[c_13094]) ).
tcf(c_13615,plain,
( c0_1(a554)
| c1_1(a554)
| c2_1(a554)
| ~ iPr_def_36 ),
inference(instantiation,[status(thm)],[c_13105]) ).
tcf(c_13635,plain,
( c3_1(a586)
| c0_1(a586)
| ~ iPr_def_24
| ~ c1_1(a586) ),
inference(instantiation,[status(thm)],[c_13075]) ).
tcf(c_13660,plain,
( c3_1(a584)
| c2_1(a584)
| ~ iPr_def_33
| ~ c1_1(a584) ),
inference(instantiation,[status(thm)],[c_13099]) ).
tcf(c_13679,plain,
( c2_1(a591)
| ~ iPr_def_18
| ~ c3_1(a591)
| ~ c1_1(a591) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_13686,plain,
( c0_1(a551)
| ~ iPr_def_37
| ~ c3_1(a551)
| ~ c1_1(a551) ),
inference(instantiation,[status(thm)],[c_13106]) ).
tcf(c_13688,plain,
( c0_1(a589)
| ~ iPr_def_37
| ~ c3_1(a589)
| ~ c1_1(a589) ),
inference(instantiation,[status(thm)],[c_13106]) ).
tcf(c_13693,plain,
( c0_1(a570)
| ~ iPr_def_37
| ~ c3_1(a570)
| ~ c1_1(a570) ),
inference(instantiation,[status(thm)],[c_13106]) ).
tcf(c_13780,plain,
( c2_1(a571)
| ~ iPr_def_13
| ~ c3_1(a571)
| ~ c0_1(a571) ),
inference(instantiation,[status(thm)],[c_13057]) ).
tcf(c_13782,plain,
( c1_1(a571)
| c2_1(a571)
| ~ iPr_def_29
| ~ c0_1(a571) ),
inference(instantiation,[status(thm)],[c_13088]) ).
tcf(c_13785,plain,
( c2_1(a571)
| ~ iPr_def_18
| ~ c3_1(a571)
| ~ c1_1(a571) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_13791,plain,
( c3_1(a568)
| ~ iPr_def_27
| ~ c1_1(a568)
| ~ c2_1(a568) ),
inference(instantiation,[status(thm)],[c_13080]) ).
tcf(c_13802,plain,
( c0_1(a578)
| c2_1(a578)
| ~ iPr_def_34
| ~ c3_1(a578) ),
inference(instantiation,[status(thm)],[c_13101]) ).
tcf(c_13809,plain,
( c1_1(a578)
| c2_1(a578)
| ~ iPr_def_11
| ~ c3_1(a578) ),
inference(instantiation,[status(thm)],[c_13054]) ).
tcf(c_13872,plain,
( c1_1(a572)
| c2_1(a572)
| ~ iPr_def_29
| ~ c0_1(a572) ),
inference(instantiation,[status(thm)],[c_13088]) ).
tcf(c_13876,plain,
( c3_1(a572)
| c1_1(a572)
| c2_1(a572)
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_13065]) ).
tcf(c_13903,plain,
( ~ iPr_def_21
| ~ c3_1(a545)
| ~ c1_1(a545)
| ~ c2_1(a545) ),
inference(instantiation,[status(thm)],[c_13068]) ).
tcf(c_13905,plain,
( c0_1(a545)
| c2_1(a545)
| ~ iPr_def_34
| ~ c3_1(a545) ),
inference(instantiation,[status(thm)],[c_13101]) ).
tcf(c_13908,plain,
( c3_1(a545)
| c2_1(a545)
| ~ iPr_def_33
| ~ c1_1(a545) ),
inference(instantiation,[status(thm)],[c_13099]) ).
tcf(c_13971,plain,
( c1_1(a572)
| ~ iPr_def_25
| ~ c0_1(a572)
| ~ c2_1(a572) ),
inference(instantiation,[status(thm)],[c_13077]) ).
tcf(c_14035,plain,
( c1_1(a537)
| c2_1(a537)
| ~ iPr_def_11
| ~ c3_1(a537) ),
inference(instantiation,[status(thm)],[c_13054]) ).
tcf(c_14077,plain,
( c3_1(a544)
| c2_1(a544)
| ~ iPr_def_33
| ~ c1_1(a544) ),
inference(instantiation,[status(thm)],[c_13099]) ).
tcf(c_14099,plain,
( c3_1(a573)
| c0_1(a573)
| c2_1(a573)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_13103]) ).
tcf(c_14102,plain,
( c3_1(a545)
| c0_1(a545)
| c2_1(a545)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_13103]) ).
tcf(c_14106,plain,
( c0_1(a551)
| c1_1(a551)
| ~ iPr_def_16
| ~ c3_1(a551) ),
inference(instantiation,[status(thm)],[c_13061]) ).
tcf(c_14109,plain,
( c0_1(a573)
| c1_1(a573)
| ~ iPr_def_16
| ~ c3_1(a573) ),
inference(instantiation,[status(thm)],[c_13061]) ).
tcf(c_14110,plain,
( c0_1(a569)
| c1_1(a569)
| ~ iPr_def_16
| ~ c3_1(a569) ),
inference(instantiation,[status(thm)],[c_13061]) ).
tcf(c_14116,plain,
( c0_1(a549)
| ~ iPr_def_37
| ~ c3_1(a549)
| ~ c1_1(a549) ),
inference(instantiation,[status(thm)],[c_13106]) ).
tcf(c_14121,plain,
( ~ iPr_def_21
| ~ c3_1(a549)
| ~ c1_1(a549)
| ~ c2_1(a549) ),
inference(instantiation,[status(thm)],[c_13068]) ).
tcf(c_14178,plain,
( c2_1(a551)
| ~ iPr_def_18
| ~ c3_1(a551)
| ~ c1_1(a551) ),
inference(instantiation,[status(thm)],[c_13064]) ).
tcf(c_14192,plain,
( c0_1(a573)
| c1_1(a573)
| c2_1(a573)
| ~ iPr_def_36 ),
inference(instantiation,[status(thm)],[c_13105]) ).
tcf(c_14225,plain,
( c0_1(a569)
| c2_1(a569)
| ~ iPr_def_34
| ~ c3_1(a569) ),
inference(instantiation,[status(thm)],[c_13101]) ).
tcf(c_14227,plain,
( c0_1(a569)
| c1_1(a569)
| c2_1(a569)
| ~ iPr_def_36 ),
inference(instantiation,[status(thm)],[c_13105]) ).
tcf(c_14260,plain,
( c0_1(a548)
| c2_1(a548)
| ~ iPr_def_34
| ~ c3_1(a548) ),
inference(instantiation,[status(thm)],[c_13101]) ).
tcf(c_14324,plain,
( ~ iPr_def_12
| ~ c0_1(a549)
| ~ c1_1(a549)
| ~ c2_1(a549) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_14363,plain,
( c1_1(a537)
| ~ iPr_def_20
| ~ c3_1(a537)
| ~ c2_1(a537) ),
inference(instantiation,[status(thm)],[c_13066]) ).
tcf(c_14364,plain,
( c1_1(a589)
| ~ iPr_def_20
| ~ c3_1(a589)
| ~ c2_1(a589) ),
inference(instantiation,[status(thm)],[c_13066]) ).
tcf(c_14365,plain,
( c1_1(a578)
| ~ iPr_def_20
| ~ c3_1(a578)
| ~ c2_1(a578) ),
inference(instantiation,[status(thm)],[c_13066]) ).
tcf(c_14366,plain,
( c1_1(a570)
| ~ iPr_def_20
| ~ c3_1(a570)
| ~ c2_1(a570) ),
inference(instantiation,[status(thm)],[c_13066]) ).
tcf(c_14367,plain,
( c1_1(a550)
| ~ iPr_def_20
| ~ c3_1(a550)
| ~ c2_1(a550) ),
inference(instantiation,[status(thm)],[c_13066]) ).
tcf(c_14572,plain,
( c0_1(a538)
| ~ iPr_def_37
| ~ c3_1(a538)
| ~ c1_1(a538) ),
inference(instantiation,[status(thm)],[c_13106]) ).
tcf(c_14577,plain,
( ~ iPr_def_21
| ~ c3_1(a538)
| ~ c1_1(a538)
| ~ c2_1(a538) ),
inference(instantiation,[status(thm)],[c_13068]) ).
tcf(c_14580,plain,
( ~ iPr_def_12
| ~ c0_1(a574)
| ~ c1_1(a574)
| ~ c2_1(a574) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_14582,plain,
( c3_1(a574)
| ~ iPr_def_28
| ~ c0_1(a574)
| ~ c1_1(a574) ),
inference(instantiation,[status(thm)],[c_13084]) ).
tcf(c_14583,plain,
( c3_1(a574)
| ~ iPr_def_27
| ~ c1_1(a574)
| ~ c2_1(a574) ),
inference(instantiation,[status(thm)],[c_13080]) ).
tcf(c_14589,plain,
( c3_1(a574)
| c2_1(a574)
| ~ iPr_def_32
| ~ c0_1(a574) ),
inference(instantiation,[status(thm)],[c_13097]) ).
tcf(c_14595,plain,
( c3_1(a596)
| c2_1(a596)
| ~ iPr_def_32
| ~ c0_1(a596) ),
inference(instantiation,[status(thm)],[c_13097]) ).
tcf(c_14986,negated_conjecture,
( iPr_def_34
| iPr_def_18 ),
inference(global_subsumption_just,[status(thm)],[c_13102,c_436,c_435,c_430,c_405,c_404,c_403,c_402,c_401,c_393,c_392,c_391,c_390,c_389,c_388,c_376,c_371,c_370,c_524,c_516,c_515,c_512,c_511,c_487,c_486,c_485,c_473,c_472,c_471,c_456,c_446,c_445,c_439,c_6278,c_6288,c_6298,c_6308,c_6318,c_6328,c_6338,c_6348,c_6358,c_13056,c_13067,c_13074,c_13076,c_13082,c_13086,c_13087,c_13093,c_13102,c_13104,c_13107,c_13112,c_13123,c_13141,c_13171,c_13173,c_13271,c_13274,c_13291,c_13575,c_13635,c_13903,c_13905,c_14035,c_14102,c_14121,c_14116,c_14192,c_14260,c_14324,c_14363,c_14582]) ).
tcf(c_15889,plain,
( c3_1(a581)
| c1_1(a581)
| ~ iPr_def_15
| ~ c2_1(a581) ),
inference(instantiation,[status(thm)],[c_13059]) ).
tcf(c_15891,plain,
( c3_1(a546)
| c1_1(a546)
| ~ iPr_def_15
| ~ c2_1(a546) ),
inference(instantiation,[status(thm)],[c_13059]) ).
tcf(c_15913,plain,
( c3_1(a572)
| c1_1(a572)
| ~ iPr_def_15
| ~ c2_1(a572) ),
inference(instantiation,[status(thm)],[c_13059]) ).
tcf(c_16152,plain,
( hskp28
| c1_1(a578)
| c2_1(a578)
| ~ hskp23 ),
inference(superposition,[status(thm)],[c_689,c_476]) ).
tcf(c_16306,plain,
( hskp28
| c1_1(a573)
| c2_1(a573)
| ~ hskp19 ),
inference(superposition,[status(thm)],[c_689,c_486]) ).
tcf(c_16389,plain,
( hskp28
| c1_1(a569)
| c2_1(a569)
| ~ hskp15 ),
inference(superposition,[status(thm)],[c_689,c_492]) ).
tcf(c_16634,plain,
( hskp28
| c1_1(a548)
| c2_1(a548)
| ~ hskp6 ),
inference(superposition,[status(thm)],[c_689,c_512]) ).
tcf(c_16730,plain,
( ~ iPr_def_21
| ~ c3_1(a589)
| ~ c1_1(a589)
| ~ c2_1(a589) ),
inference(instantiation,[status(thm)],[c_13068]) ).
tcf(c_16806,plain,
( hskp28
| ~ hskp23
| c2_1(a578) ),
inference(global_subsumption_just,[status(thm)],[c_16152,c_477,c_16152]) ).
tcf(c_16807,plain,
( hskp28
| c2_1(a578)
| ~ hskp23 ),
inference(renaming,[status(thm)],[c_16806]) ).
tcf(c_16911,plain,
( c1_1(a551)
| ~ iPr_def_20
| ~ c3_1(a551)
| ~ c2_1(a551) ),
inference(instantiation,[status(thm)],[c_13066]) ).
tcf(c_16963,plain,
( ~ iPr_def_12
| ~ c0_1(a551)
| ~ c1_1(a551)
| ~ c2_1(a551) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_17017,plain,
( c1_1(a590)
| c2_1(a590)
| ~ iPr_def_19
| ~ hskp29 ),
inference(superposition,[status(thm)],[c_13065,c_464]) ).
tcf(c_17019,plain,
( c1_1(a582)
| c2_1(a582)
| ~ iPr_def_19
| ~ hskp25 ),
inference(superposition,[status(thm)],[c_13065,c_471]) ).
tcf(c_17026,plain,
( c1_1(a552)
| c2_1(a552)
| ~ iPr_def_19
| ~ hskp8 ),
inference(superposition,[status(thm)],[c_13065,c_507]) ).
tcf(c_17284,plain,
( ~ iPr_def_12
| ~ c0_1(a570)
| ~ c1_1(a570)
| ~ c2_1(a570) ),
inference(instantiation,[status(thm)],[c_13055]) ).
tcf(c_17442,plain,
( c1_1(a583)
| c2_1(a583)
| ~ iPr_def_11
| ~ c3_1(a583) ),
inference(instantiation,[status(thm)],[c_13054]) ).
tcf(c_17452,plain,
( c0_1(a578)
| c1_1(a578)
| ~ iPr_def_16
| ~ c3_1(a578) ),
inference(instantiation,[status(thm)],[c_13061]) ).
tcf(c_17457,plain,
( c3_1(a568)
| c1_1(a568)
| ~ iPr_def_15
| ~ c2_1(a568) ),
inference(instantiation,[status(thm)],[c_13059]) ).
tcf(c_17458,plain,
( c1_1(a568)
| ~ iPr_def_20
| ~ c3_1(a568)
| ~ c2_1(a568) ),
inference(instantiation,[status(thm)],[c_13066]) ).
tcf(c_17548,plain,
( c3_1(a591)
| c2_1(a591)
| ~ iPr_def_35
| ~ hskp30 ),
inference(superposition,[status(thm)],[c_13103,c_463]) ).
tcf(c_17552,plain,
( c3_1(a577)
| c2_1(a577)
| ~ iPr_def_35
| ~ hskp22 ),
inference(superposition,[status(thm)],[c_13103,c_479]) ).
tcf(c_17557,plain,
( c3_1(a569)
| c2_1(a569)
| ~ iPr_def_35
| ~ hskp15 ),
inference(superposition,[status(thm)],[c_13103,c_492]) ).
tcf(c_17794,plain,
( ~ iPr_def_23
| ~ c3_1(a537)
| ~ c0_1(a537)
| ~ c2_1(a537) ),
inference(instantiation,[status(thm)],[c_13072]) ).
tcf(c_17839,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_17794,c_17548,c_17552,c_17557,c_17457,c_17458,c_17452,c_17442,c_17284,c_17017,c_17019,c_17026,c_16963,c_16911,c_16807,c_16730,c_16634,c_16389,c_16306,c_15913,c_15891,c_15889,c_14986,c_14595,c_14589,c_14580,c_14582,c_14583,c_14572,c_14577,c_14367,c_14366,c_14365,c_14364,c_14363,c_14324,c_14260,c_14225,c_14227,c_14192,c_14178,c_14116,c_14121,c_14110,c_14109,c_14106,c_14102,c_14099,c_14077,c_14035,c_13971,c_13905,c_13908,c_13903,c_13872,c_13876,c_13802,c_13809,c_13791,c_13780,c_13782,c_13785,c_13693,c_13688,c_13686,c_13679,c_13660,c_13635,c_13615,c_13603,c_13596,c_13594,c_13575,c_13538,c_13534,c_13526,c_13492,c_13490,c_13451,c_13433,c_13422,c_13416,c_13413,c_13410,c_13352,c_13338,c_13335,c_13333,c_13330,c_13319,c_13315,c_13306,c_13303,c_13295,c_13291,c_13285,c_13275,c_13263,c_13261,c_13253,c_13241,c_13236,c_13234,c_13230,c_13227,c_13226,c_13221,c_13217,c_13216,c_13205,c_13199,c_13195,c_13191,c_13189,c_13183,c_13181,c_13178,c_13177,c_13175,c_13173,c_13171,c_13164,c_13157,c_13141,c_13125,c_13124,c_13123,c_13121,c_13120,c_13118,c_13117,c_13112,c_13111,c_13110,c_13107,c_13104,c_13100,c_13098,c_13095,c_13093,c_13092,c_13091,c_13089,c_13087,c_13086,c_13085,c_13082,c_13081,c_13076,c_13074,c_13073,c_13067,c_13063,c_13060,c_13056,c_6358,c_6348,c_6338,c_6328,c_6318,c_6308,c_6298,c_6288,c_6278,c_5410,c_5400,c_5390,c_5380,c_5370,c_5360,c_5350,c_5340,c_5330,c_438,c_439,c_440,c_441,c_444,c_449,c_452,c_453,c_454,c_455,c_456,c_457,c_458,c_462,c_464,c_465,c_466,c_467,c_470,c_472,c_473,c_474,c_475,c_476,c_477,c_478,c_479,c_485,c_486,c_487,c_490,c_492,c_493,c_494,c_500,c_501,c_502,c_503,c_504,c_505,c_506,c_508,c_509,c_510,c_511,c_512,c_513,c_514,c_515,c_516,c_524,c_368,c_369,c_370,c_371,c_372,c_374,c_375,c_378,c_379,c_384,c_385,c_386,c_387,c_388,c_389,c_390,c_391,c_392,c_393,c_394,c_398,c_399,c_400,c_401,c_402,c_403,c_404,c_405,c_406,c_407,c_408,c_409,c_411,c_412,c_413,c_414,c_415,c_418,c_419,c_426,c_428,c_429,c_430,c_431,c_432,c_435,c_436]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN439-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.09/10.38 % Computer : n020.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Fri Sep 25 01:11:59 UTC 2026
% 0.09/10.39 % CPUTime :
% 0.09/10.39 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/10.42 Running EPR theorem proving
% 0.14/10.42 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.14/10.43
% 0.14/10.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/10.43
% 0.14/10.43 % Detected problem language: tptp
% 0.14/10.44 % Proving...
% 6.72/11.61 % SZS status Started for theBenchmark.p
% 6.72/11.61 % SZS status Unsatisfiable for theBenchmark.p
% 6.72/11.61
% 6.72/11.61 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.72/11.61
% 6.72/11.61 % ------ iProver source info
% 6.72/11.61
% 6.72/11.61 % git: date: 2026-07-19 20:42:38 +0200
% 6.72/11.61 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.72/11.61 % git: non_committed_changes: false
% 6.72/11.61
% 6.72/11.61 % ------ Parsing...% successful
% 6.72/11.61
% 6.72/11.61
% 6.72/11.61 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 6.72/11.61 %
% 6.72/11.61
% 6.72/11.61 % ------ Preprocessing... sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.72/11.61
% 6.72/11.61 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 6.72/11.61 gs_s sp: 80 0s gs_e snvd_s sp: 0 0s snvd_e
% 6.72/11.61 % ------ Proving...
% 6.72/11.61 % ------ Problem Properties
% 6.72/11.61
% 6.72/11.61 %
% 6.72/11.61 % clauses 233
% 6.72/11.61 % conjectures 221
% 6.72/11.61 % EPR 233
% 6.72/11.61 % Horn 162
% 6.72/11.61 % unary 0
% 6.72/11.61 % binary 147
% 6.72/11.61 % lits 583
% 6.72/11.61 % lits eq 0
% 6.72/11.61 % fd_pure 0
% 6.72/11.61 % fd_pseudo 0
% 6.72/11.61 % fd_cond 0
% 6.72/11.61 % fd_pseudo_cond 0
% 6.72/11.61 % AC symbols 0
% 6.72/11.61
% 6.72/11.61 % ------ Schedule EPR non Horn non eq is on
% 6.72/11.61
% 6.72/11.61 % ------ no equalities: superposition off
% 6.72/11.61
% 6.72/11.61 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 6.72/11.61
% 6.72/11.61
% 6.72/11.61 % ------
% 6.72/11.61 % Current options:
% 6.72/11.61 % ------
% 6.72/11.61
% 6.72/11.61
% 6.72/11.61 %
% 6.72/11.61
% 6.72/11.61 % ------ Proving...
% 6.72/11.61 %
% 6.72/11.61
% 6.72/11.61 % SZS status Unsatisfiable for theBenchmark.p
% 6.72/11.61
% 6.72/11.61 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.72/11.62
% 6.72/11.62
%------------------------------------------------------------------------------