%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN440-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 : n015.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:13 PM UTC 2026
% Result : Unsatisfiable 4.88s 1.23s
% Output : CNFRefutation 4.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 156
% Syntax : Number of formulae : 604 ( 2 unt; 0 def)
% Number of atoms : 2376 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2991 (1219 ~;1772 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 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 : 73 ( 72 usr; 69 prp; 0-1 aty)
% Number of functors : 37 ( 37 usr; 37 con; 0-0 aty)
% Number of variables : 325 ( 0 sgn 325 !; 0 ?; 250 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp30
| hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f34,negated_conjecture,
( ndr1_0
| ~ hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
( ndr1_0
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f66,negated_conjecture,
( ndr1_0
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
fof(f68,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( hskp2
| hskp34
| hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f71,negated_conjecture,
( hskp9
| hskp17
| hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f74,negated_conjecture,
( hskp61
| hskp60
| hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( hskp66
| hskp65
| hskp64 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( c1_1(a675)
| ~ hskp66 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( c3_1(a675)
| ~ hskp66 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( c2_1(a674)
| ~ hskp65 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( c0_1(a674)
| ~ hskp65 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( c3_1(a673)
| ~ hskp64 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( c1_1(a673)
| ~ hskp64 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( c3_1(a672)
| ~ hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( c3_1(a671)
| ~ hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( c0_1(a671)
| ~ hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( c2_1(a670)
| ~ hskp61 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( c0_1(a669)
| ~ hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( c1_1(a669)
| ~ hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( c2_1(a665)
| ~ hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( c3_1(a665)
| ~ hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( c3_1(a663)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f93,negated_conjecture,
( c2_1(a658)
| ~ hskp56 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( c3_1(a658)
| ~ hskp56 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( c3_1(a653)
| ~ hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( c1_1(a653)
| ~ hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( c3_1(a651)
| ~ hskp54 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( c2_1(a651)
| ~ hskp54 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( c3_1(a648)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( c0_1(a648)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( c0_1(a647)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f111,negated_conjecture,
( c0_1(a626)
| ~ hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( c3_1(a626)
| ~ hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( c3_1(a623)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( c2_1(a623)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause114) ).
fof(f118,negated_conjecture,
( c1_1(a618)
| ~ hskp42 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( c2_1(a617)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( c3_1(a617)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f126,negated_conjecture,
( c1_1(a608)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( c3_1(a608)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( c0_1(a608)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( c1_1(a607)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( c0_1(a607)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( c1_1(a605)
| ~ hskp36 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( c0_1(a605)
| ~ hskp36 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( c2_1(a602)
| ~ hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f136,negated_conjecture,
( c0_1(a599)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( c3_1(a599)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f140,negated_conjecture,
( c0_1(a666)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f143,negated_conjecture,
( c3_1(a646)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause143) ).
fof(f152,negated_conjecture,
( c3_1(a628)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( c2_1(a627)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
( c0_1(a627)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( c3_1(a624)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f161,negated_conjecture,
( c2_1(a613)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f164,negated_conjecture,
( c2_1(a609)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
( c2_1(a606)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause165) ).
fof(f166,negated_conjecture,
( c0_1(a603)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause166) ).
fof(f168,negated_conjecture,
( c0_1(a598)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( c2_1(a598)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
( c0_1(a597)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
( ~ hskp66
| ~ c2_1(a675) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
( ~ hskp65
| ~ c1_1(a674) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
( ~ hskp64
| ~ c0_1(a673) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
( ~ hskp63
| ~ c0_1(a672) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
( ~ hskp63
| ~ c2_1(a672) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
( ~ hskp62
| ~ c1_1(a671) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
( ~ hskp61
| ~ c1_1(a670) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
( ~ hskp61
| ~ c0_1(a670) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
( ~ hskp60
| ~ c2_1(a669) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
( ~ hskp59
| ~ c0_1(a665) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
( ~ hskp58
| ~ c0_1(a663) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( ~ hskp58
| ~ c1_1(a663) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause182) ).
fof(f184,negated_conjecture,
( ~ hskp56
| ~ c1_1(a658) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
( ~ hskp55
| ~ c2_1(a653) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
( ~ hskp54
| ~ c0_1(a651) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
( ~ hskp53
| ~ c2_1(a648) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
( ~ hskp52
| ~ c2_1(a647) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
( ~ hskp52
| ~ c1_1(a647) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause189) ).
fof(f197,negated_conjecture,
( ~ hskp45
| ~ c0_1(a623) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause197) ).
fof(f201,negated_conjecture,
( ~ hskp42
| ~ c2_1(a618) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ hskp42
| ~ c3_1(a618) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ hskp41
| ~ c1_1(a617) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause203) ).
fof(f205,negated_conjecture,
( ~ hskp37
| ~ c2_1(a607) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
( ~ hskp36
| ~ c3_1(a605) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ hskp35
| ~ c3_1(a602) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ hskp35
| ~ c1_1(a602) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause208) ).
fof(f210,negated_conjecture,
( ~ hskp33
| ~ c2_1(a599) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause210) ).
fof(f215,negated_conjecture,
( ~ hskp30
| ~ c2_1(a666) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause215) ).
fof(f216,negated_conjecture,
( ~ hskp30
| ~ c3_1(a666) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause216) ).
fof(f217,negated_conjecture,
( ~ hskp29
| ~ c1_1(a660) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
( ~ hskp29
| ~ c3_1(a660) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ hskp29
| ~ c0_1(a660) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause219) ).
fof(f227,negated_conjecture,
( ~ hskp25
| ~ c2_1(a646) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause227) ).
fof(f228,negated_conjecture,
( ~ hskp25
| ~ c0_1(a646) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause228) ).
fof(f235,negated_conjecture,
( ~ hskp20
| ~ c1_1(a635) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause235) ).
fof(f236,negated_conjecture,
( ~ hskp20
| ~ c2_1(a635) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause236) ).
fof(f237,negated_conjecture,
( ~ hskp20
| ~ c3_1(a635) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause237) ).
fof(f242,negated_conjecture,
( ~ hskp17
| ~ c2_1(a628) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause242) ).
fof(f243,negated_conjecture,
( ~ hskp17
| ~ c1_1(a628) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause243) ).
fof(f244,negated_conjecture,
( ~ hskp16
| ~ c3_1(a627) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
( ~ hskp15
| ~ c2_1(a625) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
( ~ hskp15
| ~ c1_1(a625) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
( ~ hskp15
| ~ c0_1(a625) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause247) ).
fof(f248,negated_conjecture,
( ~ hskp14
| ~ c1_1(a624) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause248) ).
fof(f249,negated_conjecture,
( ~ hskp14
| ~ c2_1(a624) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause249) ).
fof(f258,negated_conjecture,
( ~ hskp9
| ~ c3_1(a613) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause258) ).
fof(f263,negated_conjecture,
( ~ hskp6
| ~ c0_1(a609) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause263) ).
fof(f264,negated_conjecture,
( ~ hskp6
| ~ c1_1(a609) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause264) ).
fof(f265,negated_conjecture,
( ~ hskp5
| ~ c0_1(a606) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause265) ).
fof(f266,negated_conjecture,
( ~ hskp5
| ~ c3_1(a606) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause266) ).
fof(f270,negated_conjecture,
( ~ hskp3
| ~ c1_1(a603) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause270) ).
fof(f271,negated_conjecture,
( ~ hskp3
| ~ c3_1(a603) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause271) ).
fof(f274,negated_conjecture,
( ~ hskp1
| ~ c1_1(a598) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause274) ).
fof(f275,negated_conjecture,
( ~ hskp0
| ~ c3_1(a597) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause275) ).
fof(f276,negated_conjecture,
( ~ hskp0
| ~ c1_1(a597) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause276) ).
fof(f279,negated_conjecture,
! [X0] :
( hskp63
| hskp62
| c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause279) ).
fof(f280,negated_conjecture,
! [X0] :
( hskp1
| hskp0
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause280) ).
fof(f284,negated_conjecture,
! [X0] :
( hskp52
| hskp25
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause284) ).
fof(f285,negated_conjecture,
! [X0] :
( hskp17
| hskp53
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause285) ).
fof(f286,negated_conjecture,
! [X0] :
( hskp54
| hskp37
| c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause286) ).
fof(f288,negated_conjecture,
! [X0] :
( hskp29
| hskp3
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause288) ).
fof(f289,negated_conjecture,
! [X0] :
( hskp6
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause289) ).
fof(f293,negated_conjecture,
! [X0] :
( hskp15
| hskp14
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause293) ).
fof(f295,negated_conjecture,
! [X0] :
( hskp41
| hskp58
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause295) ).
fof(f297,negated_conjecture,
! [X0,X1] :
( c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause297) ).
fof(f298,negated_conjecture,
! [X0] :
( hskp37
| hskp5
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause298) ).
fof(f299,negated_conjecture,
! [X0,X1] :
( c3_1(X1)
| c3_1(X0)
| c2_1(X1)
| c1_1(X1)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause299) ).
fof(f300,negated_conjecture,
! [X0,X1] :
( hskp42
| c1_1(X0)
| c0_1(X0)
| c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause300) ).
fof(f301,negated_conjecture,
! [X0,X1] :
( c0_1(X1)
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause301) ).
fof(f302,negated_conjecture,
! [X0,X1] :
( hskp38
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause302) ).
fof(f303,negated_conjecture,
! [X0,X1] :
( hskp42
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c2_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause303) ).
fof(f305,negated_conjecture,
! [X0,X1] :
( hskp55
| c1_1(X1)
| c2_1(X1)
| c0_1(X0)
| c3_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause305) ).
fof(f306,negated_conjecture,
! [X0,X1] :
( hskp56
| c1_1(X1)
| c2_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause306) ).
fof(f307,negated_conjecture,
! [X0,X1] :
( hskp11
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause307) ).
fof(f308,negated_conjecture,
! [X0,X1] :
( hskp45
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause308) ).
fof(f309,negated_conjecture,
! [X0,X1] :
( hskp46
| c3_1(X1)
| c2_1(X1)
| c1_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause309) ).
fof(f310,negated_conjecture,
! [X0,X1] :
( hskp16
| c0_1(X1)
| c2_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause310) ).
fof(f311,negated_conjecture,
! [X0,X1] :
( hskp20
| c1_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause311) ).
fof(f312,negated_conjecture,
! [X0,X1] :
( hskp5
| c2_1(X1)
| c1_1(X0)
| c2_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause312) ).
fof(f313,negated_conjecture,
! [X0,X1] :
( hskp55
| c1_1(X1)
| c0_1(X0)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause313) ).
fof(f314,negated_conjecture,
! [X0,X1] :
( hskp41
| c2_1(X1)
| c2_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause314) ).
fof(f315,negated_conjecture,
! [X0,X1] :
( hskp36
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause315) ).
fof(f318,negated_conjecture,
! [X0,X1] :
( hskp35
| c2_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause318) ).
fof(f319,negated_conjecture,
! [X0,X1] :
( hskp57
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause319) ).
fof(f320,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c1_1(X0)
| c2_1(X2)
| c1_1(X2)
| c0_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause320) ).
fof(f321,negated_conjecture,
! [X2,X0,X1] :
( c0_1(X2)
| c1_1(X2)
| c3_1(X2)
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause321) ).
fof(f322,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X1)
| c1_1(X0)
| c2_1(X2)
| c0_1(X2)
| c3_1(X2)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause322) ).
fof(f323,negated_conjecture,
! [X2,X0,X1] :
( c0_1(X2)
| c2_1(X2)
| c3_1(X2)
| c2_1(X1)
| c0_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause323) ).
fof(f324,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X1)
| c1_1(X0)
| ~ c0_1(X2)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause324) ).
fof(f325,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| c0_1(X0)
| ~ c3_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause325) ).
fof(f326,negated_conjecture,
! [X2,X0,X1] :
( c0_1(X2)
| c0_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause326) ).
fof(f327,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c0_1(X1)
| c3_1(X0)
| ~ c0_1(X2)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause327) ).
fof(f328,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X1)
| ~ c1_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause328) ).
tcf(c_377,negated_conjecture,
( hskp30
| hskp59 ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_410,negated_conjecture,
( ndr1_0
| ~ hskp34 ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_411,negated_conjecture,
( ndr1_0
| ~ hskp33 ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_442,negated_conjecture,
( ndr1_0
| ~ hskp2 ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_444,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_445,negated_conjecture,
( hskp2
| hskp33
| hskp34 ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_447,negated_conjecture,
( hskp9
| hskp16
| hskp17 ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_450,negated_conjecture,
( hskp33
| hskp60
| hskp61 ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_451,negated_conjecture,
( hskp64
| hskp65
| hskp66 ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_452,negated_conjecture,
( c1_1(a675)
| ~ hskp66 ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_453,negated_conjecture,
( c3_1(a675)
| ~ hskp66 ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_454,negated_conjecture,
( c2_1(a674)
| ~ hskp65 ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_455,negated_conjecture,
( c0_1(a674)
| ~ hskp65 ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_456,negated_conjecture,
( c3_1(a673)
| ~ hskp64 ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_457,negated_conjecture,
( c1_1(a673)
| ~ hskp64 ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_458,negated_conjecture,
( c3_1(a672)
| ~ hskp63 ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_459,negated_conjecture,
( c3_1(a671)
| ~ hskp62 ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_460,negated_conjecture,
( c0_1(a671)
| ~ hskp62 ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_461,negated_conjecture,
( c2_1(a670)
| ~ hskp61 ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_462,negated_conjecture,
( c0_1(a669)
| ~ hskp60 ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_463,negated_conjecture,
( c1_1(a669)
| ~ hskp60 ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_464,negated_conjecture,
( c2_1(a665)
| ~ hskp59 ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_465,negated_conjecture,
( c3_1(a665)
| ~ hskp59 ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_466,negated_conjecture,
( c3_1(a663)
| ~ hskp58 ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_469,negated_conjecture,
( c2_1(a658)
| ~ hskp56 ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_470,negated_conjecture,
( c3_1(a658)
| ~ hskp56 ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_471,negated_conjecture,
( c3_1(a653)
| ~ hskp55 ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_472,negated_conjecture,
( c1_1(a653)
| ~ hskp55 ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_473,negated_conjecture,
( c3_1(a651)
| ~ hskp54 ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_474,negated_conjecture,
( c2_1(a651)
| ~ hskp54 ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_475,negated_conjecture,
( c3_1(a648)
| ~ hskp53 ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_476,negated_conjecture,
( c0_1(a648)
| ~ hskp53 ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_477,negated_conjecture,
( c0_1(a647)
| ~ hskp52 ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_487,negated_conjecture,
( c0_1(a626)
| ~ hskp46 ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_488,negated_conjecture,
( c3_1(a626)
| ~ hskp46 ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_489,negated_conjecture,
( c3_1(a623)
| ~ hskp45 ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_490,negated_conjecture,
( c2_1(a623)
| ~ hskp45 ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_494,negated_conjecture,
( c1_1(a618)
| ~ hskp42 ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_495,negated_conjecture,
( c2_1(a617)
| ~ hskp41 ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_496,negated_conjecture,
( c3_1(a617)
| ~ hskp41 ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_502,negated_conjecture,
( c1_1(a608)
| ~ hskp38 ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_503,negated_conjecture,
( c3_1(a608)
| ~ hskp38 ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_504,negated_conjecture,
( c0_1(a608)
| ~ hskp38 ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_505,negated_conjecture,
( c1_1(a607)
| ~ hskp37 ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_506,negated_conjecture,
( c0_1(a607)
| ~ hskp37 ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_507,negated_conjecture,
( c1_1(a605)
| ~ hskp36 ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_508,negated_conjecture,
( c0_1(a605)
| ~ hskp36 ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_509,negated_conjecture,
( c2_1(a602)
| ~ hskp35 ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_512,negated_conjecture,
( c0_1(a599)
| ~ hskp33 ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_513,negated_conjecture,
( c3_1(a599)
| ~ hskp33 ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_516,negated_conjecture,
( c0_1(a666)
| ~ hskp30 ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_519,negated_conjecture,
( c3_1(a646)
| ~ hskp25 ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_528,negated_conjecture,
( c3_1(a628)
| ~ hskp17 ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_529,negated_conjecture,
( c2_1(a627)
| ~ hskp16 ),
inference(cnf_transformation,[],[f153]) ).
tcf(c_530,negated_conjecture,
( c0_1(a627)
| ~ hskp16 ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_531,negated_conjecture,
( c3_1(a624)
| ~ hskp14 ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_537,negated_conjecture,
( c2_1(a613)
| ~ hskp9 ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_540,negated_conjecture,
( c2_1(a609)
| ~ hskp6 ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_541,negated_conjecture,
( c2_1(a606)
| ~ hskp5 ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_542,negated_conjecture,
( c0_1(a603)
| ~ hskp3 ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_544,negated_conjecture,
( c0_1(a598)
| ~ hskp1 ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_545,negated_conjecture,
( c2_1(a598)
| ~ hskp1 ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_546,negated_conjecture,
( c0_1(a597)
| ~ hskp0 ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_547,negated_conjecture,
( ~ hskp66
| ~ c2_1(a675) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_548,negated_conjecture,
( ~ hskp65
| ~ c1_1(a674) ),
inference(cnf_transformation,[],[f172]) ).
tcf(c_549,negated_conjecture,
( ~ hskp64
| ~ c0_1(a673) ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_550,negated_conjecture,
( ~ hskp63
| ~ c0_1(a672) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_551,negated_conjecture,
( ~ hskp63
| ~ c2_1(a672) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_552,negated_conjecture,
( ~ hskp62
| ~ c1_1(a671) ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_553,negated_conjecture,
( ~ hskp61
| ~ c1_1(a670) ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_554,negated_conjecture,
( ~ hskp61
| ~ c0_1(a670) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_555,negated_conjecture,
( ~ hskp60
| ~ c2_1(a669) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_556,negated_conjecture,
( ~ hskp59
| ~ c0_1(a665) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_557,negated_conjecture,
( ~ hskp58
| ~ c0_1(a663) ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_558,negated_conjecture,
( ~ hskp58
| ~ c1_1(a663) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_560,negated_conjecture,
( ~ hskp56
| ~ c1_1(a658) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_561,negated_conjecture,
( ~ hskp55
| ~ c2_1(a653) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_562,negated_conjecture,
( ~ hskp54
| ~ c0_1(a651) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_563,negated_conjecture,
( ~ hskp53
| ~ c2_1(a648) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_564,negated_conjecture,
( ~ hskp52
| ~ c2_1(a647) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_565,negated_conjecture,
( ~ hskp52
| ~ c1_1(a647) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_573,negated_conjecture,
( ~ hskp45
| ~ c0_1(a623) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_577,negated_conjecture,
( ~ hskp42
| ~ c2_1(a618) ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_578,negated_conjecture,
( ~ hskp42
| ~ c3_1(a618) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_579,negated_conjecture,
( ~ hskp41
| ~ c1_1(a617) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_581,negated_conjecture,
( ~ hskp37
| ~ c2_1(a607) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_582,negated_conjecture,
( ~ hskp36
| ~ c3_1(a605) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_583,negated_conjecture,
( ~ hskp35
| ~ c3_1(a602) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_584,negated_conjecture,
( ~ hskp35
| ~ c1_1(a602) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_586,negated_conjecture,
( ~ hskp33
| ~ c2_1(a599) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_591,negated_conjecture,
( ~ hskp30
| ~ c2_1(a666) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_592,negated_conjecture,
( ~ hskp30
| ~ c3_1(a666) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_593,negated_conjecture,
( ~ hskp29
| ~ c1_1(a660) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_594,negated_conjecture,
( ~ hskp29
| ~ c3_1(a660) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_595,negated_conjecture,
( ~ hskp29
| ~ c0_1(a660) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_603,negated_conjecture,
( ~ hskp25
| ~ c2_1(a646) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_604,negated_conjecture,
( ~ hskp25
| ~ c0_1(a646) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_611,negated_conjecture,
( ~ hskp20
| ~ c1_1(a635) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_612,negated_conjecture,
( ~ hskp20
| ~ c2_1(a635) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_613,negated_conjecture,
( ~ hskp20
| ~ c3_1(a635) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_618,negated_conjecture,
( ~ hskp17
| ~ c2_1(a628) ),
inference(cnf_transformation,[],[f242]) ).
tcf(c_619,negated_conjecture,
( ~ hskp17
| ~ c1_1(a628) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_620,negated_conjecture,
( ~ hskp16
| ~ c3_1(a627) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_621,negated_conjecture,
( ~ hskp15
| ~ c2_1(a625) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_622,negated_conjecture,
( ~ hskp15
| ~ c1_1(a625) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_623,negated_conjecture,
( ~ hskp15
| ~ c0_1(a625) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_624,negated_conjecture,
( ~ hskp14
| ~ c1_1(a624) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_625,negated_conjecture,
( ~ hskp14
| ~ c2_1(a624) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_634,negated_conjecture,
( ~ hskp9
| ~ c3_1(a613) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_639,negated_conjecture,
( ~ hskp6
| ~ c0_1(a609) ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_640,negated_conjecture,
( ~ hskp6
| ~ c1_1(a609) ),
inference(cnf_transformation,[],[f264]) ).
tcf(c_641,negated_conjecture,
( ~ hskp5
| ~ c0_1(a606) ),
inference(cnf_transformation,[],[f265]) ).
tcf(c_642,negated_conjecture,
( ~ hskp5
| ~ c3_1(a606) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_646,negated_conjecture,
( ~ hskp3
| ~ c1_1(a603) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_647,negated_conjecture,
( ~ hskp3
| ~ c3_1(a603) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_650,negated_conjecture,
( ~ hskp1
| ~ c1_1(a598) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_651,negated_conjecture,
( ~ hskp0
| ~ c3_1(a597) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_652,negated_conjecture,
( ~ hskp0
| ~ c1_1(a597) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_655,negated_conjecture,
! [X0: $i] :
( hskp62
| hskp63
| c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_656,negated_conjecture,
! [X0: $i] :
( hskp0
| hskp1
| c0_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_660,negated_conjecture,
! [X0: $i] :
( hskp25
| hskp52
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_661,negated_conjecture,
! [X0: $i] :
( hskp17
| hskp53
| c0_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_662,negated_conjecture,
! [X0: $i] :
( hskp37
| hskp54
| c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_664,negated_conjecture,
! [X0: $i] :
( hskp3
| hskp29
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_665,negated_conjecture,
! [X0: $i] :
( hskp6
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_669,negated_conjecture,
! [X0: $i] :
( hskp14
| hskp15
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_671,negated_conjecture,
! [X0: $i] :
( hskp41
| hskp58
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_673,negated_conjecture,
! [X0: $i,X1: $i] :
( c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c3_1(X1)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_674,negated_conjecture,
! [X0: $i] :
( hskp5
| hskp37
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_675,negated_conjecture,
! [X0: $i,X1: $i] :
( c0_1(X0)
| c2_1(X1)
| c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_676,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_677,negated_conjecture,
! [X0: $i,X1: $i] :
( c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_678,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_679,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_681,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp55
| c0_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_682,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp56
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_683,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp11
| c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_684,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp45
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_685,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_686,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp16
| c0_1(X0)
| c2_1(X0)
| c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_687,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp20
| c2_1(X1)
| c3_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_688,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp5
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_689,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp55
| c0_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_690,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp41
| c2_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_691,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp36
| c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_694,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_695,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp57
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_696,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c2_1(X2)
| c3_1(X0)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_697,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c3_1(X2)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_698,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_699,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_700,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f324]) ).
tcf(c_701,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X1)
| c1_1(X2)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X2)
| ~ c2_1(X2)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_702,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c1_1(X2)
| c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_703,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X1)
| c2_1(X2)
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_704,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| ~ ndr1_0
| ~ c0_1(X2)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f328]) ).
tcf(c_705,plain,
( hskp62
| hskp63
| c2_1(a597)
| c3_1(a597)
| c1_1(a597)
| ~ ndr1_0 ),
inference(instantiation,[status(thm)],[c_655]) ).
tcf(c_729,negated_conjecture,
ndr1_0,
inference(global_subsumption_just,[status(thm)],[c_444,c_445,c_442,c_411,c_410]) ).
tcf(c_863,negated_conjecture,
! [X0: $i] :
( hskp62
| hskp63
| c2_1(X0)
| c3_1(X0)
| c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_655,c_445,c_442,c_411,c_410,c_655]) ).
tcf(c_872,negated_conjecture,
! [X0: $i] :
( hskp3
| hskp29
| c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_664,c_445,c_442,c_411,c_410,c_664]) ).
tcf(c_878,negated_conjecture,
! [X0: $i] :
( hskp37
| hskp54
| c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_662,c_445,c_442,c_411,c_410,c_662]) ).
tcf(c_881,negated_conjecture,
! [X0: $i] :
( hskp17
| hskp53
| c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_661,c_445,c_442,c_411,c_410,c_661]) ).
tcf(c_884,negated_conjecture,
! [X0: $i] :
( hskp25
| hskp52
| c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_660,c_445,c_442,c_411,c_410,c_660]) ).
tcf(c_896,negated_conjecture,
! [X0: $i] :
( hskp0
| hskp1
| c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_656,c_445,c_442,c_411,c_410,c_656]) ).
tcf(c_902,plain,
! [X0: $i] :
( hskp41
| hskp58
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_671,c_445,c_442,c_411,c_410,c_671]) ).
tcf(c_903,negated_conjecture,
! [X0: $i] :
( hskp41
| hskp58
| c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_902]) ).
tcf(c_908,plain,
! [X0: $i] :
( hskp14
| hskp15
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_669,c_445,c_442,c_411,c_410,c_669]) ).
tcf(c_909,negated_conjecture,
! [X0: $i] :
( hskp14
| hskp15
| c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_908]) ).
tcf(c_920,plain,
! [X0: $i] :
( hskp6
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_665,c_445,c_442,c_411,c_410,c_665]) ).
tcf(c_921,negated_conjecture,
! [X0: $i] :
( hskp6
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_920]) ).
tcf(c_923,plain,
! [X0: $i] :
( hskp5
| hskp37
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_674,c_445,c_442,c_411,c_410,c_674]) ).
tcf(c_924,negated_conjecture,
! [X0: $i] :
( hskp5
| hskp37
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_923]) ).
tcf(c_926,negated_conjecture,
! [X0: $i,X1: $i] :
( c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c3_1(X1)
| c3_1(X0)
| c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_673,c_445,c_442,c_411,c_410,c_673]) ).
tcf(c_929,negated_conjecture,
! [X0: $i,X1: $i] :
( c0_1(X0)
| c2_1(X1)
| c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_675,c_445,c_442,c_411,c_410,c_675]) ).
tcf(c_931,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_676,c_445,c_442,c_411,c_410,c_676]) ).
tcf(c_933,plain,
! [X0: $i,X1: $i] :
( hskp56
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_682,c_445,c_442,c_411,c_410,c_682]) ).
tcf(c_934,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp56
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_933]) ).
tcf(c_935,plain,
! [X0: $i,X1: $i] :
( hskp55
| c0_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_681,c_445,c_442,c_411,c_410,c_681]) ).
tcf(c_936,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp55
| c0_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_935]) ).
tcf(c_939,plain,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_679,c_445,c_442,c_411,c_410,c_679]) ).
tcf(c_940,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_939]) ).
tcf(c_941,plain,
! [X0: $i,X1: $i] :
( hskp38
| c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_678,c_445,c_442,c_411,c_410,c_678]) ).
tcf(c_942,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_941]) ).
tcf(c_943,plain,
! [X0: $i,X1: $i] :
( c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_677,c_445,c_442,c_411,c_410,c_677]) ).
tcf(c_944,negated_conjecture,
! [X0: $i,X1: $i] :
( c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_943]) ).
tcf(c_946,plain,
! [X0: $i,X1: $i] :
( hskp55
| c0_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_689,c_445,c_442,c_411,c_410,c_689]) ).
tcf(c_947,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp55
| c0_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_946]) ).
tcf(c_948,plain,
! [X0: $i,X1: $i] :
( hskp5
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_688,c_445,c_442,c_411,c_410,c_688]) ).
tcf(c_949,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp5
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_948]) ).
tcf(c_950,plain,
! [X0: $i,X1: $i] :
( hskp20
| c2_1(X1)
| c3_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_687,c_445,c_442,c_411,c_410,c_687]) ).
tcf(c_951,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp20
| c2_1(X1)
| c3_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_950]) ).
tcf(c_952,plain,
! [X0: $i,X1: $i] :
( hskp16
| c0_1(X0)
| c2_1(X0)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_686,c_445,c_442,c_411,c_410,c_686]) ).
tcf(c_953,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp16
| c0_1(X0)
| c2_1(X0)
| c3_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_952]) ).
tcf(c_954,plain,
! [X0: $i,X1: $i] :
( hskp46
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_685,c_445,c_442,c_411,c_410,c_685]) ).
tcf(c_955,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_954]) ).
tcf(c_956,plain,
! [X0: $i,X1: $i] :
( hskp45
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_684,c_445,c_442,c_411,c_410,c_684]) ).
tcf(c_957,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp45
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_956]) ).
tcf(c_958,plain,
! [X0: $i,X1: $i] :
( hskp11
| c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_683,c_445,c_442,c_411,c_410,c_683]) ).
tcf(c_959,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp11
| c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_958]) ).
tcf(c_964,plain,
! [X0: $i,X1: $i] :
( hskp36
| c2_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_691,c_445,c_442,c_411,c_410,c_691]) ).
tcf(c_965,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp36
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_964]) ).
tcf(c_966,plain,
! [X0: $i,X1: $i] :
( hskp41
| c2_1(X1)
| c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_690,c_690,c_729]) ).
tcf(c_967,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp41
| c2_1(X1)
| c2_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_966]) ).
tcf(c_969,plain,
! [X0: $i,X1: $i] :
( hskp57
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_695,c_445,c_442,c_411,c_410,c_695]) ).
tcf(c_970,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp57
| c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_969]) ).
tcf(c_971,plain,
! [X0: $i,X1: $i] :
( hskp35
| c2_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_694,c_445,c_442,c_411,c_410,c_694]) ).
tcf(c_972,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c2_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_971]) ).
tcf(c_973,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c2_1(X2)
| c3_1(X0)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_696,c_445,c_442,c_411,c_410,c_696]) ).
tcf(c_974,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c2_1(X2)
| c3_1(X0)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_973]) ).
tcf(c_975,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c3_1(X2)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_697,c_445,c_442,c_411,c_410,c_697]) ).
tcf(c_976,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c3_1(X2)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_975]) ).
tcf(c_977,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_699,c_445,c_442,c_411,c_410,c_699]) ).
tcf(c_978,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_977]) ).
tcf(c_979,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_698,c_445,c_442,c_411,c_410,c_698]) ).
tcf(c_980,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_979]) ).
tcf(c_981,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c1_1(X2)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_702,c_445,c_442,c_411,c_410,c_702]) ).
tcf(c_982,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c1_1(X2)
| c1_1(X1)
| ~ c2_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_981]) ).
tcf(c_983,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X1)
| c1_1(X2)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X2)
| ~ c0_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_701,c_445,c_442,c_411,c_410,c_701]) ).
tcf(c_984,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X1)
| c1_1(X2)
| c1_1(X1)
| ~ c0_1(X2)
| ~ c2_1(X2)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_983]) ).
tcf(c_985,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_700,c_445,c_442,c_411,c_410,c_700]) ).
tcf(c_986,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| ~ c0_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_985]) ).
tcf(c_987,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X1)
| c2_1(X2)
| c3_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X2)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_703,c_445,c_442,c_411,c_410,c_703]) ).
tcf(c_988,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X1)
| c2_1(X2)
| c3_1(X0)
| ~ c0_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_987]) ).
tcf(c_989,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X2)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_704,c_445,c_442,c_411,c_410,c_704]) ).
tcf(c_990,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| ~ c0_1(X2)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_989]) ).
tcf(c_2073,plain,
! [X0: $i,X1: $i] :
( hskp55
| c0_1(X0)
| c2_1(X1)
| c3_1(X0)
| c1_1(X1)
| ~ c2_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_936,c_929]) ).
tcf(c_2097,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c2_1(X1)
| c3_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_978,c_944]) ).
tcf(c_2511,plain,
( hskp30
| ~ c0_1(a665) ),
inference(resolution,[status(thm)],[c_377,c_556]) ).
tcf(c_2518,plain,
( hskp30
| c3_1(a665) ),
inference(resolution,[status(thm)],[c_377,c_465]) ).
tcf(c_2525,plain,
( hskp30
| c2_1(a665) ),
inference(resolution,[status(thm)],[c_377,c_464]) ).
tcf(c_2538,plain,
( hskp64
| hskp65
| ~ c2_1(a675) ),
inference(resolution,[status(thm)],[c_451,c_547]) ).
tcf(c_2548,plain,
( hskp64
| hskp65
| c3_1(a675) ),
inference(resolution,[status(thm)],[c_451,c_453]) ).
tcf(c_2558,plain,
( hskp64
| hskp65
| c1_1(a675) ),
inference(resolution,[status(thm)],[c_451,c_452]) ).
tcf(c_2577,plain,
( hskp33
| hskp60
| ~ c0_1(a670) ),
inference(resolution,[status(thm)],[c_450,c_554]) ).
tcf(c_2587,plain,
( hskp33
| hskp60
| ~ c1_1(a670) ),
inference(resolution,[status(thm)],[c_450,c_553]) ).
tcf(c_2597,plain,
( hskp33
| hskp60
| c2_1(a670) ),
inference(resolution,[status(thm)],[c_450,c_461]) ).
tcf(c_2826,plain,
! [X0: $i] :
( hskp62
| c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a672) ),
inference(resolution,[status(thm)],[c_863,c_551]) ).
tcf(c_2827,plain,
( hskp62
| c2_1(a597)
| c3_1(a597)
| c1_1(a597)
| ~ c2_1(a672) ),
inference(instantiation,[status(thm)],[c_2826]) ).
tcf(c_2843,plain,
! [X0: $i] :
( hskp62
| c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a672) ),
inference(resolution,[status(thm)],[c_863,c_550]) ).
tcf(c_2844,plain,
( hskp62
| c2_1(a597)
| c3_1(a597)
| c1_1(a597)
| ~ c0_1(a672) ),
inference(instantiation,[status(thm)],[c_2843]) ).
tcf(c_2860,plain,
! [X0: $i] :
( hskp62
| c3_1(a672)
| c2_1(X0)
| c3_1(X0)
| c1_1(X0) ),
inference(resolution,[status(thm)],[c_863,c_458]) ).
tcf(c_2861,plain,
( hskp62
| c2_1(a597)
| c3_1(a597)
| c3_1(a672)
| c1_1(a597) ),
inference(instantiation,[status(thm)],[c_2860]) ).
tcf(c_2892,plain,
! [X0: $i] :
( hskp63
| c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c1_1(a671) ),
inference(resolution,[status(thm)],[c_863,c_552]) ).
tcf(c_2893,plain,
( hskp63
| c2_1(a597)
| c3_1(a597)
| c1_1(a597)
| ~ c1_1(a671) ),
inference(instantiation,[status(thm)],[c_2892]) ).
tcf(c_2909,plain,
! [X0: $i] :
( hskp63
| c0_1(a671)
| c2_1(X0)
| c3_1(X0)
| c1_1(X0) ),
inference(resolution,[status(thm)],[c_863,c_460]) ).
tcf(c_2910,plain,
( hskp63
| c0_1(a671)
| c2_1(a597)
| c3_1(a597)
| c1_1(a597) ),
inference(instantiation,[status(thm)],[c_2909]) ).
tcf(c_2926,plain,
! [X0: $i] :
( hskp63
| c3_1(a671)
| c2_1(X0)
| c3_1(X0)
| c1_1(X0) ),
inference(resolution,[status(thm)],[c_863,c_459]) ).
tcf(c_2927,plain,
( hskp63
| c2_1(a597)
| c3_1(a597)
| c3_1(a671)
| c1_1(a597) ),
inference(instantiation,[status(thm)],[c_2926]) ).
tcf(c_5896,plain,
( hskp65
| c1_1(a675)
| ~ c0_1(a673) ),
inference(resolution,[status(thm)],[c_2558,c_549]) ).
tcf(c_5906,plain,
( hskp65
| c1_1(a673)
| c1_1(a675) ),
inference(resolution,[status(thm)],[c_2558,c_457]) ).
tcf(c_5916,plain,
( hskp65
| c3_1(a673)
| c1_1(a675) ),
inference(resolution,[status(thm)],[c_2558,c_456]) ).
tcf(c_5926,plain,
( hskp65
| c3_1(a675)
| ~ c0_1(a673) ),
inference(resolution,[status(thm)],[c_2548,c_549]) ).
tcf(c_5936,plain,
( hskp65
| c3_1(a675)
| c1_1(a673) ),
inference(resolution,[status(thm)],[c_2548,c_457]) ).
tcf(c_5946,plain,
( hskp65
| c3_1(a673)
| c3_1(a675) ),
inference(resolution,[status(thm)],[c_2548,c_456]) ).
tcf(c_5956,plain,
( hskp65
| ~ c0_1(a673)
| ~ c2_1(a675) ),
inference(resolution,[status(thm)],[c_2538,c_549]) ).
tcf(c_5966,plain,
( hskp65
| c1_1(a673)
| ~ c2_1(a675) ),
inference(resolution,[status(thm)],[c_2538,c_457]) ).
tcf(c_5976,plain,
( hskp65
| c3_1(a673)
| ~ c2_1(a675) ),
inference(resolution,[status(thm)],[c_2538,c_456]) ).
tcf(c_6013,plain,
( hskp33
| c2_1(a670)
| ~ c2_1(a669) ),
inference(resolution,[status(thm)],[c_2597,c_555]) ).
tcf(c_6023,plain,
( hskp33
| c2_1(a670)
| c1_1(a669) ),
inference(resolution,[status(thm)],[c_2597,c_463]) ).
tcf(c_6033,plain,
( hskp33
| c0_1(a669)
| c2_1(a670) ),
inference(resolution,[status(thm)],[c_2597,c_462]) ).
tcf(c_6043,plain,
( hskp33
| ~ c2_1(a669)
| ~ c1_1(a670) ),
inference(resolution,[status(thm)],[c_2587,c_555]) ).
tcf(c_6053,plain,
( hskp33
| c1_1(a669)
| ~ c1_1(a670) ),
inference(resolution,[status(thm)],[c_2587,c_463]) ).
tcf(c_6063,plain,
( hskp33
| c0_1(a669)
| ~ c1_1(a670) ),
inference(resolution,[status(thm)],[c_2587,c_462]) ).
tcf(c_6073,plain,
( hskp33
| ~ c0_1(a670)
| ~ c2_1(a669) ),
inference(resolution,[status(thm)],[c_2577,c_555]) ).
tcf(c_6083,plain,
( hskp33
| c1_1(a669)
| ~ c0_1(a670) ),
inference(resolution,[status(thm)],[c_2577,c_463]) ).
tcf(c_6093,plain,
( hskp33
| c0_1(a669)
| ~ c0_1(a670) ),
inference(resolution,[status(thm)],[c_2577,c_462]) ).
tcf(c_6739,plain,
( c2_1(a665)
| ~ c3_1(a666) ),
inference(resolution,[status(thm)],[c_2525,c_592]) ).
tcf(c_6746,plain,
( c2_1(a665)
| ~ c2_1(a666) ),
inference(resolution,[status(thm)],[c_2525,c_591]) ).
tcf(c_6753,plain,
( c0_1(a666)
| c2_1(a665) ),
inference(resolution,[status(thm)],[c_2525,c_516]) ).
tcf(c_6760,plain,
( c3_1(a665)
| ~ c3_1(a666) ),
inference(resolution,[status(thm)],[c_2518,c_592]) ).
tcf(c_6767,plain,
( c3_1(a665)
| ~ c2_1(a666) ),
inference(resolution,[status(thm)],[c_2518,c_591]) ).
tcf(c_6774,plain,
( c0_1(a666)
| c3_1(a665) ),
inference(resolution,[status(thm)],[c_2518,c_516]) ).
tcf(c_6781,plain,
( ~ c0_1(a665)
| ~ c3_1(a666) ),
inference(resolution,[status(thm)],[c_2511,c_592]) ).
tcf(c_6788,plain,
( ~ c0_1(a665)
| ~ c2_1(a666) ),
inference(resolution,[status(thm)],[c_2511,c_591]) ).
tcf(c_6795,plain,
( c0_1(a666)
| ~ c0_1(a665) ),
inference(resolution,[status(thm)],[c_2511,c_516]) ).
tcf(c_8080,plain,
( hskp16
| hskp17
| ~ c3_1(a613) ),
inference(resolution,[status(thm)],[c_447,c_634]) ).
tcf(c_8090,plain,
( hskp16
| hskp17
| c2_1(a613) ),
inference(resolution,[status(thm)],[c_447,c_537]) ).
tcf(c_15862,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_2097]) ).
tcf(c_15864,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_2097]) ).
tcf(c_15867,plain,
! [X0: $i] :
( ~ iPr_def_14
| c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_2073]) ).
tcf(c_15869,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_990]) ).
tcf(c_15870,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_990]) ).
tcf(c_15873,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_988]) ).
tcf(c_15874,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_988]) ).
tcf(c_15875,negated_conjecture,
( iPr_def_19
| iPr_def_18
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_988]) ).
tcf(c_15876,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_986]) ).
tcf(c_15877,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_21
| c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_986]) ).
tcf(c_15879,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_984]) ).
tcf(c_15880,negated_conjecture,
( iPr_def_22
| iPr_def_20
| iPr_def_18 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_984]) ).
tcf(c_15881,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_982]) ).
tcf(c_15882,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_24
| c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_982]) ).
tcf(c_15884,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_25
| c3_1(X0)
| c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_25])],[c_980]) ).
tcf(c_15885,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_26
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_26])],[c_980]) ).
tcf(c_15886,negated_conjecture,
( iPr_def_26
| iPr_def_25
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_980]) ).
tcf(c_15887,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_27
| c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_976]) ).
tcf(c_15888,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_28
| c1_1(X0)
| c3_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_976]) ).
tcf(c_15889,negated_conjecture,
( iPr_def_28
| iPr_def_27
| iPr_def_23 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_976]) ).
tcf(c_15890,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_29
| c1_1(X0)
| c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_974]) ).
tcf(c_15891,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_30
| c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_974]) ).
tcf(c_15892,negated_conjecture,
( iPr_def_30
| iPr_def_29
| iPr_def_24 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_974]) ).
tcf(c_15893,negated_conjecture,
( iPr_def_15
| iPr_def_10
| hskp35 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_972]) ).
tcf(c_15894,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_31
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_31])],[c_970]) ).
tcf(c_15896,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_32
| ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_32])],[c_967]) ).
tcf(c_15897,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_33
| ~ c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_33])],[c_967]) ).
tcf(c_15898,negated_conjecture,
( iPr_def_33
| iPr_def_32
| hskp41 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_967]) ).
tcf(c_15899,negated_conjecture,
( iPr_def_31
| iPr_def_21
| hskp36 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_965]) ).
tcf(c_15903,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_35
| c1_1(X0)
| c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_35])],[c_959]) ).
tcf(c_15905,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_36
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_36])],[c_957]) ).
tcf(c_15906,negated_conjecture,
( iPr_def_36
| iPr_def_18
| hskp45 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_957]) ).
tcf(c_15907,negated_conjecture,
( iPr_def_36
| iPr_def_26
| hskp46 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_955]) ).
tcf(c_15908,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_37
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_37])],[c_953]) ).
tcf(c_15909,negated_conjecture,
( iPr_def_37
| iPr_def_16
| hskp16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_953]) ).
tcf(c_15910,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_38
| c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_38])],[c_951]) ).
tcf(c_15911,negated_conjecture,
( iPr_def_38
| iPr_def_23
| hskp20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_951]) ).
tcf(c_15912,negated_conjecture,
( iPr_def_32
| iPr_def_22
| hskp5 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_949]) ).
tcf(c_15913,negated_conjecture,
( iPr_def_27
| iPr_def_26
| hskp55 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_947]) ).
tcf(c_15914,negated_conjecture,
( iPr_def_14
| iPr_def_12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_944]) ).
tcf(c_15915,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_39
| ~ c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_39])],[c_942]) ).
tcf(c_15916,negated_conjecture,
( iPr_def_39
| iPr_def_29
| hskp38 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_942]) ).
tcf(c_15917,negated_conjecture,
( iPr_def_27
| iPr_def_21
| hskp42 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_940]) ).
tcf(c_15919,negated_conjecture,
( iPr_def_36
| iPr_def_22
| hskp56 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_934]) ).
tcf(c_15920,negated_conjecture,
( iPr_def_28
| iPr_def_27
| hskp42 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_931]) ).
tcf(c_15921,negated_conjecture,
( iPr_def_35
| iPr_def_14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_929]) ).
tcf(c_15922,negated_conjecture,
( iPr_def_28
| iPr_def_25 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_926]) ).
tcf(c_15923,negated_conjecture,
( iPr_def_15
| hskp5
| hskp37 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_924]) ).
tcf(c_15927,negated_conjecture,
( iPr_def_20
| hskp14
| hskp15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_909]) ).
tcf(c_15929,negated_conjecture,
( iPr_def_10
| hskp41
| hskp58 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_903]) ).
tcf(c_15931,negated_conjecture,
( iPr_def_27
| hskp0
| hskp1 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_896]) ).
tcf(c_15936,negated_conjecture,
( iPr_def_38
| hskp25
| hskp52 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_884]) ).
tcf(c_15937,negated_conjecture,
( iPr_def_27
| hskp17
| hskp53 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_881]) ).
tcf(c_15938,negated_conjecture,
( iPr_def_14
| hskp37
| hskp54 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_878]) ).
tcf(c_15940,negated_conjecture,
( iPr_def_37
| hskp3
| hskp29 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_872]) ).
tcf(c_15943,negated_conjecture,
( iPr_def_35
| hskp62
| hskp63 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_863]) ).
tcf(c_15949,plain,
( c2_1(a597)
| c3_1(a597)
| c1_1(a597)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_15903]) ).
tcf(c_15951,plain,
( c2_1(a597)
| c1_1(a597)
| ~ iPr_def_21
| ~ c0_1(a597) ),
inference(instantiation,[status(thm)],[c_15877]) ).
tcf(c_15958,plain,
( c2_1(a597)
| c3_1(a597)
| ~ iPr_def_38
| ~ c0_1(a597) ),
inference(instantiation,[status(thm)],[c_15910]) ).
tcf(c_15965,plain,
( c1_1(a597)
| ~ iPr_def_20
| ~ c0_1(a597)
| ~ c2_1(a597) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_15993,plain,
( ~ iPr_def_15
| ~ c0_1(a617)
| ~ c2_1(a617)
| ~ c3_1(a617) ),
inference(instantiation,[status(thm)],[c_15869]) ).
tcf(c_16004,plain,
( c1_1(a617)
| ~ iPr_def_20
| ~ c0_1(a617)
| ~ c2_1(a617) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_16007,plain,
( c1_1(a627)
| ~ iPr_def_20
| ~ c0_1(a627)
| ~ c2_1(a627) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_16010,plain,
( c1_1(a598)
| ~ iPr_def_20
| ~ c0_1(a598)
| ~ c2_1(a598) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_16042,plain,
( c0_1(a606)
| c3_1(a606)
| c1_1(a606)
| ~ iPr_def_28 ),
inference(instantiation,[status(thm)],[c_15888]) ).
tcf(c_16043,plain,
( c0_1(a673)
| ~ iPr_def_39
| ~ c3_1(a673)
| ~ c1_1(a673) ),
inference(instantiation,[status(thm)],[c_15915]) ).
tcf(c_16053,plain,
( c2_1(a671)
| ~ iPr_def_10
| ~ c0_1(a671)
| ~ c3_1(a671) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16055,plain,
( c2_1(a653)
| ~ iPr_def_10
| ~ c0_1(a653)
| ~ c3_1(a653) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16056,plain,
( c2_1(a648)
| ~ iPr_def_10
| ~ c0_1(a648)
| ~ c3_1(a648) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16057,plain,
( c2_1(a626)
| ~ iPr_def_10
| ~ c0_1(a626)
| ~ c3_1(a626) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16061,plain,
( c2_1(a599)
| ~ iPr_def_10
| ~ c0_1(a599)
| ~ c3_1(a599) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16074,plain,
( c0_1(a613)
| c3_1(a613)
| ~ iPr_def_14
| ~ c2_1(a613) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_16075,plain,
( c0_1(a606)
| c3_1(a606)
| ~ iPr_def_14
| ~ c2_1(a606) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_16081,plain,
( c0_1(a609)
| c3_1(a609)
| ~ iPr_def_14
| ~ c2_1(a609) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_16082,plain,
( c0_1(a609)
| c1_1(a609)
| ~ iPr_def_24
| ~ c2_1(a609) ),
inference(instantiation,[status(thm)],[c_15882]) ).
tcf(c_16089,plain,
( c2_1(a671)
| c1_1(a671)
| ~ iPr_def_22
| ~ c3_1(a671) ),
inference(instantiation,[status(thm)],[c_15879]) ).
tcf(c_16092,plain,
( c2_1(a648)
| c1_1(a648)
| ~ iPr_def_22
| ~ c3_1(a648) ),
inference(instantiation,[status(thm)],[c_15879]) ).
tcf(c_16098,plain,
( c2_1(a646)
| c1_1(a646)
| ~ iPr_def_22
| ~ c3_1(a646) ),
inference(instantiation,[status(thm)],[c_15879]) ).
tcf(c_16110,plain,
( c0_1(a609)
| ~ iPr_def_18
| ~ c2_1(a609)
| ~ c3_1(a609) ),
inference(instantiation,[status(thm)],[c_15873]) ).
tcf(c_16120,plain,
( c2_1(a673)
| ~ iPr_def_33
| ~ c3_1(a673)
| ~ c1_1(a673) ),
inference(instantiation,[status(thm)],[c_15897]) ).
tcf(c_16130,plain,
( c2_1(a646)
| ~ iPr_def_33
| ~ c3_1(a646)
| ~ c1_1(a646) ),
inference(instantiation,[status(thm)],[c_15897]) ).
tcf(c_16136,plain,
( c0_1(a625)
| c3_1(a625)
| c1_1(a625)
| ~ iPr_def_28 ),
inference(instantiation,[status(thm)],[c_15888]) ).
tcf(c_16153,plain,
( c2_1(a635)
| c3_1(a635)
| c1_1(a635)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_15903]) ).
tcf(c_16157,plain,
( c2_1(a603)
| c3_1(a603)
| c1_1(a603)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_15903]) ).
tcf(c_16183,plain,
( c1_1(a603)
| ~ iPr_def_20
| ~ c0_1(a603)
| ~ c2_1(a603) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_16230,plain,
( c0_1(a653)
| ~ iPr_def_39
| ~ c3_1(a653)
| ~ c1_1(a653) ),
inference(instantiation,[status(thm)],[c_15915]) ).
tcf(c_16236,plain,
( c0_1(a617)
| c1_1(a617)
| ~ iPr_def_27
| ~ c3_1(a617) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_16242,plain,
( c0_1(a625)
| c1_1(a625)
| ~ iPr_def_27
| ~ c3_1(a625) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_16244,plain,
( c0_1(a609)
| c1_1(a609)
| ~ iPr_def_27
| ~ c3_1(a609) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_16253,plain,
( ~ iPr_def_15
| ~ c0_1(a626)
| ~ c2_1(a626)
| ~ c3_1(a626) ),
inference(instantiation,[status(thm)],[c_15869]) ).
tcf(c_16277,plain,
( c1_1(a671)
| ~ iPr_def_26
| ~ c0_1(a671)
| ~ c3_1(a671) ),
inference(instantiation,[status(thm)],[c_15885]) ).
tcf(c_16278,plain,
( c1_1(a617)
| ~ iPr_def_26
| ~ c0_1(a617)
| ~ c3_1(a617) ),
inference(instantiation,[status(thm)],[c_15885]) ).
tcf(c_16287,plain,
( c1_1(a617)
| ~ iPr_def_23
| ~ c2_1(a617)
| ~ c3_1(a617) ),
inference(instantiation,[status(thm)],[c_15881]) ).
tcf(c_16312,plain,
( c2_1(a647)
| c3_1(a647)
| c1_1(a647)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_15903]) ).
tcf(c_16329,plain,
( c0_1(a666)
| c2_1(a666)
| c3_1(a666)
| ~ iPr_def_25 ),
inference(instantiation,[status(thm)],[c_15884]) ).
tcf(c_16366,plain,
( c2_1(a625)
| c1_1(a625)
| ~ iPr_def_22
| ~ c3_1(a625) ),
inference(instantiation,[status(thm)],[c_15879]) ).
tcf(c_16384,plain,
( c2_1(a669)
| ~ iPr_def_10
| ~ c0_1(a669)
| ~ c3_1(a669) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16385,plain,
( c2_1(a647)
| ~ iPr_def_10
| ~ c0_1(a647)
| ~ c3_1(a647) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16390,plain,
( c2_1(a607)
| ~ iPr_def_10
| ~ c0_1(a607)
| ~ c3_1(a607) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_16416,plain,
( ~ iPr_def_31
| ~ c0_1(a608)
| ~ c3_1(a608)
| ~ c1_1(a608) ),
inference(instantiation,[status(thm)],[c_15894]) ).
tcf(c_16477,plain,
( c0_1(a625)
| c2_1(a625)
| c1_1(a625)
| ~ iPr_def_29 ),
inference(instantiation,[status(thm)],[c_15890]) ).
tcf(c_16562,plain,
( c1_1(a671)
| ~ iPr_def_20
| ~ c0_1(a671)
| ~ c2_1(a671) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_16584,plain,
( c0_1(a624)
| c2_1(a624)
| c1_1(a624)
| ~ iPr_def_29 ),
inference(instantiation,[status(thm)],[c_15890]) ).
tcf(c_16585,plain,
( c2_1(a624)
| c1_1(a624)
| ~ iPr_def_22
| ~ c3_1(a624) ),
inference(instantiation,[status(thm)],[c_15879]) ).
tcf(c_16587,plain,
( c1_1(a624)
| ~ iPr_def_26
| ~ c0_1(a624)
| ~ c3_1(a624) ),
inference(instantiation,[status(thm)],[c_15885]) ).
tcf(c_16588,plain,
( c0_1(a624)
| c1_1(a624)
| ~ iPr_def_27
| ~ c3_1(a624) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_16590,plain,
( c2_1(a624)
| c1_1(a624)
| ~ iPr_def_21
| ~ c0_1(a624) ),
inference(instantiation,[status(thm)],[c_15877]) ).
tcf(c_16616,plain,
( ~ iPr_def_15
| ~ c0_1(a608)
| ~ c2_1(a608)
| ~ c3_1(a608) ),
inference(instantiation,[status(thm)],[c_15869]) ).
tcf(c_16685,plain,
( c0_1(a625)
| c2_1(a625)
| c3_1(a625)
| ~ iPr_def_25 ),
inference(instantiation,[status(thm)],[c_15884]) ).
tcf(c_16744,plain,
( c2_1(a666)
| c3_1(a666)
| ~ iPr_def_36
| ~ c1_1(a666) ),
inference(instantiation,[status(thm)],[c_15905]) ).
tcf(c_16767,plain,
( c2_1(a669)
| ~ iPr_def_32
| ~ c0_1(a669)
| ~ c1_1(a669) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_16772,plain,
( c2_1(a607)
| ~ iPr_def_32
| ~ c0_1(a607)
| ~ c1_1(a607) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_16775,plain,
( c2_1(a666)
| ~ iPr_def_32
| ~ c0_1(a666)
| ~ c1_1(a666) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_16797,plain,
( c0_1(a660)
| c2_1(a660)
| c3_1(a660)
| ~ iPr_def_25 ),
inference(instantiation,[status(thm)],[c_15884]) ).
tcf(c_16798,plain,
( c2_1(a605)
| ~ iPr_def_32
| ~ c0_1(a605)
| ~ c1_1(a605) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_16817,plain,
( c2_1(a669)
| c3_1(a669)
| ~ iPr_def_38
| ~ c0_1(a669) ),
inference(instantiation,[status(thm)],[c_15910]) ).
tcf(c_16826,plain,
( c2_1(a666)
| c3_1(a666)
| ~ iPr_def_38
| ~ c0_1(a666) ),
inference(instantiation,[status(thm)],[c_15910]) ).
tcf(c_16954,plain,
( c2_1(a607)
| c3_1(a607)
| ~ iPr_def_36
| ~ c1_1(a607) ),
inference(instantiation,[status(thm)],[c_15905]) ).
tcf(c_17233,plain,
( c2_1(a666)
| c3_1(a666)
| c1_1(a666)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_15903]) ).
tcf(c_17234,plain,
( c2_1(a666)
| c1_1(a666)
| ~ iPr_def_21
| ~ c0_1(a666) ),
inference(instantiation,[status(thm)],[c_15877]) ).
tcf(c_17301,plain,
( c0_1(a646)
| c1_1(a646)
| ~ iPr_def_27
| ~ c3_1(a646) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_17313,plain,
( c1_1(a623)
| ~ iPr_def_23
| ~ c2_1(a623)
| ~ c3_1(a623) ),
inference(instantiation,[status(thm)],[c_15881]) ).
tcf(c_17315,plain,
( c0_1(a623)
| c1_1(a623)
| ~ iPr_def_27
| ~ c3_1(a623) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_17378,plain,
( c2_1(a669)
| c3_1(a669)
| c1_1(a669)
| ~ iPr_def_35 ),
inference(instantiation,[status(thm)],[c_15903]) ).
tcf(c_17384,plain,
( c0_1(a670)
| c1_1(a670)
| ~ iPr_def_27
| ~ c3_1(a670) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_17391,plain,
( c0_1(a670)
| c3_1(a670)
| ~ iPr_def_14
| ~ c2_1(a670) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_17429,plain,
( c0_1(a660)
| c3_1(a660)
| ~ iPr_def_14
| ~ c2_1(a660) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_17450,plain,
( c0_1(a651)
| ~ iPr_def_12
| ~ c2_1(a651)
| ~ c1_1(a651) ),
inference(instantiation,[status(thm)],[c_15864]) ).
tcf(c_17452,plain,
( c0_1(a651)
| ~ iPr_def_18
| ~ c2_1(a651)
| ~ c3_1(a651) ),
inference(instantiation,[status(thm)],[c_15873]) ).
tcf(c_17688,plain,
( c0_1(a623)
| ~ iPr_def_12
| ~ c2_1(a623)
| ~ c1_1(a623) ),
inference(instantiation,[status(thm)],[c_15864]) ).
tcf(c_17808,plain,
( c0_1(a665)
| ~ iPr_def_18
| ~ c2_1(a665)
| ~ c3_1(a665) ),
inference(instantiation,[status(thm)],[c_15873]) ).
tcf(c_17862,plain,
( c2_1(a675)
| ~ iPr_def_33
| ~ c3_1(a675)
| ~ c1_1(a675) ),
inference(instantiation,[status(thm)],[c_15897]) ).
tcf(c_17901,plain,
( c1_1(a658)
| ~ iPr_def_23
| ~ c2_1(a658)
| ~ c3_1(a658) ),
inference(instantiation,[status(thm)],[c_15881]) ).
tcf(c_17902,plain,
( c1_1(a658)
| ~ iPr_def_26
| ~ c0_1(a658)
| ~ c3_1(a658) ),
inference(instantiation,[status(thm)],[c_15885]) ).
tcf(c_17916,plain,
( c0_1(a658)
| ~ iPr_def_18
| ~ c2_1(a658)
| ~ c3_1(a658) ),
inference(instantiation,[status(thm)],[c_15873]) ).
tcf(c_17929,plain,
( c3_1(a613)
| ~ iPr_def_16
| ~ c0_1(a613)
| ~ c2_1(a613) ),
inference(instantiation,[status(thm)],[c_15870]) ).
tcf(c_17953,plain,
( c0_1(a602)
| c3_1(a602)
| ~ iPr_def_14
| ~ c2_1(a602) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_17955,plain,
( c1_1(a602)
| ~ iPr_def_20
| ~ c0_1(a602)
| ~ c2_1(a602) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_17971,plain,
( c0_1(a663)
| c1_1(a663)
| ~ iPr_def_27
| ~ c3_1(a663) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_17982,plain,
( c3_1(a627)
| ~ iPr_def_19
| ~ c2_1(a627)
| ~ c1_1(a627) ),
inference(instantiation,[status(thm)],[c_15874]) ).
tcf(c_17993,plain,
( c3_1(a605)
| ~ iPr_def_19
| ~ c2_1(a605)
| ~ c1_1(a605) ),
inference(instantiation,[status(thm)],[c_15874]) ).
tcf(c_18043,plain,
( c1_1(a675)
| ~ iPr_def_26
| ~ c0_1(a675)
| ~ c3_1(a675) ),
inference(instantiation,[status(thm)],[c_15885]) ).
tcf(c_18057,plain,
( c1_1(a628)
| ~ iPr_def_26
| ~ c0_1(a628)
| ~ c3_1(a628) ),
inference(instantiation,[status(thm)],[c_15885]) ).
tcf(c_18058,plain,
( c2_1(a628)
| c1_1(a628)
| ~ iPr_def_22
| ~ c3_1(a628) ),
inference(instantiation,[status(thm)],[c_15879]) ).
tcf(c_18062,plain,
( c2_1(a672)
| c1_1(a672)
| ~ iPr_def_22
| ~ c3_1(a672) ),
inference(instantiation,[status(thm)],[c_15879]) ).
tcf(c_18064,plain,
( c2_1(a672)
| ~ iPr_def_33
| ~ c3_1(a672)
| ~ c1_1(a672) ),
inference(instantiation,[status(thm)],[c_15897]) ).
tcf(c_18065,plain,
( c0_1(a672)
| c2_1(a672)
| c1_1(a672)
| ~ iPr_def_29 ),
inference(instantiation,[status(thm)],[c_15890]) ).
tcf(c_18073,plain,
( c0_1(a660)
| c3_1(a660)
| c1_1(a660)
| ~ iPr_def_28 ),
inference(instantiation,[status(thm)],[c_15888]) ).
tcf(c_18206,plain,
( c0_1(a672)
| c2_1(a672)
| ~ iPr_def_37
| ~ c3_1(a672) ),
inference(instantiation,[status(thm)],[c_15908]) ).
tcf(c_18216,plain,
( c0_1(a628)
| c2_1(a628)
| ~ iPr_def_37
| ~ c3_1(a628) ),
inference(instantiation,[status(thm)],[c_15908]) ).
tcf(c_18265,plain,
( c0_1(a673)
| ~ iPr_def_18
| ~ c2_1(a673)
| ~ c3_1(a673) ),
inference(instantiation,[status(thm)],[c_15873]) ).
tcf(c_18418,plain,
( c0_1(a618)
| c2_1(a618)
| c3_1(a618)
| ~ iPr_def_25 ),
inference(instantiation,[status(thm)],[c_15884]) ).
tcf(c_18480,plain,
( c0_1(a651)
| c1_1(a651)
| ~ iPr_def_27
| ~ c3_1(a651) ),
inference(instantiation,[status(thm)],[c_15887]) ).
tcf(c_18541,plain,
( c2_1(a618)
| c3_1(a618)
| ~ iPr_def_36
| ~ c1_1(a618) ),
inference(instantiation,[status(thm)],[c_15905]) ).
tcf(c_18783,plain,
( c0_1(a606)
| ~ iPr_def_12
| ~ c2_1(a606)
| ~ c1_1(a606) ),
inference(instantiation,[status(thm)],[c_15864]) ).
tcf(c_19332,plain,
( c2_1(a618)
| ~ iPr_def_32
| ~ c0_1(a618)
| ~ c1_1(a618) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_19412,plain,
( c2_1(a608)
| ~ iPr_def_32
| ~ c0_1(a608)
| ~ c1_1(a608) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_19930,negated_conjecture,
( iPr_def_15
| hskp37 ),
inference(global_subsumption_just,[status(thm)],[c_15923,c_541,c_494,c_490,c_489,c_474,c_473,c_642,c_641,c_578,c_577,c_573,c_562,c_15914,c_15889,c_15906,c_15920,c_15923,c_15938,c_16042,c_16075,c_17313,c_17452,c_17450,c_17688,c_18480,c_18541,c_18783]) ).
tcf(c_19953,plain,
( c1_1(a674)
| ~ iPr_def_20
| ~ c0_1(a674)
| ~ c2_1(a674) ),
inference(instantiation,[status(thm)],[c_15876]) ).
tcf(c_21252,plain,
( hskp6
| ~ hskp53
| ~ c0_1(a648)
| ~ c1_1(a648) ),
inference(superposition,[status(thm)],[c_475,c_921]) ).
tcf(c_21259,plain,
( hskp6
| ~ hskp38
| ~ c0_1(a608)
| ~ c1_1(a608) ),
inference(superposition,[status(thm)],[c_503,c_921]) ).
tcf(c_21476,plain,
( c0_1(a675)
| ~ iPr_def_39
| ~ c3_1(a675)
| ~ c1_1(a675) ),
inference(instantiation,[status(thm)],[c_15915]) ).
tcf(c_21477,plain,
( c0_1(a672)
| ~ iPr_def_39
| ~ c3_1(a672)
| ~ c1_1(a672) ),
inference(instantiation,[status(thm)],[c_15915]) ).
tcf(c_21504,plain,
( c3_1(a609)
| c1_1(a609)
| ~ iPr_def_30
| ~ c2_1(a609) ),
inference(instantiation,[status(thm)],[c_15891]) ).
tcf(c_21520,plain,
( c2_1(a675)
| ~ iPr_def_10
| ~ c0_1(a675)
| ~ c3_1(a675) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_21530,plain,
( c2_1(a628)
| ~ iPr_def_10
| ~ c0_1(a628)
| ~ c3_1(a628) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_21531,plain,
( c2_1(a624)
| ~ iPr_def_10
| ~ c0_1(a624)
| ~ c3_1(a624) ),
inference(instantiation,[status(thm)],[c_15862]) ).
tcf(c_21779,plain,
( c0_1(a628)
| c2_1(a628)
| c1_1(a628)
| ~ iPr_def_29 ),
inference(instantiation,[status(thm)],[c_15890]) ).
tcf(c_21809,plain,
( c2_1(a653)
| ~ iPr_def_32
| ~ c0_1(a653)
| ~ c1_1(a653) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_22497,plain,
( c2_1(a675)
| ~ iPr_def_32
| ~ c0_1(a675)
| ~ c1_1(a675) ),
inference(instantiation,[status(thm)],[c_15896]) ).
tcf(c_22614,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_22497,c_21809,c_21779,c_21531,c_21530,c_21520,c_21504,c_21477,c_21476,c_21252,c_21259,c_19953,c_19930,c_19412,c_19332,c_18541,c_18480,c_18418,c_18265,c_18216,c_18206,c_18073,c_18065,c_18062,c_18064,c_18057,c_18058,c_18043,c_17993,c_17982,c_17971,c_17953,c_17955,c_17929,c_17916,c_17901,c_17902,c_17862,c_17808,c_17688,c_17450,c_17429,c_17391,c_17384,c_17378,c_17315,c_17301,c_17233,c_17234,c_16954,c_16826,c_16817,c_16798,c_16797,c_16775,c_16772,c_16767,c_16744,c_16685,c_16616,c_16584,c_16585,c_16587,c_16588,c_16590,c_16562,c_16477,c_16416,c_16390,c_16385,c_16384,c_16366,c_16329,c_16312,c_16287,c_16278,c_16277,c_16253,c_16244,c_16242,c_16236,c_16230,c_16183,c_16157,c_16153,c_16136,c_16130,c_16120,c_16110,c_16098,c_16092,c_16089,c_16081,c_16082,c_16075,c_16074,c_16061,c_16057,c_16056,c_16055,c_16053,c_16043,c_16010,c_16007,c_16004,c_15993,c_15965,c_15958,c_15951,c_15949,c_15943,c_15940,c_15938,c_15937,c_15936,c_15931,c_15929,c_15927,c_15920,c_15919,c_15917,c_15916,c_15913,c_15912,c_15911,c_15909,c_15907,c_15906,c_15899,c_15898,c_15893,c_15892,c_15889,c_15886,c_15880,c_15875,c_15922,c_15921,c_15914,c_8090,c_8080,c_6795,c_6788,c_6781,c_6774,c_6767,c_6760,c_6753,c_6746,c_6739,c_6093,c_6083,c_6073,c_6063,c_6053,c_6043,c_6033,c_6023,c_6013,c_5976,c_5966,c_5956,c_5946,c_5936,c_5926,c_5916,c_5906,c_5896,c_2927,c_2910,c_2893,c_2861,c_2844,c_2827,c_729,c_705,c_548,c_550,c_551,c_552,c_557,c_558,c_560,c_561,c_562,c_563,c_564,c_565,c_573,c_577,c_578,c_579,c_581,c_582,c_583,c_584,c_586,c_593,c_594,c_595,c_603,c_604,c_611,c_612,c_613,c_618,c_619,c_620,c_621,c_622,c_623,c_624,c_625,c_639,c_640,c_641,c_642,c_646,c_647,c_650,c_651,c_652,c_454,c_455,c_458,c_459,c_460,c_466,c_469,c_470,c_471,c_472,c_473,c_474,c_475,c_476,c_477,c_487,c_488,c_489,c_490,c_494,c_495,c_496,c_502,c_503,c_504,c_505,c_506,c_507,c_508,c_509,c_512,c_513,c_519,c_528,c_529,c_530,c_531,c_540,c_541,c_542,c_544,c_545,c_546]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN440-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/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 01:14:57 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.40 Running EPR theorem proving
% 0.09/0.40 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.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 4.88/1.23 % SZS status Started for theBenchmark.p
% 4.88/1.23 % SZS status Unsatisfiable for theBenchmark.p
% 4.88/1.23
% 4.88/1.23 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.88/1.23
% 4.88/1.23 % ------ iProver source info
% 4.88/1.23
% 4.88/1.23 % git: date: 2026-07-19 20:42:38 +0200
% 4.88/1.23 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.88/1.23 % git: non_committed_changes: false
% 4.88/1.23
% 4.88/1.23 % ------ Parsing...% successful
% 4.88/1.23
% 4.88/1.23
% 4.88/1.23 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 4.88/1.23 %
% 4.88/1.23
% 4.88/1.23 % ------ 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 %
% 4.88/1.23
% 4.88/1.23 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 4.88/1.23 gs_s sp: 91 0s gs_e snvd_s sp: 0 0s snvd_e
% 4.88/1.23 % ------ Proving...
% 4.88/1.23 % ------ Problem Properties
% 4.88/1.23
% 4.88/1.23 %
% 4.88/1.23 % clauses 285
% 4.88/1.23 % conjectures 257
% 4.88/1.23 % EPR 285
% 4.88/1.23 % Horn 197
% 4.88/1.23 % unary 0
% 4.88/1.23 % binary 187
% 4.88/1.23 % lits 698
% 4.88/1.23 % lits eq 0
% 4.88/1.23 % fd_pure 0
% 4.88/1.23 % fd_pseudo 0
% 4.88/1.23 % fd_cond 0
% 4.88/1.23 % fd_pseudo_cond 0
% 4.88/1.23 % AC symbols 0
% 4.88/1.23
% 4.88/1.23 % ------ Schedule EPR non Horn non eq is on
% 4.88/1.23
% 4.88/1.23 % ------ no equalities: superposition off
% 4.88/1.23
% 4.88/1.23 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 4.88/1.23
% 4.88/1.23
% 4.88/1.23 % ------
% 4.88/1.23 % Current options:
% 4.88/1.23 % ------
% 4.88/1.23
% 4.88/1.23
% 4.88/1.23 %
% 4.88/1.23
% 4.88/1.23 % ------ Proving...
% 4.88/1.23 %
% 4.88/1.23
% 4.88/1.23 % SZS status Unsatisfiable for theBenchmark.p
% 4.88/1.23
% 4.88/1.23 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.88/1.25
% 4.88/1.25
%------------------------------------------------------------------------------