%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN457-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 : n002.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:19 PM UTC 2026
% Result : Unsatisfiable 5.49s 1.66s
% Output : CNFRefutation 5.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 292
% Syntax : Number of formulae : 799 ( 2 unt; 0 def)
% Number of atoms : 2765 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 3464 (1498 ~;1966 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 112 ( 111 usr; 108 prp; 0-1 aty)
% Number of functors : 76 ( 76 usr; 76 con; 0-0 aty)
% Number of variables : 371 ( 0 sgn 371 !; 0 ?; 282 :)
% Comments :
%------------------------------------------------------------------------------
fof(f29,negated_conjecture,
( ndr1_0
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
fof(f73,negated_conjecture,
( ndr1_0
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ndr1_0
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f76,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( hskp45
| hskp44
| hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( hskp3
| hskp2
| hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( hskp54
| hskp8
| hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( hskp15
| hskp14
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( hskp65
| hskp64
| hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( hskp28
| hskp27
| hskp66 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( hskp53
| hskp52
| hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( hskp32
| hskp31
| hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( c0_1(a1724)
| ~ hskp75 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( c3_1(a1724)
| ~ hskp75 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( c0_1(a1717)
| ~ hskp74 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( c2_1(a1717)
| ~ hskp74 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( c2_1(a1716)
| ~ hskp73 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( c0_1(a1716)
| ~ hskp73 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( c1_1(a1715)
| ~ hskp72 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( c3_1(a1715)
| ~ hskp72 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( c3_1(a1713)
| ~ hskp71 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( c0_1(a1713)
| ~ hskp71 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( c1_1(a1710)
| ~ hskp70 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( c0_1(a1709)
| ~ hskp69 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( c3_1(a1709)
| ~ hskp69 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( c3_1(a1707)
| ~ hskp68 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( c0_1(a1707)
| ~ hskp68 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( c1_1(a1702)
| ~ hskp67 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( c2_1(a1702)
| ~ hskp67 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( c3_1(a1702)
| ~ hskp67 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( c0_1(a1692)
| ~ hskp66 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( c2_1(a1687)
| ~ hskp65 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( c0_1(a1686)
| ~ hskp64 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( c2_1(a1676)
| ~ hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( c3_1(a1676)
| ~ hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( c1_1(a1675)
| ~ hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( c0_1(a1675)
| ~ hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( c3_1(a1674)
| ~ hskp61 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( c3_1(a1673)
| ~ hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( c2_1(a1673)
| ~ hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( c3_1(a1669)
| ~ hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( c0_1(a1669)
| ~ hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( c3_1(a1668)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( c0_1(a1665)
| ~ hskp57 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( c3_1(a1665)
| ~ hskp57 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( c0_1(a1662)
| ~ hskp56 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( c1_1(a1662)
| ~ hskp56 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( c1_1(a1661)
| ~ hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( c3_1(a1658)
| ~ hskp54 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( c1_1(a1658)
| ~ hskp54 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( c2_1(a1656)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( c0_1(a1656)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( c0_1(a1654)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( c2_1(a1654)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( c3_1(a1654)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( c2_1(a1653)
| ~ hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( c1_1(a1653)
| ~ hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( c3_1(a1652)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( c2_1(a1652)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( c0_1(a1652)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( c3_1(a1651)
| ~ hskp49 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
( c1_1(a1651)
| ~ hskp49 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
( c0_1(a1649)
| ~ hskp48 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
( c3_1(a1644)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( c0_1(a1642)
| ~ hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
( c2_1(a1641)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
( c3_1(a1640)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause139) ).
fof(f140,negated_conjecture,
( c2_1(a1640)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
( c1_1(a1640)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
( c2_1(a1639)
| ~ hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
( c0_1(a1639)
| ~ hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
( c1_1(a1638)
| ~ hskp42 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
( c0_1(a1638)
| ~ hskp42 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
( c0_1(a1726)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
( c2_1(a1726)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
( c1_1(a1725)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
( c3_1(a1725)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
( c3_1(a1721)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
( c3_1(a1718)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
( c2_1(a1714)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( c0_1(a1714)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
( c2_1(a1705)
| ~ hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( c3_1(a1704)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
( c1_1(a1701)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
( c0_1(a1701)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
( c2_1(a1700)
| ~ hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
( c1_1(a1698)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( c3_1(a1698)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( c2_1(a1695)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
( c0_1(a1695)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
( c2_1(a1694)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
( c2_1(a1690)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
( c3_1(a1689)
| ~ hskp24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause165) ).
fof(f166,negated_conjecture,
( c2_1(a1685)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
( c2_1(a1684)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
( c3_1(a1683)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( c2_1(a1683)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
( c3_1(a1672)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
( c1_1(a1672)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
( c2_1(a1671)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
( c0_1(a1667)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
( c3_1(a1667)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
( c2_1(a1666)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
( c3_1(a1666)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
( c2_1(a1657)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
( c3_1(a1655)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
( c0_1(a1655)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
( c3_1(a1648)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
( c1_1(a1647)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( c0_1(a1646)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
( c3_1(a1643)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
( c1_1(a1637)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
( c0_1(a1637)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
( ~ hskp75
| ~ c2_1(a1724) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
( ~ hskp74
| ~ c3_1(a1717) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
( ~ hskp73
| ~ c3_1(a1716) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
( ~ hskp72
| ~ c2_1(a1715) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause189) ).
fof(f190,negated_conjecture,
( ~ hskp71
| ~ c2_1(a1713) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause190) ).
fof(f191,negated_conjecture,
( ~ hskp70
| ~ c0_1(a1710) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause191) ).
fof(f192,negated_conjecture,
( ~ hskp70
| ~ c3_1(a1710) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
( ~ hskp69
| ~ c1_1(a1709) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
( ~ hskp68
| ~ c1_1(a1707) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
( ~ hskp66
| ~ c1_1(a1692) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
( ~ hskp66
| ~ c2_1(a1692) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause196) ).
fof(f197,negated_conjecture,
( ~ hskp65
| ~ c3_1(a1687) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause197) ).
fof(f198,negated_conjecture,
( ~ hskp65
| ~ c0_1(a1687) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause198) ).
fof(f199,negated_conjecture,
( ~ hskp64
| ~ c3_1(a1686) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
( ~ hskp64
| ~ c1_1(a1686) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
( ~ hskp63
| ~ c0_1(a1676) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ hskp62
| ~ c3_1(a1675) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ hskp61
| ~ c1_1(a1674) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
( ~ hskp61
| ~ c2_1(a1674) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
( ~ hskp60
| ~ c1_1(a1673) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
( ~ hskp59
| ~ c2_1(a1669) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ hskp58
| ~ c0_1(a1668) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ hskp58
| ~ c1_1(a1668) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause208) ).
fof(f209,negated_conjecture,
( ~ hskp57
| ~ c1_1(a1665) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause209) ).
fof(f210,negated_conjecture,
( ~ hskp56
| ~ c2_1(a1662) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause210) ).
fof(f211,negated_conjecture,
( ~ hskp55
| ~ c2_1(a1661) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause211) ).
fof(f212,negated_conjecture,
( ~ hskp55
| ~ c3_1(a1661) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause212) ).
fof(f213,negated_conjecture,
( ~ hskp54
| ~ c0_1(a1658) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause213) ).
fof(f214,negated_conjecture,
( ~ hskp53
| ~ c3_1(a1656) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause214) ).
fof(f215,negated_conjecture,
( ~ hskp51
| ~ c0_1(a1653) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause215) ).
fof(f216,negated_conjecture,
( ~ hskp49
| ~ c2_1(a1651) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause216) ).
fof(f217,negated_conjecture,
( ~ hskp48
| ~ c3_1(a1649) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
( ~ hskp48
| ~ c2_1(a1649) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ hskp47
| ~ c1_1(a1644) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause219) ).
fof(f220,negated_conjecture,
( ~ hskp47
| ~ c0_1(a1644) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause220) ).
fof(f221,negated_conjecture,
( ~ hskp46
| ~ c2_1(a1642) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause221) ).
fof(f222,negated_conjecture,
( ~ hskp46
| ~ c1_1(a1642) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause222) ).
fof(f223,negated_conjecture,
( ~ hskp45
| ~ c3_1(a1641) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause223) ).
fof(f224,negated_conjecture,
( ~ hskp45
| ~ c1_1(a1641) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause224) ).
fof(f225,negated_conjecture,
( ~ hskp43
| ~ c1_1(a1639) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause225) ).
fof(f226,negated_conjecture,
( ~ hskp42
| ~ c3_1(a1638) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause226) ).
fof(f227,negated_conjecture,
( ~ hskp41
| ~ c1_1(a1726) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause227) ).
fof(f228,negated_conjecture,
( ~ hskp40
| ~ c2_1(a1725) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause228) ).
fof(f229,negated_conjecture,
( ~ hskp39
| ~ c1_1(a1721) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause229) ).
fof(f230,negated_conjecture,
( ~ hskp39
| ~ c0_1(a1721) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause230) ).
fof(f231,negated_conjecture,
( ~ hskp38
| ~ c2_1(a1718) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause231) ).
fof(f232,negated_conjecture,
( ~ hskp38
| ~ c0_1(a1718) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause232) ).
fof(f233,negated_conjecture,
( ~ hskp37
| ~ c1_1(a1714) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause233) ).
fof(f234,negated_conjecture,
( ~ hskp36
| ~ c2_1(a1712) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause234) ).
fof(f235,negated_conjecture,
( ~ hskp36
| ~ c0_1(a1712) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause235) ).
fof(f236,negated_conjecture,
( ~ hskp36
| ~ c1_1(a1712) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause236) ).
fof(f237,negated_conjecture,
( ~ hskp35
| ~ c0_1(a1706) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause237) ).
fof(f238,negated_conjecture,
( ~ hskp35
| ~ c3_1(a1706) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause238) ).
fof(f239,negated_conjecture,
( ~ hskp35
| ~ c1_1(a1706) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause239) ).
fof(f240,negated_conjecture,
( ~ hskp34
| ~ c3_1(a1705) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause240) ).
fof(f241,negated_conjecture,
( ~ hskp34
| ~ c1_1(a1705) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause241) ).
fof(f242,negated_conjecture,
( ~ hskp33
| ~ c0_1(a1704) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause242) ).
fof(f243,negated_conjecture,
( ~ hskp33
| ~ c2_1(a1704) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause243) ).
fof(f244,negated_conjecture,
( ~ hskp32
| ~ c3_1(a1701) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
( ~ hskp31
| ~ c0_1(a1700) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
( ~ hskp31
| ~ c3_1(a1700) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
( ~ hskp30
| ~ c0_1(a1698) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause247) ).
fof(f248,negated_conjecture,
( ~ hskp29
| ~ c3_1(a1695) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause248) ).
fof(f249,negated_conjecture,
( ~ hskp28
| ~ c1_1(a1694) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause249) ).
fof(f250,negated_conjecture,
( ~ hskp28
| ~ c3_1(a1694) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause250) ).
fof(f251,negated_conjecture,
( ~ hskp27
| ~ c0_1(a1693) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause251) ).
fof(f252,negated_conjecture,
( ~ hskp27
| ~ c3_1(a1693) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause252) ).
fof(f253,negated_conjecture,
( ~ hskp27
| ~ c2_1(a1693) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause253) ).
fof(f254,negated_conjecture,
( ~ hskp26
| ~ c3_1(a1691) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause254) ).
fof(f255,negated_conjecture,
( ~ hskp26
| ~ c1_1(a1691) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause255) ).
fof(f256,negated_conjecture,
( ~ hskp26
| ~ c2_1(a1691) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause256) ).
fof(f257,negated_conjecture,
( ~ hskp25
| ~ c0_1(a1690) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause257) ).
fof(f258,negated_conjecture,
( ~ hskp25
| ~ c1_1(a1690) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause258) ).
fof(f259,negated_conjecture,
( ~ hskp24
| ~ c0_1(a1689) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause259) ).
fof(f260,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1689) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause260) ).
fof(f261,negated_conjecture,
( ~ hskp23
| ~ c0_1(a1685) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause261) ).
fof(f262,negated_conjecture,
( ~ hskp23
| ~ c1_1(a1685) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause262) ).
fof(f263,negated_conjecture,
( ~ hskp22
| ~ c0_1(a1684) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause263) ).
fof(f264,negated_conjecture,
( ~ hskp22
| ~ c3_1(a1684) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause264) ).
fof(f265,negated_conjecture,
( ~ hskp21
| ~ c1_1(a1683) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause265) ).
fof(f266,negated_conjecture,
( ~ hskp20
| ~ c2_1(a1682) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause266) ).
fof(f267,negated_conjecture,
( ~ hskp20
| ~ c1_1(a1682) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause267) ).
fof(f268,negated_conjecture,
( ~ hskp20
| ~ c3_1(a1682) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause268) ).
fof(f269,negated_conjecture,
( ~ hskp19
| ~ c1_1(a1681) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause269) ).
fof(f270,negated_conjecture,
( ~ hskp19
| ~ c3_1(a1681) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause270) ).
fof(f271,negated_conjecture,
( ~ hskp19
| ~ c2_1(a1681) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause271) ).
fof(f272,negated_conjecture,
( ~ hskp18
| ~ c3_1(a1680) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause272) ).
fof(f273,negated_conjecture,
( ~ hskp18
| ~ c1_1(a1680) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause273) ).
fof(f274,negated_conjecture,
( ~ hskp18
| ~ c0_1(a1680) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause274) ).
fof(f275,negated_conjecture,
( ~ hskp17
| ~ c0_1(a1678) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause275) ).
fof(f276,negated_conjecture,
( ~ hskp17
| ~ c1_1(a1678) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause276) ).
fof(f277,negated_conjecture,
( ~ hskp17
| ~ c2_1(a1678) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause277) ).
fof(f278,negated_conjecture,
( ~ hskp16
| ~ c0_1(a1677) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause278) ).
fof(f279,negated_conjecture,
( ~ hskp16
| ~ c2_1(a1677) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause279) ).
fof(f280,negated_conjecture,
( ~ hskp16
| ~ c1_1(a1677) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause280) ).
fof(f281,negated_conjecture,
( ~ hskp15
| ~ c0_1(a1672) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause281) ).
fof(f282,negated_conjecture,
( ~ hskp14
| ~ c1_1(a1671) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause282) ).
fof(f283,negated_conjecture,
( ~ hskp14
| ~ c3_1(a1671) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause283) ).
fof(f284,negated_conjecture,
( ~ hskp13
| ~ c1_1(a1667) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause284) ).
fof(f285,negated_conjecture,
( ~ hskp12
| ~ c1_1(a1666) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause285) ).
fof(f286,negated_conjecture,
( ~ hskp11
| ~ c3_1(a1664) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause286) ).
fof(f287,negated_conjecture,
( ~ hskp11
| ~ c2_1(a1664) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause287) ).
fof(f288,negated_conjecture,
( ~ hskp11
| ~ c1_1(a1664) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause288) ).
fof(f289,negated_conjecture,
( ~ hskp10
| ~ c2_1(a1663) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause289) ).
fof(f290,negated_conjecture,
( ~ hskp10
| ~ c3_1(a1663) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause290) ).
fof(f291,negated_conjecture,
( ~ hskp10
| ~ c0_1(a1663) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause291) ).
fof(f292,negated_conjecture,
( ~ hskp9
| ~ c3_1(a1660) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause292) ).
fof(f293,negated_conjecture,
( ~ hskp9
| ~ c0_1(a1660) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause293) ).
fof(f294,negated_conjecture,
( ~ hskp9
| ~ c1_1(a1660) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause294) ).
fof(f295,negated_conjecture,
( ~ hskp8
| ~ c1_1(a1657) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause295) ).
fof(f296,negated_conjecture,
( ~ hskp8
| ~ c0_1(a1657) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause296) ).
fof(f297,negated_conjecture,
( ~ hskp7
| ~ c2_1(a1655) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause297) ).
fof(f298,negated_conjecture,
( ~ hskp6
| ~ c1_1(a1650) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause298) ).
fof(f299,negated_conjecture,
( ~ hskp6
| ~ c2_1(a1650) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause299) ).
fof(f300,negated_conjecture,
( ~ hskp6
| ~ c3_1(a1650) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause300) ).
fof(f301,negated_conjecture,
( ~ hskp5
| ~ c1_1(a1648) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause301) ).
fof(f302,negated_conjecture,
( ~ hskp5
| ~ c0_1(a1648) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause302) ).
fof(f303,negated_conjecture,
( ~ hskp4
| ~ c0_1(a1647) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause303) ).
fof(f304,negated_conjecture,
( ~ hskp4
| ~ c2_1(a1647) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause304) ).
fof(f305,negated_conjecture,
( ~ hskp3
| ~ c1_1(a1646) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause305) ).
fof(f306,negated_conjecture,
( ~ hskp3
| ~ c2_1(a1646) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause306) ).
fof(f307,negated_conjecture,
( ~ hskp2
| ~ c1_1(a1645) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause307) ).
fof(f308,negated_conjecture,
( ~ hskp2
| ~ c0_1(a1645) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause308) ).
fof(f309,negated_conjecture,
( ~ hskp2
| ~ c3_1(a1645) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause309) ).
fof(f310,negated_conjecture,
( ~ hskp1
| ~ c1_1(a1643) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause310) ).
fof(f311,negated_conjecture,
( ~ hskp1
| ~ c2_1(a1643) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause311) ).
fof(f312,negated_conjecture,
( ~ hskp0
| ~ c2_1(a1637) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause312) ).
fof(f313,negated_conjecture,
! [X0] :
( hskp10
| hskp56
| c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause313) ).
fof(f314,negated_conjecture,
! [X0] :
( hskp72
| hskp37
| c2_1(X0)
| c0_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause314) ).
fof(f315,negated_conjecture,
! [X0] :
( hskp5
| hskp4
| c0_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause315) ).
fof(f316,negated_conjecture,
! [X0] :
( hskp59
| hskp58
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause316) ).
fof(f317,negated_conjecture,
! [X0] :
( hskp18
| hskp60
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause317) ).
fof(f318,negated_conjecture,
! [X0] :
( hskp24
| hskp61
| c0_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause318) ).
fof(f319,negated_conjecture,
! [X0] :
( hskp68
| hskp35
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause319) ).
fof(f320,negated_conjecture,
! [X0] :
( hskp71
| hskp36
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause320) ).
fof(f321,negated_conjecture,
! [X0] :
( hskp30
| hskp41
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause321) ).
fof(f322,negated_conjecture,
! [X0] :
( hskp42
| hskp0
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause322) ).
fof(f323,negated_conjecture,
! [X0] :
( hskp6
| hskp48
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause323) ).
fof(f324,negated_conjecture,
! [X0] :
( hskp7
| hskp52
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause324) ).
fof(f325,negated_conjecture,
! [X0] :
( hskp55
| hskp9
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause325) ).
fof(f326,negated_conjecture,
! [X0] :
( hskp57
| hskp11
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause326) ).
fof(f327,negated_conjecture,
! [X0] :
( hskp62
| hskp61
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause327) ).
fof(f328,negated_conjecture,
! [X0] :
( hskp17
| hskp16
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause328) ).
fof(f329,negated_conjecture,
! [X0] :
( hskp20
| hskp19
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause329) ).
fof(f330,negated_conjecture,
! [X0] :
( hskp33
| hskp61
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause330) ).
fof(f331,negated_conjecture,
! [X0] :
( hskp51
| hskp50
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause331) ).
fof(f332,negated_conjecture,
! [X0] :
( hskp13
| hskp12
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause332) ).
fof(f333,negated_conjecture,
! [X0] :
( hskp38
| hskp74
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause333) ).
fof(f334,negated_conjecture,
! [X0,X1] :
( hskp1
| c3_1(X1)
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause334) ).
fof(f335,negated_conjecture,
! [X0,X1] :
( hskp49
| c0_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause335) ).
fof(f336,negated_conjecture,
! [X0,X1] :
( hskp70
| c0_1(X0)
| c1_1(X0)
| c3_1(X1)
| c0_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause336) ).
fof(f337,negated_conjecture,
! [X0,X1] :
( hskp60
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c3_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause337) ).
fof(f338,negated_conjecture,
! [X0,X1] :
( hskp21
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause338) ).
fof(f339,negated_conjecture,
! [X0,X1] :
( hskp22
| c3_1(X1)
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause339) ).
fof(f340,negated_conjecture,
! [X0,X1] :
( hskp25
| c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause340) ).
fof(f341,negated_conjecture,
! [X0,X1] :
( hskp69
| c3_1(X1)
| c2_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause341) ).
fof(f342,negated_conjecture,
! [X0,X1] :
( hskp57
| c3_1(X1)
| c1_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause342) ).
fof(f343,negated_conjecture,
! [X0,X1] :
( hskp46
| c2_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause343) ).
fof(f344,negated_conjecture,
! [X0,X1] :
( hskp2
| c1_1(X1)
| c3_1(X1)
| c3_1(X0)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause344) ).
fof(f345,negated_conjecture,
! [X0,X1] :
( hskp30
| c2_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause345) ).
fof(f346,negated_conjecture,
! [X0,X1] :
( hskp29
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause346) ).
fof(f347,negated_conjecture,
! [X0,X1] :
( hskp61
| c2_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause347) ).
fof(f348,negated_conjecture,
! [X0,X1] :
( hskp75
| c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause348) ).
fof(f349,negated_conjecture,
! [X0,X1] :
( hskp67
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause349) ).
fof(f350,negated_conjecture,
! [X0,X1] :
( hskp34
| c2_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause350) ).
fof(f351,negated_conjecture,
! [X0,X1] :
( hskp73
| c0_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause351) ).
fof(f352,negated_conjecture,
! [X0,X1] :
( hskp47
| c2_1(X0)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause352) ).
fof(f353,negated_conjecture,
! [X0,X1] :
( hskp39
| c0_1(X1)
| c2_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause353) ).
fof(f354,negated_conjecture,
! [X0,X1] :
( hskp40
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause354) ).
fof(f355,negated_conjecture,
! [X0,X1] :
( hskp63
| c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause355) ).
fof(f356,negated_conjecture,
! [X0,X1] :
( hskp26
| c1_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause356) ).
fof(f357,negated_conjecture,
! [X0,X1] :
( hskp13
| c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause357) ).
fof(f358,negated_conjecture,
! [X0,X1] :
( hskp0
| c2_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause358) ).
fof(f359,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X2)
| c1_1(X2)
| c2_1(X2)
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause359) ).
fof(f360,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X2)
| c1_1(X2)
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c0_1(X2)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause360) ).
fof(f361,negated_conjecture,
! [X2,X0,X1] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2)
| c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause361) ).
fof(f362,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X2)
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c3_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause362) ).
fof(f363,negated_conjecture,
! [X2,X0,X1] :
( c3_1(X2)
| c1_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause363) ).
fof(f364,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X2)
| c1_1(X2)
| c1_1(X0)
| c2_1(X0)
| ~ c3_1(X2)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause364) ).
tcf(c_441,negated_conjecture,
( ndr1_0
| ~ hskp47 ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_485,negated_conjecture,
( ndr1_0
| ~ hskp3 ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_486,negated_conjecture,
( ndr1_0
| ~ hskp2 ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_488,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_489,negated_conjecture,
( hskp43
| hskp44
| hskp45 ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_490,negated_conjecture,
( hskp2
| hskp3
| hskp47 ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_491,negated_conjecture,
( hskp8
| hskp53
| hskp54 ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_492,negated_conjecture,
( hskp10
| hskp14
| hskp15 ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_493,negated_conjecture,
( hskp23
| hskp64
| hskp65 ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_494,negated_conjecture,
( hskp27
| hskp28
| hskp66 ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_495,negated_conjecture,
( hskp29
| hskp52
| hskp53 ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_496,negated_conjecture,
( hskp31
| hskp32
| hskp63 ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_497,negated_conjecture,
( c0_1(a1724)
| ~ hskp75 ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_498,negated_conjecture,
( c3_1(a1724)
| ~ hskp75 ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_499,negated_conjecture,
( c0_1(a1717)
| ~ hskp74 ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_500,negated_conjecture,
( c2_1(a1717)
| ~ hskp74 ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_501,negated_conjecture,
( c2_1(a1716)
| ~ hskp73 ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_502,negated_conjecture,
( c0_1(a1716)
| ~ hskp73 ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_503,negated_conjecture,
( c1_1(a1715)
| ~ hskp72 ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_504,negated_conjecture,
( c3_1(a1715)
| ~ hskp72 ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_505,negated_conjecture,
( c3_1(a1713)
| ~ hskp71 ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_506,negated_conjecture,
( c0_1(a1713)
| ~ hskp71 ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_507,negated_conjecture,
( c1_1(a1710)
| ~ hskp70 ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_508,negated_conjecture,
( c0_1(a1709)
| ~ hskp69 ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_509,negated_conjecture,
( c3_1(a1709)
| ~ hskp69 ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_510,negated_conjecture,
( c3_1(a1707)
| ~ hskp68 ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_511,negated_conjecture,
( c0_1(a1707)
| ~ hskp68 ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_512,negated_conjecture,
( c1_1(a1702)
| ~ hskp67 ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_513,negated_conjecture,
( c2_1(a1702)
| ~ hskp67 ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_514,negated_conjecture,
( c3_1(a1702)
| ~ hskp67 ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_515,negated_conjecture,
( c0_1(a1692)
| ~ hskp66 ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_516,negated_conjecture,
( c2_1(a1687)
| ~ hskp65 ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_517,negated_conjecture,
( c0_1(a1686)
| ~ hskp64 ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_518,negated_conjecture,
( c2_1(a1676)
| ~ hskp63 ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_519,negated_conjecture,
( c3_1(a1676)
| ~ hskp63 ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_520,negated_conjecture,
( c1_1(a1675)
| ~ hskp62 ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_521,negated_conjecture,
( c0_1(a1675)
| ~ hskp62 ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_522,negated_conjecture,
( c3_1(a1674)
| ~ hskp61 ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_523,negated_conjecture,
( c3_1(a1673)
| ~ hskp60 ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_524,negated_conjecture,
( c2_1(a1673)
| ~ hskp60 ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_525,negated_conjecture,
( c3_1(a1669)
| ~ hskp59 ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_526,negated_conjecture,
( c0_1(a1669)
| ~ hskp59 ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_527,negated_conjecture,
( c3_1(a1668)
| ~ hskp58 ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_528,negated_conjecture,
( c0_1(a1665)
| ~ hskp57 ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_529,negated_conjecture,
( c3_1(a1665)
| ~ hskp57 ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_530,negated_conjecture,
( c0_1(a1662)
| ~ hskp56 ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_531,negated_conjecture,
( c1_1(a1662)
| ~ hskp56 ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_532,negated_conjecture,
( c1_1(a1661)
| ~ hskp55 ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_533,negated_conjecture,
( c3_1(a1658)
| ~ hskp54 ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_534,negated_conjecture,
( c1_1(a1658)
| ~ hskp54 ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_535,negated_conjecture,
( c2_1(a1656)
| ~ hskp53 ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_536,negated_conjecture,
( c0_1(a1656)
| ~ hskp53 ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_537,negated_conjecture,
( c0_1(a1654)
| ~ hskp52 ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_538,negated_conjecture,
( c2_1(a1654)
| ~ hskp52 ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_539,negated_conjecture,
( c3_1(a1654)
| ~ hskp52 ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_540,negated_conjecture,
( c2_1(a1653)
| ~ hskp51 ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_541,negated_conjecture,
( c1_1(a1653)
| ~ hskp51 ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_542,negated_conjecture,
( c3_1(a1652)
| ~ hskp50 ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_543,negated_conjecture,
( c2_1(a1652)
| ~ hskp50 ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_544,negated_conjecture,
( c0_1(a1652)
| ~ hskp50 ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_545,negated_conjecture,
( c3_1(a1651)
| ~ hskp49 ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_546,negated_conjecture,
( c1_1(a1651)
| ~ hskp49 ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_547,negated_conjecture,
( c0_1(a1649)
| ~ hskp48 ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_548,negated_conjecture,
( c3_1(a1644)
| ~ hskp47 ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_549,negated_conjecture,
( c0_1(a1642)
| ~ hskp46 ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_550,negated_conjecture,
( c2_1(a1641)
| ~ hskp45 ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_551,negated_conjecture,
( c3_1(a1640)
| ~ hskp44 ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_552,negated_conjecture,
( c2_1(a1640)
| ~ hskp44 ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_553,negated_conjecture,
( c1_1(a1640)
| ~ hskp44 ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_554,negated_conjecture,
( c2_1(a1639)
| ~ hskp43 ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_555,negated_conjecture,
( c0_1(a1639)
| ~ hskp43 ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_556,negated_conjecture,
( c1_1(a1638)
| ~ hskp42 ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_557,negated_conjecture,
( c0_1(a1638)
| ~ hskp42 ),
inference(cnf_transformation,[],[f145]) ).
tcf(c_558,negated_conjecture,
( c0_1(a1726)
| ~ hskp41 ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_559,negated_conjecture,
( c2_1(a1726)
| ~ hskp41 ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_560,negated_conjecture,
( c1_1(a1725)
| ~ hskp40 ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_561,negated_conjecture,
( c3_1(a1725)
| ~ hskp40 ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_562,negated_conjecture,
( c3_1(a1721)
| ~ hskp39 ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_563,negated_conjecture,
( c3_1(a1718)
| ~ hskp38 ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_564,negated_conjecture,
( c2_1(a1714)
| ~ hskp37 ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_565,negated_conjecture,
( c0_1(a1714)
| ~ hskp37 ),
inference(cnf_transformation,[],[f153]) ).
tcf(c_566,negated_conjecture,
( c2_1(a1705)
| ~ hskp34 ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_567,negated_conjecture,
( c3_1(a1704)
| ~ hskp33 ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_568,negated_conjecture,
( c1_1(a1701)
| ~ hskp32 ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_569,negated_conjecture,
( c0_1(a1701)
| ~ hskp32 ),
inference(cnf_transformation,[],[f157]) ).
tcf(c_570,negated_conjecture,
( c2_1(a1700)
| ~ hskp31 ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_571,negated_conjecture,
( c1_1(a1698)
| ~ hskp30 ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_572,negated_conjecture,
( c3_1(a1698)
| ~ hskp30 ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_573,negated_conjecture,
( c2_1(a1695)
| ~ hskp29 ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_574,negated_conjecture,
( c0_1(a1695)
| ~ hskp29 ),
inference(cnf_transformation,[],[f162]) ).
tcf(c_575,negated_conjecture,
( c2_1(a1694)
| ~ hskp28 ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_576,negated_conjecture,
( c2_1(a1690)
| ~ hskp25 ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_577,negated_conjecture,
( c3_1(a1689)
| ~ hskp24 ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_578,negated_conjecture,
( c2_1(a1685)
| ~ hskp23 ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_579,negated_conjecture,
( c2_1(a1684)
| ~ hskp22 ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_580,negated_conjecture,
( c3_1(a1683)
| ~ hskp21 ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_581,negated_conjecture,
( c2_1(a1683)
| ~ hskp21 ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_582,negated_conjecture,
( c3_1(a1672)
| ~ hskp15 ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_583,negated_conjecture,
( c1_1(a1672)
| ~ hskp15 ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_584,negated_conjecture,
( c2_1(a1671)
| ~ hskp14 ),
inference(cnf_transformation,[],[f172]) ).
tcf(c_585,negated_conjecture,
( c0_1(a1667)
| ~ hskp13 ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_586,negated_conjecture,
( c3_1(a1667)
| ~ hskp13 ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_587,negated_conjecture,
( c2_1(a1666)
| ~ hskp12 ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_588,negated_conjecture,
( c3_1(a1666)
| ~ hskp12 ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_589,negated_conjecture,
( c2_1(a1657)
| ~ hskp8 ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_590,negated_conjecture,
( c3_1(a1655)
| ~ hskp7 ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_591,negated_conjecture,
( c0_1(a1655)
| ~ hskp7 ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_592,negated_conjecture,
( c3_1(a1648)
| ~ hskp5 ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_593,negated_conjecture,
( c1_1(a1647)
| ~ hskp4 ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_594,negated_conjecture,
( c0_1(a1646)
| ~ hskp3 ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_595,negated_conjecture,
( c3_1(a1643)
| ~ hskp1 ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_596,negated_conjecture,
( c1_1(a1637)
| ~ hskp0 ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_597,negated_conjecture,
( c0_1(a1637)
| ~ hskp0 ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_598,negated_conjecture,
( ~ hskp75
| ~ c2_1(a1724) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_599,negated_conjecture,
( ~ hskp74
| ~ c3_1(a1717) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_600,negated_conjecture,
( ~ hskp73
| ~ c3_1(a1716) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_601,negated_conjecture,
( ~ hskp72
| ~ c2_1(a1715) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_602,negated_conjecture,
( ~ hskp71
| ~ c2_1(a1713) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_603,negated_conjecture,
( ~ hskp70
| ~ c0_1(a1710) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_604,negated_conjecture,
( ~ hskp70
| ~ c3_1(a1710) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_605,negated_conjecture,
( ~ hskp69
| ~ c1_1(a1709) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_606,negated_conjecture,
( ~ hskp68
| ~ c1_1(a1707) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_607,negated_conjecture,
( ~ hskp66
| ~ c1_1(a1692) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_608,negated_conjecture,
( ~ hskp66
| ~ c2_1(a1692) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_609,negated_conjecture,
( ~ hskp65
| ~ c3_1(a1687) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_610,negated_conjecture,
( ~ hskp65
| ~ c0_1(a1687) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_611,negated_conjecture,
( ~ hskp64
| ~ c3_1(a1686) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_612,negated_conjecture,
( ~ hskp64
| ~ c1_1(a1686) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_613,negated_conjecture,
( ~ hskp63
| ~ c0_1(a1676) ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_614,negated_conjecture,
( ~ hskp62
| ~ c3_1(a1675) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_615,negated_conjecture,
( ~ hskp61
| ~ c1_1(a1674) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_616,negated_conjecture,
( ~ hskp61
| ~ c2_1(a1674) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_617,negated_conjecture,
( ~ hskp60
| ~ c1_1(a1673) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_618,negated_conjecture,
( ~ hskp59
| ~ c2_1(a1669) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_619,negated_conjecture,
( ~ hskp58
| ~ c0_1(a1668) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_620,negated_conjecture,
( ~ hskp58
| ~ c1_1(a1668) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_621,negated_conjecture,
( ~ hskp57
| ~ c1_1(a1665) ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_622,negated_conjecture,
( ~ hskp56
| ~ c2_1(a1662) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_623,negated_conjecture,
( ~ hskp55
| ~ c2_1(a1661) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_624,negated_conjecture,
( ~ hskp55
| ~ c3_1(a1661) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_625,negated_conjecture,
( ~ hskp54
| ~ c0_1(a1658) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_626,negated_conjecture,
( ~ hskp53
| ~ c3_1(a1656) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_627,negated_conjecture,
( ~ hskp51
| ~ c0_1(a1653) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_628,negated_conjecture,
( ~ hskp49
| ~ c2_1(a1651) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_629,negated_conjecture,
( ~ hskp48
| ~ c3_1(a1649) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_630,negated_conjecture,
( ~ hskp48
| ~ c2_1(a1649) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_631,negated_conjecture,
( ~ hskp47
| ~ c1_1(a1644) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_632,negated_conjecture,
( ~ hskp47
| ~ c0_1(a1644) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_633,negated_conjecture,
( ~ hskp46
| ~ c2_1(a1642) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_634,negated_conjecture,
( ~ hskp46
| ~ c1_1(a1642) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_635,negated_conjecture,
( ~ hskp45
| ~ c3_1(a1641) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_636,negated_conjecture,
( ~ hskp45
| ~ c1_1(a1641) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_637,negated_conjecture,
( ~ hskp43
| ~ c1_1(a1639) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_638,negated_conjecture,
( ~ hskp42
| ~ c3_1(a1638) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_639,negated_conjecture,
( ~ hskp41
| ~ c1_1(a1726) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_640,negated_conjecture,
( ~ hskp40
| ~ c2_1(a1725) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_641,negated_conjecture,
( ~ hskp39
| ~ c1_1(a1721) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_642,negated_conjecture,
( ~ hskp39
| ~ c0_1(a1721) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_643,negated_conjecture,
( ~ hskp38
| ~ c2_1(a1718) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_644,negated_conjecture,
( ~ hskp38
| ~ c0_1(a1718) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_645,negated_conjecture,
( ~ hskp37
| ~ c1_1(a1714) ),
inference(cnf_transformation,[],[f233]) ).
tcf(c_646,negated_conjecture,
( ~ hskp36
| ~ c2_1(a1712) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_647,negated_conjecture,
( ~ hskp36
| ~ c0_1(a1712) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_648,negated_conjecture,
( ~ hskp36
| ~ c1_1(a1712) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_649,negated_conjecture,
( ~ hskp35
| ~ c0_1(a1706) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_650,negated_conjecture,
( ~ hskp35
| ~ c3_1(a1706) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_651,negated_conjecture,
( ~ hskp35
| ~ c1_1(a1706) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_652,negated_conjecture,
( ~ hskp34
| ~ c3_1(a1705) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_653,negated_conjecture,
( ~ hskp34
| ~ c1_1(a1705) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_654,negated_conjecture,
( ~ hskp33
| ~ c0_1(a1704) ),
inference(cnf_transformation,[],[f242]) ).
tcf(c_655,negated_conjecture,
( ~ hskp33
| ~ c2_1(a1704) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_656,negated_conjecture,
( ~ hskp32
| ~ c3_1(a1701) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_657,negated_conjecture,
( ~ hskp31
| ~ c0_1(a1700) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_658,negated_conjecture,
( ~ hskp31
| ~ c3_1(a1700) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_659,negated_conjecture,
( ~ hskp30
| ~ c0_1(a1698) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_660,negated_conjecture,
( ~ hskp29
| ~ c3_1(a1695) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_661,negated_conjecture,
( ~ hskp28
| ~ c1_1(a1694) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_662,negated_conjecture,
( ~ hskp28
| ~ c3_1(a1694) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_663,negated_conjecture,
( ~ hskp27
| ~ c0_1(a1693) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_664,negated_conjecture,
( ~ hskp27
| ~ c3_1(a1693) ),
inference(cnf_transformation,[],[f252]) ).
tcf(c_665,negated_conjecture,
( ~ hskp27
| ~ c2_1(a1693) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_666,negated_conjecture,
( ~ hskp26
| ~ c3_1(a1691) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_667,negated_conjecture,
( ~ hskp26
| ~ c1_1(a1691) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_668,negated_conjecture,
( ~ hskp26
| ~ c2_1(a1691) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_669,negated_conjecture,
( ~ hskp25
| ~ c0_1(a1690) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_670,negated_conjecture,
( ~ hskp25
| ~ c1_1(a1690) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_671,negated_conjecture,
( ~ hskp24
| ~ c0_1(a1689) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_672,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1689) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_673,negated_conjecture,
( ~ hskp23
| ~ c0_1(a1685) ),
inference(cnf_transformation,[],[f261]) ).
tcf(c_674,negated_conjecture,
( ~ hskp23
| ~ c1_1(a1685) ),
inference(cnf_transformation,[],[f262]) ).
tcf(c_675,negated_conjecture,
( ~ hskp22
| ~ c0_1(a1684) ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_676,negated_conjecture,
( ~ hskp22
| ~ c3_1(a1684) ),
inference(cnf_transformation,[],[f264]) ).
tcf(c_677,negated_conjecture,
( ~ hskp21
| ~ c1_1(a1683) ),
inference(cnf_transformation,[],[f265]) ).
tcf(c_678,negated_conjecture,
( ~ hskp20
| ~ c2_1(a1682) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_679,negated_conjecture,
( ~ hskp20
| ~ c1_1(a1682) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_680,negated_conjecture,
( ~ hskp20
| ~ c3_1(a1682) ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_681,negated_conjecture,
( ~ hskp19
| ~ c1_1(a1681) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_682,negated_conjecture,
( ~ hskp19
| ~ c3_1(a1681) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_683,negated_conjecture,
( ~ hskp19
| ~ c2_1(a1681) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_684,negated_conjecture,
( ~ hskp18
| ~ c3_1(a1680) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_685,negated_conjecture,
( ~ hskp18
| ~ c1_1(a1680) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_686,negated_conjecture,
( ~ hskp18
| ~ c0_1(a1680) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_687,negated_conjecture,
( ~ hskp17
| ~ c0_1(a1678) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_688,negated_conjecture,
( ~ hskp17
| ~ c1_1(a1678) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_689,negated_conjecture,
( ~ hskp17
| ~ c2_1(a1678) ),
inference(cnf_transformation,[],[f277]) ).
tcf(c_690,negated_conjecture,
( ~ hskp16
| ~ c0_1(a1677) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_691,negated_conjecture,
( ~ hskp16
| ~ c2_1(a1677) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_692,negated_conjecture,
( ~ hskp16
| ~ c1_1(a1677) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_693,negated_conjecture,
( ~ hskp15
| ~ c0_1(a1672) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_694,negated_conjecture,
( ~ hskp14
| ~ c1_1(a1671) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_695,negated_conjecture,
( ~ hskp14
| ~ c3_1(a1671) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_696,negated_conjecture,
( ~ hskp13
| ~ c1_1(a1667) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_697,negated_conjecture,
( ~ hskp12
| ~ c1_1(a1666) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_698,negated_conjecture,
( ~ hskp11
| ~ c3_1(a1664) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_699,negated_conjecture,
( ~ hskp11
| ~ c2_1(a1664) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_700,negated_conjecture,
( ~ hskp11
| ~ c1_1(a1664) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_701,negated_conjecture,
( ~ hskp10
| ~ c2_1(a1663) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_702,negated_conjecture,
( ~ hskp10
| ~ c3_1(a1663) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_703,negated_conjecture,
( ~ hskp10
| ~ c0_1(a1663) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_704,negated_conjecture,
( ~ hskp9
| ~ c3_1(a1660) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_705,negated_conjecture,
( ~ hskp9
| ~ c0_1(a1660) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_706,negated_conjecture,
( ~ hskp9
| ~ c1_1(a1660) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_707,negated_conjecture,
( ~ hskp8
| ~ c1_1(a1657) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_708,negated_conjecture,
( ~ hskp8
| ~ c0_1(a1657) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_709,negated_conjecture,
( ~ hskp7
| ~ c2_1(a1655) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_710,negated_conjecture,
( ~ hskp6
| ~ c1_1(a1650) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_711,negated_conjecture,
( ~ hskp6
| ~ c2_1(a1650) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_712,negated_conjecture,
( ~ hskp6
| ~ c3_1(a1650) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_713,negated_conjecture,
( ~ hskp5
| ~ c1_1(a1648) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_714,negated_conjecture,
( ~ hskp5
| ~ c0_1(a1648) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_715,negated_conjecture,
( ~ hskp4
| ~ c0_1(a1647) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_716,negated_conjecture,
( ~ hskp4
| ~ c2_1(a1647) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_717,negated_conjecture,
( ~ hskp3
| ~ c1_1(a1646) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_718,negated_conjecture,
( ~ hskp3
| ~ c2_1(a1646) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_719,negated_conjecture,
( ~ hskp2
| ~ c1_1(a1645) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_720,negated_conjecture,
( ~ hskp2
| ~ c0_1(a1645) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_721,negated_conjecture,
( ~ hskp2
| ~ c3_1(a1645) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_722,negated_conjecture,
( ~ hskp1
| ~ c1_1(a1643) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_723,negated_conjecture,
( ~ hskp1
| ~ c2_1(a1643) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_724,negated_conjecture,
( ~ hskp0
| ~ c2_1(a1637) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_725,negated_conjecture,
! [X0: $i] :
( hskp10
| hskp56
| c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_726,negated_conjecture,
! [X0: $i] :
( hskp37
| hskp72
| c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_727,negated_conjecture,
! [X0: $i] :
( hskp4
| hskp5
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_728,negated_conjecture,
! [X0: $i] :
( hskp58
| hskp59
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_729,negated_conjecture,
! [X0: $i] :
( hskp18
| hskp60
| c1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_730,negated_conjecture,
! [X0: $i] :
( hskp24
| hskp61
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_731,negated_conjecture,
! [X0: $i] :
( hskp35
| hskp68
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_732,negated_conjecture,
! [X0: $i] :
( hskp36
| hskp71
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_733,negated_conjecture,
! [X0: $i] :
( hskp30
| hskp41
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_734,negated_conjecture,
! [X0: $i] :
( hskp0
| hskp42
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_735,negated_conjecture,
! [X0: $i] :
( hskp6
| hskp48
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_736,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp52
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f324]) ).
tcf(c_737,negated_conjecture,
! [X0: $i] :
( hskp9
| hskp55
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_738,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp57
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_739,negated_conjecture,
! [X0: $i] :
( hskp61
| hskp62
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_740,negated_conjecture,
! [X0: $i] :
( hskp16
| hskp17
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f328]) ).
tcf(c_741,negated_conjecture,
! [X0: $i] :
( hskp19
| hskp20
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_742,negated_conjecture,
! [X0: $i] :
( hskp33
| hskp61
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f330]) ).
tcf(c_743,negated_conjecture,
! [X0: $i] :
( hskp50
| hskp51
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_744,negated_conjecture,
! [X0: $i] :
( hskp12
| hskp13
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_745,negated_conjecture,
! [X0: $i] :
( hskp38
| hskp74
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f333]) ).
tcf(c_746,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c1_1(X0)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_747,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp49
| c1_1(X1)
| c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_748,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp70
| c1_1(X0)
| c2_1(X1)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f336]) ).
tcf(c_749,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp60
| c1_1(X1)
| c1_1(X0)
| c3_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_750,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp21
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_751,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp22
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_752,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp25
| c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_753,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp69
| c1_1(X0)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f341]) ).
tcf(c_754,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp57
| c1_1(X1)
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f342]) ).
tcf(c_755,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c2_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f343]) ).
tcf(c_756,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp2
| c1_1(X1)
| c3_1(X1)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f344]) ).
tcf(c_757,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp30
| c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_758,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp29
| c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f346]) ).
tcf(c_759,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp61
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f347]) ).
tcf(c_760,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp75
| c1_1(X0)
| c2_1(X0)
| c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f348]) ).
tcf(c_761,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp67
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f349]) ).
tcf(c_762,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c1_1(X0)
| c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f350]) ).
tcf(c_763,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp73
| c1_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f351]) ).
tcf(c_764,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp47
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f352]) ).
tcf(c_765,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp39
| c2_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_766,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp40
| c1_1(X1)
| c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f354]) ).
tcf(c_767,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp63
| c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f355]) ).
tcf(c_768,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp26
| c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f356]) ).
tcf(c_769,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp13
| c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f357]) ).
tcf(c_770,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f358]) ).
tcf(c_771,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c1_1(X1)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| c3_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f359]) ).
tcf(c_772,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c2_1(X2)
| c2_1(X0)
| c3_1(X1)
| c0_1(X2)
| ~ ndr1_0
| ~ c3_1(X2)
| ~ c3_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_773,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c2_1(X2)
| c3_1(X2)
| c0_1(X2)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f361]) ).
tcf(c_774,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X2)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f362]) ).
tcf(c_775,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c1_1(X0)
| c3_1(X2)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f363]) ).
tcf(c_776,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c1_1(X0)
| c2_1(X2)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f364]) ).
tcf(c_803,negated_conjecture,
ndr1_0,
inference(global_subsumption_just,[status(thm)],[c_488,c_490,c_486,c_485,c_441]) ).
tcf(c_955,negated_conjecture,
! [X0: $i] :
( hskp37
| hskp72
| c2_1(X0)
| c3_1(X0)
| c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_726,c_490,c_486,c_485,c_441,c_726]) ).
tcf(c_958,negated_conjecture,
! [X0: $i] :
( hskp10
| hskp56
| c2_1(X0)
| c3_1(X0)
| c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_725,c_490,c_486,c_485,c_441,c_725]) ).
tcf(c_961,negated_conjecture,
! [X0: $i] :
( hskp30
| hskp41
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_733,c_490,c_486,c_485,c_441,c_733]) ).
tcf(c_964,negated_conjecture,
! [X0: $i] :
( hskp36
| hskp71
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_732,c_490,c_486,c_485,c_441,c_732]) ).
tcf(c_967,negated_conjecture,
! [X0: $i] :
( hskp35
| hskp68
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_731,c_490,c_486,c_485,c_441,c_731]) ).
tcf(c_970,negated_conjecture,
! [X0: $i] :
( hskp24
| hskp61
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_730,c_490,c_486,c_485,c_441,c_730]) ).
tcf(c_973,negated_conjecture,
! [X0: $i] :
( hskp18
| hskp60
| c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_729,c_490,c_486,c_485,c_441,c_729]) ).
tcf(c_976,negated_conjecture,
! [X0: $i] :
( hskp58
| hskp59
| c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_728,c_490,c_486,c_485,c_441,c_728]) ).
tcf(c_979,negated_conjecture,
! [X0: $i] :
( hskp4
| hskp5
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_727,c_490,c_486,c_485,c_441,c_727]) ).
tcf(c_982,plain,
! [X0: $i] :
( hskp33
| hskp61
| c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_742,c_490,c_486,c_485,c_441,c_742]) ).
tcf(c_983,negated_conjecture,
! [X0: $i] :
( hskp33
| hskp61
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_982]) ).
tcf(c_985,plain,
! [X0: $i] :
( hskp19
| hskp20
| c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_741,c_490,c_486,c_485,c_441,c_741]) ).
tcf(c_986,negated_conjecture,
! [X0: $i] :
( hskp19
| hskp20
| c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_985]) ).
tcf(c_988,plain,
! [X0: $i] :
( hskp16
| hskp17
| c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_740,c_490,c_486,c_485,c_441,c_740]) ).
tcf(c_989,negated_conjecture,
! [X0: $i] :
( hskp16
| hskp17
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_988]) ).
tcf(c_991,plain,
! [X0: $i] :
( hskp61
| hskp62
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_739,c_490,c_486,c_485,c_441,c_739]) ).
tcf(c_992,negated_conjecture,
! [X0: $i] :
( hskp61
| hskp62
| c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_991]) ).
tcf(c_994,plain,
! [X0: $i] :
( hskp11
| hskp57
| c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_738,c_490,c_486,c_485,c_441,c_738]) ).
tcf(c_995,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp57
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_994]) ).
tcf(c_997,plain,
! [X0: $i] :
( hskp9
| hskp55
| c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_737,c_490,c_486,c_485,c_441,c_737]) ).
tcf(c_998,negated_conjecture,
! [X0: $i] :
( hskp9
| hskp55
| c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_997]) ).
tcf(c_1000,plain,
! [X0: $i] :
( hskp7
| hskp52
| c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_736,c_490,c_486,c_485,c_441,c_736]) ).
tcf(c_1001,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp52
| c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1000]) ).
tcf(c_1003,plain,
! [X0: $i] :
( hskp6
| hskp48
| c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_735,c_490,c_486,c_485,c_441,c_735]) ).
tcf(c_1004,negated_conjecture,
! [X0: $i] :
( hskp6
| hskp48
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1003]) ).
tcf(c_1006,plain,
! [X0: $i] :
( hskp0
| hskp42
| c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_734,c_490,c_486,c_485,c_441,c_734]) ).
tcf(c_1007,negated_conjecture,
! [X0: $i] :
( hskp0
| hskp42
| c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1006]) ).
tcf(c_1009,plain,
! [X0: $i] :
( hskp38
| hskp74
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_745,c_490,c_486,c_485,c_441,c_745]) ).
tcf(c_1010,negated_conjecture,
! [X0: $i] :
( hskp38
| hskp74
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1009]) ).
tcf(c_1012,plain,
! [X0: $i] :
( hskp12
| hskp13
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_744,c_490,c_486,c_485,c_441,c_744]) ).
tcf(c_1013,negated_conjecture,
! [X0: $i] :
( hskp12
| hskp13
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_1012]) ).
tcf(c_1015,plain,
! [X0: $i] :
( hskp50
| hskp51
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_743,c_490,c_486,c_485,c_441,c_743]) ).
tcf(c_1016,negated_conjecture,
! [X0: $i] :
( hskp50
| hskp51
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1015]) ).
tcf(c_1018,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp70
| c1_1(X0)
| c2_1(X1)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_748,c_490,c_486,c_485,c_441,c_748]) ).
tcf(c_1020,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp49
| c1_1(X1)
| c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| c0_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_747,c_490,c_486,c_485,c_441,c_747]) ).
tcf(c_1022,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c1_1(X0)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| c0_1(X1)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_746,c_490,c_486,c_485,c_441,c_746]) ).
tcf(c_1024,plain,
! [X0: $i,X1: $i] :
( hskp57
| c1_1(X1)
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_754,c_490,c_486,c_485,c_441,c_754]) ).
tcf(c_1025,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp57
| c1_1(X1)
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1024]) ).
tcf(c_1026,plain,
! [X0: $i,X1: $i] :
( hskp69
| c1_1(X0)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_753,c_490,c_486,c_485,c_441,c_753]) ).
tcf(c_1027,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp69
| c1_1(X0)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_1026]) ).
tcf(c_1028,plain,
! [X0: $i,X1: $i] :
( hskp25
| c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_752,c_490,c_486,c_485,c_441,c_752]) ).
tcf(c_1029,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp25
| c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_1028]) ).
tcf(c_1030,plain,
! [X0: $i,X1: $i] :
( hskp22
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_751,c_490,c_486,c_485,c_441,c_751]) ).
tcf(c_1031,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp22
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1030]) ).
tcf(c_1032,plain,
! [X0: $i,X1: $i] :
( hskp21
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_750,c_490,c_486,c_485,c_441,c_750]) ).
tcf(c_1033,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp21
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_1032]) ).
tcf(c_1035,plain,
! [X0: $i,X1: $i] :
( hskp60
| c1_1(X1)
| c1_1(X0)
| c3_1(X1)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_749,c_490,c_486,c_485,c_441,c_749]) ).
tcf(c_1036,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp60
| c1_1(X1)
| c1_1(X0)
| c3_1(X1)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_1035]) ).
tcf(c_1037,plain,
! [X0: $i,X1: $i] :
( hskp75
| c1_1(X0)
| c2_1(X0)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_760,c_490,c_486,c_485,c_441,c_760]) ).
tcf(c_1038,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp75
| c1_1(X0)
| c2_1(X0)
| c3_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_1037]) ).
tcf(c_1039,plain,
! [X0: $i,X1: $i] :
( hskp61
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_759,c_490,c_486,c_485,c_441,c_759]) ).
tcf(c_1040,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp61
| c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1039]) ).
tcf(c_1042,plain,
! [X0: $i,X1: $i] :
( hskp29
| c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_758,c_490,c_486,c_485,c_441,c_758]) ).
tcf(c_1043,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp29
| c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1042]) ).
tcf(c_1044,plain,
! [X0: $i,X1: $i] :
( hskp30
| c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_757,c_490,c_486,c_485,c_441,c_757]) ).
tcf(c_1045,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp30
| c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1044]) ).
tcf(c_1046,plain,
! [X0: $i,X1: $i] :
( hskp2
| c1_1(X1)
| c3_1(X1)
| c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_756,c_490,c_486,c_485,c_441,c_756]) ).
tcf(c_1047,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp2
| c1_1(X1)
| c3_1(X1)
| c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1046]) ).
tcf(c_1048,plain,
! [X0: $i,X1: $i] :
( hskp46
| c2_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_755,c_490,c_486,c_485,c_441,c_755]) ).
tcf(c_1049,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp46
| c2_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_1048]) ).
tcf(c_1050,plain,
! [X0: $i,X1: $i] :
( hskp40
| c1_1(X1)
| c3_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_766,c_490,c_486,c_485,c_441,c_766]) ).
tcf(c_1051,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp40
| c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1050]) ).
tcf(c_1052,plain,
! [X0: $i,X1: $i] :
( hskp39
| c2_1(X0)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_765,c_490,c_486,c_485,c_441,c_765]) ).
tcf(c_1053,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp39
| c2_1(X0)
| c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1052]) ).
tcf(c_1054,plain,
! [X0: $i,X1: $i] :
( hskp47
| c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_764,c_490,c_486,c_485,c_441,c_764]) ).
tcf(c_1055,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp47
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1054]) ).
tcf(c_1056,plain,
! [X0: $i,X1: $i] :
( hskp73
| c1_1(X0)
| c0_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_763,c_490,c_486,c_485,c_441,c_763]) ).
tcf(c_1057,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp73
| c1_1(X0)
| c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_1056]) ).
tcf(c_1058,plain,
! [X0: $i,X1: $i] :
( hskp34
| c1_1(X0)
| c2_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_762,c_490,c_486,c_485,c_441,c_762]) ).
tcf(c_1059,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c1_1(X0)
| c2_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1058]) ).
tcf(c_1060,plain,
! [X0: $i,X1: $i] :
( hskp67
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_761,c_490,c_486,c_485,c_441,c_761]) ).
tcf(c_1061,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp67
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1060]) ).
tcf(c_1063,plain,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_770,c_490,c_486,c_485,c_441,c_770]) ).
tcf(c_1064,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp0
| c2_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1063]) ).
tcf(c_1065,plain,
! [X0: $i,X1: $i] :
( hskp13
| c2_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_769,c_490,c_486,c_485,c_441,c_769]) ).
tcf(c_1066,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp13
| c2_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1065]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i] :
( hskp26
| c1_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_768,c_490,c_486,c_485,c_441,c_768]) ).
tcf(c_1069,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp26
| c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1068]) ).
tcf(c_1071,plain,
! [X0: $i,X1: $i] :
( hskp63
| c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_767,c_490,c_486,c_485,c_441,c_767]) ).
tcf(c_1072,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp63
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1071]) ).
tcf(c_1073,plain,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c1_1(X1)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| c3_1(X0)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_771,c_490,c_486,c_485,c_441,c_771]) ).
tcf(c_1074,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c1_1(X1)
| c2_1(X2)
| c2_1(X1)
| c3_1(X2)
| c3_1(X0)
| c0_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1073]) ).
tcf(c_1075,plain,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c2_1(X2)
| c2_1(X0)
| c3_1(X1)
| c0_1(X2)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_772,c_490,c_486,c_485,c_441,c_772]) ).
tcf(c_1076,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c2_1(X2)
| c2_1(X0)
| c3_1(X1)
| c0_1(X2)
| ~ c3_1(X2)
| ~ c3_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1075]) ).
tcf(c_1077,plain,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c1_1(X0)
| c2_1(X2)
| c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_776,c_490,c_486,c_485,c_441,c_776]) ).
tcf(c_1078,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c1_1(X0)
| c2_1(X2)
| c2_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1077]) ).
tcf(c_1079,plain,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c1_1(X0)
| c3_1(X2)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X2)
| ~ c1_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_775,c_490,c_486,c_485,c_441,c_775]) ).
tcf(c_1080,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c1_1(X0)
| c3_1(X2)
| c0_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1079]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X2)
| ~ c2_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_774,c_490,c_486,c_485,c_441,c_774]) ).
tcf(c_1082,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X2)
| c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1081]) ).
tcf(c_1083,plain,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c2_1(X2)
| c3_1(X2)
| c0_1(X2)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_773,c_773,c_803]) ).
tcf(c_1084,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c1_1(X1)
| c2_1(X2)
| c3_1(X2)
| c0_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
inference(renaming,[status(thm)],[c_1083]) ).
tcf(c_2715,plain,
( hskp27
| hskp28
| ~ c2_1(a1692) ),
inference(resolution,[status(thm)],[c_494,c_608]) ).
tcf(c_2725,plain,
( hskp27
| hskp28
| ~ c1_1(a1692) ),
inference(resolution,[status(thm)],[c_494,c_607]) ).
tcf(c_2735,plain,
( hskp27
| hskp28
| c0_1(a1692) ),
inference(resolution,[status(thm)],[c_494,c_515]) ).
tcf(c_2754,plain,
( hskp23
| hskp64
| ~ c0_1(a1687) ),
inference(resolution,[status(thm)],[c_493,c_610]) ).
tcf(c_2764,plain,
( hskp23
| hskp64
| ~ c3_1(a1687) ),
inference(resolution,[status(thm)],[c_493,c_609]) ).
tcf(c_2774,plain,
( hskp23
| hskp64
| c2_1(a1687) ),
inference(resolution,[status(thm)],[c_493,c_516]) ).
tcf(c_2793,plain,
( hskp8
| hskp53
| ~ c0_1(a1658) ),
inference(resolution,[status(thm)],[c_491,c_625]) ).
tcf(c_2803,plain,
( hskp8
| hskp53
| c1_1(a1658) ),
inference(resolution,[status(thm)],[c_491,c_534]) ).
tcf(c_2813,plain,
( hskp8
| hskp53
| c3_1(a1658) ),
inference(resolution,[status(thm)],[c_491,c_533]) ).
tcf(c_2832,plain,
( hskp43
| hskp44
| ~ c1_1(a1641) ),
inference(resolution,[status(thm)],[c_489,c_636]) ).
tcf(c_2842,plain,
( hskp43
| hskp44
| ~ c3_1(a1641) ),
inference(resolution,[status(thm)],[c_489,c_635]) ).
tcf(c_2852,plain,
( hskp43
| hskp44
| c2_1(a1641) ),
inference(resolution,[status(thm)],[c_489,c_550]) ).
tcf(c_2871,plain,
( hskp31
| hskp63
| ~ c3_1(a1701) ),
inference(resolution,[status(thm)],[c_496,c_656]) ).
tcf(c_2881,plain,
( hskp31
| hskp63
| c0_1(a1701) ),
inference(resolution,[status(thm)],[c_496,c_569]) ).
tcf(c_2891,plain,
( hskp31
| hskp63
| c1_1(a1701) ),
inference(resolution,[status(thm)],[c_496,c_568]) ).
tcf(c_2910,plain,
( hskp10
| hskp14
| ~ c0_1(a1672) ),
inference(resolution,[status(thm)],[c_492,c_693]) ).
tcf(c_2920,plain,
( hskp10
| hskp14
| c1_1(a1672) ),
inference(resolution,[status(thm)],[c_492,c_583]) ).
tcf(c_2930,plain,
( hskp10
| hskp14
| c3_1(a1672) ),
inference(resolution,[status(thm)],[c_492,c_582]) ).
tcf(c_2949,plain,
( hskp2
| hskp47
| ~ c2_1(a1646) ),
inference(resolution,[status(thm)],[c_490,c_718]) ).
tcf(c_2959,plain,
( hskp2
| hskp47
| ~ c1_1(a1646) ),
inference(resolution,[status(thm)],[c_490,c_717]) ).
tcf(c_2969,plain,
( hskp2
| hskp47
| c0_1(a1646) ),
inference(resolution,[status(thm)],[c_490,c_594]) ).
tcf(c_17908,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| c0_1(X0)
| c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_1084]) ).
tcf(c_17909,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ~ c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_1084]) ).
tcf(c_17910,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_1084]) ).
tcf(c_17911,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1084]) ).
tcf(c_17912,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| c0_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_1082]) ).
tcf(c_17913,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_1082]) ).
tcf(c_17914,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ~ c0_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_1082]) ).
tcf(c_17915,negated_conjecture,
( iPr_def_15
| iPr_def_14
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1082]) ).
tcf(c_17916,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_1080]) ).
tcf(c_17917,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| c0_1(X0)
| ~ c3_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_1080]) ).
tcf(c_17918,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| ~ c0_1(X0)
| ~ c3_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_1080]) ).
tcf(c_17919,negated_conjecture,
( iPr_def_18
| iPr_def_17
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1080]) ).
tcf(c_17920,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_1078]) ).
tcf(c_17921,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_1078]) ).
tcf(c_17922,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_21
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_1078]) ).
tcf(c_17923,negated_conjecture,
( iPr_def_21
| iPr_def_20
| iPr_def_19 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1078]) ).
tcf(c_17924,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_1076]) ).
tcf(c_17925,negated_conjecture,
( iPr_def_22
| iPr_def_15
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1076]) ).
tcf(c_17926,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| c0_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_1074]) ).
tcf(c_17927,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_24
| c3_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_1074]) ).
tcf(c_17928,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_25
| ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_25])],[c_1074]) ).
tcf(c_17929,negated_conjecture,
( iPr_def_25
| iPr_def_24
| iPr_def_23 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1074]) ).
tcf(c_17930,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_26
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_26])],[c_1072]) ).
tcf(c_17931,negated_conjecture,
( iPr_def_26
| iPr_def_18
| hskp63 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1072]) ).
tcf(c_17932,negated_conjecture,
( iPr_def_14
| iPr_def_12
| hskp26 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1069]) ).
tcf(c_17933,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_27
| ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_1066]) ).
tcf(c_17934,negated_conjecture,
( iPr_def_27
| iPr_def_19
| hskp13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1066]) ).
tcf(c_17935,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_28
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_1064]) ).
tcf(c_17936,negated_conjecture,
( iPr_def_28
| iPr_def_27
| hskp0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1064]) ).
tcf(c_17937,negated_conjecture,
( iPr_def_18
| iPr_def_14
| hskp67 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1061]) ).
tcf(c_17938,negated_conjecture,
( iPr_def_27
| iPr_def_11
| hskp34 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1059]) ).
tcf(c_17939,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_29
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_1057]) ).
tcf(c_17940,negated_conjecture,
( iPr_def_29
| iPr_def_14
| hskp73 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1057]) ).
tcf(c_17941,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_30
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_1055]) ).
tcf(c_17942,negated_conjecture,
( iPr_def_30
| iPr_def_19
| hskp47 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1055]) ).
tcf(c_17943,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_31
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_31])],[c_1053]) ).
tcf(c_17944,negated_conjecture,
( iPr_def_31
| iPr_def_15
| hskp39 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1053]) ).
tcf(c_17945,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_32
| c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_32])],[c_1051]) ).
tcf(c_17946,negated_conjecture,
( iPr_def_32
| iPr_def_19
| hskp40 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1051]) ).
tcf(c_17947,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_33
| c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_33])],[c_1049]) ).
tcf(c_17948,negated_conjecture,
( iPr_def_33
| iPr_def_31
| hskp46 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1049]) ).
tcf(c_17949,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_34
| ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_34])],[c_1047]) ).
tcf(c_17950,negated_conjecture,
( iPr_def_34
| iPr_def_22
| hskp2 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1047]) ).
tcf(c_17951,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_35
| ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_35])],[c_1045]) ).
tcf(c_17952,negated_conjecture,
( iPr_def_35
| iPr_def_17
| hskp30 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1045]) ).
tcf(c_17953,negated_conjecture,
( iPr_def_18
| iPr_def_17
| hskp29 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1043]) ).
tcf(c_17954,negated_conjecture,
( iPr_def_35
| iPr_def_30
| hskp61 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1040]) ).
tcf(c_17955,negated_conjecture,
( iPr_def_20
| iPr_def_16
| hskp75 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1038]) ).
tcf(c_17956,negated_conjecture,
( iPr_def_32
| iPr_def_17
| hskp60 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1036]) ).
tcf(c_17957,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_36
| c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_36])],[c_1033]) ).
tcf(c_17958,negated_conjecture,
( iPr_def_36
| iPr_def_33
| hskp21 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1033]) ).
tcf(c_17959,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_37
| c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_37])],[c_1031]) ).
tcf(c_17960,negated_conjecture,
( iPr_def_37
| iPr_def_30
| hskp22 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1031]) ).
tcf(c_17961,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_38
| c0_1(X0)
| c3_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_38])],[c_1029]) ).
tcf(c_17962,negated_conjecture,
( iPr_def_38
| iPr_def_29
| hskp25 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1029]) ).
tcf(c_17963,negated_conjecture,
( iPr_def_36
| iPr_def_17
| hskp69 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1027]) ).
tcf(c_17964,negated_conjecture,
( iPr_def_32
| iPr_def_30
| hskp57 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1025]) ).
tcf(c_17965,negated_conjecture,
( iPr_def_21
| iPr_def_10
| hskp1 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1022]) ).
tcf(c_17966,negated_conjecture,
( iPr_def_33
| iPr_def_23
| hskp49 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1020]) ).
tcf(c_17967,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_39
| c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_39])],[c_1018]) ).
tcf(c_17968,negated_conjecture,
( iPr_def_39
| iPr_def_10
| hskp70 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1018]) ).
tcf(c_17969,negated_conjecture,
( iPr_def_28
| hskp50
| hskp51 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1016]) ).
tcf(c_17970,negated_conjecture,
( iPr_def_26
| hskp12
| hskp13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1013]) ).
tcf(c_17971,negated_conjecture,
( iPr_def_12
| hskp38
| hskp74 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1010]) ).
tcf(c_17972,negated_conjecture,
( iPr_def_25
| hskp0
| hskp42 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1007]) ).
tcf(c_17973,negated_conjecture,
( iPr_def_15
| hskp6
| hskp48 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1004]) ).
tcf(c_17974,negated_conjecture,
( iPr_def_25
| hskp7
| hskp52 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1001]) ).
tcf(c_17975,negated_conjecture,
( iPr_def_25
| hskp9
| hskp55 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_998]) ).
tcf(c_17976,negated_conjecture,
( iPr_def_15
| hskp11
| hskp57 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_995]) ).
tcf(c_17977,negated_conjecture,
( iPr_def_29
| hskp61
| hskp62 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_992]) ).
tcf(c_17978,negated_conjecture,
( iPr_def_18
| hskp16
| hskp17 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_989]) ).
tcf(c_17979,negated_conjecture,
( iPr_def_34
| hskp19
| hskp20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_986]) ).
tcf(c_17980,negated_conjecture,
( iPr_def_15
| hskp33
| hskp61 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_983]) ).
tcf(c_17981,negated_conjecture,
( iPr_def_17
| hskp4
| hskp5 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_979]) ).
tcf(c_17982,negated_conjecture,
( iPr_def_21
| hskp58
| hskp59 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_976]) ).
tcf(c_17983,negated_conjecture,
( iPr_def_32
| hskp18
| hskp60 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_973]) ).
tcf(c_17984,negated_conjecture,
( iPr_def_17
| hskp24
| hskp61 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_970]) ).
tcf(c_17985,negated_conjecture,
( iPr_def_33
| hskp35
| hskp68 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_967]) ).
tcf(c_17986,negated_conjecture,
( iPr_def_33
| hskp36
| hskp71 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_964]) ).
tcf(c_17987,negated_conjecture,
( iPr_def_33
| hskp30
| hskp41 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_961]) ).
tcf(c_17988,negated_conjecture,
( iPr_def_10
| hskp10
| hskp56 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_958]) ).
tcf(c_17989,negated_conjecture,
( iPr_def_10
| hskp37
| hskp72 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_955]) ).
tcf(c_23093,plain,
( c1_1(a1717)
| ~ iPr_def_11
| ~ hskp74
| ~ c2_1(a1717) ),
inference(superposition,[status(thm)],[c_499,c_17909]) ).
tcf(c_23094,plain,
( c1_1(a1716)
| ~ iPr_def_11
| ~ hskp73
| ~ c2_1(a1716) ),
inference(superposition,[status(thm)],[c_502,c_17909]) ).
tcf(c_23096,plain,
( c1_1(a1709)
| ~ iPr_def_11
| ~ hskp69
| ~ c2_1(a1709) ),
inference(superposition,[status(thm)],[c_508,c_17909]) ).
tcf(c_23097,plain,
( c1_1(a1707)
| ~ iPr_def_11
| ~ hskp68
| ~ c2_1(a1707) ),
inference(superposition,[status(thm)],[c_511,c_17909]) ).
tcf(c_23098,plain,
( hskp27
| hskp28
| c1_1(a1692)
| ~ iPr_def_11
| ~ c2_1(a1692) ),
inference(superposition,[status(thm)],[c_2735,c_17909]) ).
tcf(c_23099,plain,
( c1_1(a1686)
| ~ iPr_def_11
| ~ hskp64
| ~ c2_1(a1686) ),
inference(superposition,[status(thm)],[c_517,c_17909]) ).
tcf(c_23100,plain,
( c1_1(a1675)
| ~ iPr_def_11
| ~ hskp62
| ~ c2_1(a1675) ),
inference(superposition,[status(thm)],[c_521,c_17909]) ).
tcf(c_23102,plain,
( c1_1(a1665)
| ~ iPr_def_11
| ~ hskp57
| ~ c2_1(a1665) ),
inference(superposition,[status(thm)],[c_528,c_17909]) ).
tcf(c_23104,plain,
( c1_1(a1656)
| ~ iPr_def_11
| ~ hskp53
| ~ c2_1(a1656) ),
inference(superposition,[status(thm)],[c_536,c_17909]) ).
tcf(c_23105,plain,
( c1_1(a1654)
| ~ iPr_def_11
| ~ hskp52
| ~ c2_1(a1654) ),
inference(superposition,[status(thm)],[c_537,c_17909]) ).
tcf(c_23106,plain,
( c1_1(a1652)
| ~ iPr_def_11
| ~ hskp50
| ~ c2_1(a1652) ),
inference(superposition,[status(thm)],[c_544,c_17909]) ).
tcf(c_23109,plain,
( c1_1(a1639)
| ~ iPr_def_11
| ~ hskp43
| ~ c2_1(a1639) ),
inference(superposition,[status(thm)],[c_555,c_17909]) ).
tcf(c_23110,plain,
( c1_1(a1638)
| ~ iPr_def_11
| ~ hskp42
| ~ c2_1(a1638) ),
inference(superposition,[status(thm)],[c_557,c_17909]) ).
tcf(c_23111,plain,
( c1_1(a1726)
| ~ iPr_def_11
| ~ hskp41
| ~ c2_1(a1726) ),
inference(superposition,[status(thm)],[c_558,c_17909]) ).
tcf(c_23112,plain,
( c1_1(a1714)
| ~ iPr_def_11
| ~ hskp37
| ~ c2_1(a1714) ),
inference(superposition,[status(thm)],[c_565,c_17909]) ).
tcf(c_23114,plain,
( c1_1(a1695)
| ~ iPr_def_11
| ~ hskp29
| ~ c2_1(a1695) ),
inference(superposition,[status(thm)],[c_574,c_17909]) ).
tcf(c_23115,plain,
( c1_1(a1667)
| ~ iPr_def_11
| ~ hskp13
| ~ c2_1(a1667) ),
inference(superposition,[status(thm)],[c_585,c_17909]) ).
tcf(c_23117,plain,
( hskp2
| hskp47
| c1_1(a1646)
| ~ iPr_def_11
| ~ c2_1(a1646) ),
inference(superposition,[status(thm)],[c_2969,c_17909]) ).
tcf(c_23515,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_23117,c_23115,c_23114,c_23112,c_23111,c_23110,c_23109,c_23106,c_23105,c_23104,c_23102,c_23100,c_23099,c_23098,c_23097,c_23096,c_23094,c_23093,c_17989,c_17988,c_17987,c_17986,c_17985,c_17984,c_17983,c_17982,c_17981,c_17980,c_17979,c_17978,c_17977,c_17976,c_17975,c_17974,c_17973,c_17972,c_17971,c_17970,c_17969,c_17968,c_17967,c_17966,c_17965,c_17964,c_17963,c_17962,c_17961,c_17960,c_17959,c_17958,c_17957,c_17956,c_17955,c_17954,c_17953,c_17952,c_17951,c_17950,c_17949,c_17948,c_17947,c_17946,c_17945,c_17944,c_17943,c_17942,c_17941,c_17940,c_17939,c_17938,c_17937,c_17936,c_17935,c_17934,c_17933,c_17932,c_17931,c_17930,c_17929,c_17928,c_17927,c_17926,c_17925,c_17924,c_17923,c_17922,c_17921,c_17920,c_17919,c_17918,c_17917,c_17916,c_17915,c_17914,c_17913,c_17912,c_17911,c_17910,c_17909,c_17908,c_2969,c_2959,c_2949,c_2930,c_2920,c_2910,c_2891,c_2881,c_2871,c_2852,c_2842,c_2832,c_2813,c_2803,c_2793,c_2774,c_2764,c_2754,c_2735,c_2725,c_2715,c_724,c_723,c_722,c_721,c_720,c_719,c_716,c_715,c_714,c_713,c_712,c_711,c_710,c_709,c_708,c_707,c_706,c_705,c_704,c_703,c_702,c_701,c_700,c_699,c_698,c_697,c_696,c_695,c_694,c_692,c_691,c_690,c_689,c_688,c_687,c_686,c_685,c_684,c_683,c_682,c_681,c_680,c_679,c_678,c_677,c_676,c_675,c_674,c_673,c_672,c_671,c_670,c_669,c_668,c_667,c_666,c_665,c_664,c_663,c_662,c_661,c_660,c_659,c_658,c_657,c_655,c_654,c_653,c_652,c_651,c_650,c_649,c_648,c_647,c_646,c_645,c_644,c_643,c_642,c_641,c_640,c_639,c_638,c_637,c_634,c_633,c_632,c_631,c_630,c_629,c_628,c_627,c_626,c_624,c_623,c_622,c_621,c_620,c_619,c_618,c_617,c_616,c_615,c_614,c_613,c_612,c_611,c_606,c_605,c_604,c_603,c_602,c_601,c_600,c_599,c_598,c_597,c_596,c_595,c_593,c_592,c_591,c_590,c_589,c_588,c_587,c_586,c_585,c_584,c_581,c_580,c_579,c_578,c_577,c_576,c_575,c_574,c_573,c_572,c_571,c_570,c_567,c_566,c_565,c_564,c_563,c_562,c_561,c_560,c_559,c_558,c_557,c_556,c_555,c_554,c_553,c_552,c_551,c_549,c_548,c_547,c_546,c_545,c_544,c_543,c_542,c_541,c_540,c_539,c_538,c_537,c_536,c_535,c_532,c_531,c_530,c_529,c_528,c_527,c_526,c_525,c_524,c_523,c_522,c_521,c_520,c_519,c_518,c_517,c_514,c_513,c_512,c_511,c_510,c_509,c_508,c_507,c_506,c_505,c_504,c_503,c_502,c_501,c_500,c_499,c_498,c_497,c_495]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN457-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.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 01:19:39 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running EPR theorem proving
% 0.10/0.41 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.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 5.49/1.66 % SZS status Started for theBenchmark.p
% 5.49/1.66 % SZS status Unsatisfiable for theBenchmark.p
% 5.49/1.66
% 5.49/1.66 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 5.49/1.66
% 5.49/1.66 % ------ iProver source info
% 5.49/1.66
% 5.49/1.66 % git: date: 2026-07-19 20:42:38 +0200
% 5.49/1.66 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 5.49/1.66 % git: non_committed_changes: false
% 5.49/1.66
% 5.49/1.66 % ------ Parsing...% successful
% 5.49/1.66
% 5.49/1.66
% 5.49/1.66 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 5.49/1.66 %
% 5.49/1.66
% 5.49/1.66 % ------ 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 %
% 5.49/1.66
% 5.49/1.66 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 5.49/1.66 gs_s sp: 89 0s gs_e snvd_s sp: 0 0s snvd_e
% 5.49/1.66 % ------ Proving...
% 5.49/1.66 % ------ Problem Properties
% 5.49/1.66
% 5.49/1.66 %
% 5.49/1.66 % clauses 311
% 5.49/1.66 % conjectures 290
% 5.49/1.66 % EPR 311
% 5.49/1.66 % Horn 222
% 5.49/1.66 % unary 0
% 5.49/1.66 % binary 207
% 5.49/1.66 % lits 756
% 5.49/1.66 % lits eq 0
% 5.49/1.66 % fd_pure 0
% 5.49/1.66 % fd_pseudo 0
% 5.49/1.66 % fd_cond 0
% 5.49/1.66 % fd_pseudo_cond 0
% 5.49/1.66 % AC symbols 0
% 5.49/1.66
% 5.49/1.66 % ------ Schedule EPR non Horn non eq is on
% 5.49/1.66
% 5.49/1.66 % ------ no equalities: superposition off
% 5.49/1.66
% 5.49/1.66 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 5.49/1.66
% 5.49/1.66
% 5.49/1.66 % ------
% 5.49/1.66 % Current options:
% 5.49/1.66 % ------
% 5.49/1.66
% 5.49/1.66
% 5.49/1.66 %
% 5.49/1.66
% 5.49/1.66 % ------ Proving...
% 5.49/1.66 %
% 5.49/1.66
% 5.49/1.66 % SZS status Unsatisfiable for theBenchmark.p
% 5.49/1.66
% 5.49/1.66 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 5.49/1.68
% 5.49/1.68
%------------------------------------------------------------------------------