%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN447-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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:40:15 PM UTC 2026
% Result : Unsatisfiable 3.58s 1.15s
% Output : CNFRefutation 3.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 256
% Syntax : Number of formulae : 709 ( 2 unt; 0 def)
% Number of atoms : 2558 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 3149 (1300 ~;1849 |; 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 : 101 ( 100 usr; 97 prp; 0-1 aty)
% Number of functors : 64 ( 64 usr; 64 con; 0-0 aty)
% Number of variables : 379 ( 0 sgn 379 !; 0 ?; 287 :)
% Comments :
%------------------------------------------------------------------------------
fof(f25,negated_conjecture,
( ndr1_0
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
fof(f46,negated_conjecture,
( ndr1_0
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ndr1_0
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f64,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( hskp30
| hskp29
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( hskp14
| hskp38
| hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( hskp18
| hskp17
| hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( hskp28
| hskp27
| hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( hskp63
| hskp56
| hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( c1_1(a1105)
| ~ hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( c3_1(a1105)
| ~ hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( c2_1(a1103)
| ~ hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( c3_1(a1103)
| ~ hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( c1_1(a1103)
| ~ hskp62 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( c2_1(a1099)
| ~ hskp61 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( c2_1(a1097)
| ~ hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( c3_1(a1097)
| ~ hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( c1_1(a1095)
| ~ hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( c2_1(a1086)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( c3_1(a1086)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( c2_1(a1085)
| ~ hskp57 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( c0_1(a1085)
| ~ hskp57 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( c3_1(a1085)
| ~ hskp57 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( c0_1(a1084)
| ~ hskp56 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( c1_1(a1081)
| ~ hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( c3_1(a1081)
| ~ hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( c3_1(a1074)
| ~ hskp54 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( c0_1(a1074)
| ~ hskp54 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( c2_1(a1074)
| ~ hskp54 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( c1_1(a1073)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( c2_1(a1073)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( c0_1(a1073)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( c1_1(a1071)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( c0_1(a1071)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( c3_1(a1071)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( c2_1(a1070)
| ~ hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( c0_1(a1070)
| ~ hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( c3_1(a1069)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( c1_1(a1069)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( c1_1(a1065)
| ~ hskp49 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( c3_1(a1062)
| ~ hskp48 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( c2_1(a1062)
| ~ hskp48 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( c0_1(a1062)
| ~ hskp48 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( c2_1(a1056)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( c1_1(a1056)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( c3_1(a1056)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( c0_1(a1053)
| ~ hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( c0_1(a1052)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( c3_1(a1052)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( c2_1(a1052)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( c1_1(a1051)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( c0_1(a1051)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( c0_1(a1049)
| ~ hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( c2_1(a1049)
| ~ hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( c1_1(a1049)
| ~ hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( c1_1(a1046)
| ~ hskp42 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( c0_1(a1046)
| ~ hskp42 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( c3_1(a1045)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( c3_1(a1044)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( c0_1(a1044)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( c0_1(a1042)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( c2_1(a1042)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( c1_1(a1040)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( c3_1(a1040)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( c2_1(a1040)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( c0_1(a1037)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( c3_1(a1037)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( c3_1(a1034)
| ~ hskp36 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( c1_1(a1034)
| ~ hskp36 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( c0_1(a1033)
| ~ hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( c1_1(a1033)
| ~ hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( c3_1(a1033)
| ~ hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( c3_1(a1032)
| ~ hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
( c3_1(a1031)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
( c2_1(a1031)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
( c1_1(a1029)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( c2_1(a1029)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
( c0_1(a1028)
| ~ hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
( c3_1(a1028)
| ~ hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause139) ).
fof(f140,negated_conjecture,
( c3_1(a1022)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
( c1_1(a1022)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
( c2_1(a1021)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
( c2_1(a1102)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
( c3_1(a1101)
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
( c1_1(a1101)
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
( c1_1(a1098)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
( c0_1(a1089)
| ~ hskp24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
( c1_1(a1088)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
( c3_1(a1088)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
( c2_1(a1083)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
( c3_1(a1083)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
( c1_1(a1079)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( c2_1(a1078)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
( c0_1(a1078)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( c3_1(a1077)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
( c2_1(a1064)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
( c0_1(a1064)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
( c3_1(a1059)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
( c2_1(a1059)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( c0_1(a1048)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( c3_1(a1048)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
( c0_1(a1043)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
( c1_1(a1041)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
( c1_1(a1039)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
( c2_1(a1038)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause165) ).
fof(f166,negated_conjecture,
( c0_1(a1036)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
( c0_1(a1035)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
( c1_1(a1035)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( c1_1(a1027)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
( c2_1(a1027)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
( c0_1(a1026)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
( c2_1(a1024)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
( c1_1(a1024)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
( c2_1(a1023)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
( c0_1(a1020)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
( ~ hskp63
| ~ c2_1(a1105) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
( ~ hskp61
| ~ c3_1(a1099) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
( ~ hskp61
| ~ c0_1(a1099) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
( ~ hskp60
| ~ c0_1(a1097) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
( ~ hskp59
| ~ c0_1(a1095) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
( ~ hskp59
| ~ c3_1(a1095) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( ~ hskp58
| ~ c0_1(a1086) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
( ~ hskp56
| ~ c3_1(a1084) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
( ~ hskp56
| ~ c1_1(a1084) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
( ~ hskp55
| ~ c0_1(a1081) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
( ~ hskp51
| ~ c1_1(a1070) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
( ~ hskp50
| ~ c0_1(a1069) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
( ~ hskp49
| ~ c0_1(a1065) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
( ~ hskp49
| ~ c2_1(a1065) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause189) ).
fof(f190,negated_conjecture,
( ~ hskp46
| ~ c1_1(a1053) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause190) ).
fof(f191,negated_conjecture,
( ~ hskp46
| ~ c2_1(a1053) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause191) ).
fof(f192,negated_conjecture,
( ~ hskp44
| ~ c2_1(a1051) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
( ~ hskp42
| ~ c2_1(a1046) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
( ~ hskp41
| ~ c1_1(a1045) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
( ~ hskp41
| ~ c0_1(a1045) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
( ~ hskp40
| ~ c1_1(a1044) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause196) ).
fof(f197,negated_conjecture,
( ~ hskp39
| ~ c1_1(a1042) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause197) ).
fof(f198,negated_conjecture,
( ~ hskp37
| ~ c1_1(a1037) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause198) ).
fof(f199,negated_conjecture,
( ~ hskp36
| ~ c0_1(a1034) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
( ~ hskp34
| ~ c2_1(a1032) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
( ~ hskp34
| ~ c1_1(a1032) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ hskp33
| ~ c1_1(a1031) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ hskp32
| ~ c0_1(a1029) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
( ~ hskp31
| ~ c1_1(a1028) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
( ~ hskp30
| ~ c2_1(a1022) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
( ~ hskp29
| ~ c1_1(a1021) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ hskp29
| ~ c3_1(a1021) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ hskp28
| ~ c0_1(a1102) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause208) ).
fof(f209,negated_conjecture,
( ~ hskp28
| ~ c1_1(a1102) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause209) ).
fof(f210,negated_conjecture,
( ~ hskp27
| ~ c0_1(a1101) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause210) ).
fof(f211,negated_conjecture,
( ~ hskp26
| ~ c3_1(a1098) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause211) ).
fof(f212,negated_conjecture,
( ~ hskp26
| ~ c0_1(a1098) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause212) ).
fof(f213,negated_conjecture,
( ~ hskp25
| ~ c3_1(a1091) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause213) ).
fof(f214,negated_conjecture,
( ~ hskp25
| ~ c0_1(a1091) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause214) ).
fof(f215,negated_conjecture,
( ~ hskp25
| ~ c2_1(a1091) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause215) ).
fof(f216,negated_conjecture,
( ~ hskp24
| ~ c2_1(a1089) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause216) ).
fof(f217,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1089) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
( ~ hskp23
| ~ c2_1(a1088) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ hskp22
| ~ c1_1(a1083) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause219) ).
fof(f220,negated_conjecture,
( ~ hskp21
| ~ c3_1(a1082) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause220) ).
fof(f221,negated_conjecture,
( ~ hskp21
| ~ c2_1(a1082) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause221) ).
fof(f222,negated_conjecture,
( ~ hskp21
| ~ c0_1(a1082) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause222) ).
fof(f223,negated_conjecture,
( ~ hskp20
| ~ c0_1(a1080) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause223) ).
fof(f224,negated_conjecture,
( ~ hskp20
| ~ c2_1(a1080) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause224) ).
fof(f225,negated_conjecture,
( ~ hskp20
| ~ c1_1(a1080) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause225) ).
fof(f226,negated_conjecture,
( ~ hskp19
| ~ c0_1(a1079) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause226) ).
fof(f227,negated_conjecture,
( ~ hskp19
| ~ c2_1(a1079) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause227) ).
fof(f228,negated_conjecture,
( ~ hskp18
| ~ c1_1(a1078) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause228) ).
fof(f229,negated_conjecture,
( ~ hskp17
| ~ c0_1(a1077) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause229) ).
fof(f230,negated_conjecture,
( ~ hskp17
| ~ c2_1(a1077) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause230) ).
fof(f231,negated_conjecture,
( ~ hskp16
| ~ c3_1(a1064) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause231) ).
fof(f232,negated_conjecture,
( ~ hskp15
| ~ c1_1(a1059) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause232) ).
fof(f233,negated_conjecture,
( ~ hskp14
| ~ c0_1(a1055) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause233) ).
fof(f234,negated_conjecture,
( ~ hskp14
| ~ c1_1(a1055) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause234) ).
fof(f235,negated_conjecture,
( ~ hskp14
| ~ c2_1(a1055) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause235) ).
fof(f236,negated_conjecture,
( ~ hskp13
| ~ c2_1(a1048) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause236) ).
fof(f237,negated_conjecture,
( ~ hskp12
| ~ c1_1(a1043) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause237) ).
fof(f238,negated_conjecture,
( ~ hskp12
| ~ c3_1(a1043) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause238) ).
fof(f239,negated_conjecture,
( ~ hskp11
| ~ c3_1(a1041) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause239) ).
fof(f240,negated_conjecture,
( ~ hskp11
| ~ c2_1(a1041) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause240) ).
fof(f241,negated_conjecture,
( ~ hskp10
| ~ c2_1(a1039) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause241) ).
fof(f242,negated_conjecture,
( ~ hskp10
| ~ c0_1(a1039) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause242) ).
fof(f243,negated_conjecture,
( ~ hskp9
| ~ c1_1(a1038) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause243) ).
fof(f244,negated_conjecture,
( ~ hskp9
| ~ c0_1(a1038) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
( ~ hskp8
| ~ c3_1(a1036) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
( ~ hskp8
| ~ c1_1(a1036) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
( ~ hskp7
| ~ c2_1(a1035) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause247) ).
fof(f248,negated_conjecture,
( ~ hskp6
| ~ c2_1(a1030) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause248) ).
fof(f249,negated_conjecture,
( ~ hskp6
| ~ c3_1(a1030) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause249) ).
fof(f250,negated_conjecture,
( ~ hskp6
| ~ c0_1(a1030) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause250) ).
fof(f251,negated_conjecture,
( ~ hskp5
| ~ c3_1(a1027) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause251) ).
fof(f252,negated_conjecture,
( ~ hskp4
| ~ c2_1(a1026) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause252) ).
fof(f253,negated_conjecture,
( ~ hskp4
| ~ c1_1(a1026) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause253) ).
fof(f254,negated_conjecture,
( ~ hskp3
| ~ c0_1(a1025) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause254) ).
fof(f255,negated_conjecture,
( ~ hskp3
| ~ c3_1(a1025) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause255) ).
fof(f256,negated_conjecture,
( ~ hskp3
| ~ c2_1(a1025) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause256) ).
fof(f257,negated_conjecture,
( ~ hskp2
| ~ c3_1(a1024) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause257) ).
fof(f258,negated_conjecture,
( ~ hskp1
| ~ c1_1(a1023) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause258) ).
fof(f259,negated_conjecture,
( ~ hskp1
| ~ c0_1(a1023) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause259) ).
fof(f260,negated_conjecture,
( ~ hskp0
| ~ c1_1(a1020) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause260) ).
fof(f261,negated_conjecture,
( ~ hskp0
| ~ c2_1(a1020) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause261) ).
fof(f262,negated_conjecture,
! [X0] :
( hskp10
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause262) ).
fof(f263,negated_conjecture,
! [X0] :
( hskp45
| hskp44
| c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause263) ).
fof(f264,negated_conjecture,
! [X0] :
( hskp14
| hskp48
| c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause264) ).
fof(f265,negated_conjecture,
! [X0] :
( hskp7
| hskp36
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause265) ).
fof(f266,negated_conjecture,
! [X0] :
( hskp33
| hskp15
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause266) ).
fof(f267,negated_conjecture,
! [X0] :
( hskp48
| hskp36
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause267) ).
fof(f268,negated_conjecture,
! [X0] :
( hskp16
| hskp42
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause268) ).
fof(f269,negated_conjecture,
! [X0] :
( hskp20
| hskp19
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause269) ).
fof(f270,negated_conjecture,
! [X0] :
( hskp21
| hskp55
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause270) ).
fof(f271,negated_conjecture,
! [X0] :
( hskp26
| hskp60
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause271) ).
fof(f272,negated_conjecture,
! [X0] :
( hskp5
| hskp4
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause272) ).
fof(f273,negated_conjecture,
! [X0] :
( hskp6
| hskp32
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause273) ).
fof(f274,negated_conjecture,
! [X0] :
( hskp37
| hskp8
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause274) ).
fof(f275,negated_conjecture,
! [X0] :
( hskp41
| hskp40
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause275) ).
fof(f276,negated_conjecture,
! [X0] :
( hskp43
| hskp13
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause276) ).
fof(f277,negated_conjecture,
! [X0] :
( hskp43
| hskp10
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause277) ).
fof(f278,negated_conjecture,
! [X0] :
( hskp12
| hskp7
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause278) ).
fof(f279,negated_conjecture,
! [X0] :
( hskp51
| hskp50
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause279) ).
fof(f280,negated_conjecture,
! [X0] :
( hskp34
| hskp52
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause280) ).
fof(f281,negated_conjecture,
! [X0] :
( hskp56
| hskp22
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause281) ).
fof(f282,negated_conjecture,
! [X0] :
( hskp39
| hskp11
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause282) ).
fof(f283,negated_conjecture,
! [X0] :
( hskp47
| hskp54
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause283) ).
fof(f284,negated_conjecture,
! [X0] :
( hskp23
| hskp33
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause284) ).
fof(f285,negated_conjecture,
! [X0,X1] :
( hskp3
| c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause285) ).
fof(f286,negated_conjecture,
! [X0,X1] :
( hskp35
| c3_1(X1)
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause286) ).
fof(f287,negated_conjecture,
! [X0,X1] :
( hskp9
| c2_1(X1)
| c3_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause287) ).
fof(f288,negated_conjecture,
! [X0,X1] :
( hskp1
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause288) ).
fof(f289,negated_conjecture,
! [X0,X1] :
( hskp34
| c3_1(X1)
| c2_1(X1)
| c1_1(X0)
| c3_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause289) ).
fof(f290,negated_conjecture,
! [X0,X1] :
( hskp49
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause290) ).
fof(f291,negated_conjecture,
! [X0,X1] :
( hskp24
| c0_1(X0)
| c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause291) ).
fof(f292,negated_conjecture,
! [X0,X1] :
( hskp1
| c1_1(X1)
| c2_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause292) ).
fof(f293,negated_conjecture,
! [X0,X1] :
( hskp2
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause293) ).
fof(f294,negated_conjecture,
! [X0,X1] :
( hskp31
| c2_1(X1)
| c3_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause294) ).
fof(f295,negated_conjecture,
! [X0,X1] :
( hskp42
| c0_1(X1)
| c1_1(X1)
| c2_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause295) ).
fof(f296,negated_conjecture,
! [X0,X1] :
( hskp58
| c2_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause296) ).
fof(f297,negated_conjecture,
! [X0,X1] :
( hskp59
| c2_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause297) ).
fof(f298,negated_conjecture,
! [X0,X1] :
( hskp35
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause298) ).
fof(f299,negated_conjecture,
! [X0,X1] :
( hskp61
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause299) ).
fof(f300,negated_conjecture,
! [X0,X1] :
( hskp33
| c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause300) ).
fof(f301,negated_conjecture,
! [X0,X1] :
( hskp38
| c2_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause301) ).
fof(f302,negated_conjecture,
! [X0,X1] :
( hskp4
| c2_1(X1)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause302) ).
fof(f303,negated_conjecture,
! [X0,X1] :
( hskp47
| c1_1(X1)
| c3_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause303) ).
fof(f304,negated_conjecture,
! [X0,X1] :
( hskp57
| c2_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause304) ).
fof(f305,negated_conjecture,
! [X0,X1] :
( hskp25
| c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause305) ).
fof(f306,negated_conjecture,
! [X0,X1] :
( hskp51
| c2_1(X0)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause306) ).
fof(f307,negated_conjecture,
! [X0,X1] :
( hskp12
| c2_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause307) ).
fof(f308,negated_conjecture,
! [X0,X1] :
( hskp7
| c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause308) ).
fof(f309,negated_conjecture,
! [X0,X1] :
( hskp53
| c1_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause309) ).
fof(f310,negated_conjecture,
! [X0,X1] :
( hskp36
| c0_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause310) ).
fof(f311,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause311) ).
fof(f312,negated_conjecture,
! [X2,X0,X1] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2)
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c3_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause312) ).
fof(f313,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c3_1(X0)
| c2_1(X2)
| c1_1(X2)
| c3_1(X2)
| ~ c2_1(X1)
| ~ c0_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause313) ).
fof(f314,negated_conjecture,
! [X2,X0,X1] :
( c2_1(X1)
| c0_1(X1)
| c1_1(X2)
| c3_1(X2)
| c0_1(X2)
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause314) ).
fof(f315,negated_conjecture,
! [X2,X0,X1] :
( c0_1(X1)
| c1_1(X0)
| c3_1(X0)
| c2_1(X2)
| c1_1(X2)
| c0_1(X2)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause315) ).
fof(f316,negated_conjecture,
! [X2,X0,X1] :
( c1_1(X1)
| c3_1(X1)
| c3_1(X0)
| ~ c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause316) ).
tcf(c_389,negated_conjecture,
( ndr1_0
| ~ hskp39 ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_410,negated_conjecture,
( ndr1_0
| ~ hskp18 ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_411,negated_conjecture,
( ndr1_0
| ~ hskp17 ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_428,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_429,negated_conjecture,
( hskp0
| hskp29
| hskp30 ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_430,negated_conjecture,
( hskp14
| hskp38
| hskp46 ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_431,negated_conjecture,
( hskp17
| hskp18
| hskp39 ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_432,negated_conjecture,
( hskp27
| hskp28
| hskp43 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_433,negated_conjecture,
( hskp56
| hskp62
| hskp63 ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_434,negated_conjecture,
( c1_1(a1105)
| ~ hskp63 ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_435,negated_conjecture,
( c3_1(a1105)
| ~ hskp63 ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_436,negated_conjecture,
( c2_1(a1103)
| ~ hskp62 ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_437,negated_conjecture,
( c3_1(a1103)
| ~ hskp62 ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_438,negated_conjecture,
( c1_1(a1103)
| ~ hskp62 ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_439,negated_conjecture,
( c2_1(a1099)
| ~ hskp61 ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_440,negated_conjecture,
( c2_1(a1097)
| ~ hskp60 ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_441,negated_conjecture,
( c3_1(a1097)
| ~ hskp60 ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_442,negated_conjecture,
( c1_1(a1095)
| ~ hskp59 ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_443,negated_conjecture,
( c2_1(a1086)
| ~ hskp58 ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_444,negated_conjecture,
( c3_1(a1086)
| ~ hskp58 ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_445,negated_conjecture,
( c2_1(a1085)
| ~ hskp57 ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_446,negated_conjecture,
( c0_1(a1085)
| ~ hskp57 ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_447,negated_conjecture,
( c3_1(a1085)
| ~ hskp57 ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_448,negated_conjecture,
( c0_1(a1084)
| ~ hskp56 ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_449,negated_conjecture,
( c1_1(a1081)
| ~ hskp55 ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_450,negated_conjecture,
( c3_1(a1081)
| ~ hskp55 ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_451,negated_conjecture,
( c3_1(a1074)
| ~ hskp54 ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_452,negated_conjecture,
( c0_1(a1074)
| ~ hskp54 ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_453,negated_conjecture,
( c2_1(a1074)
| ~ hskp54 ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_454,negated_conjecture,
( c1_1(a1073)
| ~ hskp53 ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_455,negated_conjecture,
( c2_1(a1073)
| ~ hskp53 ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_456,negated_conjecture,
( c0_1(a1073)
| ~ hskp53 ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_457,negated_conjecture,
( c1_1(a1071)
| ~ hskp52 ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_458,negated_conjecture,
( c0_1(a1071)
| ~ hskp52 ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_459,negated_conjecture,
( c3_1(a1071)
| ~ hskp52 ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_460,negated_conjecture,
( c2_1(a1070)
| ~ hskp51 ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_461,negated_conjecture,
( c0_1(a1070)
| ~ hskp51 ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_462,negated_conjecture,
( c3_1(a1069)
| ~ hskp50 ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_463,negated_conjecture,
( c1_1(a1069)
| ~ hskp50 ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_464,negated_conjecture,
( c1_1(a1065)
| ~ hskp49 ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_465,negated_conjecture,
( c3_1(a1062)
| ~ hskp48 ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_466,negated_conjecture,
( c2_1(a1062)
| ~ hskp48 ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_467,negated_conjecture,
( c0_1(a1062)
| ~ hskp48 ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_468,negated_conjecture,
( c2_1(a1056)
| ~ hskp47 ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_469,negated_conjecture,
( c1_1(a1056)
| ~ hskp47 ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_470,negated_conjecture,
( c3_1(a1056)
| ~ hskp47 ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_471,negated_conjecture,
( c0_1(a1053)
| ~ hskp46 ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_472,negated_conjecture,
( c0_1(a1052)
| ~ hskp45 ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_473,negated_conjecture,
( c3_1(a1052)
| ~ hskp45 ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_474,negated_conjecture,
( c2_1(a1052)
| ~ hskp45 ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_475,negated_conjecture,
( c1_1(a1051)
| ~ hskp44 ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_476,negated_conjecture,
( c0_1(a1051)
| ~ hskp44 ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_477,negated_conjecture,
( c0_1(a1049)
| ~ hskp43 ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_478,negated_conjecture,
( c2_1(a1049)
| ~ hskp43 ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_479,negated_conjecture,
( c1_1(a1049)
| ~ hskp43 ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_480,negated_conjecture,
( c1_1(a1046)
| ~ hskp42 ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_481,negated_conjecture,
( c0_1(a1046)
| ~ hskp42 ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_482,negated_conjecture,
( c3_1(a1045)
| ~ hskp41 ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_483,negated_conjecture,
( c3_1(a1044)
| ~ hskp40 ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_484,negated_conjecture,
( c0_1(a1044)
| ~ hskp40 ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_485,negated_conjecture,
( c0_1(a1042)
| ~ hskp39 ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_486,negated_conjecture,
( c2_1(a1042)
| ~ hskp39 ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_487,negated_conjecture,
( c1_1(a1040)
| ~ hskp38 ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_488,negated_conjecture,
( c3_1(a1040)
| ~ hskp38 ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_489,negated_conjecture,
( c2_1(a1040)
| ~ hskp38 ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_490,negated_conjecture,
( c0_1(a1037)
| ~ hskp37 ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_491,negated_conjecture,
( c3_1(a1037)
| ~ hskp37 ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_492,negated_conjecture,
( c3_1(a1034)
| ~ hskp36 ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_493,negated_conjecture,
( c1_1(a1034)
| ~ hskp36 ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_494,negated_conjecture,
( c0_1(a1033)
| ~ hskp35 ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_495,negated_conjecture,
( c1_1(a1033)
| ~ hskp35 ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_496,negated_conjecture,
( c3_1(a1033)
| ~ hskp35 ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_497,negated_conjecture,
( c3_1(a1032)
| ~ hskp34 ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_498,negated_conjecture,
( c3_1(a1031)
| ~ hskp33 ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_499,negated_conjecture,
( c2_1(a1031)
| ~ hskp33 ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_500,negated_conjecture,
( c1_1(a1029)
| ~ hskp32 ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_501,negated_conjecture,
( c2_1(a1029)
| ~ hskp32 ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_502,negated_conjecture,
( c0_1(a1028)
| ~ hskp31 ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_503,negated_conjecture,
( c3_1(a1028)
| ~ hskp31 ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_504,negated_conjecture,
( c3_1(a1022)
| ~ hskp30 ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_505,negated_conjecture,
( c1_1(a1022)
| ~ hskp30 ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_506,negated_conjecture,
( c2_1(a1021)
| ~ hskp29 ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_507,negated_conjecture,
( c2_1(a1102)
| ~ hskp28 ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_508,negated_conjecture,
( c3_1(a1101)
| ~ hskp27 ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_509,negated_conjecture,
( c1_1(a1101)
| ~ hskp27 ),
inference(cnf_transformation,[],[f145]) ).
tcf(c_510,negated_conjecture,
( c1_1(a1098)
| ~ hskp26 ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_511,negated_conjecture,
( c0_1(a1089)
| ~ hskp24 ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_512,negated_conjecture,
( c1_1(a1088)
| ~ hskp23 ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_513,negated_conjecture,
( c3_1(a1088)
| ~ hskp23 ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_514,negated_conjecture,
( c2_1(a1083)
| ~ hskp22 ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_515,negated_conjecture,
( c3_1(a1083)
| ~ hskp22 ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_516,negated_conjecture,
( c1_1(a1079)
| ~ hskp19 ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_517,negated_conjecture,
( c2_1(a1078)
| ~ hskp18 ),
inference(cnf_transformation,[],[f153]) ).
tcf(c_518,negated_conjecture,
( c0_1(a1078)
| ~ hskp18 ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_519,negated_conjecture,
( c3_1(a1077)
| ~ hskp17 ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_520,negated_conjecture,
( c2_1(a1064)
| ~ hskp16 ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_521,negated_conjecture,
( c0_1(a1064)
| ~ hskp16 ),
inference(cnf_transformation,[],[f157]) ).
tcf(c_522,negated_conjecture,
( c3_1(a1059)
| ~ hskp15 ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_523,negated_conjecture,
( c2_1(a1059)
| ~ hskp15 ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_524,negated_conjecture,
( c0_1(a1048)
| ~ hskp13 ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_525,negated_conjecture,
( c3_1(a1048)
| ~ hskp13 ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_526,negated_conjecture,
( c0_1(a1043)
| ~ hskp12 ),
inference(cnf_transformation,[],[f162]) ).
tcf(c_527,negated_conjecture,
( c1_1(a1041)
| ~ hskp11 ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_528,negated_conjecture,
( c1_1(a1039)
| ~ hskp10 ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_529,negated_conjecture,
( c2_1(a1038)
| ~ hskp9 ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_530,negated_conjecture,
( c0_1(a1036)
| ~ hskp8 ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_531,negated_conjecture,
( c0_1(a1035)
| ~ hskp7 ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_532,negated_conjecture,
( c1_1(a1035)
| ~ hskp7 ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_533,negated_conjecture,
( c1_1(a1027)
| ~ hskp5 ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_534,negated_conjecture,
( c2_1(a1027)
| ~ hskp5 ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_535,negated_conjecture,
( c0_1(a1026)
| ~ hskp4 ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_536,negated_conjecture,
( c2_1(a1024)
| ~ hskp2 ),
inference(cnf_transformation,[],[f172]) ).
tcf(c_537,negated_conjecture,
( c1_1(a1024)
| ~ hskp2 ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_538,negated_conjecture,
( c2_1(a1023)
| ~ hskp1 ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_539,negated_conjecture,
( c0_1(a1020)
| ~ hskp0 ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_540,negated_conjecture,
( ~ hskp63
| ~ c2_1(a1105) ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_541,negated_conjecture,
( ~ hskp61
| ~ c3_1(a1099) ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_542,negated_conjecture,
( ~ hskp61
| ~ c0_1(a1099) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_543,negated_conjecture,
( ~ hskp60
| ~ c0_1(a1097) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_544,negated_conjecture,
( ~ hskp59
| ~ c0_1(a1095) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_545,negated_conjecture,
( ~ hskp59
| ~ c3_1(a1095) ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_546,negated_conjecture,
( ~ hskp58
| ~ c0_1(a1086) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_547,negated_conjecture,
( ~ hskp56
| ~ c3_1(a1084) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_548,negated_conjecture,
( ~ hskp56
| ~ c1_1(a1084) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_549,negated_conjecture,
( ~ hskp55
| ~ c0_1(a1081) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_550,negated_conjecture,
( ~ hskp51
| ~ c1_1(a1070) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_551,negated_conjecture,
( ~ hskp50
| ~ c0_1(a1069) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_552,negated_conjecture,
( ~ hskp49
| ~ c0_1(a1065) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_553,negated_conjecture,
( ~ hskp49
| ~ c2_1(a1065) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_554,negated_conjecture,
( ~ hskp46
| ~ c1_1(a1053) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_555,negated_conjecture,
( ~ hskp46
| ~ c2_1(a1053) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_556,negated_conjecture,
( ~ hskp44
| ~ c2_1(a1051) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_557,negated_conjecture,
( ~ hskp42
| ~ c2_1(a1046) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_558,negated_conjecture,
( ~ hskp41
| ~ c1_1(a1045) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_559,negated_conjecture,
( ~ hskp41
| ~ c0_1(a1045) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_560,negated_conjecture,
( ~ hskp40
| ~ c1_1(a1044) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_561,negated_conjecture,
( ~ hskp39
| ~ c1_1(a1042) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_562,negated_conjecture,
( ~ hskp37
| ~ c1_1(a1037) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_563,negated_conjecture,
( ~ hskp36
| ~ c0_1(a1034) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_564,negated_conjecture,
( ~ hskp34
| ~ c2_1(a1032) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_565,negated_conjecture,
( ~ hskp34
| ~ c1_1(a1032) ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_566,negated_conjecture,
( ~ hskp33
| ~ c1_1(a1031) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_567,negated_conjecture,
( ~ hskp32
| ~ c0_1(a1029) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_568,negated_conjecture,
( ~ hskp31
| ~ c1_1(a1028) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_569,negated_conjecture,
( ~ hskp30
| ~ c2_1(a1022) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_570,negated_conjecture,
( ~ hskp29
| ~ c1_1(a1021) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_571,negated_conjecture,
( ~ hskp29
| ~ c3_1(a1021) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_572,negated_conjecture,
( ~ hskp28
| ~ c0_1(a1102) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_573,negated_conjecture,
( ~ hskp28
| ~ c1_1(a1102) ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_574,negated_conjecture,
( ~ hskp27
| ~ c0_1(a1101) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_575,negated_conjecture,
( ~ hskp26
| ~ c3_1(a1098) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_576,negated_conjecture,
( ~ hskp26
| ~ c0_1(a1098) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_577,negated_conjecture,
( ~ hskp25
| ~ c3_1(a1091) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_578,negated_conjecture,
( ~ hskp25
| ~ c0_1(a1091) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_579,negated_conjecture,
( ~ hskp25
| ~ c2_1(a1091) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_580,negated_conjecture,
( ~ hskp24
| ~ c2_1(a1089) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_581,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1089) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_582,negated_conjecture,
( ~ hskp23
| ~ c2_1(a1088) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_583,negated_conjecture,
( ~ hskp22
| ~ c1_1(a1083) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_584,negated_conjecture,
( ~ hskp21
| ~ c3_1(a1082) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_585,negated_conjecture,
( ~ hskp21
| ~ c2_1(a1082) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_586,negated_conjecture,
( ~ hskp21
| ~ c0_1(a1082) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_587,negated_conjecture,
( ~ hskp20
| ~ c0_1(a1080) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_588,negated_conjecture,
( ~ hskp20
| ~ c2_1(a1080) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_589,negated_conjecture,
( ~ hskp20
| ~ c1_1(a1080) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_590,negated_conjecture,
( ~ hskp19
| ~ c0_1(a1079) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_591,negated_conjecture,
( ~ hskp19
| ~ c2_1(a1079) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_592,negated_conjecture,
( ~ hskp18
| ~ c1_1(a1078) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_593,negated_conjecture,
( ~ hskp17
| ~ c0_1(a1077) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_594,negated_conjecture,
( ~ hskp17
| ~ c2_1(a1077) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_595,negated_conjecture,
( ~ hskp16
| ~ c3_1(a1064) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_596,negated_conjecture,
( ~ hskp15
| ~ c1_1(a1059) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_597,negated_conjecture,
( ~ hskp14
| ~ c0_1(a1055) ),
inference(cnf_transformation,[],[f233]) ).
tcf(c_598,negated_conjecture,
( ~ hskp14
| ~ c1_1(a1055) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_599,negated_conjecture,
( ~ hskp14
| ~ c2_1(a1055) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_600,negated_conjecture,
( ~ hskp13
| ~ c2_1(a1048) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_601,negated_conjecture,
( ~ hskp12
| ~ c1_1(a1043) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_602,negated_conjecture,
( ~ hskp12
| ~ c3_1(a1043) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_603,negated_conjecture,
( ~ hskp11
| ~ c3_1(a1041) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_604,negated_conjecture,
( ~ hskp11
| ~ c2_1(a1041) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_605,negated_conjecture,
( ~ hskp10
| ~ c2_1(a1039) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_606,negated_conjecture,
( ~ hskp10
| ~ c0_1(a1039) ),
inference(cnf_transformation,[],[f242]) ).
tcf(c_607,negated_conjecture,
( ~ hskp9
| ~ c1_1(a1038) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_608,negated_conjecture,
( ~ hskp9
| ~ c0_1(a1038) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_609,negated_conjecture,
( ~ hskp8
| ~ c3_1(a1036) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_610,negated_conjecture,
( ~ hskp8
| ~ c1_1(a1036) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_611,negated_conjecture,
( ~ hskp7
| ~ c2_1(a1035) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_612,negated_conjecture,
( ~ hskp6
| ~ c2_1(a1030) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_613,negated_conjecture,
( ~ hskp6
| ~ c3_1(a1030) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_614,negated_conjecture,
( ~ hskp6
| ~ c0_1(a1030) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_615,negated_conjecture,
( ~ hskp5
| ~ c3_1(a1027) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_616,negated_conjecture,
( ~ hskp4
| ~ c2_1(a1026) ),
inference(cnf_transformation,[],[f252]) ).
tcf(c_617,negated_conjecture,
( ~ hskp4
| ~ c1_1(a1026) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_618,negated_conjecture,
( ~ hskp3
| ~ c0_1(a1025) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_619,negated_conjecture,
( ~ hskp3
| ~ c3_1(a1025) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_620,negated_conjecture,
( ~ hskp3
| ~ c2_1(a1025) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_621,negated_conjecture,
( ~ hskp2
| ~ c3_1(a1024) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_622,negated_conjecture,
( ~ hskp1
| ~ c1_1(a1023) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_623,negated_conjecture,
( ~ hskp1
| ~ c0_1(a1023) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_624,negated_conjecture,
( ~ hskp0
| ~ c1_1(a1020) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_625,negated_conjecture,
( ~ hskp0
| ~ c2_1(a1020) ),
inference(cnf_transformation,[],[f261]) ).
tcf(c_626,negated_conjecture,
! [X0: $i] :
( hskp10
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f262]) ).
tcf(c_627,negated_conjecture,
! [X0: $i] :
( hskp44
| hskp45
| c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_628,negated_conjecture,
! [X0: $i] :
( hskp14
| hskp48
| c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f264]) ).
tcf(c_629,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp36
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f265]) ).
tcf(c_630,negated_conjecture,
! [X0: $i] :
( hskp15
| hskp33
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_631,negated_conjecture,
! [X0: $i] :
( hskp36
| hskp48
| c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_632,negated_conjecture,
! [X0: $i] :
( hskp16
| hskp42
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_633,negated_conjecture,
! [X0: $i] :
( hskp19
| hskp20
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_634,negated_conjecture,
! [X0: $i] :
( hskp21
| hskp55
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_635,negated_conjecture,
! [X0: $i] :
( hskp26
| hskp60
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_636,negated_conjecture,
! [X0: $i] :
( hskp4
| hskp5
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_637,negated_conjecture,
! [X0: $i] :
( hskp6
| hskp32
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_638,negated_conjecture,
! [X0: $i] :
( hskp8
| hskp37
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_639,negated_conjecture,
! [X0: $i] :
( hskp40
| hskp41
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_640,negated_conjecture,
! [X0: $i] :
( hskp13
| hskp43
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_641,negated_conjecture,
! [X0: $i] :
( hskp10
| hskp43
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f277]) ).
tcf(c_642,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp12
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_643,negated_conjecture,
! [X0: $i] :
( hskp50
| hskp51
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_644,negated_conjecture,
! [X0: $i] :
( hskp34
| hskp52
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_645,negated_conjecture,
! [X0: $i] :
( hskp22
| hskp56
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_646,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp39
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_647,negated_conjecture,
! [X0: $i] :
( hskp47
| hskp54
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_648,negated_conjecture,
! [X0: $i] :
( hskp23
| hskp33
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_649,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp3
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_650,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_651,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp9
| c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c3_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_652,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_653,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_654,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp49
| c0_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_655,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp24
| c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_656,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c2_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_657,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp2
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_658,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp31
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_659,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_660,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp58
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_661,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp59
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_662,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_663,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp61
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_664,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp33
| c0_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_665,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c2_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_666,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp4
| c2_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_667,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp47
| c3_1(X0)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_668,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp57
| c2_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_669,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp25
| c0_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_670,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp51
| c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_671,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp12
| c2_1(X1)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_672,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp7
| c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_673,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp53
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_674,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp36
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_675,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_676,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_677,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X2)
| c3_1(X2)
| c3_1(X1)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_678,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_679,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c2_1(X2)
| c3_1(X1)
| c1_1(X2)
| c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_680,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| ~ ndr1_0
| ~ c0_1(X2)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_711,negated_conjecture,
ndr1_0,
inference(global_subsumption_just,[status(thm)],[c_428,c_431,c_411,c_410,c_389]) ).
tcf(c_839,negated_conjecture,
! [X0: $i] :
( hskp10
| c0_1(X0)
| c2_1(X0)
| c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_626,c_431,c_411,c_410,c_389,c_626]) ).
tcf(c_842,negated_conjecture,
! [X0: $i] :
( hskp14
| hskp48
| c0_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_628,c_628,c_711]) ).
tcf(c_845,negated_conjecture,
! [X0: $i] :
( hskp44
| hskp45
| c2_1(X0)
| c3_1(X0)
| c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_627,c_431,c_411,c_410,c_389,c_627]) ).
tcf(c_848,negated_conjecture,
! [X0: $i] :
( hskp26
| hskp60
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_635,c_431,c_411,c_410,c_389,c_635]) ).
tcf(c_851,negated_conjecture,
! [X0: $i] :
( hskp21
| hskp55
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_634,c_431,c_411,c_410,c_389,c_634]) ).
tcf(c_854,negated_conjecture,
! [X0: $i] :
( hskp19
| hskp20
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_633,c_431,c_411,c_410,c_389,c_633]) ).
tcf(c_857,negated_conjecture,
! [X0: $i] :
( hskp16
| hskp42
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_632,c_431,c_411,c_410,c_389,c_632]) ).
tcf(c_860,negated_conjecture,
! [X0: $i] :
( hskp36
| hskp48
| c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_631,c_431,c_411,c_410,c_389,c_631]) ).
tcf(c_863,negated_conjecture,
! [X0: $i] :
( hskp15
| hskp33
| c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_630,c_431,c_411,c_410,c_389,c_630]) ).
tcf(c_866,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp36
| c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_629,c_431,c_411,c_410,c_389,c_629]) ).
tcf(c_869,plain,
! [X0: $i] :
( hskp22
| hskp56
| c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_645,c_431,c_411,c_410,c_389,c_645]) ).
tcf(c_870,negated_conjecture,
! [X0: $i] :
( hskp22
| hskp56
| c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_869]) ).
tcf(c_872,plain,
! [X0: $i] :
( hskp34
| hskp52
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_644,c_431,c_411,c_410,c_389,c_644]) ).
tcf(c_873,negated_conjecture,
! [X0: $i] :
( hskp34
| hskp52
| c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_872]) ).
tcf(c_875,plain,
! [X0: $i] :
( hskp50
| hskp51
| c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_643,c_431,c_411,c_410,c_389,c_643]) ).
tcf(c_876,negated_conjecture,
! [X0: $i] :
( hskp50
| hskp51
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_875]) ).
tcf(c_878,plain,
! [X0: $i] :
( hskp7
| hskp12
| c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_642,c_431,c_411,c_410,c_389,c_642]) ).
tcf(c_879,negated_conjecture,
! [X0: $i] :
( hskp7
| hskp12
| c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_878]) ).
tcf(c_881,plain,
! [X0: $i] :
( hskp10
| hskp43
| c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_641,c_431,c_411,c_410,c_389,c_641]) ).
tcf(c_882,negated_conjecture,
! [X0: $i] :
( hskp10
| hskp43
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_881]) ).
tcf(c_884,plain,
! [X0: $i] :
( hskp13
| hskp43
| c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_640,c_431,c_411,c_410,c_389,c_640]) ).
tcf(c_885,negated_conjecture,
! [X0: $i] :
( hskp13
| hskp43
| c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_884]) ).
tcf(c_887,plain,
! [X0: $i] :
( hskp40
| hskp41
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_639,c_431,c_411,c_410,c_389,c_639]) ).
tcf(c_888,negated_conjecture,
! [X0: $i] :
( hskp40
| hskp41
| c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_887]) ).
tcf(c_890,plain,
! [X0: $i] :
( hskp8
| hskp37
| c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_638,c_431,c_411,c_410,c_389,c_638]) ).
tcf(c_891,negated_conjecture,
! [X0: $i] :
( hskp8
| hskp37
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_890]) ).
tcf(c_893,plain,
! [X0: $i] :
( hskp6
| hskp32
| c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_637,c_431,c_411,c_410,c_389,c_637]) ).
tcf(c_894,negated_conjecture,
! [X0: $i] :
( hskp6
| hskp32
| c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_893]) ).
tcf(c_896,plain,
! [X0: $i] :
( hskp4
| hskp5
| c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_636,c_431,c_411,c_410,c_389,c_636]) ).
tcf(c_897,negated_conjecture,
! [X0: $i] :
( hskp4
| hskp5
| c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_896]) ).
tcf(c_899,plain,
! [X0: $i] :
( hskp23
| hskp33
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_648,c_431,c_411,c_410,c_389,c_648]) ).
tcf(c_900,negated_conjecture,
! [X0: $i] :
( hskp23
| hskp33
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_899]) ).
tcf(c_902,plain,
! [X0: $i] :
( hskp47
| hskp54
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_647,c_431,c_411,c_410,c_389,c_647]) ).
tcf(c_903,negated_conjecture,
! [X0: $i] :
( hskp47
| hskp54
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_902]) ).
tcf(c_905,plain,
! [X0: $i] :
( hskp11
| hskp39
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_646,c_431,c_411,c_410,c_389,c_646]) ).
tcf(c_906,negated_conjecture,
! [X0: $i] :
( hskp11
| hskp39
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_905]) ).
tcf(c_908,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_652,c_431,c_411,c_410,c_389,c_652]) ).
tcf(c_910,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp9
| c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c3_1(X1)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_651,c_431,c_411,c_410,c_389,c_651]) ).
tcf(c_912,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_650,c_431,c_411,c_410,c_389,c_650]) ).
tcf(c_914,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp3
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_649,c_431,c_411,c_410,c_389,c_649]) ).
tcf(c_916,plain,
! [X0: $i,X1: $i] :
( hskp24
| c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_655,c_431,c_411,c_410,c_389,c_655]) ).
tcf(c_917,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp24
| c0_1(X1)
| c0_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_916]) ).
tcf(c_918,plain,
! [X0: $i,X1: $i] :
( hskp49
| c0_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_654,c_431,c_411,c_410,c_389,c_654]) ).
tcf(c_919,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp49
| c0_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_918]) ).
tcf(c_920,plain,
! [X0: $i,X1: $i] :
( hskp34
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_653,c_431,c_411,c_410,c_389,c_653]) ).
tcf(c_921,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp34
| c2_1(X0)
| c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_920]) ).
tcf(c_922,plain,
! [X0: $i,X1: $i] :
( hskp61
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_663,c_431,c_411,c_410,c_389,c_663]) ).
tcf(c_923,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp61
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_922]) ).
tcf(c_924,plain,
! [X0: $i,X1: $i] :
( hskp35
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_662,c_431,c_411,c_410,c_389,c_662]) ).
tcf(c_925,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp35
| c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_924]) ).
tcf(c_926,plain,
! [X0: $i,X1: $i] :
( hskp59
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_661,c_431,c_411,c_410,c_389,c_661]) ).
tcf(c_927,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp59
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_926]) ).
tcf(c_929,plain,
! [X0: $i,X1: $i] :
( hskp58
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_660,c_431,c_411,c_410,c_389,c_660]) ).
tcf(c_930,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp58
| c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_929]) ).
tcf(c_931,plain,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_659,c_431,c_411,c_410,c_389,c_659]) ).
tcf(c_932,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp42
| c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_931]) ).
tcf(c_933,plain,
! [X0: $i,X1: $i] :
( hskp31
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_658,c_431,c_411,c_410,c_389,c_658]) ).
tcf(c_934,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp31
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_933]) ).
tcf(c_935,plain,
! [X0: $i,X1: $i] :
( hskp2
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_657,c_431,c_411,c_410,c_389,c_657]) ).
tcf(c_936,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp2
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_935]) ).
tcf(c_937,plain,
! [X0: $i,X1: $i] :
( hskp1
| c2_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_656,c_431,c_411,c_410,c_389,c_656]) ).
tcf(c_938,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp1
| c2_1(X0)
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_937]) ).
tcf(c_939,plain,
! [X0: $i,X1: $i] :
( hskp51
| c2_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_670,c_431,c_411,c_410,c_389,c_670]) ).
tcf(c_940,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp51
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_939]) ).
tcf(c_941,plain,
! [X0: $i,X1: $i] :
( hskp25
| c0_1(X1)
| c2_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_669,c_431,c_411,c_410,c_389,c_669]) ).
tcf(c_942,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp25
| c0_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_941]) ).
tcf(c_943,plain,
! [X0: $i,X1: $i] :
( hskp57
| c2_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_668,c_431,c_411,c_410,c_389,c_668]) ).
tcf(c_944,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp57
| c2_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_943]) ).
tcf(c_945,plain,
! [X0: $i,X1: $i] :
( hskp47
| c3_1(X0)
| c1_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_667,c_431,c_411,c_410,c_389,c_667]) ).
tcf(c_946,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp47
| c3_1(X0)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_945]) ).
tcf(c_948,plain,
! [X0: $i,X1: $i] :
( hskp4
| c2_1(X0)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_666,c_431,c_411,c_410,c_389,c_666]) ).
tcf(c_949,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp4
| c2_1(X0)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_948]) ).
tcf(c_950,plain,
! [X0: $i,X1: $i] :
( hskp38
| c2_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_665,c_431,c_411,c_410,c_389,c_665]) ).
tcf(c_951,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp38
| c2_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_950]) ).
tcf(c_953,plain,
! [X0: $i,X1: $i] :
( hskp33
| c0_1(X1)
| c2_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_664,c_431,c_411,c_410,c_389,c_664]) ).
tcf(c_954,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp33
| c0_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_953]) ).
tcf(c_955,plain,
! [X0: $i,X1: $i] :
( ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_675,c_431,c_411,c_410,c_389,c_675]) ).
tcf(c_956,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_955]) ).
tcf(c_958,plain,
! [X0: $i,X1: $i] :
( hskp36
| c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_674,c_431,c_411,c_410,c_389,c_674]) ).
tcf(c_959,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp36
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_958]) ).
tcf(c_961,plain,
! [X0: $i,X1: $i] :
( hskp53
| c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_673,c_431,c_411,c_410,c_389,c_673]) ).
tcf(c_962,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp53
| c1_1(X0)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_961]) ).
tcf(c_964,plain,
! [X0: $i,X1: $i] :
( hskp7
| c0_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_672,c_431,c_411,c_410,c_389,c_672]) ).
tcf(c_965,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp7
| c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_964]) ).
tcf(c_966,negated_conjecture,
! [X0: $i,X1: $i] :
( hskp12
| ~ c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_671,c_431,c_411,c_410,c_389,c_671,c_956]) ).
tcf(c_968,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| ~ c1_1(X0)
| ~ c1_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_678,c_431,c_411,c_410,c_389,c_678]) ).
tcf(c_969,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c2_1(X1)
| c2_1(X0)
| c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_968]) ).
tcf(c_970,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X2)
| c3_1(X2)
| c3_1(X1)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_677,c_431,c_411,c_410,c_389,c_677]) ).
tcf(c_971,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X0)
| c2_1(X2)
| c3_1(X2)
| c3_1(X1)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c0_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_970]) ).
tcf(c_972,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_676,c_431,c_411,c_410,c_389,c_676]) ).
tcf(c_973,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X1)
| c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X0) ),
inference(renaming,[status(thm)],[c_972]) ).
tcf(c_975,plain,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c2_1(X2)
| c3_1(X1)
| c1_1(X2)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_679,c_431,c_411,c_410,c_389,c_679]) ).
tcf(c_976,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c0_1(X2)
| c0_1(X0)
| c2_1(X2)
| c3_1(X1)
| c1_1(X2)
| c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_975]) ).
tcf(c_977,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_680,c_431,c_411,c_410,c_389,c_680]) ).
tcf(c_978,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_1(X2)
| c3_1(X0)
| c1_1(X2)
| ~ c0_1(X2)
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(renaming,[status(thm)],[c_977]) ).
tcf(c_2471,plain,
( hskp56
| hskp62
| ~ c2_1(a1105) ),
inference(resolution,[status(thm)],[c_433,c_540]) ).
tcf(c_2481,plain,
( hskp56
| hskp62
| c3_1(a1105) ),
inference(resolution,[status(thm)],[c_433,c_435]) ).
tcf(c_2491,plain,
( hskp56
| hskp62
| c1_1(a1105) ),
inference(resolution,[status(thm)],[c_433,c_434]) ).
tcf(c_2510,plain,
( hskp14
| hskp38
| ~ c2_1(a1053) ),
inference(resolution,[status(thm)],[c_430,c_555]) ).
tcf(c_2520,plain,
( hskp14
| hskp38
| ~ c1_1(a1053) ),
inference(resolution,[status(thm)],[c_430,c_554]) ).
tcf(c_2530,plain,
( hskp14
| hskp38
| c0_1(a1053) ),
inference(resolution,[status(thm)],[c_430,c_471]) ).
tcf(c_2549,plain,
( hskp0
| hskp29
| ~ c2_1(a1022) ),
inference(resolution,[status(thm)],[c_429,c_569]) ).
tcf(c_2559,plain,
( hskp0
| hskp29
| c1_1(a1022) ),
inference(resolution,[status(thm)],[c_429,c_505]) ).
tcf(c_2569,plain,
( hskp0
| hskp29
| c3_1(a1022) ),
inference(resolution,[status(thm)],[c_429,c_504]) ).
tcf(c_2588,plain,
( hskp27
| hskp43
| ~ c1_1(a1102) ),
inference(resolution,[status(thm)],[c_432,c_573]) ).
tcf(c_2598,plain,
( hskp27
| hskp43
| ~ c0_1(a1102) ),
inference(resolution,[status(thm)],[c_432,c_572]) ).
tcf(c_2608,plain,
( hskp27
| hskp43
| c2_1(a1102) ),
inference(resolution,[status(thm)],[c_432,c_507]) ).
tcf(c_2627,plain,
( hskp17
| hskp39
| ~ c1_1(a1078) ),
inference(resolution,[status(thm)],[c_431,c_592]) ).
tcf(c_2637,plain,
( hskp17
| hskp39
| c0_1(a1078) ),
inference(resolution,[status(thm)],[c_431,c_518]) ).
tcf(c_2647,plain,
( hskp17
| hskp39
| c2_1(a1078) ),
inference(resolution,[status(thm)],[c_431,c_517]) ).
tcf(c_16794,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_978]) ).
tcf(c_16795,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_978]) ).
tcf(c_16796,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_978]) ).
tcf(c_16797,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_978]) ).
tcf(c_16798,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_976]) ).
tcf(c_16799,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| c1_1(X0)
| c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_976]) ).
tcf(c_16800,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_976]) ).
tcf(c_16801,negated_conjecture,
( iPr_def_15
| iPr_def_14
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_976]) ).
tcf(c_16802,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_973]) ).
tcf(c_16803,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| c1_1(X0)
| c3_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_973]) ).
tcf(c_16804,negated_conjecture,
( iPr_def_17
| iPr_def_16
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_973]) ).
tcf(c_16805,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| c1_1(X0)
| c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_971]) ).
tcf(c_16806,negated_conjecture,
( iPr_def_18
| iPr_def_16
| iPr_def_11 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_971]) ).
tcf(c_16807,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_969]) ).
tcf(c_16808,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_969]) ).
tcf(c_16809,negated_conjecture,
( iPr_def_20
| iPr_def_19
| iPr_def_17 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_969]) ).
tcf(c_16810,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_21
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_966]) ).
tcf(c_16811,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_966]) ).
tcf(c_16812,negated_conjecture,
( iPr_def_22
| iPr_def_21
| hskp12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_966]) ).
tcf(c_16813,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_965]) ).
tcf(c_16814,negated_conjecture,
( iPr_def_23
| iPr_def_15
| hskp7 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_965]) ).
tcf(c_16815,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_24
| c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_962]) ).
tcf(c_16816,negated_conjecture,
( iPr_def_24
| iPr_def_23
| hskp53 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_962]) ).
tcf(c_16817,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_25
| ~ c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_25])],[c_959]) ).
tcf(c_16818,negated_conjecture,
( iPr_def_25
| iPr_def_10
| hskp36 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_959]) ).
tcf(c_16819,negated_conjecture,
( iPr_def_23
| iPr_def_22 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_956]) ).
tcf(c_16820,negated_conjecture,
( iPr_def_19
| iPr_def_10
| hskp33 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_954]) ).
tcf(c_16821,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_26
| ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_26])],[c_951]) ).
tcf(c_16822,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_27
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_951]) ).
tcf(c_16823,negated_conjecture,
( iPr_def_27
| iPr_def_26
| hskp38 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_951]) ).
tcf(c_16824,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_28
| ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_949]) ).
tcf(c_16825,negated_conjecture,
( iPr_def_28
| iPr_def_27
| hskp4 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_949]) ).
tcf(c_16826,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_29
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_946]) ).
tcf(c_16827,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_30
| c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_946]) ).
tcf(c_16828,negated_conjecture,
( iPr_def_30
| iPr_def_29
| hskp47 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_946]) ).
tcf(c_16829,negated_conjecture,
( iPr_def_26
| iPr_def_24
| hskp57 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_944]) ).
tcf(c_16830,negated_conjecture,
( iPr_def_19
| iPr_def_10
| hskp25 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_942]) ).
tcf(c_16831,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_31
| c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_31])],[c_940]) ).
tcf(c_16832,negated_conjecture,
( iPr_def_31
| iPr_def_23
| hskp51 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_940]) ).
tcf(c_16833,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_32
| c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_32])],[c_938]) ).
tcf(c_16834,negated_conjecture,
( iPr_def_32
| iPr_def_29
| hskp1 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_938]) ).
tcf(c_16835,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_33
| c3_1(X0)
| c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_33])],[c_936]) ).
tcf(c_16836,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_34
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_34])],[c_936]) ).
tcf(c_16837,negated_conjecture,
( iPr_def_34
| iPr_def_33
| hskp2 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_936]) ).
tcf(c_16838,negated_conjecture,
( iPr_def_28
| iPr_def_13
| hskp31 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_934]) ).
tcf(c_16839,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_35
| ~ c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_35])],[c_932]) ).
tcf(c_16840,negated_conjecture,
( iPr_def_35
| iPr_def_16
| hskp42 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_932]) ).
tcf(c_16841,negated_conjecture,
( iPr_def_35
| iPr_def_32
| hskp58 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_930]) ).
tcf(c_16842,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_36
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_36])],[c_927]) ).
tcf(c_16843,negated_conjecture,
( iPr_def_36
| iPr_def_35
| hskp59 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_927]) ).
tcf(c_16844,negated_conjecture,
( iPr_def_20
| iPr_def_15
| hskp35 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_925]) ).
tcf(c_16845,negated_conjecture,
( iPr_def_25
| iPr_def_20
| hskp61 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_923]) ).
tcf(c_16846,negated_conjecture,
( iPr_def_20
| iPr_def_11
| hskp34 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_921]) ).
tcf(c_16847,negated_conjecture,
( iPr_def_26
| iPr_def_17
| hskp49 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_919]) ).
tcf(c_16848,negated_conjecture,
( iPr_def_25
| iPr_def_17
| hskp24 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_917]) ).
tcf(c_16849,negated_conjecture,
( iPr_def_33
| iPr_def_31
| hskp3 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_914]) ).
tcf(c_16850,negated_conjecture,
( iPr_def_36
| iPr_def_33
| hskp35 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_912]) ).
tcf(c_16851,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_37
| c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_37])],[c_910]) ).
tcf(c_16852,negated_conjecture,
( iPr_def_37
| iPr_def_33
| hskp9 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_910]) ).
tcf(c_16853,negated_conjecture,
( iPr_def_33
| iPr_def_31
| hskp1 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_908]) ).
tcf(c_16854,negated_conjecture,
( iPr_def_34
| hskp11
| hskp39 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_906]) ).
tcf(c_16855,negated_conjecture,
( iPr_def_10
| hskp47
| hskp54 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_903]) ).
tcf(c_16856,negated_conjecture,
( iPr_def_23
| hskp23
| hskp33 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_900]) ).
tcf(c_16857,negated_conjecture,
( iPr_def_30
| hskp4
| hskp5 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_897]) ).
tcf(c_16858,negated_conjecture,
( iPr_def_12
| hskp6
| hskp32 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_894]) ).
tcf(c_16859,negated_conjecture,
( iPr_def_25
| hskp8
| hskp37 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_891]) ).
tcf(c_16860,negated_conjecture,
( iPr_def_29
| hskp40
| hskp41 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_888]) ).
tcf(c_16861,negated_conjecture,
( iPr_def_30
| hskp13
| hskp43 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_885]) ).
tcf(c_16862,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_38
| ~ c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_38])],[c_882]) ).
tcf(c_16863,negated_conjecture,
( iPr_def_38
| hskp10
| hskp43 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_882]) ).
tcf(c_16864,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_39
| ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_39])],[c_879]) ).
tcf(c_16865,negated_conjecture,
( iPr_def_39
| hskp7
| hskp12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_879]) ).
tcf(c_16866,negated_conjecture,
( iPr_def_38
| hskp50
| hskp51 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_876]) ).
tcf(c_16867,negated_conjecture,
( iPr_def_27
| hskp34
| hskp52 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_873]) ).
tcf(c_16868,negated_conjecture,
( iPr_def_35
| hskp22
| hskp56 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_870]) ).
tcf(c_16869,negated_conjecture,
( iPr_def_19
| hskp7
| hskp36 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_866]) ).
tcf(c_16870,negated_conjecture,
( iPr_def_36
| hskp15
| hskp33 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_863]) ).
tcf(c_16871,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_40
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_40])],[c_860]) ).
tcf(c_16872,negated_conjecture,
( iPr_def_40
| hskp36
| hskp48 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_860]) ).
tcf(c_16873,negated_conjecture,
( iPr_def_20
| hskp16
| hskp42 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_857]) ).
tcf(c_16874,negated_conjecture,
( iPr_def_11
| hskp19
| hskp20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_854]) ).
tcf(c_16875,negated_conjecture,
( iPr_def_31
| hskp21
| hskp55 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_851]) ).
tcf(c_16876,negated_conjecture,
( iPr_def_31
| hskp26
| hskp60 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_848]) ).
tcf(c_16877,negated_conjecture,
( iPr_def_18
| hskp44
| hskp45 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_845]) ).
tcf(c_16878,negated_conjecture,
( iPr_def_14
| hskp14
| hskp48 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_842]) ).
tcf(c_18790,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_16878,c_16877,c_16876,c_16875,c_16874,c_16873,c_16872,c_16871,c_16870,c_16869,c_16868,c_16867,c_16866,c_16865,c_16864,c_16863,c_16862,c_16861,c_16860,c_16859,c_16858,c_16857,c_16856,c_16855,c_16854,c_16853,c_16852,c_16851,c_16850,c_16849,c_16848,c_16847,c_16846,c_16845,c_16844,c_16843,c_16842,c_16841,c_16840,c_16839,c_16838,c_16837,c_16836,c_16835,c_16834,c_16833,c_16832,c_16831,c_16830,c_16829,c_16828,c_16827,c_16826,c_16825,c_16824,c_16823,c_16822,c_16821,c_16820,c_16819,c_16818,c_16817,c_16816,c_16815,c_16814,c_16813,c_16812,c_16811,c_16810,c_16809,c_16808,c_16807,c_16806,c_16805,c_16804,c_16803,c_16802,c_16801,c_16800,c_16799,c_16798,c_16797,c_16796,c_16795,c_16794,c_2647,c_2637,c_2627,c_2608,c_2598,c_2588,c_2569,c_2559,c_2549,c_2530,c_2520,c_2510,c_2491,c_2481,c_2471,c_839,c_625,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_610,c_609,c_608,c_607,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_594,c_593,c_591,c_590,c_589,c_588,c_587,c_586,c_585,c_584,c_583,c_582,c_581,c_580,c_579,c_578,c_577,c_576,c_575,c_574,c_571,c_570,c_568,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_553,c_552,c_551,c_550,c_549,c_548,c_547,c_546,c_545,c_544,c_543,c_542,c_541,c_539,c_538,c_537,c_536,c_535,c_534,c_533,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_516,c_515,c_514,c_513,c_512,c_511,c_510,c_509,c_508,c_506,c_503,c_502,c_501,c_500,c_499,c_498,c_497,c_496,c_495,c_494,c_493,c_492,c_491,c_490,c_489,c_488,c_487,c_486,c_485,c_484,c_483,c_482,c_481,c_480,c_479,c_478,c_477,c_476,c_475,c_474,c_473,c_472,c_470,c_469,c_468,c_467,c_466,c_465,c_464,c_463,c_462,c_461,c_460,c_459,c_458,c_457,c_456,c_455,c_454,c_453,c_452,c_451,c_450,c_449,c_448,c_447,c_446,c_445,c_444,c_443,c_442,c_441,c_440,c_439,c_438,c_437,c_436]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN447-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 01:13:34 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.40 Running EPR theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 3.58/1.15 % SZS status Started for theBenchmark.p
% 3.58/1.15 % SZS status Unsatisfiable for theBenchmark.p
% 3.58/1.15
% 3.58/1.15 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.58/1.15
% 3.58/1.15 % ------ iProver source info
% 3.58/1.15
% 3.58/1.15 % git: date: 2026-07-19 20:42:38 +0200
% 3.58/1.15 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.58/1.15 % git: non_committed_changes: false
% 3.58/1.15
% 3.58/1.15 % ------ Parsing...% successful
% 3.58/1.15
% 3.58/1.15
% 3.58/1.15 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 3.58/1.15 %
% 3.58/1.15
% 3.58/1.15 % ------ 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 %
% 3.58/1.15
% 3.58/1.15 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 3.58/1.15 gs_s sp: 91 0s gs_e snvd_s sp: 0 0s snvd_e
% 3.58/1.15 % ------ Proving...
% 3.58/1.15 % ------ Problem Properties
% 3.58/1.15
% 3.58/1.15 %
% 3.58/1.15 % clauses 278
% 3.58/1.15 % conjectures 263
% 3.58/1.15 % EPR 278
% 3.58/1.15 % Horn 194
% 3.58/1.15 % unary 0
% 3.58/1.15 % binary 178
% 3.58/1.15 % lits 687
% 3.58/1.15 % lits eq 0
% 3.58/1.15 % fd_pure 0
% 3.58/1.15 % fd_pseudo 0
% 3.58/1.15 % fd_cond 0
% 3.58/1.15 % fd_pseudo_cond 0
% 3.58/1.15 % AC symbols 0
% 3.58/1.15
% 3.58/1.15 % ------ Schedule EPR non Horn non eq is on
% 3.58/1.15
% 3.58/1.15 % ------ no equalities: superposition off
% 3.58/1.15
% 3.58/1.15 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 3.58/1.15
% 3.58/1.15
% 3.58/1.15 % ------
% 3.58/1.15 % Current options:
% 3.58/1.15 % ------
% 3.58/1.15
% 3.58/1.15
% 3.58/1.15 %
% 3.58/1.15
% 3.58/1.15 % ------ Proving...
% 3.58/1.15 %
% 3.58/1.15
% 3.58/1.15 % SZS status Unsatisfiable for theBenchmark.p
% 3.58/1.15
% 3.58/1.15 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.58/1.17
% 3.58/1.17
%------------------------------------------------------------------------------