%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN460-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 : n012.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:09:25 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.19s
% Output : Refutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 317
% Syntax : Number of formulae : 1220 ( 16 unt; 177 def)
% Number of atoms : 3884 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 4702 (2038 ~;2487 |; 0 &)
% ( 177 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 218 ( 217 usr; 214 prp; 0-1 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 240 ( 0 sgn 240 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,negated_conjecture,
( ~ hskp55
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f5,negated_conjecture,
( ~ hskp54
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
fof(f38,negated_conjecture,
( ~ hskp21
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f62,negated_conjecture,
( hskp34
| hskp37
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( hskp11
| hskp3
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( hskp21
| hskp54
| hskp55 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp58
| c0_1(a2252) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f69,negated_conjecture,
( ~ hskp56
| c2_1(a2242) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f76,negated_conjecture,
( ~ hskp53
| c0_1(a2235) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp53
| c2_1(a2235) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp53
| c3_1(a2235) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp52
| c1_1(a2234) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp52
| c3_1(a2234) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp52
| c2_1(a2234) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f89,negated_conjecture,
( ~ hskp48
| c3_1(a2228) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ hskp48
| c2_1(a2228) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ hskp47
| c2_1(a2226) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp47
| c0_1(a2226) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ hskp46
| c0_1(a2218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ hskp46
| c2_1(a2218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f98,negated_conjecture,
( ~ hskp44
| c2_1(a2215) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ hskp44
| c1_1(a2215) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ hskp43
| c3_1(a2208) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ hskp43
| c0_1(a2208) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ hskp42
| c1_1(a2207) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ hskp42
| c0_1(a2207) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ hskp41
| c2_1(a2205) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ hskp41
| c1_1(a2205) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ hskp40
| c2_1(a2204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ hskp40
| c3_1(a2204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f109,negated_conjecture,
( ~ hskp38
| c1_1(a2200) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ hskp37
| c1_1(a2196) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ hskp37
| c2_1(a2196) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f116,negated_conjecture,
( ~ hskp34
| c1_1(a2189) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ hskp34
| c3_1(a2189) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ hskp33
| c1_1(a2188) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ hskp32
| c0_1(a2186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f129,negated_conjecture,
( ~ hskp26
| c0_1(a2178) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ hskp26
| c2_1(a2178) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f138,negated_conjecture,
( ~ hskp20
| c1_1(a2237) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
( ~ hskp20
| c0_1(a2237) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f140,negated_conjecture,
( ~ hskp18
| c0_1(a2222) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
( ~ hskp18
| c3_1(a2222) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
( ~ hskp17
| c2_1(a2221) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f147,negated_conjecture,
( ~ hskp12
| c2_1(a2211) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
( ~ hskp11
| c0_1(a2209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f150,negated_conjecture,
( ~ hskp7
| c2_1(a2198) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
( ~ hskp7
| c0_1(a2198) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
fof(f153,negated_conjecture,
( ~ hskp4
| c3_1(a2191) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
( ~ hskp3
| c2_1(a2190) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( ~ hskp2
| c3_1(a2187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
( ~ hskp2
| c1_1(a2187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f159,negated_conjecture,
( ~ c1_1(a2252)
| ~ hskp58 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( ~ c1_1(a2242)
| ~ hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( ~ c3_1(a2242)
| ~ hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f164,negated_conjecture,
( ~ c0_1(a2228)
| ~ hskp48 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
( ~ c1_1(a2226)
| ~ hskp47 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause165) ).
fof(f166,negated_conjecture,
( ~ c3_1(a2218)
| ~ hskp46 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
( ~ c0_1(a2215)
| ~ hskp44 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
( ~ c2_1(a2208)
| ~ hskp43 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( ~ c3_1(a2207)
| ~ hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
( ~ c0_1(a2205)
| ~ hskp41 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
( ~ c1_1(a2204)
| ~ hskp40 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f174,negated_conjecture,
( ~ c0_1(a2200)
| ~ hskp38 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
( ~ c2_1(a2200)
| ~ hskp38 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
( ~ c0_1(a2196)
| ~ hskp37 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f179,negated_conjecture,
( ~ c0_1(a2189)
| ~ hskp34 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
( ~ c3_1(a2188)
| ~ hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
( ~ c2_1(a2188)
| ~ hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( ~ c3_1(a2186)
| ~ hskp32 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
( ~ c2_1(a2186)
| ~ hskp32 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f190,negated_conjecture,
( ~ c3_1(a2178)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f199,negated_conjecture,
( ~ c3_1(a2237)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
( ~ c0_1(a2233)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
( ~ c1_1(a2233)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ c3_1(a2233)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ c2_1(a2222)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
( ~ c0_1(a2221)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
( ~ c3_1(a2221)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause205) ).
fof(f207,negated_conjecture,
( ~ c1_1(a2220)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ c3_1(a2220)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause208) ).
fof(f214,negated_conjecture,
( ~ c1_1(a2211)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause214) ).
fof(f215,negated_conjecture,
( ~ c3_1(a2211)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause215) ).
fof(f216,negated_conjecture,
( ~ c1_1(a2209)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause216) ).
fof(f217,negated_conjecture,
( ~ c2_1(a2209)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
( ~ c2_1(a2206)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ c0_1(a2206)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause219) ).
fof(f220,negated_conjecture,
( ~ c3_1(a2206)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause220) ).
fof(f226,negated_conjecture,
( ~ c3_1(a2198)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause226) ).
fof(f227,negated_conjecture,
( ~ c0_1(a2197)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause227) ).
fof(f228,negated_conjecture,
( ~ c3_1(a2197)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause228) ).
fof(f229,negated_conjecture,
( ~ c1_1(a2197)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause229) ).
fof(f232,negated_conjecture,
( ~ c2_1(a2191)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause232) ).
fof(f233,negated_conjecture,
( ~ c1_1(a2191)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause233) ).
fof(f234,negated_conjecture,
( ~ c1_1(a2190)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause234) ).
fof(f235,negated_conjecture,
( ~ c0_1(a2190)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause235) ).
fof(f236,negated_conjecture,
( ~ c2_1(a2187)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause236) ).
fof(f239,negated_conjecture,
( ~ c0_1(a2181)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause239) ).
fof(f240,negated_conjecture,
( ~ c1_1(a2181)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause240) ).
fof(f241,negated_conjecture,
( ~ c2_1(a2181)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause241) ).
fof(f243,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| hskp32
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause243) ).
fof(f244,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| hskp42
| hskp43 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp18
| c2_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp58
| c1_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp7
| hskp37 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause247) ).
fof(f249,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c0_1(X0)
| hskp41
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause249) ).
fof(f251,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp16
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause251) ).
fof(f253,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c0_1(X0)
| hskp19
| hskp52 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause253) ).
fof(f256,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause256) ).
fof(f257,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp33
| hskp34 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause257) ).
fof(f259,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp46
| hskp34 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause259) ).
fof(f264,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| c2_1(X0)
| hskp47 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause264) ).
fof(f265,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c0_1(X0)
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| c1_1(X0)
| hskp53 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause265) ).
fof(f266,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| hskp38 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause266) ).
fof(f267,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp40 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause267) ).
fof(f269,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause269) ).
fof(f270,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp32 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause270) ).
fof(f272,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause272) ).
fof(f273,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X0)
| c1_1(X1)
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause273) ).
fof(f274,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause274) ).
fof(f275,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| c3_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause275) ).
fof(f276,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause276) ).
fof(f277,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c3_1(X0)
| c3_1(X1)
| c0_1(X1)
| hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause277) ).
fof(f278,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X0)
| c2_1(X1)
| hskp44 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause278) ).
fof(f279,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c0_1(X0)
| c0_1(X1)
| hskp48 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause279) ).
fof(f280,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X0)
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause280) ).
fof(f281,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X0)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause281) ).
fof(f282,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| hskp40 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause282) ).
fof(f284,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X0)
| hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause284) ).
fof(f285,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c3_1(X2)
| c2_1(X2)
| c0_1(X2)
| c2_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause285) ).
fof(f286,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| c1_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause286) ).
fof(f287,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X2)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause287) ).
fof(f288,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X2)
| c0_1(X0)
| c1_1(X0)
| c3_1(X1)
| c3_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause288) ).
fof(f289,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c1_1(X1)
| c0_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause289) ).
fof(f291,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X2)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause291) ).
fof(f292,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause292) ).
fof(f293,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X2)
| c2_1(X0)
| c2_1(X1)
| c2_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause293) ).
fof(f294,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X2)
| ~ c1_1(X2)
| c3_1(X0)
| c3_1(X1)
| c0_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause294) ).
fof(f295,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X2)
| c0_1(X1)
| c2_1(X1)
| c2_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause295) ).
fof(f296,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c0_1(X0)
| c3_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause296) ).
fof(f312,plain,
( hskp21
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f328,plain,
( ~ hskp34
| hskp37
| ~ hskp6 ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f329,plain,
( ~ hskp11
| ~ hskp3
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f63]) ).
fof(f330,plain,
( ~ hskp21
| hskp54
| hskp55 ),
inference(consistent_polarity_flipping,[],[f64]) ).
fof(f331,plain,
( ~ hskp58
| ~ c0_1(a2252) ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f335,plain,
( ~ hskp56
| ~ c2_1(a2242) ),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f342,plain,
( hskp53
| ~ c0_1(a2235) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f343,plain,
( hskp53
| ~ c2_1(a2235) ),
inference(consistent_polarity_flipping,[],[f77]) ).
fof(f344,plain,
( hskp53
| ~ c3_1(a2235) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f345,plain,
( ~ hskp52
| ~ c1_1(a2234) ),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f346,plain,
( ~ hskp52
| ~ c3_1(a2234) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f347,plain,
( ~ hskp52
| ~ c2_1(a2234) ),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f355,plain,
( ~ hskp48
| ~ c3_1(a2228) ),
inference(consistent_polarity_flipping,[],[f89]) ).
fof(f356,plain,
( ~ hskp48
| ~ c2_1(a2228) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f357,plain,
( ~ hskp47
| ~ c2_1(a2226) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f358,plain,
( ~ hskp47
| ~ c0_1(a2226) ),
inference(consistent_polarity_flipping,[],[f92]) ).
fof(f359,plain,
( ~ hskp46
| ~ c0_1(a2218) ),
inference(consistent_polarity_flipping,[],[f93]) ).
fof(f360,plain,
( ~ hskp46
| ~ c2_1(a2218) ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f364,plain,
( ~ hskp44
| ~ c2_1(a2215) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f365,plain,
( ~ hskp44
| ~ c1_1(a2215) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f366,plain,
( hskp43
| ~ c3_1(a2208) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f367,plain,
( hskp43
| ~ c0_1(a2208) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f368,plain,
( hskp42
| ~ c1_1(a2207) ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f369,plain,
( hskp42
| ~ c0_1(a2207) ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f370,plain,
( ~ hskp41
| ~ c2_1(a2205) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f371,plain,
( ~ hskp41
| ~ c1_1(a2205) ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f372,plain,
( ~ hskp40
| ~ c2_1(a2204) ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f373,plain,
( ~ hskp40
| ~ c3_1(a2204) ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f375,plain,
( ~ hskp38
| ~ c1_1(a2200) ),
inference(consistent_polarity_flipping,[],[f109]) ).
fof(f376,plain,
( ~ hskp37
| ~ c1_1(a2196) ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f377,plain,
( ~ hskp37
| ~ c2_1(a2196) ),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f382,plain,
( hskp34
| ~ c1_1(a2189) ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f383,plain,
( hskp34
| ~ c3_1(a2189) ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f384,plain,
( ~ hskp33
| ~ c1_1(a2188) ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f385,plain,
( ~ hskp32
| ~ c0_1(a2186) ),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f395,plain,
( hskp26
| ~ c0_1(a2178) ),
inference(consistent_polarity_flipping,[],[f129]) ).
fof(f396,plain,
( hskp26
| ~ c2_1(a2178) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f404,plain,
( hskp20
| ~ c1_1(a2237) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f405,plain,
( hskp20
| ~ c0_1(a2237) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f406,plain,
( hskp18
| ~ c0_1(a2222) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f407,plain,
( hskp18
| ~ c3_1(a2222) ),
inference(consistent_polarity_flipping,[],[f141]) ).
fof(f408,plain,
( ~ hskp17
| ~ c2_1(a2221) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f413,plain,
( hskp12
| ~ c2_1(a2211) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f414,plain,
( hskp11
| ~ c0_1(a2209) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f416,plain,
( ~ hskp7
| ~ c2_1(a2198) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f417,plain,
( ~ hskp7
| ~ c0_1(a2198) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f419,plain,
( hskp4
| ~ c3_1(a2191) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f420,plain,
( hskp3
| ~ c2_1(a2190) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f421,plain,
( ~ hskp2
| ~ c3_1(a2187) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f422,plain,
( ~ hskp2
| ~ c1_1(a2187) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f425,plain,
( c1_1(a2252)
| ~ hskp58 ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f426,plain,
( c1_1(a2242)
| ~ hskp56 ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f427,plain,
( c3_1(a2242)
| ~ hskp56 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f430,plain,
( c0_1(a2228)
| ~ hskp48 ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f431,plain,
( c1_1(a2226)
| ~ hskp47 ),
inference(consistent_polarity_flipping,[],[f165]) ).
fof(f432,plain,
( c3_1(a2218)
| ~ hskp46 ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f433,plain,
( c0_1(a2215)
| ~ hskp44 ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f434,plain,
( c2_1(a2208)
| hskp43 ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f435,plain,
( c3_1(a2207)
| hskp42 ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f436,plain,
( c0_1(a2205)
| ~ hskp41 ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f437,plain,
( c1_1(a2204)
| ~ hskp40 ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f440,plain,
( c0_1(a2200)
| ~ hskp38 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f441,plain,
( c2_1(a2200)
| ~ hskp38 ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f442,plain,
( c0_1(a2196)
| ~ hskp37 ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f445,plain,
( c0_1(a2189)
| hskp34 ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f446,plain,
( c3_1(a2188)
| ~ hskp33 ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f447,plain,
( c2_1(a2188)
| ~ hskp33 ),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f448,plain,
( c3_1(a2186)
| ~ hskp32 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f449,plain,
( c2_1(a2186)
| ~ hskp32 ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f456,plain,
( c3_1(a2178)
| hskp26 ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f465,plain,
( c3_1(a2237)
| hskp20 ),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f466,plain,
( c0_1(a2233)
| hskp19 ),
inference(consistent_polarity_flipping,[],[f200]) ).
fof(f467,plain,
( c1_1(a2233)
| hskp19 ),
inference(consistent_polarity_flipping,[],[f201]) ).
fof(f468,plain,
( c3_1(a2233)
| hskp19 ),
inference(consistent_polarity_flipping,[],[f202]) ).
fof(f469,plain,
( c2_1(a2222)
| hskp18 ),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f470,plain,
( c0_1(a2221)
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f204]) ).
fof(f471,plain,
( c3_1(a2221)
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f205]) ).
fof(f473,plain,
( c1_1(a2220)
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f474,plain,
( c3_1(a2220)
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f480,plain,
( c1_1(a2211)
| hskp12 ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f481,plain,
( c3_1(a2211)
| hskp12 ),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f482,plain,
( c1_1(a2209)
| hskp11 ),
inference(consistent_polarity_flipping,[],[f216]) ).
fof(f483,plain,
( c2_1(a2209)
| hskp11 ),
inference(consistent_polarity_flipping,[],[f217]) ).
fof(f484,plain,
( c2_1(a2206)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f218]) ).
fof(f485,plain,
( c0_1(a2206)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f219]) ).
fof(f486,plain,
( c3_1(a2206)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f220]) ).
fof(f492,plain,
( c3_1(a2198)
| ~ hskp7 ),
inference(consistent_polarity_flipping,[],[f226]) ).
fof(f493,plain,
( c0_1(a2197)
| hskp6 ),
inference(consistent_polarity_flipping,[],[f227]) ).
fof(f494,plain,
( c3_1(a2197)
| hskp6 ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f495,plain,
( c1_1(a2197)
| hskp6 ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f498,plain,
( c2_1(a2191)
| hskp4 ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f499,plain,
( c1_1(a2191)
| hskp4 ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f500,plain,
( c1_1(a2190)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f501,plain,
( c0_1(a2190)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f502,plain,
( c2_1(a2187)
| ~ hskp2 ),
inference(consistent_polarity_flipping,[],[f236]) ).
fof(f505,plain,
( c0_1(a2181)
| hskp0 ),
inference(consistent_polarity_flipping,[],[f239]) ).
fof(f506,plain,
( c1_1(a2181)
| hskp0 ),
inference(consistent_polarity_flipping,[],[f240]) ).
fof(f507,plain,
( c2_1(a2181)
| hskp0 ),
inference(consistent_polarity_flipping,[],[f241]) ).
fof(f509,plain,
! [X0] :
( ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| hskp32
| hskp2 ),
inference(consistent_polarity_flipping,[],[f243]) ).
fof(f510,plain,
! [X0] :
( ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ hskp42
| ~ hskp43 ),
inference(consistent_polarity_flipping,[],[f244]) ).
fof(f511,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ hskp18
| ~ c2_1(X0) ),
inference(consistent_polarity_flipping,[],[f245]) ).
fof(f512,plain,
! [X0] :
( c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| hskp58
| ~ c1_1(X0) ),
inference(consistent_polarity_flipping,[],[f246]) ).
fof(f513,plain,
! [X0] :
( c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| hskp7
| hskp37 ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f515,plain,
! [X0] :
( c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0)
| hskp41
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f517,plain,
! [X0] :
( c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| ~ c1_1(X0)
| hskp16
| hskp17 ),
inference(consistent_polarity_flipping,[],[f251]) ).
fof(f519,plain,
! [X0] :
( c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ hskp19
| hskp52 ),
inference(consistent_polarity_flipping,[],[f253]) ).
fof(f522,plain,
! [X0] :
( c1_1(X0)
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f256]) ).
fof(f523,plain,
! [X0] :
( c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| hskp33
| ~ hskp34 ),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f525,plain,
! [X0] :
( c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| hskp46
| ~ hskp34 ),
inference(consistent_polarity_flipping,[],[f259]) ).
fof(f530,plain,
! [X0,X1] :
( ~ ndr1_0
| c3_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X0)
| hskp47 ),
inference(consistent_polarity_flipping,[],[f264]) ).
fof(f531,plain,
! [X0,X1] :
( ~ ndr1_0
| c0_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ hskp53 ),
inference(consistent_polarity_flipping,[],[f265]) ).
fof(f532,plain,
! [X0,X1] :
( ~ ndr1_0
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| hskp38 ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f533,plain,
! [X0,X1] :
( c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1)
| hskp40 ),
inference(consistent_polarity_flipping,[],[f267]) ).
fof(f535,plain,
! [X0,X1] :
( c1_1(X0)
| ~ ndr1_0
| c0_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X1)
| hskp33 ),
inference(consistent_polarity_flipping,[],[f269]) ).
fof(f536,plain,
! [X0,X1] :
( c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| hskp32 ),
inference(consistent_polarity_flipping,[],[f270]) ).
fof(f538,plain,
! [X0,X1] :
( c1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ hskp26 ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f539,plain,
! [X0,X1] :
( c2_1(X0)
| ~ ndr1_0
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f273]) ).
fof(f540,plain,
! [X0,X1] :
( c1_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X1)
| ~ hskp4 ),
inference(consistent_polarity_flipping,[],[f274]) ).
fof(f541,plain,
! [X0,X1] :
( c3_1(X0)
| ~ ndr1_0
| c2_1(X1)
| c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f275]) ).
fof(f542,plain,
! [X0,X1] :
( c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| hskp56 ),
inference(consistent_polarity_flipping,[],[f276]) ).
fof(f543,plain,
! [X0,X1] :
( c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| hskp56 ),
inference(consistent_polarity_flipping,[],[f277]) ).
fof(f544,plain,
! [X0,X1] :
( c3_1(X0)
| c0_1(X0)
| ~ ndr1_0
| c3_1(X1)
| c0_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X1)
| hskp44 ),
inference(consistent_polarity_flipping,[],[f278]) ).
fof(f545,plain,
! [X0,X1] :
( c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c3_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1)
| hskp48 ),
inference(consistent_polarity_flipping,[],[f279]) ).
fof(f546,plain,
! [X0,X1] :
( c0_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ hskp20 ),
inference(consistent_polarity_flipping,[],[f280]) ).
fof(f547,plain,
! [X0,X1] :
( c3_1(X0)
| c0_1(X0)
| ~ ndr1_0
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f281]) ).
fof(f548,plain,
! [X0,X1] :
( c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c3_1(X1)
| c0_1(X1)
| ~ c0_1(X0)
| ~ c2_1(X1)
| hskp40 ),
inference(consistent_polarity_flipping,[],[f282]) ).
fof(f550,plain,
! [X0,X1] :
( c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c0_1(X0)
| hskp33 ),
inference(consistent_polarity_flipping,[],[f284]) ).
fof(f551,plain,
! [X2,X0,X1] :
( ~ ndr1_0
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X0) ),
inference(consistent_polarity_flipping,[],[f285]) ).
fof(f552,plain,
! [X2,X0,X1] :
( c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f286]) ).
fof(f553,plain,
! [X2,X0,X1] :
( c1_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f287]) ).
fof(f554,plain,
! [X2,X0,X1] :
( c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c2_1(X1)
| c0_1(X2)
| ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c3_1(X2)
| ~ c1_1(X2) ),
inference(consistent_polarity_flipping,[],[f288]) ).
fof(f555,plain,
! [X2,X0,X1] :
( c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c2_1(X1)
| c2_1(X2)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X2)
| ~ c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f289]) ).
fof(f557,plain,
! [X2,X0,X1] :
( c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c2_1(X1)
| c0_1(X2)
| ~ c3_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f291]) ).
fof(f558,plain,
! [X2,X0,X1] :
( c0_1(X0)
| ~ ndr1_0
| c3_1(X1)
| c1_1(X2)
| c0_1(X2)
| c2_1(X2)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X1) ),
inference(consistent_polarity_flipping,[],[f292]) ).
fof(f559,plain,
! [X2,X0,X1] :
( c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c1_1(X1)
| c1_1(X2)
| ~ c2_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X2)
| ~ c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f293]) ).
fof(f560,plain,
! [X2,X0,X1] :
( c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| c2_1(X1)
| c3_1(X2)
| c1_1(X2)
| ~ c3_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f294]) ).
fof(f561,plain,
! [X2,X0,X1] :
( c2_1(X0)
| c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c3_1(X2)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| ~ c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f295]) ).
fof(f562,plain,
! [X2,X0,X1] :
( c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| c2_1(X2)
| ~ c0_1(X0)
| ~ c3_1(X2)
| ~ c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f296]) ).
fof(f564,definition,
( spl0_1
<=> ! [X2] :
( c2_1(X2)
| ~ c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f565,plain,
( ! [X2] :
( c2_1(X2)
| ~ c0_1(X2)
| ~ c3_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f567,definition,
( spl0_2
<=> ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f568,plain,
( ! [X1] :
( c2_1(X1)
| c0_1(X1)
| c3_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f570,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f574,definition,
( spl0_4
<=> ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f575,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f562,f574,f570,f567,f564]) ).
fof(f578,definition,
( spl0_5
<=> ! [X2] :
( c3_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f579,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c0_1(X2)
| c3_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f581,definition,
( spl0_6
<=> ! [X1] :
( c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f582,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f561,f567,f570,f581,f578]) ).
fof(f585,definition,
( spl0_7
<=> ! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f586,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f587,plain,
( spl0_4
| spl0_1
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f560,f585,f570,f564,f574]) ).
fof(f589,definition,
( spl0_8
<=> ! [X1] :
( c0_1(X1)
| ~ c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f590,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| c1_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f592,definition,
( spl0_9
<=> ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f593,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f594,plain,
( spl0_6
| spl0_8
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f559,f592,f570,f589,f581]) ).
fof(f596,definition,
( spl0_10
<=> ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f597,plain,
( ! [X2] :
( c2_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f599,definition,
( spl0_11
<=> ! [X1] :
( c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f600,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| ~ c1_1(X1) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f602,definition,
( spl0_12
<=> ! [X0] :
( c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f603,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f604,plain,
( spl0_10
| spl0_11
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f558,f602,f570,f599,f596]) ).
fof(f606,definition,
( spl0_13
<=> ! [X1] :
( c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f607,plain,
( ! [X1] :
( c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f609,definition,
( spl0_14
<=> ! [X0] :
( c0_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f610,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f611,plain,
( spl0_12
| spl0_13
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f557,f609,f570,f606,f602]) ).
fof(f613,definition,
( spl0_15
<=> ! [X1] :
( c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f614,plain,
( ! [X1] :
( c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f616,definition,
( spl0_16
<=> ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f617,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f619,plain,
( spl0_1
| spl0_13
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f555,f613,f570,f606,f564]) ).
fof(f621,definition,
( spl0_17
<=> ! [X2] :
( c0_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f622,plain,
( ! [X2] :
( ~ c3_1(X2)
| ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( spl0_17
| spl0_14
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f554,f606,f570,f609,f621]) ).
fof(f625,definition,
( spl0_18
<=> ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f626,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c1_1(X2)
| ~ c0_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f628,definition,
( spl0_19
<=> ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f629,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f630,plain,
( spl0_18
| spl0_10
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f553,f628,f570,f596,f625]) ).
fof(f632,definition,
( spl0_20
<=> ! [X2] :
( ~ c1_1(X2)
| ~ c3_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f633,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2)
| ~ c1_1(X2) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,definition,
( spl0_21
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f636,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f635]) ).
fof(f638,definition,
( spl0_22
<=> ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f639,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f640,plain,
( spl0_20
| spl0_21
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f552,f638,f570,f635,f632]) ).
fof(f642,definition,
( spl0_23
<=> ! [X2] :
( ~ c3_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f643,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c0_1(X2)
| ~ c3_1(X2) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f644,plain,
( spl0_23
| spl0_20
| spl0_22
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f551,f570,f638,f632,f642]) ).
fof(f646,definition,
( spl0_24
<=> hskp33 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f650,definition,
( spl0_25
<=> ! [X1] :
( c1_1(X1)
| c2_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f651,plain,
( ! [X1] :
( c2_1(X1)
| c1_1(X1)
| c3_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f650]) ).
fof(f653,definition,
( spl0_26
<=> ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f654,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f655,plain,
( spl0_24
| spl0_25
| ~ spl0_3
| spl0_26 ),
inference(avatar_split_clause,[],[f550,f653,f570,f650,f646]) ).
fof(f662,definition,
( spl0_28
<=> hskp40 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f666,definition,
( spl0_29
<=> ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f667,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f668,plain,
( spl0_28
| spl0_22
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f548,f666,f570,f638,f662]) ).
fof(f670,definition,
( spl0_30
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f673,plain,
( ~ spl0_30
| spl0_9
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f547,f638,f570,f592,f670]) ).
fof(f675,definition,
( spl0_31
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f678,plain,
( ~ spl0_31
| spl0_25
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f546,f621,f570,f650,f675]) ).
fof(f680,definition,
( spl0_32
<=> hskp48 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f683,plain,
( spl0_32
| spl0_4
| ~ spl0_3
| spl0_26 ),
inference(avatar_split_clause,[],[f545,f653,f570,f574,f680]) ).
fof(f685,definition,
( spl0_33
<=> hskp44 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f689,definition,
( spl0_34
<=> ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f690,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f691,plain,
( spl0_33
| spl0_22
| ~ spl0_3
| spl0_34 ),
inference(avatar_split_clause,[],[f544,f689,f570,f638,f685]) ).
fof(f693,definition,
( spl0_35
<=> hskp56 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f696,plain,
( spl0_35
| spl0_1
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f543,f609,f570,f564,f693]) ).
fof(f698,definition,
( spl0_36
<=> ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f699,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f700,plain,
( spl0_35
| spl0_16
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f542,f698,f570,f616,f693]) ).
fof(f701,plain,
( ~ spl0_30
| spl0_14
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f541,f599,f570,f609,f670]) ).
fof(f703,definition,
( spl0_37
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f706,plain,
( ~ spl0_37
| spl0_26
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f540,f628,f570,f653,f703]) ).
fof(f708,definition,
( spl0_38
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f712,definition,
( spl0_39
<=> ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f713,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f714,plain,
( ~ spl0_38
| spl0_15
| ~ spl0_3
| spl0_39 ),
inference(avatar_split_clause,[],[f539,f712,f570,f613,f708]) ).
fof(f716,definition,
( spl0_40
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f719,plain,
( ~ spl0_40
| spl0_13
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f538,f574,f570,f606,f716]) ).
fof(f726,definition,
( spl0_42
<=> hskp32 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f729,plain,
( spl0_42
| spl0_16
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f536,f599,f570,f616,f726]) ).
fof(f730,plain,
( spl0_24
| spl0_17
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f535,f581,f570,f621,f646]) ).
fof(f739,plain,
( spl0_28
| spl0_17
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f533,f599,f570,f621,f662]) ).
fof(f741,definition,
( spl0_45
<=> hskp38 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f744,plain,
( spl0_45
| spl0_18
| spl0_7
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f532,f570,f585,f625,f741]) ).
fof(f746,definition,
( spl0_46
<=> hskp53 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f749,plain,
( ~ spl0_46
| spl0_20
| spl0_17
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f531,f570,f621,f632,f746]) ).
fof(f751,definition,
( spl0_47
<=> hskp47 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f754,plain,
( spl0_47
| spl0_20
| spl0_5
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f530,f570,f578,f632,f751]) ).
fof(f786,definition,
( spl0_55
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f794,definition,
( spl0_57
<=> hskp34 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f798,definition,
( spl0_58
<=> hskp46 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f801,plain,
( ~ spl0_57
| spl0_58
| ~ spl0_3
| spl0_34 ),
inference(avatar_split_clause,[],[f525,f689,f570,f798,f794]) ).
fof(f811,plain,
( ~ spl0_57
| spl0_24
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f523,f698,f570,f646,f794]) ).
fof(f813,definition,
( spl0_61
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f816,plain,
( ~ spl0_61
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f522,f596,f570,f813]) ).
fof(f818,definition,
( spl0_62
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f832,definition,
( spl0_65
<=> hskp52 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f836,definition,
( spl0_66
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f839,plain,
( spl0_65
| ~ spl0_66
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f519,f564,f570,f836,f832]) ).
fof(f846,definition,
( spl0_68
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f849,plain,
( spl0_62
| spl0_68
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f517,f606,f570,f846,f818]) ).
fof(f856,definition,
( spl0_70
<=> hskp41 ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f859,plain,
( ~ spl0_30
| spl0_70
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f515,f564,f570,f856,f670]) ).
fof(f870,definition,
( spl0_73
<=> hskp37 ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f874,definition,
( spl0_74
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f877,plain,
( spl0_73
| spl0_74
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f513,f602,f570,f874,f870]) ).
fof(f879,definition,
( spl0_75
<=> hskp58 ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f882,plain,
( spl0_75
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f512,f599,f570,f879]) ).
fof(f883,plain,
( ~ spl0_55
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f511,f628,f570,f786]) ).
fof(f885,definition,
( spl0_76
<=> hskp43 ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f889,definition,
( spl0_77
<=> hskp42 ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f892,plain,
( ~ spl0_76
| ~ spl0_77
| spl0_21
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f510,f570,f635,f889,f885]) ).
fof(f894,definition,
( spl0_78
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f897,plain,
( spl0_78
| spl0_42
| spl0_21
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f509,f570,f635,f726,f894]) ).
fof(f908,definition,
( spl0_81
<=> c2_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f910,plain,
( c2_1(a2181)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f911,plain,
( spl0_61
| spl0_81 ),
inference(avatar_split_clause,[],[f507,f908,f813]) ).
fof(f913,definition,
( spl0_82
<=> c1_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f916,plain,
( spl0_61
| spl0_82 ),
inference(avatar_split_clause,[],[f506,f913,f813]) ).
fof(f918,definition,
( spl0_83
<=> c0_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f921,plain,
( spl0_61
| spl0_83 ),
inference(avatar_split_clause,[],[f505,f918,f813]) ).
fof(f933,definition,
( spl0_86
<=> c2_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f935,plain,
( c2_1(a2187)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f936,plain,
( ~ spl0_78
| spl0_86 ),
inference(avatar_split_clause,[],[f502,f933,f894]) ).
fof(f938,definition,
( spl0_87
<=> c0_1(a2190) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f941,plain,
( spl0_38
| spl0_87 ),
inference(avatar_split_clause,[],[f501,f938,f708]) ).
fof(f943,definition,
( spl0_88
<=> c1_1(a2190) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f946,plain,
( spl0_38
| spl0_88 ),
inference(avatar_split_clause,[],[f500,f943,f708]) ).
fof(f948,definition,
( spl0_89
<=> c1_1(a2191) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f951,plain,
( spl0_37
| spl0_89 ),
inference(avatar_split_clause,[],[f499,f948,f703]) ).
fof(f953,definition,
( spl0_90
<=> c2_1(a2191) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f955,plain,
( c2_1(a2191)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f956,plain,
( spl0_37
| spl0_90 ),
inference(avatar_split_clause,[],[f498,f953,f703]) ).
fof(f972,definition,
( spl0_94
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f976,definition,
( spl0_95
<=> c1_1(a2197) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f979,plain,
( spl0_94
| spl0_95 ),
inference(avatar_split_clause,[],[f495,f976,f972]) ).
fof(f981,definition,
( spl0_96
<=> c3_1(a2197) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f983,plain,
( c3_1(a2197)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f984,plain,
( spl0_94
| spl0_96 ),
inference(avatar_split_clause,[],[f494,f981,f972]) ).
fof(f986,definition,
( spl0_97
<=> c0_1(a2197) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f989,plain,
( spl0_94
| spl0_97 ),
inference(avatar_split_clause,[],[f493,f986,f972]) ).
fof(f991,definition,
( spl0_98
<=> c3_1(a2198) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f994,plain,
( ~ spl0_74
| spl0_98 ),
inference(avatar_split_clause,[],[f492,f991,f874]) ).
fof(f1021,definition,
( spl0_104
<=> c3_1(a2206) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f1023,plain,
( c3_1(a2206)
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f1021]) ).
fof(f1024,plain,
( spl0_30
| spl0_104 ),
inference(avatar_split_clause,[],[f486,f1021,f670]) ).
fof(f1026,definition,
( spl0_105
<=> c0_1(a2206) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f1029,plain,
( spl0_30
| spl0_105 ),
inference(avatar_split_clause,[],[f485,f1026,f670]) ).
fof(f1031,definition,
( spl0_106
<=> c2_1(a2206) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f1033,plain,
( c2_1(a2206)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1034,plain,
( spl0_30
| spl0_106 ),
inference(avatar_split_clause,[],[f484,f1031,f670]) ).
fof(f1036,definition,
( spl0_107
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f1040,definition,
( spl0_108
<=> c2_1(a2209) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f1042,plain,
( c2_1(a2209)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f1040]) ).
fof(f1043,plain,
( spl0_107
| spl0_108 ),
inference(avatar_split_clause,[],[f483,f1040,f1036]) ).
fof(f1045,definition,
( spl0_109
<=> c1_1(a2209) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f1048,plain,
( spl0_107
| spl0_109 ),
inference(avatar_split_clause,[],[f482,f1045,f1036]) ).
fof(f1050,definition,
( spl0_110
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f1054,definition,
( spl0_111
<=> c3_1(a2211) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f1056,plain,
( c3_1(a2211)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1057,plain,
( spl0_110
| spl0_111 ),
inference(avatar_split_clause,[],[f481,f1054,f1050]) ).
fof(f1059,definition,
( spl0_112
<=> c1_1(a2211) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f1062,plain,
( spl0_110
| spl0_112 ),
inference(avatar_split_clause,[],[f480,f1059,f1050]) ).
fof(f1089,definition,
( spl0_118
<=> c3_1(a2220) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f1091,plain,
( c3_1(a2220)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1092,plain,
( ~ spl0_68
| spl0_118 ),
inference(avatar_split_clause,[],[f474,f1089,f846]) ).
fof(f1094,definition,
( spl0_119
<=> c1_1(a2220) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f1097,plain,
( ~ spl0_68
| spl0_119 ),
inference(avatar_split_clause,[],[f473,f1094,f846]) ).
fof(f1104,definition,
( spl0_121
<=> c3_1(a2221) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1107,plain,
( ~ spl0_62
| spl0_121 ),
inference(avatar_split_clause,[],[f471,f1104,f818]) ).
fof(f1109,definition,
( spl0_122
<=> c0_1(a2221) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f1112,plain,
( ~ spl0_62
| spl0_122 ),
inference(avatar_split_clause,[],[f470,f1109,f818]) ).
fof(f1114,definition,
( spl0_123
<=> c2_1(a2222) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f1115,plain,
( ~ c2_1(a2222)
| spl0_123 ),
inference(avatar_component_clause,[],[f1114]) ).
fof(f1116,plain,
( c2_1(a2222)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f1114]) ).
fof(f1117,plain,
( spl0_55
| spl0_123 ),
inference(avatar_split_clause,[],[f469,f1114,f786]) ).
fof(f1119,definition,
( spl0_124
<=> c3_1(a2233) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f1121,plain,
( c3_1(a2233)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f1119]) ).
fof(f1122,plain,
( spl0_66
| spl0_124 ),
inference(avatar_split_clause,[],[f468,f1119,f836]) ).
fof(f1124,definition,
( spl0_125
<=> c1_1(a2233) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f1126,plain,
( c1_1(a2233)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1127,plain,
( spl0_66
| spl0_125 ),
inference(avatar_split_clause,[],[f467,f1124,f836]) ).
fof(f1129,definition,
( spl0_126
<=> c0_1(a2233) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f1132,plain,
( spl0_66
| spl0_126 ),
inference(avatar_split_clause,[],[f466,f1129,f836]) ).
fof(f1134,definition,
( spl0_127
<=> c3_1(a2237) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f1136,plain,
( c3_1(a2237)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f1134]) ).
fof(f1137,plain,
( spl0_31
| spl0_127 ),
inference(avatar_split_clause,[],[f465,f1134,f675]) ).
fof(f1139,definition,
( spl0_128
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f1183,definition,
( spl0_137
<=> c3_1(a2178) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1186,plain,
( spl0_40
| spl0_137 ),
inference(avatar_split_clause,[],[f456,f1183,f716]) ).
fof(f1226,definition,
( spl0_146
<=> c2_1(a2186) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1228,plain,
( c2_1(a2186)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f1226]) ).
fof(f1229,plain,
( ~ spl0_42
| spl0_146 ),
inference(avatar_split_clause,[],[f449,f1226,f726]) ).
fof(f1231,definition,
( spl0_147
<=> c3_1(a2186) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1233,plain,
( c3_1(a2186)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f1231]) ).
fof(f1234,plain,
( ~ spl0_42
| spl0_147 ),
inference(avatar_split_clause,[],[f448,f1231,f726]) ).
fof(f1236,definition,
( spl0_148
<=> c2_1(a2188) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1238,plain,
( c2_1(a2188)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f1236]) ).
fof(f1239,plain,
( ~ spl0_24
| spl0_148 ),
inference(avatar_split_clause,[],[f447,f1236,f646]) ).
fof(f1241,definition,
( spl0_149
<=> c3_1(a2188) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1243,plain,
( c3_1(a2188)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f1241]) ).
fof(f1244,plain,
( ~ spl0_24
| spl0_149 ),
inference(avatar_split_clause,[],[f446,f1241,f646]) ).
fof(f1246,definition,
( spl0_150
<=> c0_1(a2189) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1249,plain,
( spl0_57
| spl0_150 ),
inference(avatar_split_clause,[],[f445,f1246,f794]) ).
fof(f1269,definition,
( spl0_155
<=> c0_1(a2196) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1272,plain,
( ~ spl0_73
| spl0_155 ),
inference(avatar_split_clause,[],[f442,f1269,f870]) ).
fof(f1274,definition,
( spl0_156
<=> c2_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f1276,plain,
( c2_1(a2200)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f1274]) ).
fof(f1277,plain,
( ~ spl0_45
| spl0_156 ),
inference(avatar_split_clause,[],[f441,f1274,f741]) ).
fof(f1279,definition,
( spl0_157
<=> c0_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1282,plain,
( ~ spl0_45
| spl0_157 ),
inference(avatar_split_clause,[],[f440,f1279,f741]) ).
fof(f1294,definition,
( spl0_160
<=> c1_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1297,plain,
( ~ spl0_28
| spl0_160 ),
inference(avatar_split_clause,[],[f437,f1294,f662]) ).
fof(f1299,definition,
( spl0_161
<=> c0_1(a2205) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1302,plain,
( ~ spl0_70
| spl0_161 ),
inference(avatar_split_clause,[],[f436,f1299,f856]) ).
fof(f1304,definition,
( spl0_162
<=> c3_1(a2207) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1306,plain,
( c3_1(a2207)
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f1304]) ).
fof(f1307,plain,
( spl0_77
| spl0_162 ),
inference(avatar_split_clause,[],[f435,f1304,f889]) ).
fof(f1309,definition,
( spl0_163
<=> c2_1(a2208) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1311,plain,
( c2_1(a2208)
| ~ spl0_163 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1312,plain,
( spl0_76
| spl0_163 ),
inference(avatar_split_clause,[],[f434,f1309,f885]) ).
fof(f1314,definition,
( spl0_164
<=> c0_1(a2215) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1317,plain,
( ~ spl0_33
| spl0_164 ),
inference(avatar_split_clause,[],[f433,f1314,f685]) ).
fof(f1319,definition,
( spl0_165
<=> c3_1(a2218) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1322,plain,
( ~ spl0_58
| spl0_165 ),
inference(avatar_split_clause,[],[f432,f1319,f798]) ).
fof(f1324,definition,
( spl0_166
<=> c1_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1327,plain,
( ~ spl0_47
| spl0_166 ),
inference(avatar_split_clause,[],[f431,f1324,f751]) ).
fof(f1329,definition,
( spl0_167
<=> c0_1(a2228) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1332,plain,
( ~ spl0_32
| spl0_167 ),
inference(avatar_split_clause,[],[f430,f1329,f680]) ).
fof(f1344,definition,
( spl0_170
<=> c3_1(a2242) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1346,plain,
( c3_1(a2242)
| ~ spl0_170 ),
inference(avatar_component_clause,[],[f1344]) ).
fof(f1347,plain,
( ~ spl0_35
| spl0_170 ),
inference(avatar_split_clause,[],[f427,f1344,f693]) ).
fof(f1349,definition,
( spl0_171
<=> c1_1(a2242) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1352,plain,
( ~ spl0_35
| spl0_171 ),
inference(avatar_split_clause,[],[f426,f1349,f693]) ).
fof(f1354,definition,
( spl0_172
<=> c1_1(a2252) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f1357,plain,
( ~ spl0_75
| spl0_172 ),
inference(avatar_split_clause,[],[f425,f1354,f879]) ).
fof(f1369,definition,
( spl0_175
<=> c1_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1372,plain,
( ~ spl0_175
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f422,f894,f1369]) ).
fof(f1374,definition,
( spl0_176
<=> c3_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f1376,plain,
( ~ c3_1(a2187)
| spl0_176 ),
inference(avatar_component_clause,[],[f1374]) ).
fof(f1377,plain,
( ~ spl0_176
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f421,f894,f1374]) ).
fof(f1379,definition,
( spl0_177
<=> c2_1(a2190) ),
introduced(definition,[new_symbols(definition,[spl0_177])],[avatar_definition]) ).
fof(f1381,plain,
( ~ c2_1(a2190)
| spl0_177 ),
inference(avatar_component_clause,[],[f1379]) ).
fof(f1382,plain,
( ~ spl0_177
| spl0_38 ),
inference(avatar_split_clause,[],[f420,f708,f1379]) ).
fof(f1384,definition,
( spl0_178
<=> c3_1(a2191) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f1387,plain,
( ~ spl0_178
| spl0_37 ),
inference(avatar_split_clause,[],[f419,f703,f1384]) ).
fof(f1394,definition,
( spl0_180
<=> c0_1(a2198) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f1397,plain,
( ~ spl0_180
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f417,f874,f1394]) ).
fof(f1399,definition,
( spl0_181
<=> c2_1(a2198) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1401,plain,
( ~ c2_1(a2198)
| spl0_181 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1402,plain,
( ~ spl0_181
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f416,f874,f1399]) ).
fof(f1409,definition,
( spl0_183
<=> c0_1(a2209) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1412,plain,
( ~ spl0_183
| spl0_107 ),
inference(avatar_split_clause,[],[f414,f1036,f1409]) ).
fof(f1414,definition,
( spl0_184
<=> c2_1(a2211) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f1416,plain,
( ~ c2_1(a2211)
| spl0_184 ),
inference(avatar_component_clause,[],[f1414]) ).
fof(f1417,plain,
( ~ spl0_184
| spl0_110 ),
inference(avatar_split_clause,[],[f413,f1050,f1414]) ).
fof(f1439,definition,
( spl0_189
<=> c2_1(a2221) ),
introduced(definition,[new_symbols(definition,[spl0_189])],[avatar_definition]) ).
fof(f1441,plain,
( ~ c2_1(a2221)
| spl0_189 ),
inference(avatar_component_clause,[],[f1439]) ).
fof(f1442,plain,
( ~ spl0_189
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f408,f818,f1439]) ).
fof(f1444,definition,
( spl0_190
<=> c3_1(a2222) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f1446,plain,
( ~ c3_1(a2222)
| spl0_190 ),
inference(avatar_component_clause,[],[f1444]) ).
fof(f1447,plain,
( ~ spl0_190
| spl0_55 ),
inference(avatar_split_clause,[],[f407,f786,f1444]) ).
fof(f1449,definition,
( spl0_191
<=> c0_1(a2222) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f1452,plain,
( ~ spl0_191
| spl0_55 ),
inference(avatar_split_clause,[],[f406,f786,f1449]) ).
fof(f1454,definition,
( spl0_192
<=> c0_1(a2237) ),
introduced(definition,[new_symbols(definition,[spl0_192])],[avatar_definition]) ).
fof(f1457,plain,
( ~ spl0_192
| spl0_31 ),
inference(avatar_split_clause,[],[f405,f675,f1454]) ).
fof(f1459,definition,
( spl0_193
<=> c1_1(a2237) ),
introduced(definition,[new_symbols(definition,[spl0_193])],[avatar_definition]) ).
fof(f1462,plain,
( ~ spl0_193
| spl0_31 ),
inference(avatar_split_clause,[],[f404,f675,f1459]) ).
fof(f1499,definition,
( spl0_201
<=> c2_1(a2178) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f1501,plain,
( ~ c2_1(a2178)
| spl0_201 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1502,plain,
( ~ spl0_201
| spl0_40 ),
inference(avatar_split_clause,[],[f396,f716,f1499]) ).
fof(f1504,definition,
( spl0_202
<=> c0_1(a2178) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f1507,plain,
( ~ spl0_202
| spl0_40 ),
inference(avatar_split_clause,[],[f395,f716,f1504]) ).
fof(f1554,definition,
( spl0_212
<=> c0_1(a2186) ),
introduced(definition,[new_symbols(definition,[spl0_212])],[avatar_definition]) ).
fof(f1557,plain,
( ~ spl0_212
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f385,f726,f1554]) ).
fof(f1559,definition,
( spl0_213
<=> c1_1(a2188) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f1562,plain,
( ~ spl0_213
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f384,f646,f1559]) ).
fof(f1564,definition,
( spl0_214
<=> c3_1(a2189) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f1566,plain,
( ~ c3_1(a2189)
| spl0_214 ),
inference(avatar_component_clause,[],[f1564]) ).
fof(f1567,plain,
( ~ spl0_214
| spl0_57 ),
inference(avatar_split_clause,[],[f383,f794,f1564]) ).
fof(f1569,definition,
( spl0_215
<=> c1_1(a2189) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1571,plain,
( ~ c1_1(a2189)
| spl0_215 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1572,plain,
( ~ spl0_215
| spl0_57 ),
inference(avatar_split_clause,[],[f382,f794,f1569]) ).
fof(f1594,definition,
( spl0_220
<=> c2_1(a2196) ),
introduced(definition,[new_symbols(definition,[spl0_220])],[avatar_definition]) ).
fof(f1596,plain,
( ~ c2_1(a2196)
| spl0_220 ),
inference(avatar_component_clause,[],[f1594]) ).
fof(f1597,plain,
( ~ spl0_220
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f377,f870,f1594]) ).
fof(f1599,definition,
( spl0_221
<=> c1_1(a2196) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f1602,plain,
( ~ spl0_221
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f376,f870,f1599]) ).
fof(f1604,definition,
( spl0_222
<=> c1_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f1607,plain,
( ~ spl0_222
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f375,f741,f1604]) ).
fof(f1614,definition,
( spl0_224
<=> c3_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f1617,plain,
( ~ spl0_224
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f373,f662,f1614]) ).
fof(f1619,definition,
( spl0_225
<=> c2_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_225])],[avatar_definition]) ).
fof(f1621,plain,
( ~ c2_1(a2204)
| spl0_225 ),
inference(avatar_component_clause,[],[f1619]) ).
fof(f1622,plain,
( ~ spl0_225
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f372,f662,f1619]) ).
fof(f1624,definition,
( spl0_226
<=> c1_1(a2205) ),
introduced(definition,[new_symbols(definition,[spl0_226])],[avatar_definition]) ).
fof(f1627,plain,
( ~ spl0_226
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f371,f856,f1624]) ).
fof(f1629,definition,
( spl0_227
<=> c2_1(a2205) ),
introduced(definition,[new_symbols(definition,[spl0_227])],[avatar_definition]) ).
fof(f1631,plain,
( ~ c2_1(a2205)
| spl0_227 ),
inference(avatar_component_clause,[],[f1629]) ).
fof(f1632,plain,
( ~ spl0_227
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f370,f856,f1629]) ).
fof(f1634,definition,
( spl0_228
<=> c0_1(a2207) ),
introduced(definition,[new_symbols(definition,[spl0_228])],[avatar_definition]) ).
fof(f1637,plain,
( ~ spl0_228
| spl0_77 ),
inference(avatar_split_clause,[],[f369,f889,f1634]) ).
fof(f1639,definition,
( spl0_229
<=> c1_1(a2207) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f1642,plain,
( ~ spl0_229
| spl0_77 ),
inference(avatar_split_clause,[],[f368,f889,f1639]) ).
fof(f1644,definition,
( spl0_230
<=> c0_1(a2208) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1647,plain,
( ~ spl0_230
| spl0_76 ),
inference(avatar_split_clause,[],[f367,f885,f1644]) ).
fof(f1649,definition,
( spl0_231
<=> c3_1(a2208) ),
introduced(definition,[new_symbols(definition,[spl0_231])],[avatar_definition]) ).
fof(f1651,plain,
( ~ c3_1(a2208)
| spl0_231 ),
inference(avatar_component_clause,[],[f1649]) ).
fof(f1652,plain,
( ~ spl0_231
| spl0_76 ),
inference(avatar_split_clause,[],[f366,f885,f1649]) ).
fof(f1654,definition,
( spl0_232
<=> c1_1(a2215) ),
introduced(definition,[new_symbols(definition,[spl0_232])],[avatar_definition]) ).
fof(f1657,plain,
( ~ spl0_232
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f365,f685,f1654]) ).
fof(f1659,definition,
( spl0_233
<=> c2_1(a2215) ),
introduced(definition,[new_symbols(definition,[spl0_233])],[avatar_definition]) ).
fof(f1661,plain,
( ~ c2_1(a2215)
| spl0_233 ),
inference(avatar_component_clause,[],[f1659]) ).
fof(f1662,plain,
( ~ spl0_233
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f364,f685,f1659]) ).
fof(f1679,definition,
( spl0_237
<=> c2_1(a2218) ),
introduced(definition,[new_symbols(definition,[spl0_237])],[avatar_definition]) ).
fof(f1681,plain,
( ~ c2_1(a2218)
| spl0_237 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1682,plain,
( ~ spl0_237
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f360,f798,f1679]) ).
fof(f1684,definition,
( spl0_238
<=> c0_1(a2218) ),
introduced(definition,[new_symbols(definition,[spl0_238])],[avatar_definition]) ).
fof(f1687,plain,
( ~ spl0_238
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f359,f798,f1684]) ).
fof(f1689,definition,
( spl0_239
<=> c0_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_239])],[avatar_definition]) ).
fof(f1692,plain,
( ~ spl0_239
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f358,f751,f1689]) ).
fof(f1694,definition,
( spl0_240
<=> c2_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1696,plain,
( ~ c2_1(a2226)
| spl0_240 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1697,plain,
( ~ spl0_240
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f357,f751,f1694]) ).
fof(f1699,definition,
( spl0_241
<=> c2_1(a2228) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1701,plain,
( ~ c2_1(a2228)
| spl0_241 ),
inference(avatar_component_clause,[],[f1699]) ).
fof(f1702,plain,
( ~ spl0_241
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f356,f680,f1699]) ).
fof(f1704,definition,
( spl0_242
<=> c3_1(a2228) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f1707,plain,
( ~ spl0_242
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f355,f680,f1704]) ).
fof(f1744,definition,
( spl0_250
<=> c2_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_250])],[avatar_definition]) ).
fof(f1746,plain,
( ~ c2_1(a2234)
| spl0_250 ),
inference(avatar_component_clause,[],[f1744]) ).
fof(f1747,plain,
( ~ spl0_250
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f347,f832,f1744]) ).
fof(f1749,definition,
( spl0_251
<=> c3_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f1751,plain,
( ~ c3_1(a2234)
| spl0_251 ),
inference(avatar_component_clause,[],[f1749]) ).
fof(f1752,plain,
( ~ spl0_251
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f346,f832,f1749]) ).
fof(f1754,definition,
( spl0_252
<=> c1_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f1757,plain,
( ~ spl0_252
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f345,f832,f1754]) ).
fof(f1759,definition,
( spl0_253
<=> c3_1(a2235) ),
introduced(definition,[new_symbols(definition,[spl0_253])],[avatar_definition]) ).
fof(f1761,plain,
( ~ c3_1(a2235)
| spl0_253 ),
inference(avatar_component_clause,[],[f1759]) ).
fof(f1762,plain,
( ~ spl0_253
| spl0_46 ),
inference(avatar_split_clause,[],[f344,f746,f1759]) ).
fof(f1764,definition,
( spl0_254
<=> c2_1(a2235) ),
introduced(definition,[new_symbols(definition,[spl0_254])],[avatar_definition]) ).
fof(f1766,plain,
( ~ c2_1(a2235)
| spl0_254 ),
inference(avatar_component_clause,[],[f1764]) ).
fof(f1767,plain,
( ~ spl0_254
| spl0_46 ),
inference(avatar_split_clause,[],[f343,f746,f1764]) ).
fof(f1769,definition,
( spl0_255
<=> c0_1(a2235) ),
introduced(definition,[new_symbols(definition,[spl0_255])],[avatar_definition]) ).
fof(f1772,plain,
( ~ spl0_255
| spl0_46 ),
inference(avatar_split_clause,[],[f342,f746,f1769]) ).
fof(f1778,definition,
( spl0_257
<=> hskp54 ),
introduced(definition,[new_symbols(definition,[spl0_257])],[avatar_definition]) ).
fof(f1797,definition,
( spl0_261
<=> hskp55 ),
introduced(definition,[new_symbols(definition,[spl0_261])],[avatar_definition]) ).
fof(f1812,definition,
( spl0_264
<=> c2_1(a2242) ),
introduced(definition,[new_symbols(definition,[spl0_264])],[avatar_definition]) ).
fof(f1814,plain,
( ~ c2_1(a2242)
| spl0_264 ),
inference(avatar_component_clause,[],[f1812]) ).
fof(f1815,plain,
( ~ spl0_264
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f335,f693,f1812]) ).
fof(f1832,definition,
( spl0_268
<=> c0_1(a2252) ),
introduced(definition,[new_symbols(definition,[spl0_268])],[avatar_definition]) ).
fof(f1835,plain,
( ~ spl0_268
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f331,f879,f1832]) ).
fof(f1836,plain,
( spl0_261
| spl0_257
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f330,f1139,f1778,f1797]) ).
fof(f1837,plain,
( ~ spl0_110
| ~ spl0_38
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f329,f1036,f708,f1050]) ).
fof(f1838,plain,
( ~ spl0_94
| spl0_73
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f328,f794,f870,f972]) ).
fof(f1862,plain,
( spl0_3
| spl0_128 ),
inference(avatar_split_clause,[],[f312,f1139,f570]) ).
fof(f1895,plain,
( spl0_3
| ~ spl0_257 ),
inference(avatar_split_clause,[],[f5,f1778,f570]) ).
fof(f1896,plain,
( spl0_3
| ~ spl0_261 ),
inference(avatar_split_clause,[],[f4,f1797,f570]) ).
fof(f1904,plain,
( ~ c0_1(a2234)
| c1_1(a2234)
| ~ spl0_4
| spl0_251 ),
inference(resolution,[],[f575,f1751]) ).
fof(f1917,plain,
( ~ c0_1(a2189)
| c1_1(a2189)
| ~ spl0_4
| spl0_214 ),
inference(resolution,[],[f575,f1566]) ).
fof(f1942,definition,
( spl0_269
<=> c0_1(a2220) ),
introduced(definition,[new_symbols(definition,[spl0_269])],[avatar_definition]) ).
fof(f1947,definition,
( spl0_270
<=> c0_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_270])],[avatar_definition]) ).
fof(f1957,definition,
( spl0_272
<=> c0_1(a2211) ),
introduced(definition,[new_symbols(definition,[spl0_272])],[avatar_definition]) ).
fof(f1977,definition,
( spl0_276
<=> c0_1(a2188) ),
introduced(definition,[new_symbols(definition,[spl0_276])],[avatar_definition]) ).
fof(f1987,definition,
( spl0_278
<=> c0_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_278])],[avatar_definition]) ).
fof(f1997,definition,
( spl0_280
<=> c0_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f2000,plain,
( spl0_252
| ~ spl0_280
| ~ spl0_4
| spl0_251 ),
inference(avatar_split_clause,[],[f1904,f1749,f574,f1997,f1754]) ).
fof(f2002,definition,
( spl0_281
<=> c0_1(a2242) ),
introduced(definition,[new_symbols(definition,[spl0_281])],[avatar_definition]) ).
fof(f2009,definition,
( spl0_282
<=> c1_1(a2206) ),
introduced(definition,[new_symbols(definition,[spl0_282])],[avatar_definition]) ).
fof(f2052,plain,
( c1_1(a2222)
| c0_1(a2222)
| ~ spl0_10
| spl0_123 ),
inference(resolution,[],[f597,f1115]) ).
fof(f2096,definition,
( spl0_287
<=> c1_1(a2222) ),
introduced(definition,[new_symbols(definition,[spl0_287])],[avatar_definition]) ).
fof(f2098,plain,
( c1_1(a2222)
| ~ spl0_287 ),
inference(avatar_component_clause,[],[f2096]) ).
fof(f2116,definition,
( spl0_290
<=> c1_1(a2186) ),
introduced(definition,[new_symbols(definition,[spl0_290])],[avatar_definition]) ).
fof(f2117,plain,
( ~ c1_1(a2186)
| spl0_290 ),
inference(avatar_component_clause,[],[f2116]) ).
fof(f2132,definition,
( spl0_292
<=> c1_1(a2208) ),
introduced(definition,[new_symbols(definition,[spl0_292])],[avatar_definition]) ).
fof(f2149,definition,
( spl0_295
<=> c1_1(a2228) ),
introduced(definition,[new_symbols(definition,[spl0_295])],[avatar_definition]) ).
fof(f2161,definition,
( spl0_297
<=> c1_1(a2235) ),
introduced(definition,[new_symbols(definition,[spl0_297])],[avatar_definition]) ).
fof(f2169,plain,
( ~ c0_1(a2181)
| c3_1(a2181)
| ~ spl0_5
| ~ spl0_81 ),
inference(resolution,[],[f910,f579]) ).
fof(f2171,definition,
( spl0_298
<=> c3_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_298])],[avatar_definition]) ).
fof(f2173,plain,
( c3_1(a2181)
| ~ spl0_298 ),
inference(avatar_component_clause,[],[f2171]) ).
fof(f2177,plain,
( c1_1(a2206)
| ~ c0_1(a2206)
| ~ spl0_6
| ~ spl0_106 ),
inference(resolution,[],[f582,f1033]) ).
fof(f2181,plain,
( c3_1(a2181)
| ~ c1_1(a2181)
| ~ spl0_11
| ~ spl0_81 ),
inference(resolution,[],[f600,f910]) ).
fof(f2182,plain,
( ~ spl0_82
| spl0_298
| ~ spl0_11
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f2181,f908,f599,f2171,f913]) ).
fof(f2186,plain,
( c3_1(a2191)
| ~ c1_1(a2191)
| ~ spl0_11
| ~ spl0_90 ),
inference(resolution,[],[f955,f600]) ).
fof(f2189,plain,
( ~ spl0_89
| spl0_178
| ~ spl0_11
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f2186,f953,f599,f1384,f948]) ).
fof(f2236,plain,
( ~ c1_1(a2190)
| ~ c0_1(a2190)
| ~ spl0_13
| spl0_177 ),
inference(resolution,[],[f607,f1381]) ).
fof(f2253,plain,
( ~ spl0_87
| ~ spl0_88
| ~ spl0_13
| spl0_177 ),
inference(avatar_split_clause,[],[f2236,f1379,f606,f943,f938]) ).
fof(f2273,plain,
( ~ c1_1(a2204)
| ~ c0_1(a2204)
| ~ spl0_13
| spl0_225 ),
inference(resolution,[],[f607,f1621]) ).
fof(f2301,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_12
| ~ spl0_14 ),
inference(resolution,[],[f610,f603]) ).
fof(f2312,plain,
( ~ c3_1(a2226)
| c0_1(a2226)
| ~ spl0_14
| spl0_240 ),
inference(resolution,[],[f610,f1696]) ).
fof(f2313,plain,
( ~ c3_1(a2218)
| c0_1(a2218)
| ~ spl0_14
| spl0_237 ),
inference(resolution,[],[f610,f1681]) ).
fof(f2329,plain,
( ~ c3_1(a2178)
| c0_1(a2178)
| ~ spl0_14
| spl0_201 ),
inference(resolution,[],[f610,f1501]) ).
fof(f2339,plain,
( ~ c3_1(a2198)
| c0_1(a2198)
| ~ spl0_14
| spl0_181 ),
inference(resolution,[],[f610,f1401]) ).
fof(f2344,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_12
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f2301]) ).
fof(f2352,definition,
( spl0_301
<=> c3_1(a2209) ),
introduced(definition,[new_symbols(definition,[spl0_301])],[avatar_definition]) ).
fof(f2353,plain,
( c3_1(a2209)
| ~ spl0_301 ),
inference(avatar_component_clause,[],[f2352]) ).
fof(f2373,definition,
( spl0_305
<=> c3_1(a2196) ),
introduced(definition,[new_symbols(definition,[spl0_305])],[avatar_definition]) ).
fof(f2375,plain,
( ~ c3_1(a2196)
| spl0_305 ),
inference(avatar_component_clause,[],[f2373]) ).
fof(f2378,definition,
( spl0_306
<=> c3_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_306])],[avatar_definition]) ).
fof(f2380,plain,
( ~ c3_1(a2200)
| spl0_306 ),
inference(avatar_component_clause,[],[f2378]) ).
fof(f2388,definition,
( spl0_308
<=> c3_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_308])],[avatar_definition]) ).
fof(f2389,plain,
( c3_1(a2226)
| ~ spl0_308 ),
inference(avatar_component_clause,[],[f2388]) ).
fof(f2398,definition,
( spl0_310
<=> c3_1(a2252) ),
introduced(definition,[new_symbols(definition,[spl0_310])],[avatar_definition]) ).
fof(f2399,plain,
( c3_1(a2252)
| ~ spl0_310 ),
inference(avatar_component_clause,[],[f2398]) ).
fof(f2400,plain,
( ~ c3_1(a2252)
| spl0_310 ),
inference(avatar_component_clause,[],[f2398]) ).
fof(f2404,plain,
( c3_1(a2209)
| ~ c1_1(a2209)
| ~ spl0_11
| ~ spl0_108 ),
inference(resolution,[],[f1042,f600]) ).
fof(f2406,plain,
( ~ spl0_109
| spl0_301
| ~ spl0_11
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f2404,f1040,f599,f2352,f1045]) ).
fof(f2412,plain,
( ~ c0_1(a2196)
| c1_1(a2196)
| ~ spl0_4
| spl0_305 ),
inference(resolution,[],[f2375,f575]) ).
fof(f2413,plain,
( ~ c0_1(a2200)
| c1_1(a2200)
| ~ spl0_4
| spl0_306 ),
inference(resolution,[],[f2380,f575]) ).
fof(f2421,plain,
( c0_1(a2209)
| ~ spl0_12
| ~ spl0_14
| ~ spl0_301 ),
inference(resolution,[],[f2344,f2353]) ).
fof(f2425,plain,
( spl0_183
| ~ spl0_12
| ~ spl0_14
| ~ spl0_301 ),
inference(avatar_split_clause,[],[f2421,f2352,f609,f602,f1409]) ).
fof(f2436,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_11
| ~ spl0_15 ),
inference(resolution,[],[f614,f600]) ).
fof(f2452,plain,
( ~ c1_1(a2204)
| c3_1(a2204)
| ~ spl0_15
| spl0_225 ),
inference(resolution,[],[f614,f1621]) ).
fof(f2476,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_11
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f2436]) ).
fof(f2493,plain,
( ~ c1_1(a2208)
| ~ spl0_11
| ~ spl0_15
| spl0_231 ),
inference(resolution,[],[f2476,f1651]) ).
fof(f2515,plain,
( ~ c1_1(a2222)
| ~ spl0_11
| ~ spl0_15
| spl0_190 ),
inference(resolution,[],[f2476,f1446]) ).
fof(f2549,plain,
( ~ c0_1(a2196)
| ~ c3_1(a2196)
| ~ spl0_1
| spl0_220 ),
inference(resolution,[],[f565,f1596]) ).
fof(f2562,plain,
( ~ c0_1(a2221)
| ~ c3_1(a2221)
| ~ spl0_1
| spl0_189 ),
inference(resolution,[],[f565,f1441]) ).
fof(f2619,plain,
( spl0_191
| spl0_287
| ~ spl0_10
| spl0_123 ),
inference(avatar_split_clause,[],[f2052,f1114,f596,f2096,f1449]) ).
fof(f2626,plain,
( ~ spl0_292
| ~ spl0_11
| ~ spl0_15
| spl0_231 ),
inference(avatar_split_clause,[],[f2493,f1649,f613,f599,f2132]) ).
fof(f2628,plain,
( ~ spl0_287
| ~ spl0_11
| ~ spl0_15
| spl0_190 ),
inference(avatar_split_clause,[],[f2515,f1444,f613,f599,f2096]) ).
fof(f2661,plain,
( c0_1(a2186)
| ~ spl0_12
| ~ spl0_14
| ~ spl0_147 ),
inference(resolution,[],[f1233,f2344]) ).
fof(f2664,plain,
( c1_1(a2188)
| ~ c0_1(a2188)
| ~ spl0_6
| ~ spl0_148 ),
inference(resolution,[],[f1238,f582]) ).
fof(f2667,plain,
( c1_1(a2200)
| ~ c0_1(a2200)
| ~ spl0_6
| ~ spl0_156 ),
inference(resolution,[],[f1276,f582]) ).
fof(f2688,plain,
( c3_1(a2222)
| ~ c1_1(a2222)
| ~ spl0_11
| ~ spl0_123 ),
inference(resolution,[],[f1116,f600]) ).
fof(f2690,plain,
( ~ c0_1(a2222)
| c1_1(a2222)
| ~ spl0_4
| spl0_190 ),
inference(resolution,[],[f1446,f575]) ).
fof(f2733,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_10
| ~ spl0_12 ),
inference(resolution,[],[f597,f603]) ).
fof(f2755,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_10
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f2733]) ).
fof(f2825,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_14
| ~ spl0_16 ),
inference(resolution,[],[f617,f610]) ).
fof(f2833,plain,
( ~ c1_1(a2208)
| c0_1(a2208)
| ~ spl0_16
| ~ spl0_163 ),
inference(resolution,[],[f617,f1311]) ).
fof(f2843,plain,
( ~ c1_1(a2222)
| c0_1(a2222)
| ~ spl0_16
| ~ spl0_123 ),
inference(resolution,[],[f617,f1116]) ).
fof(f2845,plain,
( ~ c1_1(a2209)
| c0_1(a2209)
| ~ spl0_16
| ~ spl0_108 ),
inference(resolution,[],[f617,f1042]) ).
fof(f2852,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_14
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f2825]) ).
fof(f2857,plain,
( ~ c1_1(a2252)
| c0_1(a2252)
| ~ spl0_17
| ~ spl0_310 ),
inference(resolution,[],[f622,f2399]) ).
fof(f2907,plain,
( ~ c1_1(a2206)
| ~ c0_1(a2206)
| ~ spl0_18
| ~ spl0_106 ),
inference(resolution,[],[f626,f1033]) ).
fof(f2909,plain,
( ~ c1_1(a2181)
| ~ c0_1(a2181)
| ~ spl0_18
| ~ spl0_81 ),
inference(resolution,[],[f626,f910]) ).
fof(f2911,plain,
( ~ spl0_83
| ~ spl0_82
| ~ spl0_18
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f2909,f908,f625,f913,f918]) ).
fof(f2914,plain,
( ! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_10
| ~ spl0_19 ),
inference(resolution,[],[f629,f597]) ).
fof(f2925,plain,
( c1_1(a2200)
| ~ c3_1(a2200)
| ~ spl0_19
| ~ spl0_156 ),
inference(resolution,[],[f629,f1276]) ).
fof(f2927,plain,
( c1_1(a2188)
| ~ c3_1(a2188)
| ~ spl0_19
| ~ spl0_148 ),
inference(resolution,[],[f629,f1238]) ).
fof(f2939,plain,
( c1_1(a2206)
| ~ c3_1(a2206)
| ~ spl0_19
| ~ spl0_106 ),
inference(resolution,[],[f629,f1033]) ).
fof(f2943,plain,
( ! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_10
| ~ spl0_19 ),
inference(duplicate_literal_removal,[],[f2914]) ).
fof(f2946,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_14
| ~ spl0_20 ),
inference(resolution,[],[f633,f610]) ).
fof(f2973,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_14
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f2946]) ).
fof(f3001,plain,
( ~ c0_1(a2200)
| c3_1(a2200)
| ~ spl0_5
| ~ spl0_156 ),
inference(resolution,[],[f579,f1276]) ).
fof(f3044,plain,
( ~ c3_1(a2206)
| ~ c1_1(a2206)
| ~ spl0_20
| ~ spl0_106 ),
inference(resolution,[],[f633,f1033]) ).
fof(f3076,plain,
( ~ c0_1(a2181)
| ~ c1_1(a2181)
| ~ spl0_21
| ~ spl0_298 ),
inference(resolution,[],[f636,f2173]) ).
fof(f3079,plain,
( ~ spl0_82
| ~ spl0_83
| ~ spl0_21
| ~ spl0_298 ),
inference(avatar_split_clause,[],[f3076,f2171,f635,f918,f913]) ).
fof(f3100,plain,
( ~ c0_1(a2187)
| c1_1(a2187)
| ~ spl0_4
| spl0_176 ),
inference(resolution,[],[f1376,f575]) ).
fof(f3121,plain,
( c0_1(a2222)
| c3_1(a2222)
| ~ spl0_22
| ~ spl0_123 ),
inference(resolution,[],[f639,f1116]) ).
fof(f3124,plain,
( c0_1(a2187)
| c3_1(a2187)
| ~ spl0_22
| ~ spl0_86 ),
inference(resolution,[],[f639,f935]) ).
fof(f3136,plain,
( spl0_176
| spl0_270
| ~ spl0_22
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f3124,f933,f638,f1947,f1374]) ).
fof(f3185,plain,
( spl0_212
| ~ spl0_12
| ~ spl0_14
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f2661,f1231,f609,f602,f1554]) ).
fof(f3194,plain,
( spl0_17
| ~ spl0_14
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f2852,f616,f609,f621]) ).
fof(f3195,plain,
( spl0_17
| ~ spl0_14
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2973,f632,f609,f621]) ).
fof(f3204,plain,
( ~ c3_1(a2206)
| ~ c1_1(a2206)
| ~ spl0_20
| ~ spl0_106 ),
inference(resolution,[],[f1033,f633]) ).
fof(f3211,plain,
( ~ c3_1(a2186)
| ~ c1_1(a2186)
| ~ spl0_20
| ~ spl0_146 ),
inference(resolution,[],[f1228,f633]) ).
fof(f3241,plain,
( c1_1(a2188)
| c0_1(a2188)
| ~ spl0_7
| ~ spl0_149 ),
inference(resolution,[],[f586,f1243]) ).
fof(f3242,plain,
( c1_1(a2186)
| c0_1(a2186)
| ~ spl0_7
| ~ spl0_147 ),
inference(resolution,[],[f586,f1233]) ).
fof(f3272,plain,
( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_8
| ~ spl0_10 ),
inference(resolution,[],[f590,f597]) ).
fof(f3282,plain,
( c0_1(a2208)
| c1_1(a2208)
| ~ spl0_8
| ~ spl0_163 ),
inference(resolution,[],[f590,f1311]) ).
fof(f3290,plain,
( c0_1(a2222)
| c1_1(a2222)
| ~ spl0_8
| ~ spl0_123 ),
inference(resolution,[],[f590,f1116]) ).
fof(f3292,plain,
( c0_1(a2187)
| c1_1(a2187)
| ~ spl0_8
| ~ spl0_86 ),
inference(resolution,[],[f590,f935]) ).
fof(f3298,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0) )
| ~ spl0_8
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f3272]) ).
fof(f3301,plain,
( spl0_175
| spl0_270
| ~ spl0_8
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f3292,f933,f589,f1947,f1369]) ).
fof(f3302,plain,
( spl0_287
| spl0_191
| ~ spl0_8
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f3290,f1114,f589,f1449,f2096]) ).
fof(f3309,plain,
( spl0_292
| spl0_230
| ~ spl0_8
| ~ spl0_163 ),
inference(avatar_split_clause,[],[f3282,f1309,f589,f1644,f2132]) ).
fof(f3326,plain,
( ~ spl0_104
| spl0_282
| ~ spl0_19
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f2939,f1031,f628,f2009,f1021]) ).
fof(f3341,plain,
( spl0_287
| ~ spl0_191
| ~ spl0_4
| spl0_190 ),
inference(avatar_split_clause,[],[f2690,f1444,f574,f1449,f2096]) ).
fof(f3346,plain,
( spl0_222
| ~ spl0_157
| ~ spl0_4
| spl0_306 ),
inference(avatar_split_clause,[],[f2413,f2378,f574,f1279,f1604]) ).
fof(f3439,plain,
( c1_1(a2234)
| c0_1(a2234)
| ~ spl0_10
| spl0_250 ),
inference(resolution,[],[f1746,f597]) ).
fof(f3440,plain,
( ~ c1_1(a2235)
| c3_1(a2235)
| ~ spl0_15
| spl0_254 ),
inference(resolution,[],[f1766,f614]) ).
fof(f3441,plain,
( c1_1(a2235)
| c0_1(a2235)
| ~ spl0_10
| spl0_254 ),
inference(resolution,[],[f1766,f597]) ).
fof(f3511,plain,
( c0_1(a2186)
| ~ spl0_8
| ~ spl0_10
| spl0_290 ),
inference(resolution,[],[f3298,f2117]) ).
fof(f3535,plain,
( spl0_212
| ~ spl0_8
| ~ spl0_10
| spl0_290 ),
inference(avatar_split_clause,[],[f3511,f2116,f596,f589,f1554]) ).
fof(f3559,plain,
( ~ spl0_278
| ~ spl0_160
| ~ spl0_13
| spl0_225 ),
inference(avatar_split_clause,[],[f2273,f1619,f606,f1294,f1987]) ).
fof(f3612,plain,
( c0_1(a2226)
| c3_1(a2226)
| ~ spl0_2
| spl0_240 ),
inference(resolution,[],[f568,f1696]) ).
fof(f3617,plain,
( c0_1(a2204)
| c3_1(a2204)
| ~ spl0_2
| spl0_225 ),
inference(resolution,[],[f568,f1621]) ).
fof(f3657,plain,
( ~ c3_1(a2186)
| c0_1(a2186)
| ~ spl0_12
| ~ spl0_146 ),
inference(resolution,[],[f603,f1228]) ).
fof(f3661,plain,
( spl0_212
| ~ spl0_147
| ~ spl0_12
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f3657,f1226,f602,f1231,f1554]) ).
fof(f3667,plain,
( ~ c1_1(a2242)
| ~ c0_1(a2242)
| ~ spl0_13
| spl0_264 ),
inference(resolution,[],[f607,f1814]) ).
fof(f3672,plain,
( ~ c1_1(a2228)
| ~ c0_1(a2228)
| ~ spl0_13
| spl0_241 ),
inference(resolution,[],[f607,f1701]) ).
fof(f3695,plain,
( ~ c1_1(a2211)
| ~ c0_1(a2211)
| ~ spl0_13
| spl0_184 ),
inference(resolution,[],[f607,f1416]) ).
fof(f3710,plain,
( ~ c1_1(a2242)
| c0_1(a2242)
| ~ spl0_17
| ~ spl0_170 ),
inference(resolution,[],[f622,f1346]) ).
fof(f3718,plain,
( ~ c1_1(a2226)
| c0_1(a2226)
| ~ spl0_17
| ~ spl0_308 ),
inference(resolution,[],[f622,f2389]) ).
fof(f3732,plain,
( ~ c1_1(a2186)
| c0_1(a2186)
| ~ spl0_17
| ~ spl0_147 ),
inference(resolution,[],[f622,f1233]) ).
fof(f3748,plain,
( ~ c1_1(a2211)
| c0_1(a2211)
| ~ spl0_17
| ~ spl0_111 ),
inference(resolution,[],[f622,f1056]) ).
fof(f3749,plain,
( ~ c1_1(a2209)
| c0_1(a2209)
| ~ spl0_17
| ~ spl0_301 ),
inference(resolution,[],[f622,f2353]) ).
fof(f3756,plain,
( ~ c1_1(a2220)
| c0_1(a2220)
| ~ spl0_17
| ~ spl0_118 ),
inference(resolution,[],[f622,f1091]) ).
fof(f3762,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_18 ),
inference(resolution,[],[f626,f607]) ).
fof(f3771,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_18 ),
inference(duplicate_literal_removal,[],[f3762]) ).
fof(f3778,plain,
( c1_1(a2186)
| ~ c3_1(a2186)
| ~ spl0_19
| ~ spl0_146 ),
inference(resolution,[],[f629,f1228]) ).
fof(f3786,plain,
( ~ c0_1(a2242)
| ~ c1_1(a2242)
| ~ spl0_21
| ~ spl0_170 ),
inference(resolution,[],[f636,f1346]) ).
fof(f3831,plain,
( ~ c0_1(a2220)
| ~ c1_1(a2220)
| ~ spl0_21
| ~ spl0_118 ),
inference(resolution,[],[f636,f1091]) ).
fof(f3842,plain,
( c0_1(a2208)
| c3_1(a2208)
| ~ spl0_22
| ~ spl0_163 ),
inference(resolution,[],[f639,f1311]) ).
fof(f3880,plain,
( c1_1(a2234)
| c3_1(a2234)
| ~ spl0_25
| spl0_250 ),
inference(resolution,[],[f651,f1746]) ).
fof(f3883,plain,
( c1_1(a2228)
| c3_1(a2228)
| ~ spl0_25
| spl0_241 ),
inference(resolution,[],[f651,f1701]) ).
fof(f3934,plain,
( ~ c0_1(a2234)
| c1_1(a2234)
| ~ spl0_26
| spl0_250 ),
inference(resolution,[],[f654,f1746]) ).
fof(f3942,plain,
( ~ c0_1(a2205)
| c1_1(a2205)
| ~ spl0_26
| spl0_227 ),
inference(resolution,[],[f654,f1631]) ).
fof(f4003,plain,
( spl0_251
| spl0_252
| ~ spl0_25
| spl0_250 ),
inference(avatar_split_clause,[],[f3880,f1744,f650,f1754,f1749]) ).
fof(f4008,plain,
( ~ spl0_147
| spl0_290
| ~ spl0_19
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f3778,f1226,f628,f2116,f1231]) ).
fof(f4022,plain,
( ~ spl0_167
| ~ spl0_295
| ~ spl0_13
| spl0_241 ),
inference(avatar_split_clause,[],[f3672,f1699,f606,f2149,f1329]) ).
fof(f4025,plain,
( spl0_269
| ~ spl0_119
| ~ spl0_17
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f3756,f1089,f621,f1094,f1942]) ).
fof(f4027,plain,
( spl0_183
| ~ spl0_109
| ~ spl0_17
| ~ spl0_301 ),
inference(avatar_split_clause,[],[f3749,f2352,f621,f1045,f1409]) ).
fof(f4028,plain,
( spl0_272
| ~ spl0_112
| ~ spl0_17
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f3748,f1054,f621,f1059,f1957]) ).
fof(f4037,plain,
( spl0_239
| ~ spl0_166
| ~ spl0_17
| ~ spl0_308 ),
inference(avatar_split_clause,[],[f3718,f2388,f621,f1324,f1689]) ).
fof(f4040,plain,
( spl0_281
| ~ spl0_171
| ~ spl0_17
| ~ spl0_170 ),
inference(avatar_split_clause,[],[f3710,f1344,f621,f1349,f2002]) ).
fof(f4062,plain,
( spl0_224
| spl0_278
| ~ spl0_2
| spl0_225 ),
inference(avatar_split_clause,[],[f3617,f1619,f567,f1987,f1614]) ).
fof(f4066,plain,
( spl0_268
| ~ spl0_172
| ~ spl0_17
| ~ spl0_310 ),
inference(avatar_split_clause,[],[f2857,f2398,f621,f1354,f1832]) ).
fof(f4077,plain,
( spl0_183
| ~ spl0_109
| ~ spl0_16
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f2845,f1040,f616,f1045,f1409]) ).
fof(f4087,plain,
( spl0_308
| spl0_239
| ~ spl0_2
| spl0_240 ),
inference(avatar_split_clause,[],[f3612,f1694,f567,f1689,f2388]) ).
fof(f4105,plain,
( ~ spl0_276
| spl0_213
| ~ spl0_6
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f2664,f1236,f581,f1559,f1977]) ).
fof(f4117,plain,
( spl0_253
| ~ spl0_297
| ~ spl0_15
| spl0_254 ),
inference(avatar_split_clause,[],[f3440,f1764,f613,f2161,f1759]) ).
fof(f4126,plain,
( ~ spl0_306
| spl0_222
| ~ spl0_19
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f2925,f1274,f628,f1604,f2378]) ).
fof(f4127,plain,
( ~ spl0_149
| spl0_213
| ~ spl0_19
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f2927,f1236,f628,f1559,f1241]) ).
fof(f4132,plain,
( spl0_252
| ~ spl0_280
| ~ spl0_26
| spl0_250 ),
inference(avatar_split_clause,[],[f3934,f1744,f653,f1997,f1754]) ).
fof(f4137,plain,
( spl0_226
| ~ spl0_161
| ~ spl0_26
| spl0_227 ),
inference(avatar_split_clause,[],[f3942,f1629,f653,f1299,f1624]) ).
fof(f4148,plain,
( ~ spl0_171
| ~ spl0_281
| ~ spl0_21
| ~ spl0_170 ),
inference(avatar_split_clause,[],[f3786,f1344,f635,f2002,f1349]) ).
fof(f4155,plain,
( ~ spl0_119
| ~ spl0_269
| ~ spl0_21
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f3831,f1089,f635,f1942,f1094]) ).
fof(f4182,plain,
( ~ spl0_290
| ~ spl0_147
| ~ spl0_20
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f3211,f1226,f632,f1231,f2116]) ).
fof(f4183,plain,
( spl0_242
| spl0_295
| ~ spl0_25
| spl0_241 ),
inference(avatar_split_clause,[],[f3883,f1699,f650,f2149,f1704]) ).
fof(f4202,plain,
( ~ spl0_305
| ~ spl0_155
| ~ spl0_1
| spl0_220 ),
inference(avatar_split_clause,[],[f2549,f1594,f564,f1269,f2373]) ).
fof(f4207,plain,
( ~ spl0_121
| ~ spl0_122
| ~ spl0_1
| spl0_189 ),
inference(avatar_split_clause,[],[f2562,f1439,f564,f1109,f1104]) ).
fof(f4214,plain,
( spl0_215
| ~ spl0_150
| ~ spl0_4
| spl0_214 ),
inference(avatar_split_clause,[],[f1917,f1564,f574,f1246,f1569]) ).
fof(f4219,plain,
( spl0_175
| ~ spl0_270
| ~ spl0_4
| spl0_176 ),
inference(avatar_split_clause,[],[f3100,f1374,f574,f1947,f1369]) ).
fof(f4221,plain,
( spl0_298
| ~ spl0_83
| ~ spl0_5
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f2169,f908,f578,f918,f2171]) ).
fof(f4244,plain,
( spl0_280
| spl0_252
| ~ spl0_10
| spl0_250 ),
inference(avatar_split_clause,[],[f3439,f1744,f596,f1754,f1997]) ).
fof(f4270,plain,
( ~ spl0_281
| ~ spl0_171
| ~ spl0_13
| spl0_264 ),
inference(avatar_split_clause,[],[f3667,f1812,f606,f1349,f2002]) ).
fof(f4290,plain,
( spl0_212
| ~ spl0_290
| ~ spl0_17
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f3732,f1231,f621,f2116,f1554]) ).
fof(f4317,plain,
( ~ spl0_105
| spl0_282
| ~ spl0_6
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f2177,f1031,f581,f2009,f1026]) ).
fof(f4319,plain,
( ~ spl0_157
| spl0_222
| ~ spl0_6
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f2667,f1274,f581,f1604,f1279]) ).
fof(f4327,plain,
( ~ spl0_105
| ~ spl0_282
| ~ spl0_18
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f2907,f1031,f625,f2009,f1026]) ).
fof(f4331,plain,
( spl0_276
| spl0_213
| ~ spl0_7
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f3241,f1241,f585,f1559,f1977]) ).
fof(f4332,plain,
( spl0_212
| spl0_290
| ~ spl0_7
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f3242,f1231,f585,f2116,f1554]) ).
fof(f4338,plain,
( ~ spl0_287
| spl0_190
| ~ spl0_11
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f2688,f1114,f599,f1444,f2096]) ).
fof(f4362,plain,
( ~ spl0_272
| ~ spl0_112
| ~ spl0_13
| spl0_184 ),
inference(avatar_split_clause,[],[f3695,f1414,f606,f1059,f1957]) ).
fof(f4376,plain,
( spl0_255
| spl0_297
| ~ spl0_10
| spl0_254 ),
inference(avatar_split_clause,[],[f3441,f1764,f596,f2161,f1769]) ).
fof(f4445,plain,
( c1_1(a2207)
| c0_1(a2207)
| ~ spl0_7
| ~ spl0_162 ),
inference(resolution,[],[f586,f1306]) ).
fof(f4450,plain,
( c1_1(a2237)
| c0_1(a2237)
| ~ spl0_7
| ~ spl0_127 ),
inference(resolution,[],[f586,f1136]) ).
fof(f4461,plain,
( spl0_192
| spl0_193
| ~ spl0_7
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f4450,f1134,f585,f1459,f1454]) ).
fof(f4462,plain,
( spl0_228
| spl0_229
| ~ spl0_7
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f4445,f1304,f585,f1639,f1634]) ).
fof(f4480,plain,
( c3_1(a2222)
| c1_1(a2222)
| ~ spl0_9
| ~ spl0_123 ),
inference(resolution,[],[f593,f1116]) ).
fof(f4486,plain,
( c3_1(a2187)
| c1_1(a2187)
| ~ spl0_9
| ~ spl0_86 ),
inference(resolution,[],[f593,f935]) ).
fof(f4489,plain,
( spl0_175
| spl0_176
| ~ spl0_9
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f4486,f933,f592,f1374,f1369]) ).
fof(f4634,plain,
( spl0_7
| ~ spl0_10
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f2755,f602,f596,f585]) ).
fof(f4635,plain,
( spl0_7
| ~ spl0_10
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2943,f628,f596,f585]) ).
fof(f4678,plain,
( ~ c0_1(a2222)
| ~ spl0_13
| ~ spl0_18
| ~ spl0_287 ),
inference(resolution,[],[f3771,f2098]) ).
fof(f4816,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_20 ),
inference(resolution,[],[f633,f607]) ).
fof(f4818,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_20 ),
inference(resolution,[],[f633,f565]) ).
fof(f4819,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f4818]) ).
fof(f4820,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f4816]) ).
fof(f4842,plain,
( ~ c0_1(a2233)
| ~ c1_1(a2233)
| ~ spl0_21
| ~ spl0_124 ),
inference(resolution,[],[f636,f1121]) ).
fof(f4845,plain,
( ~ c0_1(a2197)
| ~ c1_1(a2197)
| ~ spl0_21
| ~ spl0_96 ),
inference(resolution,[],[f636,f983]) ).
fof(f4906,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_6
| ~ spl0_26 ),
inference(resolution,[],[f654,f582]) ).
fof(f4924,plain,
( ~ c0_1(a2215)
| c1_1(a2215)
| ~ spl0_26
| spl0_233 ),
inference(resolution,[],[f654,f1661]) ).
fof(f4929,plain,
( ~ c0_1(a2196)
| c1_1(a2196)
| ~ spl0_26
| spl0_220 ),
inference(resolution,[],[f654,f1596]) ).
fof(f4960,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_6
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f4906]) ).
fof(f5013,plain,
( spl0_224
| ~ spl0_160
| ~ spl0_15
| spl0_225 ),
inference(avatar_split_clause,[],[f2452,f1619,f613,f1294,f1614]) ).
fof(f5030,plain,
( spl0_230
| ~ spl0_292
| ~ spl0_16
| ~ spl0_163 ),
inference(avatar_split_clause,[],[f2833,f1309,f616,f2132,f1644]) ).
fof(f5032,plain,
( spl0_191
| ~ spl0_287
| ~ spl0_16
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f2843,f1114,f616,f2096,f1449]) ).
fof(f5036,plain,
( spl0_190
| spl0_191
| ~ spl0_22
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f3121,f1114,f638,f1449,f1444]) ).
fof(f5038,plain,
( spl0_231
| spl0_230
| ~ spl0_22
| ~ spl0_163 ),
inference(avatar_split_clause,[],[f3842,f1309,f638,f1644,f1649]) ).
fof(f5200,plain,
( ~ c0_1(a2189)
| ~ spl0_6
| ~ spl0_26
| spl0_215 ),
inference(resolution,[],[f4960,f1571]) ).
fof(f5216,plain,
( ~ spl0_150
| ~ spl0_6
| ~ spl0_26
| spl0_215 ),
inference(avatar_split_clause,[],[f5200,f1569,f653,f581,f1246]) ).
fof(f5223,plain,
( spl0_287
| spl0_190
| ~ spl0_9
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f4480,f1114,f592,f1444,f2096]) ).
fof(f5231,plain,
( spl0_239
| ~ spl0_308
| ~ spl0_14
| spl0_240 ),
inference(avatar_split_clause,[],[f2312,f1694,f609,f2388,f1689]) ).
fof(f5232,plain,
( spl0_238
| ~ spl0_165
| ~ spl0_14
| spl0_237 ),
inference(avatar_split_clause,[],[f2313,f1679,f609,f1319,f1684]) ).
fof(f5241,plain,
( spl0_202
| ~ spl0_137
| ~ spl0_14
| spl0_201 ),
inference(avatar_split_clause,[],[f2329,f1499,f609,f1183,f1504]) ).
fof(f5246,plain,
( spl0_180
| ~ spl0_98
| ~ spl0_14
| spl0_181 ),
inference(avatar_split_clause,[],[f2339,f1399,f609,f991,f1394]) ).
fof(f5257,plain,
( ~ spl0_191
| ~ spl0_13
| ~ spl0_18
| ~ spl0_287 ),
inference(avatar_split_clause,[],[f4678,f2096,f625,f606,f1449]) ).
fof(f5376,plain,
( ~ c0_1(a2233)
| ~ spl0_13
| ~ spl0_18
| ~ spl0_125 ),
inference(resolution,[],[f3771,f1126]) ).
fof(f5382,plain,
( ~ spl0_126
| ~ spl0_13
| ~ spl0_18
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f5376,f1124,f625,f606,f1129]) ).
fof(f5408,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_23 ),
inference(resolution,[],[f643,f565]) ).
fof(f5424,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_23 ),
inference(duplicate_literal_removal,[],[f5408]) ).
fof(f5442,plain,
( ~ c0_1(a2206)
| ~ spl0_1
| ~ spl0_23
| ~ spl0_104 ),
inference(resolution,[],[f5424,f1023]) ).
fof(f5454,plain,
( ~ c0_1(a2228)
| c3_1(a2228)
| ~ spl0_29
| spl0_241 ),
inference(resolution,[],[f667,f1701]) ).
fof(f5486,plain,
( spl0_242
| ~ spl0_167
| ~ spl0_29
| spl0_241 ),
inference(avatar_split_clause,[],[f5454,f1699,f666,f1329,f1704]) ).
fof(f5491,plain,
( ~ c1_1(a2252)
| c0_1(a2252)
| ~ spl0_34
| spl0_310 ),
inference(resolution,[],[f690,f2400]) ).
fof(f5495,plain,
( ~ c1_1(a2235)
| c0_1(a2235)
| ~ spl0_34
| spl0_253 ),
inference(resolution,[],[f690,f1761]) ).
fof(f5521,plain,
( ~ c1_1(a2222)
| c0_1(a2222)
| ~ spl0_34
| spl0_190 ),
inference(resolution,[],[f690,f1446]) ).
fof(f5545,plain,
( spl0_191
| ~ spl0_287
| ~ spl0_34
| spl0_190 ),
inference(avatar_split_clause,[],[f5521,f1444,f689,f2096,f1449]) ).
fof(f5563,plain,
( spl0_255
| ~ spl0_297
| ~ spl0_34
| spl0_253 ),
inference(avatar_split_clause,[],[f5495,f1759,f689,f2161,f1769]) ).
fof(f5565,plain,
( spl0_268
| ~ spl0_172
| ~ spl0_34
| spl0_310 ),
inference(avatar_split_clause,[],[f5491,f2398,f689,f1354,f1832]) ).
fof(f5575,plain,
( ~ c1_1(a2242)
| c0_1(a2242)
| ~ spl0_36
| spl0_264 ),
inference(resolution,[],[f699,f1814]) ).
fof(f5581,plain,
( ~ c1_1(a2226)
| c0_1(a2226)
| ~ spl0_36
| spl0_240 ),
inference(resolution,[],[f699,f1696]) ).
fof(f5587,plain,
( ~ c1_1(a2204)
| c0_1(a2204)
| ~ spl0_36
| spl0_225 ),
inference(resolution,[],[f699,f1621]) ).
fof(f5619,plain,
( spl0_278
| ~ spl0_160
| ~ spl0_36
| spl0_225 ),
inference(avatar_split_clause,[],[f5587,f1619,f698,f1294,f1987]) ).
fof(f5624,plain,
( spl0_239
| ~ spl0_166
| ~ spl0_36
| spl0_240 ),
inference(avatar_split_clause,[],[f5581,f1694,f698,f1324,f1689]) ).
fof(f5629,plain,
( spl0_281
| ~ spl0_171
| ~ spl0_36
| spl0_264 ),
inference(avatar_split_clause,[],[f5575,f1812,f698,f1349,f2002]) ).
fof(f5632,plain,
( spl0_221
| ~ spl0_155
| ~ spl0_4
| spl0_305 ),
inference(avatar_split_clause,[],[f2412,f2373,f574,f1269,f1599]) ).
fof(f5635,plain,
( spl0_306
| ~ spl0_157
| ~ spl0_5
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f3001,f1274,f578,f1279,f2378]) ).
fof(f5641,plain,
( ~ spl0_282
| ~ spl0_104
| ~ spl0_20
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f3044,f1031,f632,f1021,f2009]) ).
fof(f5642,plain,
( ~ spl0_282
| ~ spl0_104
| ~ spl0_20
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f3204,f1031,f632,f1021,f2009]) ).
fof(f5644,plain,
( spl0_21
| ~ spl0_13
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f4820,f632,f606,f635]) ).
fof(f5647,plain,
( spl0_232
| ~ spl0_164
| ~ spl0_26
| spl0_233 ),
inference(avatar_split_clause,[],[f4924,f1659,f653,f1314,f1654]) ).
fof(f5648,plain,
( spl0_221
| ~ spl0_155
| ~ spl0_26
| spl0_220 ),
inference(avatar_split_clause,[],[f4929,f1594,f653,f1269,f1599]) ).
fof(f5658,plain,
( ~ spl0_105
| ~ spl0_1
| ~ spl0_23
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f5442,f1021,f642,f564,f1026]) ).
fof(f5665,plain,
( ~ spl0_125
| ~ spl0_126
| ~ spl0_21
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f4842,f1119,f635,f1129,f1124]) ).
fof(f5666,plain,
( ~ spl0_95
| ~ spl0_97
| ~ spl0_21
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f4845,f981,f635,f986,f976]) ).
fof(f5676,plain,
( spl0_21
| ~ spl0_1
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f4819,f632,f564,f635]) ).
fof(f5795,plain,
( ~ c1_1(a2242)
| ~ c3_1(a2242)
| ~ spl0_39
| spl0_264 ),
inference(resolution,[],[f713,f1814]) ).
fof(f5830,plain,
( ~ spl0_170
| ~ spl0_171
| ~ spl0_39
| spl0_264 ),
inference(avatar_split_clause,[],[f5795,f1812,f712,f1349,f1344]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f576]) ).
cnf(s2,plain,
( spl0_2
| ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f583]) ).
cnf(s3,plain,
( spl0_1
| ~ spl0_3
| spl0_4
| spl0_7 ),
inference(sat_conversion,[],[f587]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_6
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f594]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f604]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f611]) ).
cnf(s8,plain,
( spl0_1
| ~ spl0_3
| spl0_13
| spl0_15 ),
inference(sat_conversion,[],[f619]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_13
| spl0_14
| spl0_17 ),
inference(sat_conversion,[],[f623]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_10
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f630]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_20
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f640]) ).
cnf(s12,plain,
( ~ spl0_3
| spl0_20
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f644]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_24
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f655]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_22
| spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f668]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_9
| spl0_22
| ~ spl0_30 ),
inference(sat_conversion,[],[f673]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_17
| spl0_25
| ~ spl0_31 ),
inference(sat_conversion,[],[f678]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_4
| spl0_26
| spl0_32 ),
inference(sat_conversion,[],[f683]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_22
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f691]) ).
cnf(s20,plain,
( spl0_1
| ~ spl0_3
| spl0_14
| spl0_35 ),
inference(sat_conversion,[],[f696]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_16
| spl0_35
| spl0_36 ),
inference(sat_conversion,[],[f700]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_11
| spl0_14
| ~ spl0_30 ),
inference(sat_conversion,[],[f701]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_19
| spl0_26
| ~ spl0_37 ),
inference(sat_conversion,[],[f706]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_15
| ~ spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f714]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_4
| spl0_13
| ~ spl0_40 ),
inference(sat_conversion,[],[f719]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_11
| spl0_16
| spl0_42 ),
inference(sat_conversion,[],[f729]) ).
cnf(s28,plain,
( ~ spl0_3
| spl0_6
| spl0_17
| spl0_24 ),
inference(sat_conversion,[],[f730]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_11
| spl0_17
| spl0_28 ),
inference(sat_conversion,[],[f739]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_7
| spl0_18
| spl0_45 ),
inference(sat_conversion,[],[f744]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_17
| spl0_20
| ~ spl0_46 ),
inference(sat_conversion,[],[f749]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_5
| spl0_20
| spl0_47 ),
inference(sat_conversion,[],[f754]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_34
| ~ spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f801]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_24
| spl0_36
| ~ spl0_57 ),
inference(sat_conversion,[],[f811]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_10
| ~ spl0_61 ),
inference(sat_conversion,[],[f816]) ).
cnf(s44,plain,
( spl0_1
| ~ spl0_3
| spl0_65
| ~ spl0_66 ),
inference(sat_conversion,[],[f839]) ).
cnf(s46,plain,
( ~ spl0_3
| spl0_13
| spl0_62
| spl0_68 ),
inference(sat_conversion,[],[f849]) ).
cnf(s48,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_30
| spl0_70 ),
inference(sat_conversion,[],[f859]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_12
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f877]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_11
| spl0_75 ),
inference(sat_conversion,[],[f882]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_19
| ~ spl0_55 ),
inference(sat_conversion,[],[f883]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_21
| ~ spl0_76
| ~ spl0_77 ),
inference(sat_conversion,[],[f892]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_21
| spl0_42
| spl0_78 ),
inference(sat_conversion,[],[f897]) ).
cnf(s56,plain,
( spl0_61
| spl0_81 ),
inference(sat_conversion,[],[f911]) ).
cnf(s57,plain,
( spl0_61
| spl0_82 ),
inference(sat_conversion,[],[f916]) ).
cnf(s58,plain,
( spl0_61
| spl0_83 ),
inference(sat_conversion,[],[f921]) ).
cnf(s61,plain,
( ~ spl0_78
| spl0_86 ),
inference(sat_conversion,[],[f936]) ).
cnf(s62,plain,
( spl0_38
| spl0_87 ),
inference(sat_conversion,[],[f941]) ).
cnf(s63,plain,
( spl0_38
| spl0_88 ),
inference(sat_conversion,[],[f946]) ).
cnf(s64,plain,
( spl0_37
| spl0_89 ),
inference(sat_conversion,[],[f951]) ).
cnf(s65,plain,
( spl0_37
| spl0_90 ),
inference(sat_conversion,[],[f956]) ).
cnf(s68,plain,
( spl0_94
| spl0_95 ),
inference(sat_conversion,[],[f979]) ).
cnf(s69,plain,
( spl0_94
| spl0_96 ),
inference(sat_conversion,[],[f984]) ).
cnf(s70,plain,
( spl0_94
| spl0_97 ),
inference(sat_conversion,[],[f989]) ).
cnf(s71,plain,
( ~ spl0_74
| spl0_98 ),
inference(sat_conversion,[],[f994]) ).
cnf(s77,plain,
( spl0_30
| spl0_104 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s78,plain,
( spl0_30
| spl0_105 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s79,plain,
( spl0_30
| spl0_106 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s80,plain,
( spl0_107
| spl0_108 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s81,plain,
( spl0_107
| spl0_109 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s82,plain,
( spl0_110
| spl0_111 ),
inference(sat_conversion,[],[f1057]) ).
cnf(s83,plain,
( spl0_110
| spl0_112 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s89,plain,
( ~ spl0_68
| spl0_118 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s90,plain,
( ~ spl0_68
| spl0_119 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s92,plain,
( ~ spl0_62
| spl0_121 ),
inference(sat_conversion,[],[f1107]) ).
cnf(s93,plain,
( ~ spl0_62
| spl0_122 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s94,plain,
( spl0_55
| spl0_123 ),
inference(sat_conversion,[],[f1117]) ).
cnf(s95,plain,
( spl0_66
| spl0_124 ),
inference(sat_conversion,[],[f1122]) ).
cnf(s96,plain,
( spl0_66
| spl0_125 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s97,plain,
( spl0_66
| spl0_126 ),
inference(sat_conversion,[],[f1132]) ).
cnf(s98,plain,
( spl0_31
| spl0_127 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s107,plain,
( spl0_40
| spl0_137 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s114,plain,
( ~ spl0_42
| spl0_146 ),
inference(sat_conversion,[],[f1229]) ).
cnf(s115,plain,
( ~ spl0_42
| spl0_147 ),
inference(sat_conversion,[],[f1234]) ).
cnf(s116,plain,
( ~ spl0_24
| spl0_148 ),
inference(sat_conversion,[],[f1239]) ).
cnf(s117,plain,
( ~ spl0_24
| spl0_149 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s118,plain,
( spl0_57
| spl0_150 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s121,plain,
( ~ spl0_73
| spl0_155 ),
inference(sat_conversion,[],[f1272]) ).
cnf(s122,plain,
( ~ spl0_45
| spl0_156 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s123,plain,
( ~ spl0_45
| spl0_157 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s126,plain,
( ~ spl0_28
| spl0_160 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s127,plain,
( ~ spl0_70
| spl0_161 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s128,plain,
( spl0_77
| spl0_162 ),
inference(sat_conversion,[],[f1307]) ).
cnf(s129,plain,
( spl0_76
| spl0_163 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s130,plain,
( ~ spl0_33
| spl0_164 ),
inference(sat_conversion,[],[f1317]) ).
cnf(s131,plain,
( ~ spl0_58
| spl0_165 ),
inference(sat_conversion,[],[f1322]) ).
cnf(s132,plain,
( ~ spl0_47
| spl0_166 ),
inference(sat_conversion,[],[f1327]) ).
cnf(s133,plain,
( ~ spl0_32
| spl0_167 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s136,plain,
( ~ spl0_35
| spl0_170 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s137,plain,
( ~ spl0_35
| spl0_171 ),
inference(sat_conversion,[],[f1352]) ).
cnf(s138,plain,
( ~ spl0_75
| spl0_172 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s141,plain,
( ~ spl0_78
| ~ spl0_175 ),
inference(sat_conversion,[],[f1372]) ).
cnf(s142,plain,
( ~ spl0_78
| ~ spl0_176 ),
inference(sat_conversion,[],[f1377]) ).
cnf(s143,plain,
( spl0_38
| ~ spl0_177 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s144,plain,
( spl0_37
| ~ spl0_178 ),
inference(sat_conversion,[],[f1387]) ).
cnf(s146,plain,
( ~ spl0_74
| ~ spl0_180 ),
inference(sat_conversion,[],[f1397]) ).
cnf(s147,plain,
( ~ spl0_74
| ~ spl0_181 ),
inference(sat_conversion,[],[f1402]) ).
cnf(s149,plain,
( spl0_107
| ~ spl0_183 ),
inference(sat_conversion,[],[f1412]) ).
cnf(s150,plain,
( spl0_110
| ~ spl0_184 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s155,plain,
( ~ spl0_62
| ~ spl0_189 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s156,plain,
( spl0_55
| ~ spl0_190 ),
inference(sat_conversion,[],[f1447]) ).
cnf(s157,plain,
( spl0_55
| ~ spl0_191 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s158,plain,
( spl0_31
| ~ spl0_192 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s159,plain,
( spl0_31
| ~ spl0_193 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s167,plain,
( spl0_40
| ~ spl0_201 ),
inference(sat_conversion,[],[f1502]) ).
cnf(s168,plain,
( spl0_40
| ~ spl0_202 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s178,plain,
( ~ spl0_42
| ~ spl0_212 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s179,plain,
( ~ spl0_24
| ~ spl0_213 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s180,plain,
( spl0_57
| ~ spl0_214 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s181,plain,
( spl0_57
| ~ spl0_215 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s186,plain,
( ~ spl0_73
| ~ spl0_220 ),
inference(sat_conversion,[],[f1597]) ).
cnf(s187,plain,
( ~ spl0_73
| ~ spl0_221 ),
inference(sat_conversion,[],[f1602]) ).
cnf(s188,plain,
( ~ spl0_45
| ~ spl0_222 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s190,plain,
( ~ spl0_28
| ~ spl0_224 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s191,plain,
( ~ spl0_28
| ~ spl0_225 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s192,plain,
( ~ spl0_70
| ~ spl0_226 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s193,plain,
( ~ spl0_70
| ~ spl0_227 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s194,plain,
( spl0_77
| ~ spl0_228 ),
inference(sat_conversion,[],[f1637]) ).
cnf(s195,plain,
( spl0_77
| ~ spl0_229 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s196,plain,
( spl0_76
| ~ spl0_230 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s197,plain,
( spl0_76
| ~ spl0_231 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s198,plain,
( ~ spl0_33
| ~ spl0_232 ),
inference(sat_conversion,[],[f1657]) ).
cnf(s199,plain,
( ~ spl0_33
| ~ spl0_233 ),
inference(sat_conversion,[],[f1662]) ).
cnf(s203,plain,
( ~ spl0_58
| ~ spl0_237 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s204,plain,
( ~ spl0_58
| ~ spl0_238 ),
inference(sat_conversion,[],[f1687]) ).
cnf(s205,plain,
( ~ spl0_47
| ~ spl0_239 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s206,plain,
( ~ spl0_47
| ~ spl0_240 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s207,plain,
( ~ spl0_32
| ~ spl0_241 ),
inference(sat_conversion,[],[f1702]) ).
cnf(s208,plain,
( ~ spl0_32
| ~ spl0_242 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s216,plain,
( ~ spl0_65
| ~ spl0_250 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s217,plain,
( ~ spl0_65
| ~ spl0_251 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s218,plain,
( ~ spl0_65
| ~ spl0_252 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s219,plain,
( spl0_46
| ~ spl0_253 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s220,plain,
( spl0_46
| ~ spl0_254 ),
inference(sat_conversion,[],[f1767]) ).
cnf(s221,plain,
( spl0_46
| ~ spl0_255 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s228,plain,
( ~ spl0_35
| ~ spl0_264 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s232,plain,
( ~ spl0_75
| ~ spl0_268 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s233,plain,
( ~ spl0_128
| spl0_257
| spl0_261 ),
inference(sat_conversion,[],[f1836]) ).
cnf(s234,plain,
( ~ spl0_38
| ~ spl0_107
| ~ spl0_110 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s235,plain,
( ~ spl0_57
| spl0_73
| ~ spl0_94 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s259,plain,
( spl0_3
| spl0_128 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s292,plain,
( spl0_3
| ~ spl0_257 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s293,plain,
( spl0_3
| ~ spl0_261 ),
inference(sat_conversion,[],[f1896]) ).
cnf(s308,plain,
( ~ spl0_4
| spl0_251
| spl0_252
| ~ spl0_280 ),
inference(sat_conversion,[],[f2000]) ).
cnf(s355,plain,
( ~ spl0_11
| ~ spl0_81
| ~ spl0_82
| spl0_298 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s357,plain,
( ~ spl0_11
| ~ spl0_89
| ~ spl0_90
| spl0_178 ),
inference(sat_conversion,[],[f2189]) ).
cnf(s364,plain,
( ~ spl0_13
| ~ spl0_87
| ~ spl0_88
| spl0_177 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s379,plain,
( ~ spl0_11
| ~ spl0_108
| ~ spl0_109
| spl0_301 ),
inference(sat_conversion,[],[f2406]) ).
cnf(s380,plain,
( ~ spl0_12
| ~ spl0_14
| spl0_183
| ~ spl0_301 ),
inference(sat_conversion,[],[f2425]) ).
cnf(s417,plain,
( ~ spl0_10
| spl0_123
| spl0_191
| spl0_287 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s424,plain,
( ~ spl0_11
| ~ spl0_15
| spl0_231
| ~ spl0_292 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s426,plain,
( ~ spl0_11
| ~ spl0_15
| spl0_190
| ~ spl0_287 ),
inference(sat_conversion,[],[f2628]) ).
cnf(s459,plain,
( ~ spl0_18
| ~ spl0_81
| ~ spl0_82
| ~ spl0_83 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s465,plain,
( ~ spl0_21
| ~ spl0_82
| ~ spl0_83
| ~ spl0_298 ),
inference(sat_conversion,[],[f3079]) ).
cnf(s482,plain,
( ~ spl0_22
| ~ spl0_86
| spl0_176
| spl0_270 ),
inference(sat_conversion,[],[f3136]) ).
cnf(s528,plain,
( ~ spl0_12
| ~ spl0_14
| ~ spl0_147
| spl0_212 ),
inference(sat_conversion,[],[f3185]) ).
cnf(s539,plain,
( ~ spl0_14
| ~ spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f3194]) ).
cnf(s540,plain,
( ~ spl0_14
| spl0_17
| ~ spl0_20 ),
inference(sat_conversion,[],[f3195]) ).
cnf(s549,plain,
( ~ spl0_8
| ~ spl0_86
| spl0_175
| spl0_270 ),
inference(sat_conversion,[],[f3301]) ).
cnf(s550,plain,
( ~ spl0_8
| ~ spl0_123
| spl0_191
| spl0_287 ),
inference(sat_conversion,[],[f3302]) ).
cnf(s557,plain,
( ~ spl0_8
| ~ spl0_163
| spl0_230
| spl0_292 ),
inference(sat_conversion,[],[f3309]) ).
cnf(s574,plain,
( ~ spl0_19
| ~ spl0_104
| ~ spl0_106
| spl0_282 ),
inference(sat_conversion,[],[f3326]) ).
cnf(s592,plain,
( ~ spl0_4
| spl0_190
| ~ spl0_191
| spl0_287 ),
inference(sat_conversion,[],[f3341]) ).
cnf(s597,plain,
( ~ spl0_4
| ~ spl0_157
| spl0_222
| spl0_306 ),
inference(sat_conversion,[],[f3346]) ).
cnf(s653,plain,
( ~ spl0_8
| ~ spl0_10
| spl0_212
| spl0_290 ),
inference(sat_conversion,[],[f3535]) ).
cnf(s676,plain,
( ~ spl0_13
| ~ spl0_160
| spl0_225
| ~ spl0_278 ),
inference(sat_conversion,[],[f3559]) ).
cnf(s707,plain,
( ~ spl0_12
| ~ spl0_146
| ~ spl0_147
| spl0_212 ),
inference(sat_conversion,[],[f3661]) ).
cnf(s744,plain,
( ~ spl0_25
| spl0_250
| spl0_251
| spl0_252 ),
inference(sat_conversion,[],[f4003]) ).
cnf(s749,plain,
( ~ spl0_19
| ~ spl0_146
| ~ spl0_147
| spl0_290 ),
inference(sat_conversion,[],[f4008]) ).
cnf(s763,plain,
( ~ spl0_13
| ~ spl0_167
| spl0_241
| ~ spl0_295 ),
inference(sat_conversion,[],[f4022]) ).
cnf(s766,plain,
( ~ spl0_17
| ~ spl0_118
| ~ spl0_119
| spl0_269 ),
inference(sat_conversion,[],[f4025]) ).
cnf(s768,plain,
( ~ spl0_17
| ~ spl0_109
| spl0_183
| ~ spl0_301 ),
inference(sat_conversion,[],[f4027]) ).
cnf(s769,plain,
( ~ spl0_17
| ~ spl0_111
| ~ spl0_112
| spl0_272 ),
inference(sat_conversion,[],[f4028]) ).
cnf(s778,plain,
( ~ spl0_17
| ~ spl0_166
| spl0_239
| ~ spl0_308 ),
inference(sat_conversion,[],[f4037]) ).
cnf(s781,plain,
( ~ spl0_17
| ~ spl0_170
| ~ spl0_171
| spl0_281 ),
inference(sat_conversion,[],[f4040]) ).
cnf(s803,plain,
( ~ spl0_2
| spl0_224
| spl0_225
| spl0_278 ),
inference(sat_conversion,[],[f4062]) ).
cnf(s807,plain,
( ~ spl0_17
| ~ spl0_172
| spl0_268
| ~ spl0_310 ),
inference(sat_conversion,[],[f4066]) ).
cnf(s818,plain,
( ~ spl0_16
| ~ spl0_108
| ~ spl0_109
| spl0_183 ),
inference(sat_conversion,[],[f4077]) ).
cnf(s828,plain,
( ~ spl0_2
| spl0_239
| spl0_240
| spl0_308 ),
inference(sat_conversion,[],[f4087]) ).
cnf(s846,plain,
( ~ spl0_6
| ~ spl0_148
| spl0_213
| ~ spl0_276 ),
inference(sat_conversion,[],[f4105]) ).
cnf(s858,plain,
( ~ spl0_15
| spl0_253
| spl0_254
| ~ spl0_297 ),
inference(sat_conversion,[],[f4117]) ).
cnf(s867,plain,
( ~ spl0_19
| ~ spl0_156
| spl0_222
| ~ spl0_306 ),
inference(sat_conversion,[],[f4126]) ).
cnf(s868,plain,
( ~ spl0_19
| ~ spl0_148
| ~ spl0_149
| spl0_213 ),
inference(sat_conversion,[],[f4127]) ).
cnf(s873,plain,
( ~ spl0_26
| spl0_250
| spl0_252
| ~ spl0_280 ),
inference(sat_conversion,[],[f4132]) ).
cnf(s878,plain,
( ~ spl0_26
| ~ spl0_161
| spl0_226
| spl0_227 ),
inference(sat_conversion,[],[f4137]) ).
cnf(s889,plain,
( ~ spl0_21
| ~ spl0_170
| ~ spl0_171
| ~ spl0_281 ),
inference(sat_conversion,[],[f4148]) ).
cnf(s896,plain,
( ~ spl0_21
| ~ spl0_118
| ~ spl0_119
| ~ spl0_269 ),
inference(sat_conversion,[],[f4155]) ).
cnf(s922,plain,
( ~ spl0_20
| ~ spl0_146
| ~ spl0_147
| ~ spl0_290 ),
inference(sat_conversion,[],[f4182]) ).
cnf(s923,plain,
( ~ spl0_25
| spl0_241
| spl0_242
| spl0_295 ),
inference(sat_conversion,[],[f4183]) ).
cnf(s942,plain,
( ~ spl0_1
| ~ spl0_155
| spl0_220
| ~ spl0_305 ),
inference(sat_conversion,[],[f4202]) ).
cnf(s947,plain,
( ~ spl0_1
| ~ spl0_121
| ~ spl0_122
| spl0_189 ),
inference(sat_conversion,[],[f4207]) ).
cnf(s954,plain,
( ~ spl0_4
| ~ spl0_150
| spl0_214
| spl0_215 ),
inference(sat_conversion,[],[f4214]) ).
cnf(s959,plain,
( ~ spl0_4
| spl0_175
| spl0_176
| ~ spl0_270 ),
inference(sat_conversion,[],[f4219]) ).
cnf(s961,plain,
( ~ spl0_5
| ~ spl0_81
| ~ spl0_83
| spl0_298 ),
inference(sat_conversion,[],[f4221]) ).
cnf(s984,plain,
( ~ spl0_10
| spl0_250
| spl0_252
| spl0_280 ),
inference(sat_conversion,[],[f4244]) ).
cnf(s1010,plain,
( ~ spl0_13
| ~ spl0_171
| spl0_264
| ~ spl0_281 ),
inference(sat_conversion,[],[f4270]) ).
cnf(s1030,plain,
( ~ spl0_17
| ~ spl0_147
| spl0_212
| ~ spl0_290 ),
inference(sat_conversion,[],[f4290]) ).
cnf(s1056,plain,
( ~ spl0_6
| ~ spl0_105
| ~ spl0_106
| spl0_282 ),
inference(sat_conversion,[],[f4317]) ).
cnf(s1058,plain,
( ~ spl0_6
| ~ spl0_156
| ~ spl0_157
| spl0_222 ),
inference(sat_conversion,[],[f4319]) ).
cnf(s1066,plain,
( ~ spl0_18
| ~ spl0_105
| ~ spl0_106
| ~ spl0_282 ),
inference(sat_conversion,[],[f4327]) ).
cnf(s1070,plain,
( ~ spl0_7
| ~ spl0_149
| spl0_213
| spl0_276 ),
inference(sat_conversion,[],[f4331]) ).
cnf(s1071,plain,
( ~ spl0_7
| ~ spl0_147
| spl0_212
| spl0_290 ),
inference(sat_conversion,[],[f4332]) ).
cnf(s1077,plain,
( ~ spl0_11
| ~ spl0_123
| spl0_190
| ~ spl0_287 ),
inference(sat_conversion,[],[f4338]) ).
cnf(s1101,plain,
( ~ spl0_13
| ~ spl0_112
| spl0_184
| ~ spl0_272 ),
inference(sat_conversion,[],[f4362]) ).
cnf(s1115,plain,
( ~ spl0_10
| spl0_254
| spl0_255
| spl0_297 ),
inference(sat_conversion,[],[f4376]) ).
cnf(s1135,plain,
( ~ spl0_7
| ~ spl0_127
| spl0_192
| spl0_193 ),
inference(sat_conversion,[],[f4461]) ).
cnf(s1136,plain,
( ~ spl0_7
| ~ spl0_162
| spl0_228
| spl0_229 ),
inference(sat_conversion,[],[f4462]) ).
cnf(s1138,plain,
( ~ spl0_9
| ~ spl0_86
| spl0_175
| spl0_176 ),
inference(sat_conversion,[],[f4489]) ).
cnf(s1213,plain,
( spl0_7
| ~ spl0_10
| ~ spl0_12 ),
inference(sat_conversion,[],[f4634]) ).
cnf(s1215,plain,
( spl0_7
| ~ spl0_10
| ~ spl0_19 ),
inference(sat_conversion,[],[f4635]) ).
cnf(s1249,plain,
( ~ spl0_15
| ~ spl0_160
| spl0_224
| spl0_225 ),
inference(sat_conversion,[],[f5013]) ).
cnf(s1280,plain,
( ~ spl0_16
| ~ spl0_163
| spl0_230
| ~ spl0_292 ),
inference(sat_conversion,[],[f5030]) ).
cnf(s1282,plain,
( ~ spl0_16
| ~ spl0_123
| spl0_191
| ~ spl0_287 ),
inference(sat_conversion,[],[f5032]) ).
cnf(s1286,plain,
( ~ spl0_22
| ~ spl0_123
| spl0_190
| spl0_191 ),
inference(sat_conversion,[],[f5036]) ).
cnf(s1288,plain,
( ~ spl0_22
| ~ spl0_163
| spl0_230
| spl0_231 ),
inference(sat_conversion,[],[f5038]) ).
cnf(s1305,plain,
( ~ spl0_6
| ~ spl0_26
| ~ spl0_150
| spl0_215 ),
inference(sat_conversion,[],[f5216]) ).
cnf(s1312,plain,
( ~ spl0_9
| ~ spl0_123
| spl0_190
| spl0_287 ),
inference(sat_conversion,[],[f5223]) ).
cnf(s1320,plain,
( ~ spl0_14
| spl0_239
| spl0_240
| ~ spl0_308 ),
inference(sat_conversion,[],[f5231]) ).
cnf(s1321,plain,
( ~ spl0_14
| ~ spl0_165
| spl0_237
| spl0_238 ),
inference(sat_conversion,[],[f5232]) ).
cnf(s1330,plain,
( ~ spl0_14
| ~ spl0_137
| spl0_201
| spl0_202 ),
inference(sat_conversion,[],[f5241]) ).
cnf(s1335,plain,
( ~ spl0_14
| ~ spl0_98
| spl0_180
| spl0_181 ),
inference(sat_conversion,[],[f5246]) ).
cnf(s1346,plain,
( ~ spl0_13
| ~ spl0_18
| ~ spl0_191
| ~ spl0_287 ),
inference(sat_conversion,[],[f5257]) ).
cnf(s1357,plain,
( ~ spl0_13
| ~ spl0_18
| ~ spl0_125
| ~ spl0_126 ),
inference(sat_conversion,[],[f5382]) ).
cnf(s1364,plain,
( ~ spl0_29
| ~ spl0_167
| spl0_241
| spl0_242 ),
inference(sat_conversion,[],[f5486]) ).
cnf(s1377,plain,
( ~ spl0_34
| spl0_190
| spl0_191
| ~ spl0_287 ),
inference(sat_conversion,[],[f5545]) ).
cnf(s1395,plain,
( ~ spl0_34
| spl0_253
| spl0_255
| ~ spl0_297 ),
inference(sat_conversion,[],[f5563]) ).
cnf(s1397,plain,
( ~ spl0_34
| ~ spl0_172
| spl0_268
| spl0_310 ),
inference(sat_conversion,[],[f5565]) ).
cnf(s1411,plain,
( ~ spl0_36
| ~ spl0_160
| spl0_225
| spl0_278 ),
inference(sat_conversion,[],[f5619]) ).
cnf(s1416,plain,
( ~ spl0_36
| ~ spl0_166
| spl0_239
| spl0_240 ),
inference(sat_conversion,[],[f5624]) ).
cnf(s1421,plain,
( ~ spl0_36
| ~ spl0_171
| spl0_264
| spl0_281 ),
inference(sat_conversion,[],[f5629]) ).
cnf(s1424,plain,
( ~ spl0_4
| ~ spl0_155
| spl0_221
| spl0_305 ),
inference(sat_conversion,[],[f5632]) ).
cnf(s1427,plain,
( ~ spl0_5
| ~ spl0_156
| ~ spl0_157
| spl0_306 ),
inference(sat_conversion,[],[f5635]) ).
cnf(s1433,plain,
( ~ spl0_20
| ~ spl0_104
| ~ spl0_106
| ~ spl0_282 ),
inference(sat_conversion,[],[f5641]) ).
cnf(s1434,plain,
( ~ spl0_20
| ~ spl0_104
| ~ spl0_106
| ~ spl0_282 ),
inference(sat_conversion,[],[f5642]) ).
cnf(s1436,plain,
( ~ spl0_13
| ~ spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f5644]) ).
cnf(s1439,plain,
( ~ spl0_26
| ~ spl0_164
| spl0_232
| spl0_233 ),
inference(sat_conversion,[],[f5647]) ).
cnf(s1440,plain,
( ~ spl0_26
| ~ spl0_155
| spl0_220
| spl0_221 ),
inference(sat_conversion,[],[f5648]) ).
cnf(s1450,plain,
( ~ spl0_1
| ~ spl0_23
| ~ spl0_104
| ~ spl0_105 ),
inference(sat_conversion,[],[f5658]) ).
cnf(s1457,plain,
( ~ spl0_21
| ~ spl0_124
| ~ spl0_125
| ~ spl0_126 ),
inference(sat_conversion,[],[f5665]) ).
cnf(s1458,plain,
( ~ spl0_21
| ~ spl0_95
| ~ spl0_96
| ~ spl0_97 ),
inference(sat_conversion,[],[f5666]) ).
cnf(s1468,plain,
( ~ spl0_1
| ~ spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f5676]) ).
cnf(s1481,plain,
( ~ spl0_39
| ~ spl0_170
| ~ spl0_171
| spl0_264 ),
inference(sat_conversion,[],[f5830]) ).
cnf(s1482,plain,
spl0_3,
inference(rat,[],[s233,s259,s292,s293]) ).
cnf(s1483,plain,
( ~ spl0_45
| ~ spl0_6 ),
inference(rat,[],[s1058,s122,s123,s188]) ).
cnf(s1485,plain,
( spl0_30
| ~ spl0_18
| ~ spl0_6 ),
inference(rat,[],[s1056,s1066,s78,s79]) ).
cnf(s1487,plain,
( spl0_46
| ~ spl0_15
| ~ spl0_10 ),
inference(rat,[],[s858,s1115,s219,s220,s221]) ).
cnf(s1488,plain,
( spl0_17
| ~ spl0_46
| ~ spl0_14 ),
inference(rat,[],[s32,s540,s1482]) ).
cnf(s1491,plain,
( ~ spl0_28
| ~ spl0_15 ),
inference(rat,[],[s1249,s126,s190,s191]) ).
cnf(s1492,plain,
( ~ spl0_58
| ~ spl0_14 ),
inference(rat,[],[s1321,s131,s203,s204]) ).
cnf(s1493,plain,
( spl0_57
| ~ spl0_4 ),
inference(rat,[],[s954,s118,s180,s181]) ).
cnf(s1494,plain,
( ~ spl0_75
| ~ spl0_17
| ~ spl0_34 ),
inference(rat,[],[s807,s1397,s138,s232]) ).
cnf(s1495,plain,
( ~ spl0_123
| spl0_191
| spl0_287
| spl0_190
| ~ spl0_30 ),
inference(rat,[],[s16,s1312,s1286,s1482]) ).
cnf(s1496,plain,
( spl0_61
| ~ spl0_18 ),
inference(rat,[],[s459,s56,s57,s58]) ).
cnf(s1497,plain,
( ~ spl0_287
| spl0_190
| ~ spl0_34
| ~ spl0_14
| ~ spl0_18
| spl0_1 ),
inference(rat,[],[s1494,s51,s1488,s426,s1487,s8,s1346,s1377,s41,s1496,s1482]) ).
cnf(s1498,plain,
( spl0_190
| ~ spl0_14
| ~ spl0_30
| ~ spl0_18
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s417,s1495,s592,s1497,s41,s1496,s38,s1492,s1493,s1482]) ).
cnf(s1503,plain,
( ~ spl0_24
| ~ spl0_19 ),
inference(rat,[],[s868,s116,s117,s179]) ).
cnf(s1508,plain,
( ~ spl0_42
| ~ spl0_17
| ~ spl0_7 ),
inference(rat,[],[s1030,s1071,s115,s178]) ).
cnf(s1510,plain,
( ~ spl0_78
| ~ spl0_9 ),
inference(rat,[],[s1138,s61,s141,s142]) ).
cnf(s1521,plain,
( spl0_66
| ~ spl0_21 ),
inference(rat,[],[s1457,s95,s96,s97]) ).
cnf(s1522,plain,
( ~ spl0_65
| ~ spl0_25 ),
inference(rat,[],[s744,s216,s217,s218]) ).
cnf(s1523,plain,
( ~ spl0_78
| ~ spl0_30
| ~ spl0_4 ),
inference(rat,[],[s16,s482,s959,s1510,s61,s141,s142,s1482]) ).
cnf(s1524,plain,
( ~ spl0_14
| ~ spl0_30
| ~ spl0_18
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s1488,s1508,s1487,s54,s8,s1357,s1521,s96,s97,s44,s1522,s13,s1503,s1215,s52,s156,s1498,s878,s127,s192,s193,s48,s41,s1496,s1523,s1482]) ).
cnf(s1525,plain,
( ~ spl0_17
| ~ spl0_170
| ~ spl0_171
| spl0_264
| spl0_14
| spl0_78
| ~ spl0_10 ),
inference(rat,[],[s1508,s1213,s54,s6,s889,s1010,s781,s1482]) ).
cnf(s1526,plain,
( ~ spl0_18
| ~ spl0_6
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s1495,s1077,s94,s156,s157,s52,s1503,s40,s1421,s1010,s9,s1525,s136,s137,s228,s20,s22,s1524,s1523,s41,s1496,s1485,s1493,s1482]) ).
cnf(s1527,plain,
( ~ spl0_65
| ~ spl0_10
| ~ spl0_4 ),
inference(rat,[],[s984,s308,s216,s217,s218]) ).
cnf(s1528,plain,
( spl0_21
| spl0_42
| ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s11,s1434,s1056,s77,s78,s79,s482,s959,s1523,s61,s141,s142,s54,s1482]) ).
cnf(s1529,plain,
( ~ spl0_35
| ~ spl0_36
| ~ spl0_21 ),
inference(rat,[],[s889,s1421,s136,s137,s228]) ).
cnf(s1530,plain,
( ~ spl0_17
| ~ spl0_6
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s38,s1494,s1492,s51,s20,s355,s1529,s40,s465,s1503,s56,s57,s58,s10,s41,s1527,s44,s1521,s1528,s1508,s1493,s31,s1526,s1483,s1482]) ).
cnf(s1531,plain,
( spl0_31
| ~ spl0_7 ),
inference(rat,[],[s1135,s98,s158,s159]) ).
cnf(s1532,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s846,s1070,s116,s117,s179,s40,s1416,s132,s205,s206,s33,s922,s1071,s114,s115,s178,s1528,s1521,s44,s1522,s17,s1531,s1530,s31,s1526,s1483,s2,s1493,s1,s1482]) ).
cnf(s1533,plain,
( ~ spl0_78
| spl0_6
| ~ spl0_4 ),
inference(rat,[],[s4,s549,s959,s1510,s61,s141,s142,s1482]) ).
cnf(s1534,plain,
( ~ spl0_18
| ~ spl0_17
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s1312,s1377,s38,s94,s156,s157,s1492,s4,s52,s6,s653,s1215,s707,s1030,s1508,s114,s115,s178,s54,s1357,s1521,s96,s97,s44,s1527,s41,s1496,s1493,s1533,s1530,s1482]) ).
cnf(s1535,plain,
( ~ spl0_21
| spl0_2
| spl0_1 ),
inference(rat,[],[s961,s465,s56,s57,s58,s41,s1527,s44,s1521,s1,s1532,s1482]) ).
cnf(s1536,plain,
( ~ spl0_17
| spl0_2
| spl0_1 ),
inference(rat,[],[s1492,s38,s6,s1377,s1436,s1312,s11,s4,s1286,s653,s94,s156,s157,s10,s52,s749,s707,s1030,s114,s115,s178,s54,s1534,s1533,s1530,s1493,s1,s1535,s1482]) ).
cnf(s1539,plain,
( ~ spl0_74
| ~ spl0_14 ),
inference(rat,[],[s1335,s71,s146,s147]) ).
cnf(s1540,plain,
( spl0_77
| ~ spl0_7 ),
inference(rat,[],[s1136,s128,s194,s195]) ).
cnf(s1541,plain,
( ~ spl0_6
| spl0_2
| spl0_1 ),
inference(rat,[],[s1288,s129,s196,s197,s53,s1540,s11,s922,s1071,s114,s115,s178,s31,s1528,s1526,s1483,s1,s1535,s1482]) ).
cnf(s1542,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s9,s1436,s540,s11,s1286,s94,s156,s157,s52,s1503,s28,s1541,s1536,s1535,s1482]) ).
cnf(s1543,plain,
( ~ spl0_6
| ~ spl0_4
| spl0_17
| spl0_1 ),
inference(rat,[],[s11,s922,s1288,s1071,s129,s196,s197,s114,s115,s178,s53,s1528,s1521,s44,s1522,s17,s1540,s1531,s31,s1526,s1483,s1482]) ).
cnf(s1544,plain,
( spl0_21
| spl0_22
| spl0_17 ),
inference(rat,[],[s9,s1436,s540,s11,s1482]) ).
cnf(s1545,plain,
( ~ spl0_4
| spl0_17
| spl0_1 ),
inference(rat,[],[s1496,s10,s41,s1527,s44,s1521,s1544,s1286,s94,s156,s157,s52,s1503,s28,s1543,s1482]) ).
cnf(s1546,plain,
( spl0_17
| spl0_1 ),
inference(rat,[],[s1288,s129,s196,s197,s53,s1544,s1521,s44,s1522,s17,s1540,s1531,s3,s1545,s1482]) ).
cnf(s1547,plain,
( ~ spl0_4
| spl0_21
| spl0_1 ),
inference(rat,[],[s1492,s38,s6,s1377,s1436,s1312,s11,s4,s1286,s653,s94,s156,s157,s10,s52,s749,s707,s1030,s114,s115,s178,s54,s1533,s1534,s1530,s1493,s1546,s1482]) ).
cnf(s1548,plain,
( spl0_21
| spl0_1 ),
inference(rat,[],[s27,s1280,s424,s557,s4,s1056,s1433,s8,s77,s78,s79,s1436,s16,s11,s1288,s129,s196,s197,s1510,s53,s54,s1540,s1508,s3,s1547,s1546,s1482]) ).
cnf(s1549,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s38,s1492,s1494,s20,s51,s1529,s355,s40,s465,s1503,s56,s57,s58,s10,s41,s1527,s1534,s1493,s1546,s44,s1521,s1548,s1482]) ).
cnf(s1550,plain,
( spl0_57
| ~ spl0_26
| ~ spl0_6 ),
inference(rat,[],[s1305,s118,s181]) ).
cnf(s1552,plain,
( ~ spl0_47
| ~ spl0_14
| ~ spl0_2 ),
inference(rat,[],[s828,s1320,s205,s206]) ).
cnf(s1553,plain,
( spl0_40
| ~ spl0_14 ),
inference(rat,[],[s1330,s107,s167,s168]) ).
cnf(s1555,plain,
( ~ spl0_70
| ~ spl0_26 ),
inference(rat,[],[s878,s127,s192,s193]) ).
cnf(s1556,plain,
( spl0_10
| spl0_18
| spl0_47
| spl0_1 ),
inference(rat,[],[s1433,s574,s77,s79,s48,s1555,s33,s961,s13,s465,s1503,s56,s57,s58,s10,s41,s1522,s44,s1521,s1548,s1482]) ).
cnf(s1557,plain,
( ~ spl0_28
| ~ spl0_13
| ~ spl0_2 ),
inference(rat,[],[s676,s803,s126,s190,s191]) ).
cnf(s1558,plain,
( spl0_26
| spl0_28
| spl0_1 ),
inference(rat,[],[s1286,s94,s156,s157,s15,s52,s1364,s1503,s133,s207,s208,s13,s18,s1522,s44,s1521,s1548,s1549,s1482]) ).
cnf(s1559,plain,
( ~ spl0_14
| spl0_1 ),
inference(rat,[],[s1496,s1556,s41,s984,s873,s1558,s1557,s25,s1553,s1552,s1542,s218,s216,s44,s1521,s1548,s1549,s1482]) ).
cnf(s1560,plain,
spl0_1,
inference(rat,[],[s889,s781,s136,s137,s20,s1559,s1548,s1546,s1482]) ).
cnf(s1561,plain,
( spl0_76
| ~ spl0_22 ),
inference(rat,[],[s1288,s129,s196,s197]) ).
cnf(s1563,plain,
( spl0_10
| spl0_7
| ~ spl0_4 ),
inference(rat,[],[s867,s597,s122,s123,s188,s31,s10,s1496,s41,s1482]) ).
cnf(s1564,plain,
( spl0_21
| ~ spl0_4 ),
inference(rat,[],[s1286,s94,s156,s157,s52,s1215,s1563,s1540,s53,s1561,s11,s1468,s1482,s1560]) ).
cnf(s1566,plain,
( spl0_46
| ~ spl0_10
| ~ spl0_34 ),
inference(rat,[],[s1115,s1395,s219,s220,s221]) ).
cnf(s1567,plain,
( spl0_61
| ~ spl0_11
| ~ spl0_21 ),
inference(rat,[],[s355,s465,s56,s57,s58]) ).
cnf(s1568,plain,
( ~ spl0_73
| ~ spl0_4 ),
inference(rat,[],[s942,s1424,s121,s186,s187,s1560]) ).
cnf(s1569,plain,
~ spl0_4,
inference(rat,[],[s1458,s68,s69,s70,s235,s1568,s1564,s1493]) ).
cnf(s1570,plain,
( spl0_10
| spl0_17
| spl0_7 ),
inference(rat,[],[s28,s1483,s1503,s31,s10,s1496,s41,s1482]) ).
cnf(s1571,plain,
( spl0_55
| ~ spl0_22 ),
inference(rat,[],[s1286,s94,s156,s157]) ).
cnf(s1572,plain,
( spl0_20
| spl0_21 ),
inference(rat,[],[s778,s828,s132,s205,s206,s2,s33,s1427,s867,s1483,s122,s123,s188,s31,s1496,s1570,s41,s1215,s52,s1571,s1540,s53,s1561,s11,s1482]) ).
cnf(s1573,plain,
spl0_21,
inference(rat,[],[s1572,s1468,s1560]) ).
cnf(s1575,plain,
( ~ spl0_14
| spl0_17
| spl0_10 ),
inference(rat,[],[s528,s115,s178,s27,s539,s5,s1567,s41,s1482,s1573]) ).
cnf(s1576,plain,
( spl0_17
| spl0_10 ),
inference(rat,[],[s763,s923,s133,s207,s208,s18,s1550,s40,s1411,s676,s9,s1575,s17,s126,s191,s1531,s28,s30,s1570,s1567,s1503,s10,s1496,s41,s1482,s1569,s1573]) ).
cnf(s1577,plain,
( spl0_26
| ~ spl0_13
| spl0_24 ),
inference(rat,[],[s763,s923,s133,s207,s208,s13,s18,s1482,s1569]) ).
cnf(s1586,plain,
( ~ spl0_73
| ~ spl0_26 ),
inference(rat,[],[s1440,s121,s186,s187]) ).
cnf(s1596,plain,
( ~ spl0_33
| ~ spl0_26 ),
inference(rat,[],[s1439,s130,s198,s199]) ).
cnf(s1600,plain,
~ spl0_62,
inference(rat,[],[s947,s92,s93,s155,s1560]) ).
cnf(s1603,plain,
spl0_94,
inference(rat,[],[s1458,s68,s69,s70,s1573]) ).
cnf(s1604,plain,
( spl0_110
| ~ spl0_13
| ~ spl0_17 ),
inference(rat,[],[s769,s1101,s82,s83,s150]) ).
cnf(s1605,plain,
( spl0_107
| ~ spl0_16 ),
inference(rat,[],[s818,s80,s81,s149]) ).
cnf(s1606,plain,
( spl0_38
| ~ spl0_13 ),
inference(rat,[],[s364,s62,s63,s143]) ).
cnf(s1607,plain,
( ~ spl0_14
| spl0_10 ),
inference(rat,[],[s528,s115,s178,s27,s1605,s234,s1606,s1604,s25,s1553,s5,s1567,s41,s1576,s1482,s1569,s1573]) ).
cnf(s1608,plain,
spl0_10,
inference(rat,[],[s766,s896,s89,s90,s46,s1577,s1550,s2,s40,s828,s1416,s778,s132,s205,s206,s33,s1434,s574,s77,s79,s22,s1607,s1576,s1503,s961,s10,s465,s1567,s1496,s56,s57,s58,s41,s1573,s1482,s1600]) ).
cnf(s1609,plain,
( ~ spl0_17
| ~ spl0_12
| ~ spl0_14 ),
inference(rat,[],[s27,s379,s380,s1605,s80,s81,s149,s234,s1508,s1604,s1606,s25,s1553,s1213,s1482,s1608,s1569]) ).
cnf(s1610,plain,
( ~ spl0_26
| ~ spl0_14 ),
inference(rat,[],[s1571,s19,s52,s1566,s1503,s1488,s28,s1609,s1550,s50,s235,s1596,s1586,s1539,s1482,s1608,s1603]) ).
cnf(s1611,plain,
( ~ spl0_35
| ~ spl0_39 ),
inference(rat,[],[s1481,s136,s137,s228]) ).
cnf(s1612,plain,
~ spl0_14,
inference(rat,[],[s234,s1604,s1605,s539,s21,s1611,s1411,s24,s676,s1491,s126,s191,s15,s1571,s52,s1364,s1503,s133,s207,s208,s1577,s18,s1610,s1606,s25,s1553,s1482,s1569]) ).
cnf(s1613,plain,
( ~ spl0_19
| spl0_6
| ~ spl0_13 ),
inference(rat,[],[s27,s379,s768,s1605,s80,s81,s149,s234,s1508,s1604,s28,s1503,s1215,s1606,s1482,s1608]) ).
cnf(s1614,plain,
( ~ spl0_26
| ~ spl0_13 ),
inference(rat,[],[s4,s550,s1312,s1377,s19,s1571,s94,s156,s157,s52,s1613,s1550,s235,s1596,s1586,s1482,s1603]) ).
cnf(s1615,plain,
~ spl0_13,
inference(rat,[],[s4,s1056,s550,s1312,s1433,s1282,s12,s21,s1450,s1611,s1411,s77,s78,s79,s24,s676,s22,s1491,s126,s191,s357,s15,s64,s65,s144,s1571,s94,s156,s157,s23,s52,s1364,s1503,s133,s207,s208,s1577,s18,s1614,s1606,s1482,s1560,s1612,s1569]) ).
cnf(s1617,plain,
spl0_17,
inference(rat,[],[s9,s1612,s1482,s1615]) ).
cnf(s1619,plain,
spl0_68,
inference(rat,[],[s46,s1600,s1482,s1615]) ).
cnf(s1625,plain,
spl0_119,
inference(rat,[],[s90,s1619]) ).
cnf(s1626,plain,
spl0_118,
inference(rat,[],[s89,s1619]) ).
cnf(s1631,plain,
~ spl0_269,
inference(rat,[],[s896,s1625,s1573,s1626]) ).
cnf(s1632,plain,
$false,
inference(rat,[],[s766,s1625,s1617,s1631,s1626]) ).
fof(f5831,plain,
$false,
inference(avatar_sat_refutation,[],[s1632]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN460-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 16:06:04 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.12 Running first-order model finding
% 0.09/0.12 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.09/0.19 % (3486673)Will run a generic schedule for satisfiability detection.
% 0.09/0.19 % (3486679)% WARNING: option uhcvi not known.
% 0.09/0.19 % (3486678)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4242024475_2999 on theBenchmark for (2999ds/0Mi)
% 0.09/0.19 % (3486681)dis+10_1_sil=32000:sp=arity:random_seed=396987513:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.09/0.19 % (3486679)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3594260652:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.09/0.19 % (3486680)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2727005481:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.09/0.19 % (3486682)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3269772265:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.09/0.19 % (3486683)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=207577787:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.09/0.19 % (3486684)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3923514185:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.09/0.19 % Detected minimum model sizes of [1]
% 0.09/0.19 % Detected maximum model sizes of [59]
% 0.09/0.19 % TRYING [1]
% 0.09/0.19 % TRYING [2]
% 0.09/0.19 % TRYING [3]
% 0.09/0.19 % TRYING [4]
% 0.09/0.19 % (3486681)Instruction limit reached!
% 0.09/0.19 % (3486681)------------------------------
% 0.09/0.19 % (3486681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.19 % (3486681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.19 % (3486681)CaDiCaL version: 2.1.3
% 0.09/0.19 % (3486681)Termination reason: Instruction limit
% 0.09/0.19 % (3486681)Termination phase: Saturation
% 0.09/0.19 % (3486681)Time elapsed: 0.035 s
% 0.09/0.19 % (3486681)Peak memory usage: 13 MB
% 0.09/0.19 % (3486681)Instructions burned: 105 (million)
% 0.09/0.19 % (3486684) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3486673-3486684"...
% 0.09/0.19 % TRYING [5]
% 0.09/0.19 % (3486682)Instruction limit reached!
% 0.09/0.19 % (3486682)------------------------------
% 0.09/0.19 % (3486682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.19 % (3486682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.19 % (3486682)CaDiCaL version: 2.1.3
% 0.09/0.19 % (3486682)Termination reason: Instruction limit
% 0.09/0.19 % (3486682)Termination phase: Saturation
% 0.09/0.19 % (3486682)Time elapsed: 0.039 s
% 0.09/0.19 % (3486682)Peak memory usage: 14 MB
% 0.09/0.19 % (3486682)Instructions burned: 117 (million)
% 0.09/0.19 % (3486684)...printing done.
% 0.09/0.19 % (3486684)Refutation found. Thanks to Tanya!
% 0.09/0.19 % SZS status Unsatisfiable for theBenchmark
% 0.09/0.19 % SZS output start Proof for theBenchmark
% See solution above
% 0.09/0.20 % (3486684)------------------------------
% 0.09/0.20 % (3486684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.20 % (3486684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.20 % (3486684)CaDiCaL version: 2.1.3
% 0.09/0.20 % (3486684)Termination reason: Refutation
% 0.09/0.20 % (3486684)Time elapsed: 0.040 s
% 0.09/0.20 % (3486684)Peak memory usage: 14 MB
% 0.09/0.20 % (3486684)Instructions burned: 125 (million)
% 0.09/0.20 % (3486673)Success in time 0.068 s
% 0.09/0.20 % Vampire exiting
%------------------------------------------------------------------------------