%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN447-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 : Tue Sep 29 02:08:37 PM UTC 2026
% Result : Unsatisfiable 0.18s 0.33s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 318
% Syntax : Number of formulae : 1118 ( 34 unt; 181 def)
% Number of atoms : 3283 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 3805 (1640 ~;1984 |; 0 &)
% ( 181 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 223 ( 222 usr; 219 prp; 0-1 aty)
% Number of functors : 36 ( 36 usr; 36 con; 0-0 aty)
% Number of variables : 166 ( 0 sgn 166 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp63
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( ~ hskp62
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f8,negated_conjecture,
( ~ hskp56
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f65,negated_conjecture,
( hskp0
| hskp29
| hskp30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f67,negated_conjecture,
( hskp39
| hskp17
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( hskp43
| hskp27
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( hskp62
| hskp56
| hskp63 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp63
| c1_1(a1105) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp63
| c3_1(a1105) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp62
| c2_1(a1103) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp62
| c3_1(a1103) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f81,negated_conjecture,
( ~ hskp57
| c2_1(a1085) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp57
| c0_1(a1085) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp57
| c3_1(a1085) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ hskp56
| c0_1(a1084) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f90,negated_conjecture,
( ~ hskp53
| c1_1(a1073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ hskp53
| c2_1(a1073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp53
| c0_1(a1073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f96,negated_conjecture,
( ~ hskp51
| c2_1(a1070) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f100,negated_conjecture,
( ~ hskp49
| c1_1(a1065) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f104,negated_conjecture,
( ~ hskp47
| c2_1(a1056) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ hskp47
| c1_1(a1056) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ hskp47
| c3_1(a1056) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f108,negated_conjecture,
( ~ hskp45
| c0_1(a1052) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ hskp45
| c3_1(a1052) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ hskp45
| c2_1(a1052) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ hskp44
| c1_1(a1051) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ hskp44
| c0_1(a1051) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ hskp43
| c0_1(a1049) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ hskp43
| c2_1(a1049) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ hskp43
| c1_1(a1049) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ hskp42
| c1_1(a1046) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ hskp42
| c0_1(a1046) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f121,negated_conjecture,
( ~ hskp39
| c0_1(a1042) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ hskp39
| c2_1(a1042) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ hskp38
| c1_1(a1040) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ hskp38
| c3_1(a1040) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ hskp38
| c2_1(a1040) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ hskp37
| c0_1(a1037) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ hskp37
| c3_1(a1037) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ hskp36
| c3_1(a1034) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( ~ hskp36
| c1_1(a1034) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ hskp35
| c0_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( ~ hskp35
| c1_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ hskp35
| c3_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f134,negated_conjecture,
( ~ hskp33
| c3_1(a1031) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
( ~ hskp33
| c2_1(a1031) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f138,negated_conjecture,
( ~ hskp31
| c0_1(a1028) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
( ~ hskp31
| c3_1(a1028) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f140,negated_conjecture,
( ~ hskp30
| c3_1(a1022) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
( ~ hskp30
| c1_1(a1022) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
( ~ hskp29
| c2_1(a1021) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
( ~ hskp28
| c2_1(a1102) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
( ~ hskp27
| c3_1(a1101) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause144) ).
fof(f147,negated_conjecture,
( ~ hskp24
| c0_1(a1089) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
( ~ hskp23
| c1_1(a1088) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
( ~ hskp23
| c3_1(a1088) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
( ~ hskp22
| c2_1(a1083) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
( ~ hskp22
| c3_1(a1083) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
( ~ hskp19
| c1_1(a1079) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( ~ hskp18
| c2_1(a1078) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
( ~ hskp18
| c0_1(a1078) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( ~ hskp17
| c3_1(a1077) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f158,negated_conjecture,
( ~ hskp15
| c3_1(a1059) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
( ~ hskp15
| c2_1(a1059) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( ~ hskp13
| c0_1(a1048) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( ~ hskp13
| c3_1(a1048) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f166,negated_conjecture,
( ~ hskp8
| c0_1(a1036) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
( ~ hskp7
| c0_1(a1035) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
( ~ hskp7
| c1_1(a1035) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f175,negated_conjecture,
( ~ hskp0
| c0_1(a1020) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
( ~ c2_1(a1105)
| ~ hskp63 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f183,negated_conjecture,
( ~ c3_1(a1084)
| ~ hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
( ~ c1_1(a1084)
| ~ hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f186,negated_conjecture,
( ~ c1_1(a1070)
| ~ hskp51 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause186) ).
fof(f188,negated_conjecture,
( ~ c0_1(a1065)
| ~ hskp49 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
( ~ c2_1(a1065)
| ~ hskp49 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f192,negated_conjecture,
( ~ c2_1(a1051)
| ~ hskp44 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
( ~ c2_1(a1046)
| ~ hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause193) ).
fof(f197,negated_conjecture,
( ~ c1_1(a1042)
| ~ hskp39 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause197) ).
fof(f199,negated_conjecture,
( ~ c0_1(a1034)
| ~ hskp36 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f202,negated_conjecture,
( ~ c1_1(a1031)
| ~ hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause202) ).
fof(f204,negated_conjecture,
( ~ c1_1(a1028)
| ~ hskp31 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
( ~ c2_1(a1022)
| ~ hskp30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
( ~ c1_1(a1021)
| ~ hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ c3_1(a1021)
| ~ hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ c0_1(a1102)
| ~ hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause208) ).
fof(f209,negated_conjecture,
( ~ c1_1(a1102)
| ~ hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause209) ).
fof(f210,negated_conjecture,
( ~ c0_1(a1101)
| ~ hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause210) ).
fof(f213,negated_conjecture,
( ~ c3_1(a1091)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause213) ).
fof(f214,negated_conjecture,
( ~ c0_1(a1091)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause214) ).
fof(f215,negated_conjecture,
( ~ c2_1(a1091)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause215) ).
fof(f216,negated_conjecture,
( ~ c2_1(a1089)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause216) ).
fof(f217,negated_conjecture,
( ~ c1_1(a1089)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
( ~ c2_1(a1088)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ c1_1(a1083)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause219) ).
fof(f223,negated_conjecture,
( ~ c0_1(a1080)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause223) ).
fof(f224,negated_conjecture,
( ~ c2_1(a1080)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause224) ).
fof(f225,negated_conjecture,
( ~ c1_1(a1080)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause225) ).
fof(f226,negated_conjecture,
( ~ c0_1(a1079)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause226) ).
fof(f227,negated_conjecture,
( ~ c2_1(a1079)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause227) ).
fof(f228,negated_conjecture,
( ~ c1_1(a1078)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause228) ).
fof(f229,negated_conjecture,
( ~ c0_1(a1077)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause229) ).
fof(f230,negated_conjecture,
( ~ c2_1(a1077)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause230) ).
fof(f232,negated_conjecture,
( ~ c1_1(a1059)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause232) ).
fof(f236,negated_conjecture,
( ~ c2_1(a1048)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause236) ).
fof(f245,negated_conjecture,
( ~ c3_1(a1036)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
( ~ c1_1(a1036)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
( ~ c2_1(a1035)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause247) ).
fof(f260,negated_conjecture,
( ~ c1_1(a1020)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause260) ).
fof(f261,negated_conjecture,
( ~ c2_1(a1020)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause261) ).
fof(f263,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| hskp44
| hskp45 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause263) ).
fof(f266,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X0)
| hskp15
| hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause266) ).
fof(f269,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp19
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause269) ).
fof(f274,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp8
| hskp37 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause274) ).
fof(f276,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp13
| hskp43 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause276) ).
fof(f281,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp22
| hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause281) ).
fof(f284,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp33
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause284) ).
fof(f290,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0)
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| hskp49 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause290) ).
fof(f291,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| c0_1(X0)
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause291) ).
fof(f294,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c1_1(X0)
| c3_1(X0)
| c2_1(X1)
| hskp31 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause294) ).
fof(f295,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause295) ).
fof(f298,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp35 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause298) ).
fof(f300,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause300) ).
fof(f301,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X0)
| c2_1(X1)
| hskp38 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause301) ).
fof(f303,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X1)
| hskp47 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause303) ).
fof(f304,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X1)
| hskp57 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause304) ).
fof(f305,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause305) ).
fof(f306,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c2_1(X0)
| hskp51 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause306) ).
fof(f308,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause308) ).
fof(f309,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X0)
| hskp53 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause309) ).
fof(f310,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X0)
| hskp36 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause310) ).
fof(f311,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause311) ).
fof(f312,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c1_1(X2)
| c3_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause312) ).
fof(f313,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X1)
| c3_1(X2)
| c1_1(X2)
| c2_1(X2)
| c3_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause313) ).
fof(f314,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c2_1(X0)
| c0_1(X2)
| c3_1(X2)
| c1_1(X2)
| c0_1(X1)
| c2_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause314) ).
fof(f315,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2)
| c3_1(X0)
| c1_1(X0)
| c0_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause315) ).
fof(f317,plain,
( ~ hskp63
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f1]) ).
fof(f318,plain,
( ~ hskp62
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f2]) ).
fof(f324,plain,
( hskp56
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f381,plain,
( hskp0
| ~ hskp29
| ~ hskp30 ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f382,plain,
( hskp39
| hskp17
| ~ hskp18 ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f383,plain,
( hskp62
| ~ hskp56
| hskp63 ),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f384,plain,
( ~ hskp63
| ~ c1_1(a1105) ),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f385,plain,
( ~ hskp63
| ~ c3_1(a1105) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f386,plain,
( ~ hskp62
| ~ c3_1(a1103) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f392,plain,
( hskp57
| c2_1(a1085) ),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f393,plain,
( hskp57
| c0_1(a1085) ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f394,plain,
( hskp57
| ~ c3_1(a1085) ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f395,plain,
( hskp56
| c0_1(a1084) ),
inference(consistent_polarity_flipping,[],[f84]) ).
fof(f399,plain,
( ~ hskp53
| ~ c1_1(a1073) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f404,plain,
( ~ hskp49
| ~ c1_1(a1065) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f408,plain,
( hskp47
| c2_1(a1056) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f409,plain,
( hskp47
| ~ c1_1(a1056) ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f410,plain,
( hskp47
| ~ c3_1(a1056) ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f411,plain,
( ~ hskp45
| ~ c3_1(a1052) ),
inference(consistent_polarity_flipping,[],[f109]) ).
fof(f412,plain,
( hskp44
| ~ c1_1(a1051) ),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f413,plain,
( hskp44
| c0_1(a1051) ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f414,plain,
( ~ hskp43
| ~ c1_1(a1049) ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f415,plain,
( hskp42
| ~ c1_1(a1046) ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f416,plain,
( hskp42
| c0_1(a1046) ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f419,plain,
( ~ hskp38
| ~ c1_1(a1040) ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f420,plain,
( ~ hskp38
| ~ c3_1(a1040) ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f421,plain,
( ~ hskp37
| ~ c3_1(a1037) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f422,plain,
( hskp36
| ~ c3_1(a1034) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f423,plain,
( hskp36
| ~ c1_1(a1034) ),
inference(consistent_polarity_flipping,[],[f129]) ).
fof(f424,plain,
( hskp35
| c0_1(a1033) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f425,plain,
( hskp35
| ~ c1_1(a1033) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f426,plain,
( hskp35
| ~ c3_1(a1033) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f428,plain,
( ~ hskp33
| ~ c3_1(a1031) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f430,plain,
( ~ hskp31
| ~ c3_1(a1028) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f431,plain,
( hskp30
| ~ c3_1(a1022) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f432,plain,
( hskp30
| ~ c1_1(a1022) ),
inference(consistent_polarity_flipping,[],[f141]) ).
fof(f433,plain,
( hskp29
| c2_1(a1021) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f434,plain,
( ~ hskp27
| ~ c3_1(a1101) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f437,plain,
( hskp23
| ~ c1_1(a1088) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f438,plain,
( hskp23
| ~ c3_1(a1088) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f439,plain,
( hskp22
| c2_1(a1083) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f440,plain,
( hskp22
| ~ c3_1(a1083) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f441,plain,
( ~ hskp19
| ~ c1_1(a1079) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f442,plain,
( hskp18
| c2_1(a1078) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f443,plain,
( hskp18
| c0_1(a1078) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f444,plain,
( ~ hskp17
| ~ c3_1(a1077) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f445,plain,
( hskp15
| ~ c3_1(a1059) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f446,plain,
( hskp15
| c2_1(a1059) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f447,plain,
( ~ hskp13
| ~ c3_1(a1048) ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f451,plain,
( hskp7
| c0_1(a1035) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f452,plain,
( hskp7
| ~ c1_1(a1035) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f459,plain,
( c3_1(a1084)
| hskp56 ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f460,plain,
( c1_1(a1084)
| hskp56 ),
inference(consistent_polarity_flipping,[],[f184]) ).
fof(f462,plain,
( c1_1(a1070)
| ~ hskp51 ),
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f465,plain,
( ~ c2_1(a1051)
| hskp44 ),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f466,plain,
( ~ c2_1(a1046)
| hskp42 ),
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f469,plain,
( c1_1(a1042)
| ~ hskp39 ),
inference(consistent_polarity_flipping,[],[f197]) ).
fof(f471,plain,
( ~ c0_1(a1034)
| hskp36 ),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f473,plain,
( c1_1(a1031)
| ~ hskp33 ),
inference(consistent_polarity_flipping,[],[f202]) ).
fof(f474,plain,
( c1_1(a1028)
| ~ hskp31 ),
inference(consistent_polarity_flipping,[],[f204]) ).
fof(f475,plain,
( ~ c2_1(a1022)
| hskp30 ),
inference(consistent_polarity_flipping,[],[f205]) ).
fof(f476,plain,
( c1_1(a1021)
| hskp29 ),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f477,plain,
( c3_1(a1021)
| hskp29 ),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f478,plain,
( c1_1(a1102)
| ~ hskp28 ),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f480,plain,
( c3_1(a1091)
| ~ hskp25 ),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f481,plain,
( c1_1(a1089)
| ~ hskp24 ),
inference(consistent_polarity_flipping,[],[f217]) ).
fof(f482,plain,
( ~ c2_1(a1088)
| hskp23 ),
inference(consistent_polarity_flipping,[],[f218]) ).
fof(f483,plain,
( c1_1(a1083)
| hskp22 ),
inference(consistent_polarity_flipping,[],[f219]) ).
fof(f485,plain,
( c1_1(a1080)
| ~ hskp20 ),
inference(consistent_polarity_flipping,[],[f225]) ).
fof(f486,plain,
( c1_1(a1078)
| hskp18 ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f488,plain,
( c1_1(a1059)
| hskp15 ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f494,plain,
( c3_1(a1036)
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f245]) ).
fof(f495,plain,
( c1_1(a1036)
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f246]) ).
fof(f496,plain,
( ~ c2_1(a1035)
| hskp7 ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f504,plain,
( c1_1(a1020)
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f260]) ).
fof(f506,plain,
! [X0] :
( ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0)
| ~ hskp44
| hskp45 ),
inference(consistent_polarity_flipping,[],[f263]) ).
fof(f509,plain,
! [X0] :
( c3_1(X0)
| ndr1_0
| c2_1(X0)
| c0_1(X0)
| ~ hskp15
| hskp33 ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f512,plain,
! [X0] :
( ~ c0_1(X0)
| ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| hskp19
| hskp20 ),
inference(consistent_polarity_flipping,[],[f269]) ).
fof(f517,plain,
! [X0] :
( c3_1(X0)
| c1_1(X0)
| ndr1_0
| c0_1(X0)
| hskp8
| hskp37 ),
inference(consistent_polarity_flipping,[],[f274]) ).
fof(f519,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c3_1(X0)
| hskp13
| hskp43 ),
inference(consistent_polarity_flipping,[],[f276]) ).
fof(f524,plain,
! [X0] :
( c1_1(X0)
| c3_1(X0)
| ndr1_0
| c2_1(X0)
| ~ hskp22
| ~ hskp56 ),
inference(consistent_polarity_flipping,[],[f281]) ).
fof(f527,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| hskp33
| ~ hskp23 ),
inference(consistent_polarity_flipping,[],[f284]) ).
fof(f533,plain,
! [X0,X1] :
( ndr1_0
| c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| hskp49 ),
inference(consistent_polarity_flipping,[],[f290]) ).
fof(f534,plain,
! [X0,X1] :
( ndr1_0
| c1_1(X0)
| c3_1(X0)
| ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1)
| c0_1(X0)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f291]) ).
fof(f537,plain,
! [X0,X1] :
( ~ c2_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X0)
| c2_1(X1)
| hskp31 ),
inference(consistent_polarity_flipping,[],[f294]) ).
fof(f538,plain,
! [X0,X1] :
( c1_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| ~ c1_1(X1)
| c0_1(X1)
| ~ hskp42 ),
inference(consistent_polarity_flipping,[],[f295]) ).
fof(f541,plain,
! [X0,X1] :
( c1_1(X0)
| ndr1_0
| ~ c2_1(X1)
| c3_1(X1)
| c2_1(X0)
| ~ c3_1(X0)
| c0_1(X1)
| ~ hskp35 ),
inference(consistent_polarity_flipping,[],[f298]) ).
fof(f543,plain,
! [X0,X1] :
( c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0)
| ndr1_0
| c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| hskp33 ),
inference(consistent_polarity_flipping,[],[f300]) ).
fof(f544,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X0)
| c2_1(X1)
| hskp38 ),
inference(consistent_polarity_flipping,[],[f301]) ).
fof(f546,plain,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ hskp47 ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f547,plain,
! [X0,X1] :
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| c2_1(X1)
| ~ hskp57 ),
inference(consistent_polarity_flipping,[],[f304]) ).
fof(f548,plain,
! [X0,X1] :
( ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0)
| ndr1_0
| c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| hskp25 ),
inference(consistent_polarity_flipping,[],[f305]) ).
fof(f549,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X0)
| c2_1(X0)
| hskp51 ),
inference(consistent_polarity_flipping,[],[f306]) ).
fof(f551,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1)
| ~ hskp7 ),
inference(consistent_polarity_flipping,[],[f308]) ).
fof(f552,plain,
! [X0,X1] :
( c3_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c2_1(X1)
| c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X0)
| hskp53 ),
inference(consistent_polarity_flipping,[],[f309]) ).
fof(f553,plain,
! [X0,X1] :
( c1_1(X0)
| c3_1(X0)
| ndr1_0
| c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| ~ hskp36 ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f554,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c0_1(X1)
| c1_1(X0)
| c3_1(X1)
| ~ c2_1(X1)
| ndr1_0
| ~ c2_1(X0) ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f555,plain,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f312]) ).
fof(f556,plain,
! [X2,X0,X1] :
( ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X2)
| ~ c1_1(X2)
| c2_1(X2)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X1)
| ~ c1_1(X1) ),
inference(consistent_polarity_flipping,[],[f313]) ).
fof(f557,plain,
! [X2,X0,X1] :
( c1_1(X0)
| ndr1_0
| c1_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X2)
| ~ c3_1(X2)
| ~ c1_1(X2)
| c0_1(X1)
| c2_1(X1) ),
inference(consistent_polarity_flipping,[],[f314]) ).
fof(f558,plain,
! [X2,X0,X1] :
( ndr1_0
| ~ c2_1(X0)
| ~ c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| ~ c1_1(X2)
| c2_1(X2)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X1) ),
inference(consistent_polarity_flipping,[],[f315]) ).
fof(f561,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f562,plain,
( ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c1_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f564,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f565,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f567,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f575,definition,
( spl0_5
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f576,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| ~ c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f578,definition,
( spl0_6
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f579,plain,
( ! [X1] :
( c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f581,definition,
( spl0_7
<=> ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f582,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_3 ),
inference(avatar_split_clause,[],[f558,f567,f581,f578,f575]) ).
fof(f585,definition,
( spl0_8
<=> ! [X2] :
( c0_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f586,plain,
( ! [X2] :
( c0_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,definition,
( spl0_9
<=> ! [X1] :
( c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f589,plain,
( ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f591,definition,
( spl0_10
<=> ! [X0] :
( c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f592,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( spl0_8
| spl0_9
| spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f557,f591,f567,f588,f585]) ).
fof(f595,definition,
( spl0_11
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f596,plain,
( ! [X2] :
( c2_1(X2)
| ~ c3_1(X2)
| ~ c1_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f598,definition,
( spl0_12
<=> ! [X1] :
( ~ c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f599,plain,
( ! [X1] :
( c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f600,plain,
( spl0_11
| spl0_12
| spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f556,f567,f564,f598,f595]) ).
fof(f601,plain,
( spl0_8
| spl0_12
| spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f555,f581,f567,f598,f585]) ).
fof(f603,definition,
( spl0_13
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f604,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f606,definition,
( spl0_14
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f607,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f608,plain,
( spl0_3
| spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f554,f606,f603,f567]) ).
fof(f610,definition,
( spl0_15
<=> hskp36 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f614,definition,
( spl0_16
<=> ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f615,plain,
( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f616,plain,
( ~ spl0_15
| spl0_1
| spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f553,f614,f567,f561,f610]) ).
fof(f618,definition,
( spl0_17
<=> hskp53 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f622,definition,
( spl0_18
<=> ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f623,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f624,plain,
( spl0_17
| spl0_13
| spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f552,f622,f567,f603,f618]) ).
fof(f626,definition,
( spl0_19
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f629,plain,
( ~ spl0_19
| spl0_6
| spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f551,f603,f567,f578,f626]) ).
fof(f635,definition,
( spl0_21
<=> ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f636,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f635]) ).
fof(f639,definition,
( spl0_22
<=> hskp51 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f643,definition,
( spl0_23
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f644,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f645,plain,
( spl0_22
| spl0_13
| spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f549,f643,f567,f603,f639]) ).
fof(f647,definition,
( spl0_24
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f650,plain,
( spl0_24
| spl0_9
| spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f548,f561,f567,f588,f647]) ).
fof(f652,definition,
( spl0_25
<=> hskp57 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f655,plain,
( ~ spl0_25
| spl0_21
| spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f547,f622,f567,f635,f652]) ).
fof(f657,definition,
( spl0_26
<=> hskp47 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f661,definition,
( spl0_27
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f662,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f664,definition,
( spl0_28
<=> ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f665,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f666,plain,
( ~ spl0_26
| spl0_27
| spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f546,f664,f567,f661,f657]) ).
fof(f672,definition,
( spl0_30
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f673,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f675,definition,
( spl0_31
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f676,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f679,definition,
( spl0_32
<=> hskp38 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f682,plain,
( spl0_32
| spl0_21
| spl0_3
| spl0_31 ),
inference(avatar_split_clause,[],[f544,f675,f567,f635,f679]) ).
fof(f684,definition,
( spl0_33
<=> hskp33 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f687,plain,
( spl0_33
| spl0_9
| spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f543,f561,f567,f588,f684]) ).
fof(f694,definition,
( spl0_35
<=> hskp35 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f697,plain,
( ~ spl0_35
| spl0_6
| spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f541,f591,f567,f578,f694]) ).
fof(f703,definition,
( spl0_37
<=> ! [X1] :
( c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f704,plain,
( ! [X1] :
( c2_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f706,definition,
( spl0_38
<=> ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f707,plain,
( ! [X0] :
( c0_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f718,definition,
( spl0_41
<=> hskp42 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f721,plain,
( ~ spl0_41
| spl0_12
| spl0_3
| spl0_37 ),
inference(avatar_split_clause,[],[f538,f703,f567,f598,f718]) ).
fof(f723,definition,
( spl0_42
<=> hskp31 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f726,plain,
( spl0_42
| spl0_30
| spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f537,f581,f567,f672,f723]) ).
fof(f744,definition,
( spl0_47
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f747,plain,
( spl0_47
| spl0_8
| spl0_16
| spl0_3 ),
inference(avatar_split_clause,[],[f534,f567,f614,f585,f744]) ).
fof(f749,definition,
( spl0_48
<=> hskp49 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f752,plain,
( spl0_48
| spl0_8
| spl0_21
| spl0_3 ),
inference(avatar_split_clause,[],[f533,f567,f635,f585,f749]) ).
fof(f774,definition,
( spl0_53
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f777,plain,
( ~ spl0_53
| spl0_33
| spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f527,f603,f567,f684,f774]) ).
fof(f784,definition,
( spl0_55
<=> hskp39 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f793,definition,
( spl0_57
<=> hskp56 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f797,definition,
( spl0_58
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f800,plain,
( ~ spl0_57
| ~ spl0_58
| spl0_3
| spl0_37 ),
inference(avatar_split_clause,[],[f524,f703,f567,f797,f793]) ).
fof(f819,definition,
( spl0_63
<=> hskp43 ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f828,definition,
( spl0_65
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f831,plain,
( spl0_63
| spl0_65
| spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f519,f664,f567,f828,f819]) ).
fof(f842,definition,
( spl0_68
<=> hskp37 ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f846,definition,
( spl0_69
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f849,plain,
( spl0_68
| spl0_69
| spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f517,f614,f567,f846,f842]) ).
fof(f883,definition,
( spl0_77
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f887,definition,
( spl0_78
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f890,plain,
( spl0_77
| spl0_78
| spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f512,f564,f567,f887,f883]) ).
fof(f905,definition,
( spl0_82
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f908,plain,
( spl0_33
| ~ spl0_82
| spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f509,f706,f567,f905,f684]) ).
fof(f916,definition,
( spl0_84
<=> hskp45 ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f920,definition,
( spl0_85
<=> hskp44 ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f923,plain,
( spl0_84
| ~ spl0_85
| spl0_11
| spl0_3 ),
inference(avatar_split_clause,[],[f506,f567,f595,f920,f916]) ).
fof(f926,definition,
( spl0_86
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f930,definition,
( spl0_87
<=> c2_1(a1020) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f933,plain,
( ~ spl0_86
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f261,f930,f926]) ).
fof(f935,definition,
( spl0_88
<=> c1_1(a1020) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f938,plain,
( ~ spl0_86
| spl0_88 ),
inference(avatar_split_clause,[],[f504,f935,f926]) ).
fof(f1000,definition,
( spl0_101
<=> c2_1(a1035) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f1002,plain,
( ~ c2_1(a1035)
| spl0_101 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1003,plain,
( spl0_19
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f496,f1000,f626]) ).
fof(f1005,definition,
( spl0_102
<=> c1_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f1008,plain,
( ~ spl0_69
| spl0_102 ),
inference(avatar_split_clause,[],[f495,f1005,f846]) ).
fof(f1010,definition,
( spl0_103
<=> c3_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f1012,plain,
( c3_1(a1036)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f1010]) ).
fof(f1013,plain,
( ~ spl0_69
| spl0_103 ),
inference(avatar_split_clause,[],[f494,f1010,f846]) ).
fof(f1055,definition,
( spl0_112
<=> c2_1(a1048) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f1058,plain,
( ~ spl0_65
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f236,f1055,f828]) ).
fof(f1075,definition,
( spl0_116
<=> c1_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f1078,plain,
( spl0_82
| spl0_116 ),
inference(avatar_split_clause,[],[f488,f1075,f905]) ).
fof(f1085,definition,
( spl0_118
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f1089,definition,
( spl0_119
<=> c2_1(a1077) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f1092,plain,
( ~ spl0_118
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f230,f1089,f1085]) ).
fof(f1094,definition,
( spl0_120
<=> c0_1(a1077) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f1096,plain,
( ~ c0_1(a1077)
| spl0_120 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1097,plain,
( ~ spl0_118
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f229,f1094,f1085]) ).
fof(f1099,definition,
( spl0_121
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1103,definition,
( spl0_122
<=> c1_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f1106,plain,
( spl0_121
| spl0_122 ),
inference(avatar_split_clause,[],[f486,f1103,f1099]) ).
fof(f1108,definition,
( spl0_123
<=> c2_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f1110,plain,
( ~ c2_1(a1079)
| spl0_123 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1111,plain,
( ~ spl0_78
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f227,f1108,f887]) ).
fof(f1113,definition,
( spl0_124
<=> c0_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f1115,plain,
( ~ c0_1(a1079)
| spl0_124 ),
inference(avatar_component_clause,[],[f1113]) ).
fof(f1116,plain,
( ~ spl0_78
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f226,f1113,f887]) ).
fof(f1118,definition,
( spl0_125
<=> c1_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f1121,plain,
( ~ spl0_77
| spl0_125 ),
inference(avatar_split_clause,[],[f485,f1118,f883]) ).
fof(f1123,definition,
( spl0_126
<=> c2_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f1126,plain,
( ~ spl0_77
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f224,f1123,f883]) ).
fof(f1128,definition,
( spl0_127
<=> c0_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f1130,plain,
( ~ c0_1(a1080)
| spl0_127 ),
inference(avatar_component_clause,[],[f1128]) ).
fof(f1131,plain,
( ~ spl0_77
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f223,f1128,f883]) ).
fof(f1148,definition,
( spl0_131
<=> c1_1(a1083) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1151,plain,
( spl0_58
| spl0_131 ),
inference(avatar_split_clause,[],[f483,f1148,f797]) ).
fof(f1153,definition,
( spl0_132
<=> c2_1(a1088) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1155,plain,
( ~ c2_1(a1088)
| spl0_132 ),
inference(avatar_component_clause,[],[f1153]) ).
fof(f1156,plain,
( spl0_53
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f482,f1153,f774]) ).
fof(f1158,definition,
( spl0_133
<=> c1_1(a1089) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1161,plain,
( ~ spl0_47
| spl0_133 ),
inference(avatar_split_clause,[],[f481,f1158,f744]) ).
fof(f1163,definition,
( spl0_134
<=> c2_1(a1089) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f1165,plain,
( ~ c2_1(a1089)
| spl0_134 ),
inference(avatar_component_clause,[],[f1163]) ).
fof(f1166,plain,
( ~ spl0_47
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f216,f1163,f744]) ).
fof(f1168,definition,
( spl0_135
<=> c2_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f1170,plain,
( ~ c2_1(a1091)
| spl0_135 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1171,plain,
( ~ spl0_24
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f215,f1168,f647]) ).
fof(f1173,definition,
( spl0_136
<=> c0_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f1175,plain,
( ~ c0_1(a1091)
| spl0_136 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1176,plain,
( ~ spl0_24
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f214,f1173,f647]) ).
fof(f1178,definition,
( spl0_137
<=> c3_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1181,plain,
( ~ spl0_24
| spl0_137 ),
inference(avatar_split_clause,[],[f480,f1178,f647]) ).
fof(f1193,definition,
( spl0_140
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1197,definition,
( spl0_141
<=> c0_1(a1101) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1199,plain,
( ~ c0_1(a1101)
| spl0_141 ),
inference(avatar_component_clause,[],[f1197]) ).
fof(f1200,plain,
( ~ spl0_140
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f210,f1197,f1193]) ).
fof(f1202,definition,
( spl0_142
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1206,definition,
( spl0_143
<=> c1_1(a1102) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1209,plain,
( ~ spl0_142
| spl0_143 ),
inference(avatar_split_clause,[],[f478,f1206,f1202]) ).
fof(f1211,definition,
( spl0_144
<=> c0_1(a1102) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1213,plain,
( ~ c0_1(a1102)
| spl0_144 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1214,plain,
( ~ spl0_142
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f208,f1211,f1202]) ).
fof(f1216,definition,
( spl0_145
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1220,definition,
( spl0_146
<=> c3_1(a1021) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1223,plain,
( spl0_145
| spl0_146 ),
inference(avatar_split_clause,[],[f477,f1220,f1216]) ).
fof(f1225,definition,
( spl0_147
<=> c1_1(a1021) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1228,plain,
( spl0_145
| spl0_147 ),
inference(avatar_split_clause,[],[f476,f1225,f1216]) ).
fof(f1230,definition,
( spl0_148
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1234,definition,
( spl0_149
<=> c2_1(a1022) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1236,plain,
( ~ c2_1(a1022)
| spl0_149 ),
inference(avatar_component_clause,[],[f1234]) ).
fof(f1237,plain,
( spl0_148
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f475,f1234,f1230]) ).
fof(f1239,definition,
( spl0_150
<=> c1_1(a1028) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1242,plain,
( ~ spl0_42
| spl0_150 ),
inference(avatar_split_clause,[],[f474,f1239,f723]) ).
fof(f1249,definition,
( spl0_152
<=> c1_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1252,plain,
( ~ spl0_33
| spl0_152 ),
inference(avatar_split_clause,[],[f473,f1249,f684]) ).
fof(f1264,definition,
( spl0_155
<=> c0_1(a1034) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1266,plain,
( ~ c0_1(a1034)
| spl0_155 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1267,plain,
( spl0_15
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f471,f1264,f610]) ).
fof(f1274,definition,
( spl0_157
<=> c1_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1277,plain,
( ~ spl0_55
| spl0_157 ),
inference(avatar_split_clause,[],[f469,f1274,f784]) ).
fof(f1294,definition,
( spl0_161
<=> c2_1(a1046) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1296,plain,
( ~ c2_1(a1046)
| spl0_161 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1297,plain,
( spl0_41
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f466,f1294,f718]) ).
fof(f1299,definition,
( spl0_162
<=> c2_1(a1051) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1301,plain,
( ~ c2_1(a1051)
| spl0_162 ),
inference(avatar_component_clause,[],[f1299]) ).
fof(f1302,plain,
( spl0_85
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f465,f1299,f920]) ).
fof(f1318,definition,
( spl0_166
<=> c2_1(a1065) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1320,plain,
( ~ c2_1(a1065)
| spl0_166 ),
inference(avatar_component_clause,[],[f1318]) ).
fof(f1321,plain,
( ~ spl0_48
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f189,f1318,f749]) ).
fof(f1323,definition,
( spl0_167
<=> c0_1(a1065) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1325,plain,
( ~ c0_1(a1065)
| spl0_167 ),
inference(avatar_component_clause,[],[f1323]) ).
fof(f1326,plain,
( ~ spl0_48
| ~ spl0_167 ),
inference(avatar_split_clause,[],[f188,f1323,f749]) ).
fof(f1333,definition,
( spl0_169
<=> c1_1(a1070) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1336,plain,
( ~ spl0_22
| spl0_169 ),
inference(avatar_split_clause,[],[f462,f1333,f639]) ).
fof(f1343,definition,
( spl0_171
<=> c1_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1346,plain,
( spl0_57
| spl0_171 ),
inference(avatar_split_clause,[],[f460,f1343,f793]) ).
fof(f1348,definition,
( spl0_172
<=> c3_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f1350,plain,
( c3_1(a1084)
| ~ spl0_172 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1351,plain,
( spl0_57
| spl0_172 ),
inference(avatar_split_clause,[],[f459,f1348,f793]) ).
fof(f1383,definition,
( spl0_179
<=> hskp63 ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f1387,definition,
( spl0_180
<=> c2_1(a1105) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f1389,plain,
( ~ c2_1(a1105)
| spl0_180 ),
inference(avatar_component_clause,[],[f1387]) ).
fof(f1390,plain,
( ~ spl0_179
| ~ spl0_180 ),
inference(avatar_split_clause,[],[f176,f1387,f1383]) ).
fof(f1392,definition,
( spl0_181
<=> c0_1(a1020) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1394,plain,
( c0_1(a1020)
| ~ spl0_181 ),
inference(avatar_component_clause,[],[f1392]) ).
fof(f1395,plain,
( spl0_181
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f175,f926,f1392]) ).
fof(f1427,definition,
( spl0_188
<=> c1_1(a1035) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f1430,plain,
( ~ spl0_188
| spl0_19 ),
inference(avatar_split_clause,[],[f452,f626,f1427]) ).
fof(f1432,definition,
( spl0_189
<=> c0_1(a1035) ),
introduced(definition,[new_symbols(definition,[spl0_189])],[avatar_definition]) ).
fof(f1434,plain,
( c0_1(a1035)
| ~ spl0_189 ),
inference(avatar_component_clause,[],[f1432]) ).
fof(f1435,plain,
( spl0_189
| spl0_19 ),
inference(avatar_split_clause,[],[f451,f626,f1432]) ).
fof(f1437,definition,
( spl0_190
<=> c0_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f1439,plain,
( c0_1(a1036)
| ~ spl0_190 ),
inference(avatar_component_clause,[],[f1437]) ).
fof(f1440,plain,
( spl0_190
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f166,f846,f1437]) ).
fof(f1462,definition,
( spl0_195
<=> c3_1(a1048) ),
introduced(definition,[new_symbols(definition,[spl0_195])],[avatar_definition]) ).
fof(f1465,plain,
( ~ spl0_195
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f447,f828,f1462]) ).
fof(f1467,definition,
( spl0_196
<=> c0_1(a1048) ),
introduced(definition,[new_symbols(definition,[spl0_196])],[avatar_definition]) ).
fof(f1469,plain,
( c0_1(a1048)
| ~ spl0_196 ),
inference(avatar_component_clause,[],[f1467]) ).
fof(f1470,plain,
( spl0_196
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f160,f828,f1467]) ).
fof(f1472,definition,
( spl0_197
<=> c2_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_197])],[avatar_definition]) ).
fof(f1474,plain,
( c2_1(a1059)
| ~ spl0_197 ),
inference(avatar_component_clause,[],[f1472]) ).
fof(f1475,plain,
( spl0_197
| spl0_82 ),
inference(avatar_split_clause,[],[f446,f905,f1472]) ).
fof(f1477,definition,
( spl0_198
<=> c3_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_198])],[avatar_definition]) ).
fof(f1480,plain,
( ~ spl0_198
| spl0_82 ),
inference(avatar_split_clause,[],[f445,f905,f1477]) ).
fof(f1492,definition,
( spl0_201
<=> c3_1(a1077) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f1495,plain,
( ~ spl0_201
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f444,f1085,f1492]) ).
fof(f1497,definition,
( spl0_202
<=> c0_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f1499,plain,
( c0_1(a1078)
| ~ spl0_202 ),
inference(avatar_component_clause,[],[f1497]) ).
fof(f1500,plain,
( spl0_202
| spl0_121 ),
inference(avatar_split_clause,[],[f443,f1099,f1497]) ).
fof(f1502,definition,
( spl0_203
<=> c2_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f1504,plain,
( c2_1(a1078)
| ~ spl0_203 ),
inference(avatar_component_clause,[],[f1502]) ).
fof(f1505,plain,
( spl0_203
| spl0_121 ),
inference(avatar_split_clause,[],[f442,f1099,f1502]) ).
fof(f1507,definition,
( spl0_204
<=> c1_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f1510,plain,
( ~ spl0_204
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f441,f887,f1507]) ).
fof(f1512,definition,
( spl0_205
<=> c3_1(a1083) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f1515,plain,
( ~ spl0_205
| spl0_58 ),
inference(avatar_split_clause,[],[f440,f797,f1512]) ).
fof(f1517,definition,
( spl0_206
<=> c2_1(a1083) ),
introduced(definition,[new_symbols(definition,[spl0_206])],[avatar_definition]) ).
fof(f1519,plain,
( c2_1(a1083)
| ~ spl0_206 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1520,plain,
( spl0_206
| spl0_58 ),
inference(avatar_split_clause,[],[f439,f797,f1517]) ).
fof(f1522,definition,
( spl0_207
<=> c3_1(a1088) ),
introduced(definition,[new_symbols(definition,[spl0_207])],[avatar_definition]) ).
fof(f1525,plain,
( ~ spl0_207
| spl0_53 ),
inference(avatar_split_clause,[],[f438,f774,f1522]) ).
fof(f1527,definition,
( spl0_208
<=> c1_1(a1088) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f1530,plain,
( ~ spl0_208
| spl0_53 ),
inference(avatar_split_clause,[],[f437,f774,f1527]) ).
fof(f1532,definition,
( spl0_209
<=> c0_1(a1089) ),
introduced(definition,[new_symbols(definition,[spl0_209])],[avatar_definition]) ).
fof(f1534,plain,
( c0_1(a1089)
| ~ spl0_209 ),
inference(avatar_component_clause,[],[f1532]) ).
fof(f1535,plain,
( spl0_209
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f147,f744,f1532]) ).
fof(f1547,definition,
( spl0_212
<=> c3_1(a1101) ),
introduced(definition,[new_symbols(definition,[spl0_212])],[avatar_definition]) ).
fof(f1550,plain,
( ~ spl0_212
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f434,f1193,f1547]) ).
fof(f1552,definition,
( spl0_213
<=> c2_1(a1102) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f1554,plain,
( c2_1(a1102)
| ~ spl0_213 ),
inference(avatar_component_clause,[],[f1552]) ).
fof(f1555,plain,
( spl0_213
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f143,f1202,f1552]) ).
fof(f1557,definition,
( spl0_214
<=> c2_1(a1021) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f1559,plain,
( c2_1(a1021)
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1560,plain,
( spl0_214
| spl0_145 ),
inference(avatar_split_clause,[],[f433,f1216,f1557]) ).
fof(f1562,definition,
( spl0_215
<=> c1_1(a1022) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1565,plain,
( ~ spl0_215
| spl0_148 ),
inference(avatar_split_clause,[],[f432,f1230,f1562]) ).
fof(f1567,definition,
( spl0_216
<=> c3_1(a1022) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1570,plain,
( ~ spl0_216
| spl0_148 ),
inference(avatar_split_clause,[],[f431,f1230,f1567]) ).
fof(f1572,definition,
( spl0_217
<=> c3_1(a1028) ),
introduced(definition,[new_symbols(definition,[spl0_217])],[avatar_definition]) ).
fof(f1575,plain,
( ~ spl0_217
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f430,f723,f1572]) ).
fof(f1577,definition,
( spl0_218
<=> c0_1(a1028) ),
introduced(definition,[new_symbols(definition,[spl0_218])],[avatar_definition]) ).
fof(f1579,plain,
( c0_1(a1028)
| ~ spl0_218 ),
inference(avatar_component_clause,[],[f1577]) ).
fof(f1580,plain,
( spl0_218
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f138,f723,f1577]) ).
fof(f1592,definition,
( spl0_221
<=> c2_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f1594,plain,
( c2_1(a1031)
| ~ spl0_221 ),
inference(avatar_component_clause,[],[f1592]) ).
fof(f1595,plain,
( spl0_221
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f135,f684,f1592]) ).
fof(f1597,definition,
( spl0_222
<=> c3_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f1600,plain,
( ~ spl0_222
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f428,f684,f1597]) ).
fof(f1607,definition,
( spl0_224
<=> c3_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f1610,plain,
( ~ spl0_224
| spl0_35 ),
inference(avatar_split_clause,[],[f426,f694,f1607]) ).
fof(f1612,definition,
( spl0_225
<=> c1_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_225])],[avatar_definition]) ).
fof(f1615,plain,
( ~ spl0_225
| spl0_35 ),
inference(avatar_split_clause,[],[f425,f694,f1612]) ).
fof(f1617,definition,
( spl0_226
<=> c0_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_226])],[avatar_definition]) ).
fof(f1619,plain,
( c0_1(a1033)
| ~ spl0_226 ),
inference(avatar_component_clause,[],[f1617]) ).
fof(f1620,plain,
( spl0_226
| spl0_35 ),
inference(avatar_split_clause,[],[f424,f694,f1617]) ).
fof(f1622,definition,
( spl0_227
<=> c1_1(a1034) ),
introduced(definition,[new_symbols(definition,[spl0_227])],[avatar_definition]) ).
fof(f1625,plain,
( ~ spl0_227
| spl0_15 ),
inference(avatar_split_clause,[],[f423,f610,f1622]) ).
fof(f1627,definition,
( spl0_228
<=> c3_1(a1034) ),
introduced(definition,[new_symbols(definition,[spl0_228])],[avatar_definition]) ).
fof(f1630,plain,
( ~ spl0_228
| spl0_15 ),
inference(avatar_split_clause,[],[f422,f610,f1627]) ).
fof(f1632,definition,
( spl0_229
<=> c3_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f1635,plain,
( ~ spl0_229
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f421,f842,f1632]) ).
fof(f1637,definition,
( spl0_230
<=> c0_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1639,plain,
( c0_1(a1037)
| ~ spl0_230 ),
inference(avatar_component_clause,[],[f1637]) ).
fof(f1640,plain,
( spl0_230
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f126,f842,f1637]) ).
fof(f1642,definition,
( spl0_231
<=> c2_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_231])],[avatar_definition]) ).
fof(f1644,plain,
( c2_1(a1040)
| ~ spl0_231 ),
inference(avatar_component_clause,[],[f1642]) ).
fof(f1645,plain,
( spl0_231
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f125,f679,f1642]) ).
fof(f1647,definition,
( spl0_232
<=> c3_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_232])],[avatar_definition]) ).
fof(f1650,plain,
( ~ spl0_232
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f420,f679,f1647]) ).
fof(f1652,definition,
( spl0_233
<=> c1_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_233])],[avatar_definition]) ).
fof(f1655,plain,
( ~ spl0_233
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f419,f679,f1652]) ).
fof(f1657,definition,
( spl0_234
<=> c2_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_234])],[avatar_definition]) ).
fof(f1659,plain,
( c2_1(a1042)
| ~ spl0_234 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1660,plain,
( spl0_234
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f122,f784,f1657]) ).
fof(f1662,definition,
( spl0_235
<=> c0_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_235])],[avatar_definition]) ).
fof(f1664,plain,
( c0_1(a1042)
| ~ spl0_235 ),
inference(avatar_component_clause,[],[f1662]) ).
fof(f1665,plain,
( spl0_235
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f121,f784,f1662]) ).
fof(f1682,definition,
( spl0_239
<=> c0_1(a1046) ),
introduced(definition,[new_symbols(definition,[spl0_239])],[avatar_definition]) ).
fof(f1684,plain,
( c0_1(a1046)
| ~ spl0_239 ),
inference(avatar_component_clause,[],[f1682]) ).
fof(f1685,plain,
( spl0_239
| spl0_41 ),
inference(avatar_split_clause,[],[f416,f718,f1682]) ).
fof(f1687,definition,
( spl0_240
<=> c1_1(a1046) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1690,plain,
( ~ spl0_240
| spl0_41 ),
inference(avatar_split_clause,[],[f415,f718,f1687]) ).
fof(f1692,definition,
( spl0_241
<=> c1_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1695,plain,
( ~ spl0_241
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f414,f819,f1692]) ).
fof(f1697,definition,
( spl0_242
<=> c2_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f1700,plain,
( spl0_242
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f114,f819,f1697]) ).
fof(f1702,definition,
( spl0_243
<=> c0_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f1704,plain,
( c0_1(a1049)
| ~ spl0_243 ),
inference(avatar_component_clause,[],[f1702]) ).
fof(f1705,plain,
( spl0_243
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f113,f819,f1702]) ).
fof(f1707,definition,
( spl0_244
<=> c0_1(a1051) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f1709,plain,
( c0_1(a1051)
| ~ spl0_244 ),
inference(avatar_component_clause,[],[f1707]) ).
fof(f1710,plain,
( spl0_244
| spl0_85 ),
inference(avatar_split_clause,[],[f413,f920,f1707]) ).
fof(f1712,definition,
( spl0_245
<=> c1_1(a1051) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f1715,plain,
( ~ spl0_245
| spl0_85 ),
inference(avatar_split_clause,[],[f412,f920,f1712]) ).
fof(f1717,definition,
( spl0_246
<=> c2_1(a1052) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f1720,plain,
( spl0_246
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f110,f916,f1717]) ).
fof(f1722,definition,
( spl0_247
<=> c3_1(a1052) ),
introduced(definition,[new_symbols(definition,[spl0_247])],[avatar_definition]) ).
fof(f1725,plain,
( ~ spl0_247
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f411,f916,f1722]) ).
fof(f1727,definition,
( spl0_248
<=> c0_1(a1052) ),
introduced(definition,[new_symbols(definition,[spl0_248])],[avatar_definition]) ).
fof(f1729,plain,
( c0_1(a1052)
| ~ spl0_248 ),
inference(avatar_component_clause,[],[f1727]) ).
fof(f1730,plain,
( spl0_248
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f108,f916,f1727]) ).
fof(f1737,definition,
( spl0_250
<=> c3_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_250])],[avatar_definition]) ).
fof(f1740,plain,
( ~ spl0_250
| spl0_26 ),
inference(avatar_split_clause,[],[f410,f657,f1737]) ).
fof(f1742,definition,
( spl0_251
<=> c1_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f1745,plain,
( ~ spl0_251
| spl0_26 ),
inference(avatar_split_clause,[],[f409,f657,f1742]) ).
fof(f1747,definition,
( spl0_252
<=> c2_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f1749,plain,
( c2_1(a1056)
| ~ spl0_252 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1750,plain,
( spl0_252
| spl0_26 ),
inference(avatar_split_clause,[],[f408,f657,f1747]) ).
fof(f1767,definition,
( spl0_256
<=> c1_1(a1065) ),
introduced(definition,[new_symbols(definition,[spl0_256])],[avatar_definition]) ).
fof(f1770,plain,
( ~ spl0_256
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f404,f749,f1767]) ).
fof(f1787,definition,
( spl0_260
<=> c2_1(a1070) ),
introduced(definition,[new_symbols(definition,[spl0_260])],[avatar_definition]) ).
fof(f1789,plain,
( c2_1(a1070)
| ~ spl0_260 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1790,plain,
( spl0_260
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f96,f639,f1787]) ).
fof(f1807,definition,
( spl0_264
<=> c0_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_264])],[avatar_definition]) ).
fof(f1809,plain,
( c0_1(a1073)
| ~ spl0_264 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1810,plain,
( spl0_264
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f92,f618,f1807]) ).
fof(f1812,definition,
( spl0_265
<=> c2_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_265])],[avatar_definition]) ).
fof(f1815,plain,
( spl0_265
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f91,f618,f1812]) ).
fof(f1817,definition,
( spl0_266
<=> c1_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_266])],[avatar_definition]) ).
fof(f1820,plain,
( ~ spl0_266
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f399,f618,f1817]) ).
fof(f1847,definition,
( spl0_272
<=> c0_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_272])],[avatar_definition]) ).
fof(f1849,plain,
( c0_1(a1084)
| ~ spl0_272 ),
inference(avatar_component_clause,[],[f1847]) ).
fof(f1850,plain,
( spl0_272
| spl0_57 ),
inference(avatar_split_clause,[],[f395,f793,f1847]) ).
fof(f1852,definition,
( spl0_273
<=> c3_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_273])],[avatar_definition]) ).
fof(f1855,plain,
( ~ spl0_273
| spl0_25 ),
inference(avatar_split_clause,[],[f394,f652,f1852]) ).
fof(f1857,definition,
( spl0_274
<=> c0_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_274])],[avatar_definition]) ).
fof(f1859,plain,
( c0_1(a1085)
| ~ spl0_274 ),
inference(avatar_component_clause,[],[f1857]) ).
fof(f1860,plain,
( spl0_274
| spl0_25 ),
inference(avatar_split_clause,[],[f393,f652,f1857]) ).
fof(f1862,definition,
( spl0_275
<=> c2_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_275])],[avatar_definition]) ).
fof(f1865,plain,
( spl0_275
| spl0_25 ),
inference(avatar_split_clause,[],[f392,f652,f1862]) ).
fof(f1901,definition,
( spl0_283
<=> hskp62 ),
introduced(definition,[new_symbols(definition,[spl0_283])],[avatar_definition]) ).
fof(f1906,definition,
( spl0_284
<=> c3_1(a1103) ),
introduced(definition,[new_symbols(definition,[spl0_284])],[avatar_definition]) ).
fof(f1909,plain,
( ~ spl0_284
| ~ spl0_283 ),
inference(avatar_split_clause,[],[f386,f1901,f1906]) ).
fof(f1911,definition,
( spl0_285
<=> c2_1(a1103) ),
introduced(definition,[new_symbols(definition,[spl0_285])],[avatar_definition]) ).
fof(f1913,plain,
( c2_1(a1103)
| ~ spl0_285 ),
inference(avatar_component_clause,[],[f1911]) ).
fof(f1914,plain,
( spl0_285
| ~ spl0_283 ),
inference(avatar_split_clause,[],[f72,f1901,f1911]) ).
fof(f1916,definition,
( spl0_286
<=> c3_1(a1105) ),
introduced(definition,[new_symbols(definition,[spl0_286])],[avatar_definition]) ).
fof(f1919,plain,
( ~ spl0_286
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f385,f1383,f1916]) ).
fof(f1921,definition,
( spl0_287
<=> c1_1(a1105) ),
introduced(definition,[new_symbols(definition,[spl0_287])],[avatar_definition]) ).
fof(f1924,plain,
( ~ spl0_287
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f384,f1383,f1921]) ).
fof(f1925,plain,
( spl0_179
| ~ spl0_57
| spl0_283 ),
inference(avatar_split_clause,[],[f383,f1901,f793,f1383]) ).
fof(f1926,plain,
( spl0_142
| spl0_140
| spl0_63 ),
inference(avatar_split_clause,[],[f68,f819,f1193,f1202]) ).
fof(f1927,plain,
( ~ spl0_121
| spl0_118
| spl0_55 ),
inference(avatar_split_clause,[],[f382,f784,f1085,f1099]) ).
fof(f1929,plain,
( ~ spl0_148
| ~ spl0_145
| spl0_86 ),
inference(avatar_split_clause,[],[f381,f926,f1216,f1230]) ).
fof(f1986,plain,
( ~ spl0_3
| spl0_57 ),
inference(avatar_split_clause,[],[f324,f793,f567]) ).
fof(f1992,plain,
( ~ spl0_3
| ~ spl0_283 ),
inference(avatar_split_clause,[],[f318,f1901,f567]) ).
fof(f1993,plain,
( ~ spl0_3
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f317,f1383,f567]) ).
fof(f2019,plain,
( ~ c2_1(a1034)
| c3_1(a1034)
| ~ spl0_6
| spl0_155 ),
inference(resolution,[],[f579,f1266]) ).
fof(f2024,plain,
( ~ c2_1(a1101)
| c3_1(a1101)
| ~ spl0_6
| spl0_141 ),
inference(resolution,[],[f579,f1199]) ).
fof(f2062,definition,
( spl0_291
<=> c2_1(a1101) ),
introduced(definition,[new_symbols(definition,[spl0_291])],[avatar_definition]) ).
fof(f2067,definition,
( spl0_292
<=> c2_1(a1028) ),
introduced(definition,[new_symbols(definition,[spl0_292])],[avatar_definition]) ).
fof(f2072,definition,
( spl0_293
<=> c2_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_293])],[avatar_definition]) ).
fof(f2077,definition,
( spl0_294
<=> c2_1(a1034) ),
introduced(definition,[new_symbols(definition,[spl0_294])],[avatar_definition]) ).
fof(f2082,definition,
( spl0_295
<=> c2_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_295])],[avatar_definition]) ).
fof(f2112,definition,
( spl0_301
<=> c2_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_301])],[avatar_definition]) ).
fof(f2113,plain,
( c2_1(a1084)
| ~ spl0_301 ),
inference(avatar_component_clause,[],[f2112]) ).
fof(f2114,plain,
( ~ c2_1(a1084)
| spl0_301 ),
inference(avatar_component_clause,[],[f2112]) ).
fof(f2123,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_2
| ~ spl0_8 ),
inference(resolution,[],[f586,f565]) ).
fof(f2174,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_2
| ~ spl0_8 ),
inference(duplicate_literal_removal,[],[f2123]) ).
fof(f2195,plain,
( c2_1(a1065)
| c1_1(a1065)
| ~ spl0_9
| spl0_167 ),
inference(resolution,[],[f589,f1325]) ).
fof(f2251,definition,
( spl0_307
<=> c1_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_307])],[avatar_definition]) ).
fof(f2398,plain,
( c1_1(a1091)
| ~ c3_1(a1091)
| ~ spl0_10
| spl0_135 ),
inference(resolution,[],[f592,f1170]) ).
fof(f2412,definition,
( spl0_319
<=> c3_1(a1020) ),
introduced(definition,[new_symbols(definition,[spl0_319])],[avatar_definition]) ).
fof(f2413,plain,
( c3_1(a1020)
| ~ spl0_319 ),
inference(avatar_component_clause,[],[f2412]) ).
fof(f2427,definition,
( spl0_322
<=> c3_1(a1035) ),
introduced(definition,[new_symbols(definition,[spl0_322])],[avatar_definition]) ).
fof(f2442,definition,
( spl0_325
<=> c3_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_325])],[avatar_definition]) ).
fof(f2443,plain,
( c3_1(a1078)
| ~ spl0_325 ),
inference(avatar_component_clause,[],[f2442]) ).
fof(f2447,definition,
( spl0_326
<=> c3_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_326])],[avatar_definition]) ).
fof(f2452,definition,
( spl0_327
<=> c3_1(a1089) ),
introduced(definition,[new_symbols(definition,[spl0_327])],[avatar_definition]) ).
fof(f2457,definition,
( spl0_328
<=> c3_1(a1102) ),
introduced(definition,[new_symbols(definition,[spl0_328])],[avatar_definition]) ).
fof(f2458,plain,
( c3_1(a1102)
| ~ spl0_328 ),
inference(avatar_component_clause,[],[f2457]) ).
fof(f2467,definition,
( spl0_330
<=> c3_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_330])],[avatar_definition]) ).
fof(f2472,definition,
( spl0_331
<=> c3_1(a1046) ),
introduced(definition,[new_symbols(definition,[spl0_331])],[avatar_definition]) ).
fof(f2482,definition,
( spl0_333
<=> c3_1(a1051) ),
introduced(definition,[new_symbols(definition,[spl0_333])],[avatar_definition]) ).
fof(f2492,definition,
( spl0_335
<=> c3_1(a1065) ),
introduced(definition,[new_symbols(definition,[spl0_335])],[avatar_definition]) ).
fof(f2497,definition,
( spl0_336
<=> c3_1(a1070) ),
introduced(definition,[new_symbols(definition,[spl0_336])],[avatar_definition]) ).
fof(f2512,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(resolution,[],[f596,f582]) ).
fof(f2568,plain,
( ~ c3_1(a1091)
| ~ c1_1(a1091)
| ~ spl0_11
| spl0_135 ),
inference(resolution,[],[f596,f1170]) ).
fof(f2574,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f2512]) ).
fof(f2576,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_6
| ~ spl0_14 ),
inference(resolution,[],[f607,f579]) ).
fof(f2578,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_6
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f2576]) ).
fof(f2580,plain,
( spl0_1
| ~ spl0_6
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f2578,f606,f578,f561]) ).
fof(f2581,plain,
( ~ c1_1(a1020)
| ~ c3_1(a1020)
| ~ spl0_2
| ~ spl0_181 ),
inference(resolution,[],[f1394,f565]) ).
fof(f2588,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_6
| ~ spl0_13 ),
inference(resolution,[],[f604,f579]) ).
fof(f2591,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_6
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f2588]) ).
fof(f2594,plain,
( c3_1(a1031)
| ~ spl0_6
| ~ spl0_13
| ~ spl0_221 ),
inference(resolution,[],[f2591,f1594]) ).
fof(f2596,plain,
( spl0_222
| ~ spl0_6
| ~ spl0_13
| ~ spl0_221 ),
inference(avatar_split_clause,[],[f2594,f1592,f603,f578,f1597]) ).
fof(f2600,plain,
( ! [X0] :
( c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_13
| ~ spl0_16 ),
inference(resolution,[],[f615,f604]) ).
fof(f2614,plain,
( c1_1(a1065)
| c3_1(a1065)
| ~ spl0_16
| spl0_167 ),
inference(resolution,[],[f615,f1325]) ).
fof(f2649,plain,
( ! [X0] :
( c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_13
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f2600]) ).
fof(f2681,plain,
( spl0_335
| spl0_256
| ~ spl0_16
| spl0_167 ),
inference(avatar_split_clause,[],[f2614,f1323,f614,f1767,f2492]) ).
fof(f2694,plain,
( spl0_1
| ~ spl0_13
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f2649,f614,f603,f561]) ).
fof(f2703,plain,
( c3_1(a1056)
| c1_1(a1056)
| ~ spl0_1
| ~ spl0_252 ),
inference(resolution,[],[f562,f1749]) ).
fof(f2737,plain,
( c1_1(a1065)
| ~ c3_1(a1065)
| ~ spl0_10
| spl0_166 ),
inference(resolution,[],[f592,f1320]) ).
fof(f2741,plain,
( c1_1(a1051)
| ~ c3_1(a1051)
| ~ spl0_10
| spl0_162 ),
inference(resolution,[],[f592,f1301]) ).
fof(f2743,plain,
( c1_1(a1046)
| ~ c3_1(a1046)
| ~ spl0_10
| spl0_161 ),
inference(resolution,[],[f592,f1296]) ).
fof(f2762,plain,
( c1_1(a1079)
| ~ c3_1(a1079)
| ~ spl0_10
| spl0_123 ),
inference(resolution,[],[f592,f1110]) ).
fof(f2773,plain,
( c1_1(a1035)
| ~ c3_1(a1035)
| ~ spl0_10
| spl0_101 ),
inference(resolution,[],[f592,f1002]) ).
fof(f2789,plain,
( ~ c1_1(a1031)
| c3_1(a1031)
| ~ spl0_18
| ~ spl0_221 ),
inference(resolution,[],[f623,f1594]) ).
fof(f2794,plain,
( c2_1(a1037)
| c3_1(a1037)
| ~ spl0_21
| ~ spl0_230 ),
inference(resolution,[],[f636,f1639]) ).
fof(f2797,plain,
( c2_1(a1020)
| c3_1(a1020)
| ~ spl0_21
| ~ spl0_181 ),
inference(resolution,[],[f636,f1394]) ).
fof(f2802,plain,
( spl0_222
| ~ spl0_152
| ~ spl0_18
| ~ spl0_221 ),
inference(avatar_split_clause,[],[f2789,f1592,f622,f1249,f1597]) ).
fof(f2863,plain,
( ~ c2_1(a1033)
| c1_1(a1033)
| ~ spl0_14
| ~ spl0_226 ),
inference(resolution,[],[f607,f1619]) ).
fof(f2874,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_8
| ~ spl0_23 ),
inference(resolution,[],[f644,f586]) ).
fof(f2879,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_8
| ~ spl0_23 ),
inference(duplicate_literal_removal,[],[f2874]) ).
fof(f2893,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_8
| ~ spl0_27 ),
inference(resolution,[],[f662,f586]) ).
fof(f2898,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_8
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f2893]) ).
fof(f2900,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f2898,f661,f585,f581]) ).
fof(f2905,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_8
| ~ spl0_28 ),
inference(resolution,[],[f665,f586]) ).
fof(f2911,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_8
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f2905]) ).
fof(f2913,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f2911,f664,f585,f581]) ).
fof(f2931,plain,
( ~ c2_1(a1049)
| c1_1(a1049)
| ~ spl0_14
| ~ spl0_243 ),
inference(resolution,[],[f1704,f607]) ).
fof(f2936,plain,
( ~ c2_1(a1073)
| c1_1(a1073)
| ~ spl0_14
| ~ spl0_264 ),
inference(resolution,[],[f1809,f607]) ).
fof(f2938,plain,
( spl0_266
| ~ spl0_265
| ~ spl0_14
| ~ spl0_264 ),
inference(avatar_split_clause,[],[f2936,f1807,f606,f1812,f1817]) ).
fof(f2978,plain,
( c2_1(a1091)
| ~ c1_1(a1091)
| ~ spl0_5
| spl0_136 ),
inference(resolution,[],[f576,f1175]) ).
fof(f2980,plain,
( c2_1(a1080)
| ~ c1_1(a1080)
| ~ spl0_5
| spl0_127 ),
inference(resolution,[],[f576,f1130]) ).
fof(f2985,plain,
( c3_1(a1040)
| c1_1(a1040)
| ~ spl0_1
| ~ spl0_231 ),
inference(resolution,[],[f1644,f562]) ).
fof(f3029,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_12
| ~ spl0_13 ),
inference(resolution,[],[f604,f599]) ).
fof(f3031,plain,
( ~ c2_1(a1085)
| c3_1(a1085)
| ~ spl0_13
| ~ spl0_274 ),
inference(resolution,[],[f604,f1859]) ).
fof(f3037,plain,
( ~ c2_1(a1037)
| c3_1(a1037)
| ~ spl0_13
| ~ spl0_230 ),
inference(resolution,[],[f604,f1639]) ).
fof(f3038,plain,
( ~ c2_1(a1033)
| c3_1(a1033)
| ~ spl0_13
| ~ spl0_226 ),
inference(resolution,[],[f604,f1619]) ).
fof(f3044,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_12
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f3029]) ).
fof(f3048,plain,
( spl0_273
| ~ spl0_275
| ~ spl0_13
| ~ spl0_274 ),
inference(avatar_split_clause,[],[f3031,f1857,f603,f1862,f1852]) ).
fof(f3049,plain,
( spl0_18
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f3044,f603,f598,f622]) ).
fof(f3053,plain,
( spl0_229
| spl0_295
| ~ spl0_21
| ~ spl0_230 ),
inference(avatar_split_clause,[],[f2794,f1637,f635,f2082,f1632]) ).
fof(f3100,plain,
( ~ c1_1(a1102)
| ~ c2_1(a1102)
| ~ spl0_12
| spl0_144 ),
inference(resolution,[],[f599,f1213]) ).
fof(f3120,plain,
( ~ c1_1(a1070)
| c3_1(a1070)
| ~ spl0_18
| ~ spl0_260 ),
inference(resolution,[],[f623,f1789]) ).
fof(f3146,plain,
( ~ c1_1(a1036)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_103 ),
inference(resolution,[],[f2574,f1012]) ).
fof(f3148,plain,
( ~ c1_1(a1020)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_319 ),
inference(resolution,[],[f2574,f2413]) ).
fof(f3150,plain,
( ~ spl0_88
| ~ spl0_7
| ~ spl0_11
| ~ spl0_319 ),
inference(avatar_split_clause,[],[f3148,f2412,f595,f581,f935]) ).
fof(f3151,plain,
( ~ spl0_102
| ~ spl0_7
| ~ spl0_11
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f3146,f1010,f595,f581,f1005]) ).
fof(f3214,plain,
( ~ c2_1(a1028)
| c3_1(a1028)
| ~ spl0_13
| ~ spl0_218 ),
inference(resolution,[],[f1579,f604]) ).
fof(f3217,plain,
( ~ c2_1(a1042)
| c3_1(a1042)
| ~ spl0_13
| ~ spl0_235 ),
inference(resolution,[],[f1664,f604]) ).
fof(f3237,plain,
( ~ c1_1(a1070)
| ~ c3_1(a1070)
| ~ spl0_7
| ~ spl0_260 ),
inference(resolution,[],[f582,f1789]) ).
fof(f3241,plain,
( ~ c1_1(a1042)
| ~ c3_1(a1042)
| ~ spl0_7
| ~ spl0_234 ),
inference(resolution,[],[f582,f1659]) ).
fof(f3246,plain,
( ~ c1_1(a1021)
| ~ c3_1(a1021)
| ~ spl0_7
| ~ spl0_214 ),
inference(resolution,[],[f582,f1559]) ).
fof(f3274,plain,
( ~ c3_1(a1084)
| ~ c1_1(a1084)
| ~ spl0_11
| spl0_301 ),
inference(resolution,[],[f596,f2114]) ).
fof(f3292,plain,
( ~ c3_1(a1089)
| ~ c1_1(a1089)
| ~ spl0_11
| spl0_134 ),
inference(resolution,[],[f596,f1165]) ).
fof(f3344,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_16
| ~ spl0_21 ),
inference(resolution,[],[f636,f615]) ).
fof(f3355,plain,
( c2_1(a1051)
| c3_1(a1051)
| ~ spl0_21
| ~ spl0_244 ),
inference(resolution,[],[f636,f1709]) ).
fof(f3357,plain,
( c2_1(a1046)
| c3_1(a1046)
| ~ spl0_21
| ~ spl0_239 ),
inference(resolution,[],[f636,f1684]) ).
fof(f3361,plain,
( c2_1(a1033)
| c3_1(a1033)
| ~ spl0_21
| ~ spl0_226 ),
inference(resolution,[],[f636,f1619]) ).
fof(f3362,plain,
( c2_1(a1028)
| c3_1(a1028)
| ~ spl0_21
| ~ spl0_218 ),
inference(resolution,[],[f636,f1579]) ).
fof(f3363,plain,
( c2_1(a1089)
| c3_1(a1089)
| ~ spl0_21
| ~ spl0_209 ),
inference(resolution,[],[f636,f1534]) ).
fof(f3367,plain,
( c2_1(a1048)
| c3_1(a1048)
| ~ spl0_21
| ~ spl0_196 ),
inference(resolution,[],[f636,f1469]) ).
fof(f3370,plain,
( c2_1(a1035)
| c3_1(a1035)
| ~ spl0_21
| ~ spl0_189 ),
inference(resolution,[],[f636,f1434]) ).
fof(f3374,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| c1_1(X0) )
| ~ spl0_16
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f3344]) ).
fof(f3383,plain,
( spl0_327
| spl0_134
| ~ spl0_21
| ~ spl0_209 ),
inference(avatar_split_clause,[],[f3363,f1532,f635,f1163,f2452]) ).
fof(f3384,plain,
( spl0_217
| spl0_292
| ~ spl0_21
| ~ spl0_218 ),
inference(avatar_split_clause,[],[f3362,f1577,f635,f2067,f1572]) ).
fof(f3387,plain,
( spl0_331
| spl0_161
| ~ spl0_21
| ~ spl0_239 ),
inference(avatar_split_clause,[],[f3357,f1682,f635,f1294,f2472]) ).
fof(f3389,plain,
( spl0_333
| spl0_162
| ~ spl0_21
| ~ spl0_244 ),
inference(avatar_split_clause,[],[f3355,f1707,f635,f1299,f2482]) ).
fof(f3433,plain,
( ~ c1_1(a1078)
| ~ c3_1(a1078)
| ~ spl0_7
| ~ spl0_203 ),
inference(resolution,[],[f1504,f582]) ).
fof(f3460,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_9
| ~ spl0_21 ),
inference(resolution,[],[f589,f636]) ).
fof(f3473,plain,
( c2_1(a1034)
| c1_1(a1034)
| ~ spl0_9
| spl0_155 ),
inference(resolution,[],[f589,f1266]) ).
fof(f3478,plain,
( c2_1(a1079)
| c1_1(a1079)
| ~ spl0_9
| spl0_124 ),
inference(resolution,[],[f589,f1115]) ).
fof(f3493,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_9
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f3460]) ).
fof(f3523,plain,
( c2_1(a1089)
| ~ c1_1(a1089)
| ~ spl0_23
| ~ spl0_209 ),
inference(resolution,[],[f644,f1534]) ).
fof(f3546,plain,
( ~ c1_1(a1078)
| ~ c2_1(a1078)
| ~ spl0_27
| ~ spl0_202 ),
inference(resolution,[],[f662,f1499]) ).
fof(f3559,plain,
( c2_1(a1051)
| c1_1(a1051)
| ~ spl0_30
| ~ spl0_244 ),
inference(resolution,[],[f673,f1709]) ).
fof(f3588,plain,
( ~ c1_1(a1028)
| c3_1(a1028)
| ~ spl0_31
| ~ spl0_218 ),
inference(resolution,[],[f676,f1579]) ).
fof(f3639,plain,
( c3_1(a1105)
| c1_1(a1105)
| ~ spl0_37
| spl0_180 ),
inference(resolution,[],[f704,f1389]) ).
fof(f3651,plain,
( c3_1(a1022)
| c1_1(a1022)
| ~ spl0_37
| spl0_149 ),
inference(resolution,[],[f704,f1236]) ).
fof(f3653,plain,
( c3_1(a1088)
| c1_1(a1088)
| ~ spl0_37
| spl0_132 ),
inference(resolution,[],[f704,f1155]) ).
fof(f3678,plain,
( spl0_287
| spl0_286
| ~ spl0_37
| spl0_180 ),
inference(avatar_split_clause,[],[f3639,f1387,f703,f1916,f1921]) ).
fof(f3680,plain,
( ~ spl0_213
| ~ spl0_143
| ~ spl0_12
| spl0_144 ),
inference(avatar_split_clause,[],[f3100,f1211,f598,f1206,f1552]) ).
fof(f3682,plain,
( spl0_37
| ~ spl0_16
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f3374,f635,f614,f703]) ).
fof(f3683,plain,
( spl0_37
| ~ spl0_9
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f3493,f635,f588,f703]) ).
fof(f3711,plain,
( ~ c2_1(a1052)
| c3_1(a1052)
| ~ spl0_13
| ~ spl0_248 ),
inference(resolution,[],[f1729,f604]) ).
fof(f3712,plain,
( spl0_247
| ~ spl0_246
| ~ spl0_13
| ~ spl0_248 ),
inference(avatar_split_clause,[],[f3711,f1727,f603,f1717,f1722]) ).
fof(f3714,plain,
( spl0_228
| ~ spl0_294
| ~ spl0_6
| spl0_155 ),
inference(avatar_split_clause,[],[f2019,f1264,f578,f2077,f1627]) ).
fof(f3723,plain,
( ~ spl0_171
| ~ spl0_172
| ~ spl0_11
| spl0_301 ),
inference(avatar_split_clause,[],[f3274,f2112,f595,f1348,f1343]) ).
fof(f3731,plain,
( ~ spl0_333
| spl0_245
| ~ spl0_10
| spl0_162 ),
inference(avatar_split_clause,[],[f2741,f1299,f591,f1712,f2482]) ).
fof(f3735,plain,
( spl0_217
| ~ spl0_150
| ~ spl0_31
| ~ spl0_218 ),
inference(avatar_split_clause,[],[f3588,f1577,f675,f1239,f1572]) ).
fof(f3770,plain,
( ~ spl0_133
| spl0_134
| ~ spl0_23
| ~ spl0_209 ),
inference(avatar_split_clause,[],[f3523,f1532,f643,f1163,f1158]) ).
fof(f3775,plain,
( ~ spl0_137
| spl0_307
| ~ spl0_10
| spl0_135 ),
inference(avatar_split_clause,[],[f2398,f1168,f591,f2251,f1178]) ).
fof(f3795,plain,
( spl0_217
| ~ spl0_292
| ~ spl0_13
| ~ spl0_218 ),
inference(avatar_split_clause,[],[f3214,f1577,f603,f2067,f1572]) ).
fof(f3802,plain,
( spl0_251
| spl0_250
| ~ spl0_1
| ~ spl0_252 ),
inference(avatar_split_clause,[],[f2703,f1747,f561,f1737,f1742]) ).
fof(f3814,plain,
( ~ spl0_203
| ~ spl0_122
| ~ spl0_27
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f3546,f1497,f661,f1103,f1502]) ).
fof(f3834,plain,
( ~ spl0_307
| ~ spl0_137
| ~ spl0_11
| spl0_135 ),
inference(avatar_split_clause,[],[f2568,f1168,f595,f1178,f2251]) ).
fof(f3840,plain,
( ~ spl0_330
| ~ spl0_157
| ~ spl0_7
| ~ spl0_234 ),
inference(avatar_split_clause,[],[f3241,f1657,f581,f1274,f2467]) ).
fof(f3842,plain,
( ~ spl0_146
| ~ spl0_147
| ~ spl0_7
| ~ spl0_214 ),
inference(avatar_split_clause,[],[f3246,f1557,f581,f1225,f1220]) ).
fof(f3846,plain,
( ~ spl0_325
| ~ spl0_122
| ~ spl0_7
| ~ spl0_203 ),
inference(avatar_split_clause,[],[f3433,f1502,f581,f1103,f2442]) ).
fof(f3847,plain,
( spl0_11
| ~ spl0_8
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f2879,f643,f585,f595]) ).
fof(f3852,plain,
( spl0_225
| ~ spl0_293
| ~ spl0_14
| ~ spl0_226 ),
inference(avatar_split_clause,[],[f2863,f1617,f606,f2072,f1612]) ).
fof(f3855,plain,
( spl0_241
| ~ spl0_242
| ~ spl0_14
| ~ spl0_243 ),
inference(avatar_split_clause,[],[f2931,f1702,f606,f1697,f1692]) ).
fof(f3857,plain,
( spl0_322
| spl0_101
| ~ spl0_21
| ~ spl0_189 ),
inference(avatar_split_clause,[],[f3370,f1432,f635,f1000,f2427]) ).
fof(f3892,plain,
( ~ spl0_307
| spl0_135
| ~ spl0_5
| spl0_136 ),
inference(avatar_split_clause,[],[f2978,f1173,f575,f1168,f2251]) ).
fof(f3942,plain,
( ~ c1_1(a1084)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_172 ),
inference(resolution,[],[f2174,f1350]) ).
fof(f3963,plain,
( ~ c1_1(a1102)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_328 ),
inference(resolution,[],[f2174,f2458]) ).
fof(f3968,plain,
( ~ c1_1(a1078)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_325 ),
inference(resolution,[],[f2174,f2443]) ).
fof(f3991,plain,
( ~ spl0_171
| ~ spl0_2
| ~ spl0_8
| ~ spl0_172 ),
inference(avatar_split_clause,[],[f3942,f1348,f585,f564,f1343]) ).
fof(f3993,plain,
( ~ spl0_336
| ~ spl0_169
| ~ spl0_7
| ~ spl0_260 ),
inference(avatar_split_clause,[],[f3237,f1787,f581,f1333,f2497]) ).
fof(f3995,plain,
( spl0_336
| ~ spl0_169
| ~ spl0_18
| ~ spl0_260 ),
inference(avatar_split_clause,[],[f3120,f1787,f622,f1333,f2497]) ).
fof(f4104,plain,
( ~ c1_1(a1084)
| ~ c3_1(a1084)
| ~ spl0_7
| ~ spl0_301 ),
inference(resolution,[],[f582,f2113]) ).
fof(f4137,plain,
( ~ spl0_172
| ~ spl0_171
| ~ spl0_7
| ~ spl0_301 ),
inference(avatar_split_clause,[],[f4104,f2112,f581,f1343,f1348]) ).
fof(f4213,plain,
( ~ c2_1(a1078)
| c3_1(a1078)
| ~ spl0_13
| ~ spl0_202 ),
inference(resolution,[],[f604,f1499]) ).
fof(f4319,plain,
( ~ c1_1(a1102)
| c3_1(a1102)
| ~ spl0_18
| ~ spl0_213 ),
inference(resolution,[],[f623,f1554]) ).
fof(f4321,plain,
( ~ c1_1(a1083)
| c3_1(a1083)
| ~ spl0_18
| ~ spl0_206 ),
inference(resolution,[],[f623,f1519]) ).
fof(f4322,plain,
( ~ c1_1(a1059)
| c3_1(a1059)
| ~ spl0_18
| ~ spl0_197 ),
inference(resolution,[],[f623,f1474]) ).
fof(f4338,plain,
( ~ c1_1(a1084)
| ~ c2_1(a1084)
| ~ spl0_27
| ~ spl0_272 ),
inference(resolution,[],[f662,f1849]) ).
fof(f4385,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_12
| ~ spl0_28 ),
inference(resolution,[],[f665,f599]) ).
fof(f4407,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_12
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f4385]) ).
fof(f4420,plain,
( ~ c1_1(a1089)
| c3_1(a1089)
| ~ spl0_31
| ~ spl0_209 ),
inference(resolution,[],[f676,f1534]) ).
fof(f4458,plain,
( c2_1(a1101)
| c3_1(a1101)
| ~ spl0_38
| spl0_141 ),
inference(resolution,[],[f707,f1199]) ).
fof(f4460,plain,
( c2_1(a1079)
| c3_1(a1079)
| ~ spl0_38
| spl0_124 ),
inference(resolution,[],[f707,f1115]) ).
fof(f4461,plain,
( c2_1(a1077)
| c3_1(a1077)
| ~ spl0_38
| spl0_120 ),
inference(resolution,[],[f707,f1096]) ).
fof(f4486,plain,
( spl0_198
| ~ spl0_116
| ~ spl0_18
| ~ spl0_197 ),
inference(avatar_split_clause,[],[f4322,f1472,f622,f1075,f1477]) ).
fof(f4490,plain,
( ~ spl0_319
| ~ spl0_88
| ~ spl0_2
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f2581,f1392,f564,f935,f2412]) ).
fof(f4507,plain,
( ~ spl0_335
| spl0_256
| ~ spl0_10
| spl0_166 ),
inference(avatar_split_clause,[],[f2737,f1318,f591,f1767,f2492]) ).
fof(f4509,plain,
( ~ spl0_331
| spl0_240
| ~ spl0_10
| spl0_161 ),
inference(avatar_split_clause,[],[f2743,f1294,f591,f1687,f2472]) ).
fof(f4518,plain,
( ~ spl0_322
| spl0_188
| ~ spl0_10
| spl0_101 ),
inference(avatar_split_clause,[],[f2773,f1000,f591,f1427,f2427]) ).
fof(f4542,plain,
( ~ spl0_133
| ~ spl0_327
| ~ spl0_11
| spl0_134 ),
inference(avatar_split_clause,[],[f3292,f1163,f595,f2452,f1158]) ).
fof(f4550,plain,
( spl0_245
| spl0_162
| ~ spl0_30
| ~ spl0_244 ),
inference(avatar_split_clause,[],[f3559,f1707,f672,f1299,f1712]) ).
fof(f4562,plain,
( spl0_212
| spl0_291
| ~ spl0_38
| spl0_141 ),
inference(avatar_split_clause,[],[f4458,f1197,f706,f2062,f1547]) ).
fof(f4563,plain,
( spl0_326
| spl0_123
| ~ spl0_38
| spl0_124 ),
inference(avatar_split_clause,[],[f4460,f1113,f706,f1108,f2447]) ).
fof(f4564,plain,
( spl0_201
| spl0_119
| ~ spl0_38
| spl0_120 ),
inference(avatar_split_clause,[],[f4461,f1094,f706,f1089,f1492]) ).
fof(f4570,plain,
( spl0_229
| ~ spl0_295
| ~ spl0_13
| ~ spl0_230 ),
inference(avatar_split_clause,[],[f3037,f1637,f603,f2082,f1632]) ).
fof(f4577,plain,
( spl0_327
| ~ spl0_133
| ~ spl0_31
| ~ spl0_209 ),
inference(avatar_split_clause,[],[f4420,f1532,f675,f1158,f2452]) ).
fof(f4605,plain,
( spl0_205
| ~ spl0_131
| ~ spl0_18
| ~ spl0_206 ),
inference(avatar_split_clause,[],[f4321,f1517,f622,f1148,f1512]) ).
fof(f4608,plain,
( ~ spl0_143
| ~ spl0_2
| ~ spl0_8
| ~ spl0_328 ),
inference(avatar_split_clause,[],[f3963,f2457,f585,f564,f1206]) ).
fof(f4610,plain,
( ~ spl0_122
| ~ spl0_2
| ~ spl0_8
| ~ spl0_325 ),
inference(avatar_split_clause,[],[f3968,f2442,f585,f564,f1103]) ).
fof(f4613,plain,
( ~ spl0_125
| spl0_126
| ~ spl0_5
| spl0_127 ),
inference(avatar_split_clause,[],[f2980,f1128,f575,f1123,f1118]) ).
fof(f4616,plain,
( spl0_227
| spl0_294
| ~ spl0_9
| spl0_155 ),
inference(avatar_split_clause,[],[f3473,f1264,f588,f2077,f1622]) ).
fof(f4625,plain,
( spl0_215
| spl0_216
| ~ spl0_37
| spl0_149 ),
inference(avatar_split_clause,[],[f3651,f1234,f703,f1567,f1562]) ).
fof(f4629,plain,
( spl0_330
| ~ spl0_234
| ~ spl0_13
| ~ spl0_235 ),
inference(avatar_split_clause,[],[f3217,f1662,f603,f1657,f2467]) ).
fof(f4630,plain,
( spl0_328
| ~ spl0_143
| ~ spl0_18
| ~ spl0_213 ),
inference(avatar_split_clause,[],[f4319,f1552,f622,f1206,f2457]) ).
fof(f4658,plain,
( ~ c1_1(a1042)
| c3_1(a1042)
| ~ spl0_18
| ~ spl0_234 ),
inference(resolution,[],[f1659,f623]) ).
fof(f4684,plain,
( ~ c1_1(a1042)
| ~ c3_1(a1042)
| ~ spl0_2
| ~ spl0_235 ),
inference(resolution,[],[f565,f1664]) ).
fof(f4693,plain,
( ~ c1_1(a1036)
| ~ c3_1(a1036)
| ~ spl0_2
| ~ spl0_190 ),
inference(resolution,[],[f565,f1439]) ).
fof(f4726,plain,
( spl0_319
| spl0_87
| ~ spl0_21
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f2797,f1392,f635,f930,f2412]) ).
fof(f4730,plain,
( spl0_224
| spl0_293
| ~ spl0_21
| ~ spl0_226 ),
inference(avatar_split_clause,[],[f3361,f1617,f635,f2072,f1607]) ).
fof(f4732,plain,
( spl0_195
| spl0_112
| ~ spl0_21
| ~ spl0_196 ),
inference(avatar_split_clause,[],[f3367,f1467,f635,f1055,f1462]) ).
fof(f4741,plain,
( spl0_208
| spl0_207
| ~ spl0_37
| spl0_132 ),
inference(avatar_split_clause,[],[f3653,f1153,f703,f1522,f1527]) ).
fof(f4744,plain,
( spl0_325
| ~ spl0_203
| ~ spl0_13
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f4213,f1497,f603,f1502,f2442]) ).
fof(f4760,plain,
( spl0_224
| ~ spl0_293
| ~ spl0_13
| ~ spl0_226 ),
inference(avatar_split_clause,[],[f3038,f1617,f603,f2072,f1607]) ).
fof(f4766,plain,
( spl0_233
| spl0_232
| ~ spl0_1
| ~ spl0_231 ),
inference(avatar_split_clause,[],[f2985,f1642,f561,f1647,f1652]) ).
fof(f4772,plain,
( ~ spl0_330
| ~ spl0_157
| ~ spl0_2
| ~ spl0_235 ),
inference(avatar_split_clause,[],[f4684,f1662,f564,f1274,f2467]) ).
fof(f4773,plain,
( ~ spl0_103
| ~ spl0_102
| ~ spl0_2
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f4693,f1437,f564,f1005,f1010]) ).
fof(f4780,plain,
( spl0_212
| ~ spl0_291
| ~ spl0_6
| spl0_141 ),
inference(avatar_split_clause,[],[f2024,f1197,f578,f2062,f1547]) ).
fof(f4790,plain,
( spl0_256
| spl0_166
| ~ spl0_9
| spl0_167 ),
inference(avatar_split_clause,[],[f2195,f1323,f588,f1318,f1767]) ).
fof(f4797,plain,
( spl0_204
| spl0_123
| ~ spl0_9
| spl0_124 ),
inference(avatar_split_clause,[],[f3478,f1113,f588,f1108,f1507]) ).
fof(f4813,plain,
( ~ spl0_326
| spl0_204
| ~ spl0_10
| spl0_123 ),
inference(avatar_split_clause,[],[f2762,f1108,f591,f1507,f2447]) ).
fof(f4836,plain,
( spl0_7
| ~ spl0_12
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f4407,f664,f598,f581]) ).
fof(f4837,plain,
( spl0_330
| ~ spl0_157
| ~ spl0_18
| ~ spl0_234 ),
inference(avatar_split_clause,[],[f4658,f1657,f622,f1274,f2467]) ).
fof(f4857,plain,
( ~ spl0_301
| ~ spl0_171
| ~ spl0_27
| ~ spl0_272 ),
inference(avatar_split_clause,[],[f4338,f1847,f661,f1343,f2112]) ).
fof(f4945,plain,
( c3_1(a1103)
| ~ spl0_6
| ~ spl0_13
| ~ spl0_285 ),
inference(resolution,[],[f2591,f1913]) ).
fof(f4993,plain,
( spl0_284
| ~ spl0_6
| ~ spl0_13
| ~ spl0_285 ),
inference(avatar_split_clause,[],[f4945,f1911,f603,f578,f1906]) ).
cnf(s2,plain,
( spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f583]) ).
cnf(s3,plain,
( spl0_3
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f593]) ).
cnf(s4,plain,
( spl0_2
| spl0_3
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f600]) ).
cnf(s5,plain,
( spl0_3
| spl0_7
| spl0_8
| spl0_12 ),
inference(sat_conversion,[],[f601]) ).
cnf(s6,plain,
( spl0_3
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f608]) ).
cnf(s7,plain,
( spl0_1
| spl0_3
| ~ spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f616]) ).
cnf(s8,plain,
( spl0_3
| spl0_13
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f624]) ).
cnf(s9,plain,
( spl0_3
| spl0_6
| spl0_13
| ~ spl0_19 ),
inference(sat_conversion,[],[f629]) ).
cnf(s11,plain,
( spl0_3
| spl0_13
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f645]) ).
cnf(s12,plain,
( spl0_1
| spl0_3
| spl0_9
| spl0_24 ),
inference(sat_conversion,[],[f650]) ).
cnf(s13,plain,
( spl0_3
| spl0_18
| spl0_21
| ~ spl0_25 ),
inference(sat_conversion,[],[f655]) ).
cnf(s14,plain,
( spl0_3
| ~ spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f666]) ).
cnf(s16,plain,
( spl0_3
| spl0_21
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f682]) ).
cnf(s17,plain,
( spl0_1
| spl0_3
| spl0_9
| spl0_33 ),
inference(sat_conversion,[],[f687]) ).
cnf(s19,plain,
( spl0_3
| spl0_6
| spl0_10
| ~ spl0_35 ),
inference(sat_conversion,[],[f697]) ).
cnf(s22,plain,
( spl0_3
| spl0_12
| spl0_37
| ~ spl0_41 ),
inference(sat_conversion,[],[f721]) ).
cnf(s23,plain,
( spl0_3
| spl0_7
| spl0_30
| spl0_42 ),
inference(sat_conversion,[],[f726]) ).
cnf(s26,plain,
( spl0_3
| spl0_8
| spl0_16
| spl0_47 ),
inference(sat_conversion,[],[f747]) ).
cnf(s27,plain,
( spl0_3
| spl0_8
| spl0_21
| spl0_48 ),
inference(sat_conversion,[],[f752]) ).
cnf(s33,plain,
( spl0_3
| spl0_13
| spl0_33
| ~ spl0_53 ),
inference(sat_conversion,[],[f777]) ).
cnf(s36,plain,
( spl0_3
| spl0_37
| ~ spl0_57
| ~ spl0_58 ),
inference(sat_conversion,[],[f800]) ).
cnf(s41,plain,
( spl0_3
| spl0_28
| spl0_63
| spl0_65 ),
inference(sat_conversion,[],[f831]) ).
cnf(s43,plain,
( spl0_3
| spl0_16
| spl0_68
| spl0_69 ),
inference(sat_conversion,[],[f849]) ).
cnf(s48,plain,
( spl0_2
| spl0_3
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f890]) ).
cnf(s51,plain,
( spl0_3
| spl0_33
| spl0_38
| ~ spl0_82 ),
inference(sat_conversion,[],[f908]) ).
cnf(s54,plain,
( spl0_3
| spl0_11
| spl0_84
| ~ spl0_85 ),
inference(sat_conversion,[],[f923]) ).
cnf(s56,plain,
( ~ spl0_86
| ~ spl0_87 ),
inference(sat_conversion,[],[f933]) ).
cnf(s57,plain,
( ~ spl0_86
| spl0_88 ),
inference(sat_conversion,[],[f938]) ).
cnf(s70,plain,
( spl0_19
| ~ spl0_101 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s71,plain,
( ~ spl0_69
| spl0_102 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s72,plain,
( ~ spl0_69
| spl0_103 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s81,plain,
( ~ spl0_65
| ~ spl0_112 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s85,plain,
( spl0_82
| spl0_116 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s87,plain,
( ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s88,plain,
( ~ spl0_118
| ~ spl0_120 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s89,plain,
( spl0_121
| spl0_122 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s90,plain,
( ~ spl0_78
| ~ spl0_123 ),
inference(sat_conversion,[],[f1111]) ).
cnf(s91,plain,
( ~ spl0_78
| ~ spl0_124 ),
inference(sat_conversion,[],[f1116]) ).
cnf(s92,plain,
( ~ spl0_77
| spl0_125 ),
inference(sat_conversion,[],[f1121]) ).
cnf(s93,plain,
( ~ spl0_77
| ~ spl0_126 ),
inference(sat_conversion,[],[f1126]) ).
cnf(s94,plain,
( ~ spl0_77
| ~ spl0_127 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s98,plain,
( spl0_58
| spl0_131 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s99,plain,
( spl0_53
| ~ spl0_132 ),
inference(sat_conversion,[],[f1156]) ).
cnf(s100,plain,
( ~ spl0_47
| spl0_133 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s101,plain,
( ~ spl0_47
| ~ spl0_134 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s102,plain,
( ~ spl0_24
| ~ spl0_135 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s103,plain,
( ~ spl0_24
| ~ spl0_136 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s104,plain,
( ~ spl0_24
| spl0_137 ),
inference(sat_conversion,[],[f1181]) ).
cnf(s107,plain,
( ~ spl0_140
| ~ spl0_141 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s108,plain,
( ~ spl0_142
| spl0_143 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s109,plain,
( ~ spl0_142
| ~ spl0_144 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s110,plain,
( spl0_145
| spl0_146 ),
inference(sat_conversion,[],[f1223]) ).
cnf(s111,plain,
( spl0_145
| spl0_147 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s112,plain,
( spl0_148
| ~ spl0_149 ),
inference(sat_conversion,[],[f1237]) ).
cnf(s113,plain,
( ~ spl0_42
| spl0_150 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s115,plain,
( ~ spl0_33
| spl0_152 ),
inference(sat_conversion,[],[f1252]) ).
cnf(s118,plain,
( spl0_15
| ~ spl0_155 ),
inference(sat_conversion,[],[f1267]) ).
cnf(s120,plain,
( ~ spl0_55
| spl0_157 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s124,plain,
( spl0_41
| ~ spl0_161 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s125,plain,
( spl0_85
| ~ spl0_162 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s128,plain,
( ~ spl0_48
| ~ spl0_166 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s129,plain,
( ~ spl0_48
| ~ spl0_167 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s131,plain,
( ~ spl0_22
| spl0_169 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s133,plain,
( spl0_57
| spl0_171 ),
inference(sat_conversion,[],[f1346]) ).
cnf(s134,plain,
( spl0_57
| spl0_172 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s141,plain,
( ~ spl0_179
| ~ spl0_180 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s142,plain,
( ~ spl0_86
| spl0_181 ),
inference(sat_conversion,[],[f1395]) ).
cnf(s149,plain,
( spl0_19
| ~ spl0_188 ),
inference(sat_conversion,[],[f1430]) ).
cnf(s150,plain,
( spl0_19
| spl0_189 ),
inference(sat_conversion,[],[f1435]) ).
cnf(s151,plain,
( ~ spl0_69
| spl0_190 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s156,plain,
( ~ spl0_65
| ~ spl0_195 ),
inference(sat_conversion,[],[f1465]) ).
cnf(s157,plain,
( ~ spl0_65
| spl0_196 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s158,plain,
( spl0_82
| spl0_197 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s159,plain,
( spl0_82
| ~ spl0_198 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s162,plain,
( ~ spl0_118
| ~ spl0_201 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s163,plain,
( spl0_121
| spl0_202 ),
inference(sat_conversion,[],[f1500]) ).
cnf(s164,plain,
( spl0_121
| spl0_203 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s165,plain,
( ~ spl0_78
| ~ spl0_204 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s166,plain,
( spl0_58
| ~ spl0_205 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s167,plain,
( spl0_58
| spl0_206 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s168,plain,
( spl0_53
| ~ spl0_207 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s169,plain,
( spl0_53
| ~ spl0_208 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s170,plain,
( ~ spl0_47
| spl0_209 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s173,plain,
( ~ spl0_140
| ~ spl0_212 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s174,plain,
( ~ spl0_142
| spl0_213 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s175,plain,
( spl0_145
| spl0_214 ),
inference(sat_conversion,[],[f1560]) ).
cnf(s176,plain,
( spl0_148
| ~ spl0_215 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s177,plain,
( spl0_148
| ~ spl0_216 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s178,plain,
( ~ spl0_42
| ~ spl0_217 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s179,plain,
( ~ spl0_42
| spl0_218 ),
inference(sat_conversion,[],[f1580]) ).
cnf(s182,plain,
( ~ spl0_33
| spl0_221 ),
inference(sat_conversion,[],[f1595]) ).
cnf(s183,plain,
( ~ spl0_33
| ~ spl0_222 ),
inference(sat_conversion,[],[f1600]) ).
cnf(s185,plain,
( spl0_35
| ~ spl0_224 ),
inference(sat_conversion,[],[f1610]) ).
cnf(s186,plain,
( spl0_35
| ~ spl0_225 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s187,plain,
( spl0_35
| spl0_226 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s188,plain,
( spl0_15
| ~ spl0_227 ),
inference(sat_conversion,[],[f1625]) ).
cnf(s189,plain,
( spl0_15
| ~ spl0_228 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s190,plain,
( ~ spl0_68
| ~ spl0_229 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s191,plain,
( ~ spl0_68
| spl0_230 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s192,plain,
( ~ spl0_32
| spl0_231 ),
inference(sat_conversion,[],[f1645]) ).
cnf(s193,plain,
( ~ spl0_32
| ~ spl0_232 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s194,plain,
( ~ spl0_32
| ~ spl0_233 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s195,plain,
( ~ spl0_55
| spl0_234 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s196,plain,
( ~ spl0_55
| spl0_235 ),
inference(sat_conversion,[],[f1665]) ).
cnf(s200,plain,
( spl0_41
| spl0_239 ),
inference(sat_conversion,[],[f1685]) ).
cnf(s201,plain,
( spl0_41
| ~ spl0_240 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s202,plain,
( ~ spl0_63
| ~ spl0_241 ),
inference(sat_conversion,[],[f1695]) ).
cnf(s203,plain,
( ~ spl0_63
| spl0_242 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s204,plain,
( ~ spl0_63
| spl0_243 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s205,plain,
( spl0_85
| spl0_244 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s206,plain,
( spl0_85
| ~ spl0_245 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s207,plain,
( ~ spl0_84
| spl0_246 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s208,plain,
( ~ spl0_84
| ~ spl0_247 ),
inference(sat_conversion,[],[f1725]) ).
cnf(s209,plain,
( ~ spl0_84
| spl0_248 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s211,plain,
( spl0_26
| ~ spl0_250 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s212,plain,
( spl0_26
| ~ spl0_251 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s213,plain,
( spl0_26
| spl0_252 ),
inference(sat_conversion,[],[f1750]) ).
cnf(s217,plain,
( ~ spl0_48
| ~ spl0_256 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s221,plain,
( ~ spl0_22
| spl0_260 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s225,plain,
( ~ spl0_17
| spl0_264 ),
inference(sat_conversion,[],[f1810]) ).
cnf(s226,plain,
( ~ spl0_17
| spl0_265 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s227,plain,
( ~ spl0_17
| ~ spl0_266 ),
inference(sat_conversion,[],[f1820]) ).
cnf(s233,plain,
( spl0_57
| spl0_272 ),
inference(sat_conversion,[],[f1850]) ).
cnf(s234,plain,
( spl0_25
| ~ spl0_273 ),
inference(sat_conversion,[],[f1855]) ).
cnf(s235,plain,
( spl0_25
| spl0_274 ),
inference(sat_conversion,[],[f1860]) ).
cnf(s236,plain,
( spl0_25
| spl0_275 ),
inference(sat_conversion,[],[f1865]) ).
cnf(s244,plain,
( ~ spl0_283
| ~ spl0_284 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s245,plain,
( ~ spl0_283
| spl0_285 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s246,plain,
( ~ spl0_179
| ~ spl0_286 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s247,plain,
( ~ spl0_179
| ~ spl0_287 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s248,plain,
( ~ spl0_57
| spl0_179
| spl0_283 ),
inference(sat_conversion,[],[f1925]) ).
cnf(s249,plain,
( spl0_63
| spl0_140
| spl0_142 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s250,plain,
( spl0_55
| spl0_118
| ~ spl0_121 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s252,plain,
( spl0_86
| ~ spl0_145
| ~ spl0_148 ),
inference(sat_conversion,[],[f1929]) ).
cnf(s309,plain,
( ~ spl0_3
| spl0_57 ),
inference(sat_conversion,[],[f1986]) ).
cnf(s315,plain,
( ~ spl0_3
| ~ spl0_283 ),
inference(sat_conversion,[],[f1992]) ).
cnf(s316,plain,
( ~ spl0_3
| ~ spl0_179 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s405,plain,
( spl0_1
| ~ spl0_6
| ~ spl0_14 ),
inference(sat_conversion,[],[f2580]) ).
cnf(s407,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_221
| spl0_222 ),
inference(sat_conversion,[],[f2596]) ).
cnf(s440,plain,
( ~ spl0_16
| spl0_167
| spl0_256
| spl0_335 ),
inference(sat_conversion,[],[f2681]) ).
cnf(s453,plain,
( spl0_1
| ~ spl0_13
| ~ spl0_16 ),
inference(sat_conversion,[],[f2694]) ).
cnf(s466,plain,
( ~ spl0_18
| ~ spl0_152
| ~ spl0_221
| spl0_222 ),
inference(sat_conversion,[],[f2802]) ).
cnf(s475,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_27 ),
inference(sat_conversion,[],[f2900]) ).
cnf(s476,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_28 ),
inference(sat_conversion,[],[f2913]) ).
cnf(s481,plain,
( ~ spl0_14
| ~ spl0_264
| ~ spl0_265
| spl0_266 ),
inference(sat_conversion,[],[f2938]) ).
cnf(s488,plain,
( ~ spl0_13
| spl0_273
| ~ spl0_274
| ~ spl0_275 ),
inference(sat_conversion,[],[f3048]) ).
cnf(s489,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18 ),
inference(sat_conversion,[],[f3049]) ).
cnf(s493,plain,
( ~ spl0_21
| spl0_229
| ~ spl0_230
| spl0_295 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s513,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_88
| ~ spl0_319 ),
inference(sat_conversion,[],[f3150]) ).
cnf(s514,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_102
| ~ spl0_103 ),
inference(sat_conversion,[],[f3151]) ).
cnf(s583,plain,
( ~ spl0_21
| spl0_134
| ~ spl0_209
| spl0_327 ),
inference(sat_conversion,[],[f3383]) ).
cnf(s584,plain,
( ~ spl0_21
| spl0_217
| ~ spl0_218
| spl0_292 ),
inference(sat_conversion,[],[f3384]) ).
cnf(s587,plain,
( ~ spl0_21
| spl0_161
| ~ spl0_239
| spl0_331 ),
inference(sat_conversion,[],[f3387]) ).
cnf(s589,plain,
( ~ spl0_21
| spl0_162
| ~ spl0_244
| spl0_333 ),
inference(sat_conversion,[],[f3389]) ).
cnf(s640,plain,
( ~ spl0_37
| spl0_180
| spl0_286
| spl0_287 ),
inference(sat_conversion,[],[f3678]) ).
cnf(s644,plain,
( ~ spl0_12
| ~ spl0_143
| spl0_144
| ~ spl0_213 ),
inference(sat_conversion,[],[f3680]) ).
cnf(s646,plain,
( ~ spl0_16
| ~ spl0_21
| spl0_37 ),
inference(sat_conversion,[],[f3682]) ).
cnf(s647,plain,
( ~ spl0_9
| ~ spl0_21
| spl0_37 ),
inference(sat_conversion,[],[f3683]) ).
cnf(s657,plain,
( ~ spl0_13
| ~ spl0_246
| spl0_247
| ~ spl0_248 ),
inference(sat_conversion,[],[f3712]) ).
cnf(s659,plain,
( ~ spl0_6
| spl0_155
| spl0_228
| ~ spl0_294 ),
inference(sat_conversion,[],[f3714]) ).
cnf(s668,plain,
( ~ spl0_11
| ~ spl0_171
| ~ spl0_172
| spl0_301 ),
inference(sat_conversion,[],[f3723]) ).
cnf(s676,plain,
( ~ spl0_10
| spl0_162
| spl0_245
| ~ spl0_333 ),
inference(sat_conversion,[],[f3731]) ).
cnf(s680,plain,
( ~ spl0_31
| ~ spl0_150
| spl0_217
| ~ spl0_218 ),
inference(sat_conversion,[],[f3735]) ).
cnf(s717,plain,
( ~ spl0_23
| ~ spl0_133
| spl0_134
| ~ spl0_209 ),
inference(sat_conversion,[],[f3770]) ).
cnf(s722,plain,
( ~ spl0_10
| spl0_135
| ~ spl0_137
| spl0_307 ),
inference(sat_conversion,[],[f3775]) ).
cnf(s742,plain,
( ~ spl0_13
| spl0_217
| ~ spl0_218
| ~ spl0_292 ),
inference(sat_conversion,[],[f3795]) ).
cnf(s748,plain,
( ~ spl0_1
| spl0_250
| spl0_251
| ~ spl0_252 ),
inference(sat_conversion,[],[f3802]) ).
cnf(s760,plain,
( ~ spl0_27
| ~ spl0_122
| ~ spl0_202
| ~ spl0_203 ),
inference(sat_conversion,[],[f3814]) ).
cnf(s780,plain,
( ~ spl0_11
| spl0_135
| ~ spl0_137
| ~ spl0_307 ),
inference(sat_conversion,[],[f3834]) ).
cnf(s786,plain,
( ~ spl0_7
| ~ spl0_157
| ~ spl0_234
| ~ spl0_330 ),
inference(sat_conversion,[],[f3840]) ).
cnf(s788,plain,
( ~ spl0_7
| ~ spl0_146
| ~ spl0_147
| ~ spl0_214 ),
inference(sat_conversion,[],[f3842]) ).
cnf(s792,plain,
( ~ spl0_7
| ~ spl0_122
| ~ spl0_203
| ~ spl0_325 ),
inference(sat_conversion,[],[f3846]) ).
cnf(s793,plain,
( ~ spl0_8
| spl0_11
| ~ spl0_23 ),
inference(sat_conversion,[],[f3847]) ).
cnf(s798,plain,
( ~ spl0_14
| spl0_225
| ~ spl0_226
| ~ spl0_293 ),
inference(sat_conversion,[],[f3852]) ).
cnf(s801,plain,
( ~ spl0_14
| spl0_241
| ~ spl0_242
| ~ spl0_243 ),
inference(sat_conversion,[],[f3855]) ).
cnf(s803,plain,
( ~ spl0_21
| spl0_101
| ~ spl0_189
| spl0_322 ),
inference(sat_conversion,[],[f3857]) ).
cnf(s831,plain,
( ~ spl0_5
| spl0_135
| spl0_136
| ~ spl0_307 ),
inference(sat_conversion,[],[f3892]) ).
cnf(s839,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_171
| ~ spl0_172 ),
inference(sat_conversion,[],[f3991]) ).
cnf(s841,plain,
( ~ spl0_7
| ~ spl0_169
| ~ spl0_260
| ~ spl0_336 ),
inference(sat_conversion,[],[f3993]) ).
cnf(s843,plain,
( ~ spl0_18
| ~ spl0_169
| ~ spl0_260
| spl0_336 ),
inference(sat_conversion,[],[f3995]) ).
cnf(s852,plain,
( ~ spl0_7
| ~ spl0_171
| ~ spl0_172
| ~ spl0_301 ),
inference(sat_conversion,[],[f4137]) ).
cnf(s891,plain,
( ~ spl0_18
| ~ spl0_116
| ~ spl0_197
| spl0_198 ),
inference(sat_conversion,[],[f4486]) ).
cnf(s895,plain,
( ~ spl0_2
| ~ spl0_88
| ~ spl0_181
| ~ spl0_319 ),
inference(sat_conversion,[],[f4490]) ).
cnf(s912,plain,
( ~ spl0_10
| spl0_166
| spl0_256
| ~ spl0_335 ),
inference(sat_conversion,[],[f4507]) ).
cnf(s914,plain,
( ~ spl0_10
| spl0_161
| spl0_240
| ~ spl0_331 ),
inference(sat_conversion,[],[f4509]) ).
cnf(s923,plain,
( ~ spl0_10
| spl0_101
| spl0_188
| ~ spl0_322 ),
inference(sat_conversion,[],[f4518]) ).
cnf(s947,plain,
( ~ spl0_11
| ~ spl0_133
| spl0_134
| ~ spl0_327 ),
inference(sat_conversion,[],[f4542]) ).
cnf(s955,plain,
( ~ spl0_30
| spl0_162
| ~ spl0_244
| spl0_245 ),
inference(sat_conversion,[],[f4550]) ).
cnf(s967,plain,
( ~ spl0_38
| spl0_141
| spl0_212
| spl0_291 ),
inference(sat_conversion,[],[f4562]) ).
cnf(s968,plain,
( ~ spl0_38
| spl0_123
| spl0_124
| spl0_326 ),
inference(sat_conversion,[],[f4563]) ).
cnf(s969,plain,
( ~ spl0_38
| spl0_119
| spl0_120
| spl0_201 ),
inference(sat_conversion,[],[f4564]) ).
cnf(s975,plain,
( ~ spl0_13
| spl0_229
| ~ spl0_230
| ~ spl0_295 ),
inference(sat_conversion,[],[f4570]) ).
cnf(s982,plain,
( ~ spl0_31
| ~ spl0_133
| ~ spl0_209
| spl0_327 ),
inference(sat_conversion,[],[f4577]) ).
cnf(s1011,plain,
( ~ spl0_18
| ~ spl0_131
| spl0_205
| ~ spl0_206 ),
inference(sat_conversion,[],[f4605]) ).
cnf(s1015,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_143
| ~ spl0_328 ),
inference(sat_conversion,[],[f4608]) ).
cnf(s1017,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_122
| ~ spl0_325 ),
inference(sat_conversion,[],[f4610]) ).
cnf(s1020,plain,
( ~ spl0_5
| ~ spl0_125
| spl0_126
| spl0_127 ),
inference(sat_conversion,[],[f4613]) ).
cnf(s1023,plain,
( ~ spl0_9
| spl0_155
| spl0_227
| spl0_294 ),
inference(sat_conversion,[],[f4616]) ).
cnf(s1032,plain,
( ~ spl0_37
| spl0_149
| spl0_215
| spl0_216 ),
inference(sat_conversion,[],[f4625]) ).
cnf(s1036,plain,
( ~ spl0_13
| ~ spl0_234
| ~ spl0_235
| spl0_330 ),
inference(sat_conversion,[],[f4629]) ).
cnf(s1037,plain,
( ~ spl0_18
| ~ spl0_143
| ~ spl0_213
| spl0_328 ),
inference(sat_conversion,[],[f4630]) ).
cnf(s1051,plain,
( ~ spl0_21
| spl0_87
| ~ spl0_181
| spl0_319 ),
inference(sat_conversion,[],[f4726]) ).
cnf(s1055,plain,
( ~ spl0_21
| spl0_224
| ~ spl0_226
| spl0_293 ),
inference(sat_conversion,[],[f4730]) ).
cnf(s1057,plain,
( ~ spl0_21
| spl0_112
| spl0_195
| ~ spl0_196 ),
inference(sat_conversion,[],[f4732]) ).
cnf(s1066,plain,
( ~ spl0_37
| spl0_132
| spl0_207
| spl0_208 ),
inference(sat_conversion,[],[f4741]) ).
cnf(s1069,plain,
( ~ spl0_13
| ~ spl0_202
| ~ spl0_203
| spl0_325 ),
inference(sat_conversion,[],[f4744]) ).
cnf(s1085,plain,
( ~ spl0_13
| spl0_224
| ~ spl0_226
| ~ spl0_293 ),
inference(sat_conversion,[],[f4760]) ).
cnf(s1090,plain,
( ~ spl0_1
| ~ spl0_231
| spl0_232
| spl0_233 ),
inference(sat_conversion,[],[f4766]) ).
cnf(s1096,plain,
( ~ spl0_2
| ~ spl0_157
| ~ spl0_235
| ~ spl0_330 ),
inference(sat_conversion,[],[f4772]) ).
cnf(s1097,plain,
( ~ spl0_2
| ~ spl0_102
| ~ spl0_103
| ~ spl0_190 ),
inference(sat_conversion,[],[f4773]) ).
cnf(s1104,plain,
( ~ spl0_6
| spl0_141
| spl0_212
| ~ spl0_291 ),
inference(sat_conversion,[],[f4780]) ).
cnf(s1115,plain,
( ~ spl0_9
| spl0_166
| spl0_167
| spl0_256 ),
inference(sat_conversion,[],[f4790]) ).
cnf(s1122,plain,
( ~ spl0_9
| spl0_123
| spl0_124
| spl0_204 ),
inference(sat_conversion,[],[f4797]) ).
cnf(s1139,plain,
( ~ spl0_10
| spl0_123
| spl0_204
| ~ spl0_326 ),
inference(sat_conversion,[],[f4813]) ).
cnf(s1162,plain,
( spl0_7
| ~ spl0_12
| ~ spl0_28 ),
inference(sat_conversion,[],[f4836]) ).
cnf(s1163,plain,
( ~ spl0_18
| ~ spl0_157
| ~ spl0_234
| spl0_330 ),
inference(sat_conversion,[],[f4837]) ).
cnf(s1183,plain,
( ~ spl0_27
| ~ spl0_171
| ~ spl0_272
| ~ spl0_301 ),
inference(sat_conversion,[],[f4857]) ).
cnf(s1189,plain,
( ~ spl0_6
| ~ spl0_13
| spl0_284
| ~ spl0_285 ),
inference(sat_conversion,[],[f4993]) ).
cnf(s1191,plain,
( spl0_13
| spl0_18
| spl0_3 ),
inference(rat,[],[s481,s225,s226,s227,s6,s8]) ).
cnf(s1192,plain,
( spl0_9
| spl0_8
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s1191,s489,s4,s780,s722,s466,s102,s104,s115,s182,s183,s3,s12,s17]) ).
cnf(s1193,plain,
( ~ spl0_48
| ~ spl0_9 ),
inference(rat,[],[s1115,s128,s129,s217]) ).
cnf(s1194,plain,
( spl0_13
| ~ spl0_21
| spl0_6
| spl0_3 ),
inference(rat,[],[s1055,s798,s185,s186,s187,s19,s923,s803,s70,s149,s150,s9,s6]) ).
cnf(s1197,plain,
( ~ spl0_33
| ~ spl0_18 ),
inference(rat,[],[s466,s115,s182,s183]) ).
cnf(s1200,plain,
( spl0_25
| ~ spl0_13 ),
inference(rat,[],[s488,s234,s235,s236]) ).
cnf(s1202,plain,
( spl0_82
| ~ spl0_18 ),
inference(rat,[],[s891,s85,s158,s159]) ).
cnf(s1204,plain,
( spl0_41
| ~ spl0_10
| ~ spl0_21 ),
inference(rat,[],[s587,s914,s124,s200,s201]) ).
cnf(s1205,plain,
( spl0_53
| ~ spl0_37 ),
inference(rat,[],[s1066,s99,s168,s169]) ).
cnf(s1206,plain,
( spl0_58
| ~ spl0_18 ),
inference(rat,[],[s1011,s98,s166,s167]) ).
cnf(s1207,plain,
( ~ spl0_65
| ~ spl0_21 ),
inference(rat,[],[s1057,s81,s156,s157]) ).
cnf(s1208,plain,
( ~ spl0_63
| ~ spl0_14 ),
inference(rat,[],[s801,s202,s203,s204]) ).
cnf(s1215,plain,
( ~ spl0_78
| ~ spl0_9 ),
inference(rat,[],[s1122,s90,s91,s165]) ).
cnf(s1218,plain,
( spl0_85
| ~ spl0_10
| ~ spl0_21 ),
inference(rat,[],[s589,s676,s125,s205,s206]) ).
cnf(s1219,plain,
( ~ spl0_84
| ~ spl0_13 ),
inference(rat,[],[s657,s207,s208,s209]) ).
cnf(s1220,plain,
( spl0_8
| spl0_6
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s1055,s1085,s185,s187,s19,s1218,s54,s1219,s947,s583,s100,s101,s170,s26,s453,s1194,s27,s1193,s1192]) ).
cnf(s1235,plain,
( ~ spl0_172
| ~ spl0_171
| ~ spl0_11
| ~ spl0_7 ),
inference(rat,[],[s668,s852]) ).
cnf(s1237,plain,
( ~ spl0_55
| ~ spl0_13
| ~ spl0_7 ),
inference(rat,[],[s786,s1036,s120,s195,s196]) ).
cnf(s1240,plain,
( ~ spl0_68
| ~ spl0_13
| ~ spl0_21 ),
inference(rat,[],[s493,s975,s190,s191]) ).
cnf(s1241,plain,
( ~ spl0_21
| ~ spl0_7
| spl0_6
| spl0_3
| spl0_1 ),
inference(rat,[],[s1055,s1085,s185,s187,s19,s1218,s54,s514,s71,s72,s43,s1240,s1219,s453,s1194]) ).
cnf(s1244,plain,
( ~ spl0_118
| ~ spl0_38 ),
inference(rat,[],[s969,s87,s88,s162]) ).
cnf(s1245,plain,
( ~ spl0_13
| spl0_21
| ~ spl0_7
| spl0_3 ),
inference(rat,[],[s792,s1069,s89,s163,s164,s250,s1244,s51,s1202,s1197,s13,s1237,s1200]) ).
cnf(s1246,plain,
( spl0_6
| spl0_5
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s841,s843,s131,s221,s11,s793,s1235,s133,s134,s36,s1205,s33,s1206,s1197,s1191,s1245,s1241,s1220,s2]) ).
cnf(s1247,plain,
( ~ spl0_6
| spl0_3
| spl0_1 ),
inference(rat,[],[s407,s182,s183,s17,s1023,s659,s118,s188,s189,s7,s453,s6,s405]) ).
cnf(s1248,plain,
( ~ spl0_77
| ~ spl0_5 ),
inference(rat,[],[s1020,s92,s93,s94]) ).
cnf(s1249,plain,
( ~ spl0_13
| spl0_224
| ~ spl0_226
| spl0_18
| spl0_3 ),
inference(rat,[],[s1055,s1085,s13,s1200]) ).
cnf(s1250,plain,
( spl0_224
| spl0_3
| ~ spl0_226
| spl0_18 ),
inference(rat,[],[s1191,s1249]) ).
cnf(s1251,plain,
( spl0_6
| spl0_3
| spl0_1
| spl0_2 ),
inference(rat,[],[s1250,s185,s187,s19,s722,s831,s102,s103,s104,s1197,s12,s17,s1215,s48,s1248,s1246]) ).
cnf(s1252,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s1251,s1247]) ).
cnf(s1253,plain,
~ spl0_3,
inference(rat,[],[s248,s309,s315,s316]) ).
cnf(s1254,plain,
( spl0_121
| ~ spl0_8
| ~ spl0_13
| ~ spl0_2 ),
inference(rat,[],[s1017,s1069,s89,s163,s164]) ).
cnf(s1255,plain,
( ~ spl0_55
| ~ spl0_13
| ~ spl0_2 ),
inference(rat,[],[s1096,s1036,s120,s195,s196]) ).
cnf(s1256,plain,
( spl0_21
| ~ spl0_13
| spl0_1 ),
inference(rat,[],[s1254,s250,s27,s1244,s1193,s51,s17,s1202,s1197,s13,s1200,s1255,s1252,s1253]) ).
cnf(s1257,plain,
( ~ spl0_69
| ~ spl0_2 ),
inference(rat,[],[s1097,s71,s72,s151]) ).
cnf(s1258,plain,
( ~ spl0_13
| spl0_1 ),
inference(rat,[],[s1240,s43,s1256,s453,s1257,s1252,s1253]) ).
cnf(s1259,plain,
spl0_1,
inference(rat,[],[s839,s133,s134,s27,s36,s1193,s1205,s17,s33,s1206,s1197,s1194,s1191,s1258,s1252,s1247,s1253]) ).
cnf(s1260,plain,
spl0_26,
inference(rat,[],[s748,s211,s212,s213,s1259]) ).
cnf(s1261,plain,
( ~ spl0_8
| spl0_7 ),
inference(rat,[],[s14,s475,s476,s1260,s1253]) ).
cnf(s1262,plain,
( ~ spl0_78
| ~ spl0_10
| ~ spl0_38 ),
inference(rat,[],[s968,s1139,s90,s91,s165]) ).
cnf(s1263,plain,
( spl0_121
| ~ spl0_27 ),
inference(rat,[],[s760,s89,s163,s164]) ).
cnf(s1264,plain,
~ spl0_32,
inference(rat,[],[s1090,s192,s193,s194,s1259]) ).
cnf(s1265,plain,
( spl0_21
| ~ spl0_13 ),
inference(rat,[],[s680,s113,s178,s179,s23,s955,s125,s205,s206,s54,s947,s982,s100,s101,s170,s26,s440,s912,s3,s1193,s128,s129,s217,s27,s1261,s16,s1245,s1219,s1253,s1264]) ).
cnf(s1266,plain,
( spl0_121
| ~ spl0_7
| ~ spl0_13 ),
inference(rat,[],[s792,s1069,s89,s163,s164]) ).
cnf(s1267,plain,
( ~ spl0_18
| spl0_38 ),
inference(rat,[],[s51,s1202,s1197,s1253]) ).
cnf(s1268,plain,
( ~ spl0_69
| ~ spl0_7
| ~ spl0_11 ),
inference(rat,[],[s514,s71,s72]) ).
cnf(s1279,plain,
( spl0_145
| ~ spl0_7 ),
inference(rat,[],[s788,s110,s111,s175]) ).
cnf(s1280,plain,
( spl0_148
| ~ spl0_37 ),
inference(rat,[],[s1032,s112,s176,s177]) ).
cnf(s1288,plain,
( ~ spl0_142
| ~ spl0_12 ),
inference(rat,[],[s644,s108,s109,s174]) ).
cnf(s1290,plain,
( ~ spl0_283
| ~ spl0_6
| ~ spl0_13 ),
inference(rat,[],[s1189,s244,s245]) ).
cnf(s1292,plain,
( ~ spl0_171
| spl0_57
| ~ spl0_27
| ~ spl0_11 ),
inference(rat,[],[s668,s1183,s233,s134]) ).
cnf(s1293,plain,
( spl0_57
| ~ spl0_11
| ~ spl0_27 ),
inference(rat,[],[s133,s1292]) ).
cnf(s1294,plain,
( ~ spl0_179
| ~ spl0_37 ),
inference(rat,[],[s640,s141,s246,s247]) ).
cnf(s1295,plain,
( ~ spl0_42
| ~ spl0_13 ),
inference(rat,[],[s742,s584,s178,s179,s1265]) ).
cnf(s1296,plain,
( spl0_7
| spl0_179
| spl0_5
| ~ spl0_13 ),
inference(rat,[],[s955,s125,s205,s206,s54,s1293,s14,s248,s1162,s1290,s5,s23,s2,s1261,s1219,s1295,s1253,s1260]) ).
cnf(s1297,plain,
( ~ spl0_9
| spl0_2
| ~ spl0_13 ),
inference(rat,[],[s4,s513,s489,s1051,s1267,s56,s57,s142,s1244,s252,s250,s1279,s1266,s1237,s1296,s1294,s1280,s1248,s48,s647,s1215,s1265,s1253]) ).
cnf(s1298,plain,
( spl0_7
| spl0_2
| ~ spl0_13 ),
inference(rat,[],[s1296,s1294,s1248,s36,s48,s1293,s1262,s54,s1267,s1206,s14,s1218,s489,s1162,s3,s5,s1261,s1219,s1265,s1297,s1253,s1260]) ).
cnf(s1299,plain,
( spl0_2
| ~ spl0_13 ),
inference(rat,[],[s513,s1051,s56,s57,s142,s252,s1280,s646,s43,s1268,s4,s489,s1267,s1244,s250,s1279,s1266,s1237,s1298,s1240,s1265,s1253]) ).
cnf(s1300,plain,
( spl0_7
| ~ spl0_13 ),
inference(rat,[],[s250,s1244,s1263,s1267,s14,s489,s1162,s5,s1261,s1255,s1299,s1253,s1260]) ).
cnf(s1301,plain,
( ~ spl0_21
| ~ spl0_13 ),
inference(rat,[],[s895,s1051,s56,s57,s142,s252,s1279,s1300,s1280,s646,s43,s1257,s1299,s1240,s1253]) ).
cnf(s1302,plain,
~ spl0_13,
inference(rat,[],[s1301,s1265]) ).
cnf(s1303,plain,
spl0_18,
inference(rat,[],[s1191,s1253,s1302]) ).
cnf(s1304,plain,
spl0_14,
inference(rat,[],[s6,s1253,s1302]) ).
cnf(s1305,plain,
~ spl0_33,
inference(rat,[],[s1197,s1303]) ).
cnf(s1307,plain,
spl0_58,
inference(rat,[],[s1206,s1303]) ).
cnf(s1308,plain,
spl0_38,
inference(rat,[],[s1267,s1303]) ).
cnf(s1310,plain,
~ spl0_63,
inference(rat,[],[s1208,s1304]) ).
cnf(s1311,plain,
~ spl0_53,
inference(rat,[],[s33,s1302,s1253,s1305]) ).
cnf(s1312,plain,
~ spl0_118,
inference(rat,[],[s1244,s1308]) ).
cnf(s1316,plain,
~ spl0_37,
inference(rat,[],[s1205,s1311]) ).
cnf(s1317,plain,
~ spl0_57,
inference(rat,[],[s36,s1253,s1307,s1316]) ).
cnf(s1319,plain,
spl0_172,
inference(rat,[],[s134,s1317]) ).
cnf(s1320,plain,
spl0_171,
inference(rat,[],[s133,s1317]) ).
cnf(s1321,plain,
( spl0_8
| spl0_7 ),
inference(rat,[],[s48,s1248,s1262,s1096,s2,s3,s1163,s1104,s1193,s120,s195,s196,s967,s27,s250,s107,s173,s1207,s1263,s249,s41,s14,s1288,s1162,s5,s1260,s1310,s1312,s1303,s1308,s1253]) ).
cnf(s1322,plain,
spl0_7,
inference(rat,[],[s1321,s1261]) ).
cnf(s1324,plain,
~ spl0_11,
inference(rat,[],[s1235,s1319,s1320,s1322]) ).
cnf(s1326,plain,
( ~ spl0_140
| ~ spl0_6 ),
inference(rat,[],[s1104,s967,s107,s173,s1308]) ).
cnf(s1327,plain,
~ spl0_21,
inference(rat,[],[s3,s1204,s1015,s22,s4,s1037,s1288,s108,s174,s249,s1326,s647,s1194,s1253,s1316,s1324,s1303,s1310,s1302]) ).
cnf(s1329,plain,
( ~ spl0_169
| ~ spl0_260 ),
inference(rat,[],[s841,s843,s1303,s1322]) ).
cnf(s1330,plain,
~ spl0_22,
inference(rat,[],[s1329,s131,s221]) ).
cnf(s1331,plain,
spl0_23,
inference(rat,[],[s11,s1302,s1253,s1330]) ).
cnf(s1332,plain,
~ spl0_8,
inference(rat,[],[s793,s1324,s1331]) ).
cnf(s1333,plain,
spl0_48,
inference(rat,[],[s27,s1327,s1253,s1332]) ).
cnf(s1334,plain,
~ spl0_256,
inference(rat,[],[s217,s1333]) ).
cnf(s1335,plain,
~ spl0_167,
inference(rat,[],[s129,s1333]) ).
cnf(s1336,plain,
~ spl0_166,
inference(rat,[],[s128,s1333]) ).
cnf(s1337,plain,
~ spl0_9,
inference(rat,[],[s1193,s1333]) ).
cnf(s1338,plain,
~ spl0_47,
inference(rat,[],[s717,s100,s101,s170,s1331]) ).
cnf(s1339,plain,
spl0_10,
inference(rat,[],[s3,s1332,s1253,s1337]) ).
cnf(s1340,plain,
spl0_16,
inference(rat,[],[s26,s1332,s1253,s1338]) ).
cnf(s1342,plain,
~ spl0_335,
inference(rat,[],[s912,s1336,s1334,s1339]) ).
cnf(s1346,plain,
$false,
inference(rat,[],[s440,s1335,s1334,s1340,s1342]) ).
fof(f4995,plain,
$false,
inference(avatar_sat_refutation,[],[s1346]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN447-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n009.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 16:04:34 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.33 % (3186581)Will run a generic schedule for satisfiability detection.
% 0.18/0.33 % (3186591)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=524578086:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.33 % (3186587)% WARNING: option uhcvi not known.
% 0.18/0.33 % (3186586)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3338171429_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.33 % (3186587)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1827458273:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.33 % (3186588)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1874687302:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.33 % (3186589)dis+10_1_sil=32000:sp=arity:random_seed=2764215682:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.33 % (3186590)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2730915649:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.33 % (3186592)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4085691248:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.33 % Detected minimum model sizes of [1]
% 0.18/0.33 % Detected maximum model sizes of [64]
% 0.18/0.33 % TRYING [1]
% 0.18/0.33 % TRYING [2]
% 0.18/0.33 % TRYING [3]
% 0.18/0.33 % TRYING [4]
% 0.18/0.33 % (3186591)Instruction limit reached!
% 0.18/0.33 % (3186591)------------------------------
% 0.18/0.33 % (3186591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (3186591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (3186591)CaDiCaL version: 2.1.3
% 0.18/0.33 % (3186591)Termination reason: Instruction limit
% 0.18/0.33 % (3186591)Termination phase: Saturation
% 0.18/0.33 % (3186591)Time elapsed: 0.047 s
% 0.18/0.33 % (3186591)Peak memory usage: 14 MB
% 0.18/0.33 % (3186591)Instructions burned: 133 (million)
% 0.18/0.33 % (3186600)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=902140270:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.18/0.33 % TRYING [5]
% 0.18/0.33 % Detected minimum model sizes of [1]
% 0.18/0.33 % Detected maximum model sizes of [64]
% 0.18/0.33 % TRYING [1]
% 0.18/0.33 % TRYING [2]
% 0.18/0.33 % TRYING [3]
% 0.18/0.33 % (3186592) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3186581-3186592"...
% 0.18/0.33 % (3186587) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3186581-3186587"...
% 0.18/0.33 % TRYING [4]
% 0.18/0.33 % (3186589)Instruction limit reached!
% 0.18/0.33 % (3186589)------------------------------
% 0.18/0.33 % (3186589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (3186589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (3186589)CaDiCaL version: 2.1.3
% 0.18/0.33 % (3186589)Termination reason: Instruction limit
% 0.18/0.33 % (3186589)Termination phase: Saturation
% 0.18/0.33 % (3186589)Time elapsed: 0.064 s
% 0.18/0.33 % (3186589)Peak memory usage: 13 MB
% 0.18/0.33 % (3186589)Instructions burned: 103 (million)
% 0.18/0.33 % (3186592)...printing done.
% 0.18/0.33 % (3186592)Refutation found. Thanks to Tanya!
% 0.18/0.33 % SZS status Unsatisfiable for theBenchmark
% 0.18/0.33 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.33 % (3186592)------------------------------
% 0.18/0.33 % (3186592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (3186592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (3186592)CaDiCaL version: 2.1.3
% 0.18/0.33 % (3186592)Termination reason: Refutation
% 0.18/0.33 % (3186592)Time elapsed: 0.066 s
% 0.18/0.33 % (3186592)Peak memory usage: 14 MB
% 0.18/0.33 % (3186592)Instructions burned: 109 (million)
% 0.18/0.33 % (3186581)Success in time 0.105 s
% 0.18/0.34 % Vampire exiting
%------------------------------------------------------------------------------