%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN439-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 01:50:53 PM UTC 2026
% Result : Unsatisfiable 3.54s 1.17s
% Output : Refutation 4.09s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp52
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f13,negated_conjecture,
( ~ hskp40
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
fof(f22,negated_conjecture,
( ~ hskp31
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
fof(f54,negated_conjecture,
( hskp36
| hskp34
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( hskp16
| hskp17
| hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( hskp6
| hskp27
| hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( hskp40
| hskp31
| hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp52
| c2_1(a595) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp52
| c1_1(a595) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
fof(f61,negated_conjecture,
( ~ hskp51
| c3_1(a583) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp50
| c0_1(a574) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp50
| c1_1(a574) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp49
| c2_1(a568) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f68,negated_conjecture,
( ~ hskp46
| c1_1(a562) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp45
| c0_1(a561) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp44
| c0_1(a559) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp44
| c2_1(a559) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f76,negated_conjecture,
( ~ hskp41
| c3_1(a555) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp41
| c0_1(a555) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp40
| c3_1(a551) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp40
| c2_1(a551) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp39
| c3_1(a549) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp39
| c2_1(a549) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp39
| c1_1(a549) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp38
| c2_1(a547) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ hskp38
| c1_1(a547) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ hskp38
| c0_1(a547) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ hskp37
| c1_1(a544) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ hskp36
| c0_1(a541) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp36
| c1_1(a541) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ hskp36
| c2_1(a541) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ hskp35
| c2_1(a538) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ hskp35
| c1_1(a538) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp35
| c3_1(a538) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ hskp34
| c0_1(a537) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ hskp34
| c3_1(a537) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ hskp33
| c1_1(a536) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ hskp33
| c2_1(a536) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ hskp33
| c0_1(a536) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ hskp32
| c0_1(a596) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f100,negated_conjecture,
( ~ hskp28
| c2_1(a589) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ hskp28
| c3_1(a589) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ hskp27
| c1_1(a586) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ hskp26
| c0_1(a584) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ hskp26
| c1_1(a584) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f106,negated_conjecture,
( ~ hskp23
| c3_1(a578) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ hskp22
| c1_1(a577) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f109,negated_conjecture,
( ~ hskp18
| c0_1(a572) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ hskp17
| c0_1(a571) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ hskp17
| c3_1(a571) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ hskp16
| c3_1(a570) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ hskp16
| c1_1(a570) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f118,negated_conjecture,
( ~ hskp11
| c1_1(a560) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ hskp10
| c3_1(a558) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ hskp7
| c0_1(a550) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ hskp7
| c3_1(a550) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ hskp6
| c3_1(a548) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ hskp5
| c2_1(a546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ hskp4
| c1_1(a545) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f127,negated_conjecture,
( ~ hskp0
| c1_1(a535) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ hskp0
| c0_1(a535) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( ~ c0_1(a595)
| ~ hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ c2_1(a583)
| ~ hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( ~ c3_1(a574)
| ~ hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ c0_1(a568)
| ~ hskp49 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( ~ c1_1(a568)
| ~ hskp49 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f137,negated_conjecture,
( ~ c3_1(a562)
| ~ hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
( ~ c0_1(a562)
| ~ hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
( ~ c3_1(a561)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause139) ).
fof(f140,negated_conjecture,
( ~ c2_1(a561)
| ~ hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
( ~ c3_1(a559)
| ~ hskp44 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause141) ).
fof(f144,negated_conjecture,
( ~ c2_1(a555)
| ~ hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
( ~ c0_1(a551)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
( ~ c2_1(a544)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
( ~ c3_1(a544)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
( ~ c1_1(a537)
| ~ hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
( ~ c3_1(a596)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
( ~ c2_1(a596)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
( ~ c0_1(a594)
| ~ hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
( ~ c3_1(a594)
| ~ hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( ~ c1_1(a594)
| ~ hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause153) ).
fof(f159,negated_conjecture,
( ~ c0_1(a589)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( ~ c0_1(a586)
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( ~ c3_1(a586)
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
( ~ c3_1(a584)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
( ~ c3_1(a582)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
( ~ c2_1(a582)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
( ~ c1_1(a582)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause165) ).
fof(f168,negated_conjecture,
( ~ c0_1(a578)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( ~ c1_1(a578)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
( ~ c3_1(a577)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
( ~ c0_1(a577)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause171) ).
fof(f177,negated_conjecture,
( ~ c2_1(a573)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
( ~ c0_1(a573)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
( ~ c1_1(a573)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
( ~ c3_1(a572)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
( ~ c1_1(a572)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( ~ c2_1(a571)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
( ~ c0_1(a570)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
( ~ c0_1(a569)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
( ~ c1_1(a569)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
( ~ c2_1(a569)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause186) ).
fof(f192,negated_conjecture,
( ~ c3_1(a560)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
( ~ c0_1(a560)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
( ~ c1_1(a558)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
( ~ c0_1(a558)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
( ~ c0_1(a554)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause196) ).
fof(f197,negated_conjecture,
( ~ c2_1(a554)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause197) ).
fof(f198,negated_conjecture,
( ~ c1_1(a554)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause198) ).
fof(f199,negated_conjecture,
( ~ c3_1(a552)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
( ~ c1_1(a552)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
( ~ c2_1(a552)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ c1_1(a550)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ c2_1(a548)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
( ~ c0_1(a548)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
( ~ c3_1(a546)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
( ~ c1_1(a546)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ c2_1(a545)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ c0_1(a545)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause208) ).
fof(f209,negated_conjecture,
( ~ c1_1(a543)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause209) ).
fof(f210,negated_conjecture,
( ~ c0_1(a543)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause210) ).
fof(f211,negated_conjecture,
( ~ c3_1(a543)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause211) ).
fof(f216,negated_conjecture,
( ~ c2_1(a535)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause216) ).
fof(f217,negated_conjecture,
! [X0] :
( ~ ndr1_0
| hskp28
| c1_1(X0)
| c0_1(X0)
| c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp44
| hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
fof(f220,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c1_1(X0)
| hskp19
| hskp50 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause220) ).
fof(f223,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp7
| hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause223) ).
fof(f224,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp9
| hskp41 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause224) ).
fof(f226,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp22
| hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause226) ).
fof(f228,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause228) ).
fof(f230,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| c0_1(X1)
| hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause230) ).
fof(f231,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause231) ).
fof(f232,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause232) ).
fof(f234,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| hskp51 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause234) ).
fof(f235,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause235) ).
fof(f236,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause236) ).
fof(f237,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause237) ).
fof(f238,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X1)
| c1_1(X0)
| c2_1(X0)
| c3_1(X1)
| hskp35 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause238) ).
fof(f239,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause239) ).
fof(f240,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X1)
| c1_1(X0)
| c2_1(X0)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause240) ).
fof(f241,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c3_1(X1)
| c0_1(X1)
| hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause241) ).
fof(f242,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause242) ).
fof(f244,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c2_1(X1)
| hskp49 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X1)
| hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c2_1(X1)
| c0_1(X1)
| hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause247) ).
fof(f248,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause248) ).
fof(f250,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| hskp34 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause250) ).
fof(f251,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1)
| hskp46 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause251) ).
fof(f252,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c3_1(X1)
| hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause252) ).
fof(f253,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause253) ).
fof(f255,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause255) ).
fof(f256,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X1)
| hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause256) ).
fof(f257,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c0_1(X2)
| c0_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause257) ).
fof(f258,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c2_1(X2)
| c3_1(X2)
| c1_1(X2)
| c1_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause258) ).
fof(f259,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X2)
| ~ c3_1(X2)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause259) ).
fof(f260,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c0_1(X2)
| c2_1(X1)
| c1_1(X1)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause260) ).
fof(f262,definition,
( spl0_1
<=> ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| ~ c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f263,plain,
( ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| ~ c1_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f265,definition,
( spl0_2
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f266,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c2_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f271,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f272,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f260,f271,f268,f265,f262]) ).
fof(f275,definition,
( spl0_5
<=> ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f276,plain,
( ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,definition,
( spl0_6
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f279,plain,
( ! [X1] :
( c3_1(X1)
| ~ c2_1(X1)
| c1_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f281,definition,
( spl0_7
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f282,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f283,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f259,f281,f268,f278,f275]) ).
fof(f285,definition,
( spl0_8
<=> ! [X2] :
( c2_1(X2)
| c1_1(X2)
| c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f286,plain,
( ! [X2] :
( c3_1(X2)
| c1_1(X2)
| c2_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f288,definition,
( spl0_9
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f289,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f291,definition,
( spl0_10
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f292,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f293,plain,
( spl0_8
| spl0_9
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f258,f291,f268,f288,f285]) ).
fof(f295,definition,
( spl0_11
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f296,plain,
( ! [X1] :
( c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,definition,
( spl0_12
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f299,plain,
( ! [X0] :
( c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f300,plain,
( spl0_1
| spl0_11
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f257,f298,f268,f295,f262]) ).
fof(f302,definition,
( spl0_13
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f305,definition,
( spl0_14
<=> ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f306,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f307,plain,
( spl0_13
| spl0_10
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f256,f305,f268,f291,f302]) ).
fof(f309,definition,
( spl0_15
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f312,definition,
( spl0_16
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f313,plain,
( ! [X1] :
( c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f315,definition,
( spl0_17
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f316,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f317,plain,
( spl0_15
| spl0_16
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f255,f315,f268,f312,f309]) ).
fof(f323,definition,
( spl0_19
<=> hskp38 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f325,plain,
( spl0_19
| spl0_9
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f253,f305,f268,f288,f323]) ).
fof(f327,definition,
( spl0_20
<=> hskp32 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f330,definition,
( spl0_21
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f331,plain,
( ! [X1] :
( c3_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,definition,
( spl0_22
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f334,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f335,plain,
( spl0_20
| spl0_21
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f252,f333,f268,f330,f327]) ).
fof(f337,definition,
( spl0_23
<=> hskp46 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f339,plain,
( spl0_23
| spl0_12
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f251,f305,f268,f298,f337]) ).
fof(f341,definition,
( spl0_24
<=> hskp34 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f344,definition,
( spl0_25
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f345,plain,
( ! [X1] :
( c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f346,plain,
( spl0_24
| spl0_25
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f250,f271,f268,f344,f341]) ).
fof(f355,definition,
( spl0_28
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f356,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f357,plain,
( spl0_23
| spl0_16
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f248,f355,f268,f312,f337]) ).
fof(f359,definition,
( spl0_29
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f361,plain,
( spl0_29
| spl0_25
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f247,f305,f268,f344,f359]) ).
fof(f363,definition,
( spl0_30
<=> ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f364,plain,
( ! [X1] :
( c0_1(X1)
| ~ c3_1(X1)
| c2_1(X1) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f365,plain,
( spl0_23
| spl0_30
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f246,f291,f268,f363,f337]) ).
fof(f367,definition,
( spl0_31
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f370,definition,
( spl0_32
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f371,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f372,plain,
( spl0_31
| spl0_9
| ~ spl0_3
| spl0_32 ),
inference(avatar_split_clause,[],[f245,f370,f268,f288,f367]) ).
fof(f374,definition,
( spl0_33
<=> hskp49 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f377,definition,
( spl0_34
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f378,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f379,plain,
( spl0_33
| spl0_7
| ~ spl0_3
| spl0_34 ),
inference(avatar_split_clause,[],[f244,f377,f268,f281,f374]) ).
fof(f384,definition,
( spl0_36
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f385,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f388,definition,
( spl0_37
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f391,definition,
( spl0_38
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f392,plain,
( ! [X1] :
( c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f393,plain,
( spl0_37
| spl0_38
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f242,f275,f268,f391,f388]) ).
fof(f395,definition,
( spl0_39
<=> hskp39 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f397,plain,
( spl0_39
| spl0_25
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f241,f291,f268,f344,f395]) ).
fof(f399,definition,
( spl0_40
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f401,plain,
( spl0_40
| spl0_21
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f240,f265,f268,f330,f399]) ).
fof(f403,definition,
( spl0_41
<=> hskp37 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f406,definition,
( spl0_42
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f407,plain,
( ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f408,plain,
( spl0_41
| spl0_42
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f239,f355,f268,f406,f403]) ).
fof(f410,definition,
( spl0_43
<=> hskp35 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f412,plain,
( spl0_43
| spl0_21
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f238,f384,f268,f330,f410]) ).
fof(f413,plain,
( spl0_24
| spl0_8
| spl0_14
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f237,f268,f305,f285,f341]) ).
fof(f415,definition,
( spl0_44
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f417,plain,
( spl0_44
| spl0_8
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f236,f271,f268,f285,f415]) ).
fof(f419,definition,
( spl0_45
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f421,plain,
( spl0_45
| spl0_11
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f235,f344,f268,f295,f419]) ).
fof(f423,definition,
( spl0_46
<=> hskp51 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f425,plain,
( spl0_46
| spl0_8
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f234,f275,f268,f285,f423]) ).
fof(f431,definition,
( spl0_48
<=> hskp45 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f434,definition,
( spl0_49
<=> ! [X1] :
( c2_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f435,plain,
( ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f436,plain,
( spl0_48
| spl0_49
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f232,f262,f268,f434,f431]) ).
fof(f438,definition,
( spl0_50
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f441,definition,
( spl0_51
<=> ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f442,plain,
( ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f444,definition,
( spl0_52
<=> ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f445,plain,
( ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f446,plain,
( spl0_50
| spl0_51
| ~ spl0_3
| spl0_52 ),
inference(avatar_split_clause,[],[f231,f444,f268,f441,f438]) ).
fof(f448,definition,
( spl0_53
<=> hskp33 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f450,plain,
( spl0_53
| spl0_49
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f230,f333,f268,f434,f448]) ).
fof(f458,plain,
( spl0_19
| spl0_8
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f228,f363,f268,f285,f323]) ).
fof(f470,definition,
( spl0_59
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f473,definition,
( spl0_60
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f475,plain,
( spl0_59
| spl0_60
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f226,f333,f268,f473,f470]) ).
fof(f484,definition,
( spl0_63
<=> hskp41 ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f487,definition,
( spl0_64
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f489,plain,
( spl0_63
| spl0_64
| ~ spl0_3
| spl0_52 ),
inference(avatar_split_clause,[],[f224,f444,f268,f487,f484]) ).
fof(f491,definition,
( spl0_65
<=> hskp40 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f494,definition,
( spl0_66
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f496,plain,
( spl0_65
| spl0_66
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f223,f355,f268,f494,f491]) ).
fof(f509,definition,
( spl0_70
<=> hskp50 ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f512,definition,
( spl0_71
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f514,plain,
( spl0_70
| spl0_71
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f220,f384,f268,f512,f509]) ).
fof(f523,definition,
( spl0_74
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f526,definition,
( spl0_75
<=> hskp44 ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f528,plain,
( spl0_74
| spl0_75
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f218,f363,f268,f526,f523]) ).
fof(f530,definition,
( spl0_76
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f532,plain,
( spl0_51
| spl0_76
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f217,f268,f530,f441]) ).
fof(f535,definition,
( spl0_77
<=> c2_1(a535) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f537,plain,
( ~ spl0_44
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f216,f535,f415]) ).
fof(f557,definition,
( spl0_82
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f560,definition,
( spl0_83
<=> c3_1(a543) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f561,plain,
( ~ c3_1(a543)
| spl0_83 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f562,plain,
( ~ spl0_82
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f211,f560,f557]) ).
fof(f564,definition,
( spl0_84
<=> c0_1(a543) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f565,plain,
( ~ c0_1(a543)
| spl0_84 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f566,plain,
( ~ spl0_82
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f210,f564,f557]) ).
fof(f568,definition,
( spl0_85
<=> c1_1(a543) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f570,plain,
( ~ spl0_82
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f209,f568,f557]) ).
fof(f573,definition,
( spl0_86
<=> c0_1(a545) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f574,plain,
( ~ c0_1(a545)
| spl0_86 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f575,plain,
( ~ spl0_29
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f208,f573,f359]) ).
fof(f577,definition,
( spl0_87
<=> c2_1(a545) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f579,plain,
( ~ spl0_29
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f207,f577,f359]) ).
fof(f582,definition,
( spl0_88
<=> c1_1(a546) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f584,plain,
( ~ spl0_40
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f206,f582,f399]) ).
fof(f586,definition,
( spl0_89
<=> c3_1(a546) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f587,plain,
( ~ c3_1(a546)
| spl0_89 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f588,plain,
( ~ spl0_40
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f205,f586,f399]) ).
fof(f591,definition,
( spl0_90
<=> c0_1(a548) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f592,plain,
( ~ c0_1(a548)
| spl0_90 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( ~ spl0_50
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f204,f591,f438]) ).
fof(f595,definition,
( spl0_91
<=> c2_1(a548) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f597,plain,
( ~ spl0_50
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f203,f595,f438]) ).
fof(f600,definition,
( spl0_92
<=> c1_1(a550) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f602,plain,
( ~ spl0_66
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f202,f600,f494]) ).
fof(f605,definition,
( spl0_93
<=> c2_1(a552) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f607,plain,
( ~ spl0_37
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f201,f605,f388]) ).
fof(f609,definition,
( spl0_94
<=> c1_1(a552) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f611,plain,
( ~ spl0_37
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f200,f609,f388]) ).
fof(f613,definition,
( spl0_95
<=> c3_1(a552) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f614,plain,
( ~ c3_1(a552)
| spl0_95 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f615,plain,
( ~ spl0_37
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f199,f613,f388]) ).
fof(f618,definition,
( spl0_96
<=> c1_1(a554) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f620,plain,
( ~ spl0_64
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f198,f618,f487]) ).
fof(f622,definition,
( spl0_97
<=> c2_1(a554) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f624,plain,
( ~ spl0_64
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f197,f622,f487]) ).
fof(f626,definition,
( spl0_98
<=> c0_1(a554) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f627,plain,
( ~ c0_1(a554)
| spl0_98 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f628,plain,
( ~ spl0_64
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f196,f626,f487]) ).
fof(f631,definition,
( spl0_99
<=> c0_1(a558) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f632,plain,
( ~ c0_1(a558)
| spl0_99 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f633,plain,
( ~ spl0_15
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f195,f631,f309]) ).
fof(f635,definition,
( spl0_100
<=> c1_1(a558) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f637,plain,
( ~ spl0_15
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f194,f635,f309]) ).
fof(f640,definition,
( spl0_101
<=> c0_1(a560) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f641,plain,
( ~ c0_1(a560)
| spl0_101 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f642,plain,
( ~ spl0_74
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f193,f640,f523]) ).
fof(f644,definition,
( spl0_102
<=> c3_1(a560) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f645,plain,
( ~ c3_1(a560)
| spl0_102 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f646,plain,
( ~ spl0_74
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f192,f644,f523]) ).
fof(f672,definition,
( spl0_108
<=> c2_1(a569) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f674,plain,
( ~ spl0_31
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f186,f672,f367]) ).
fof(f676,definition,
( spl0_109
<=> c1_1(a569) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f678,plain,
( ~ spl0_31
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f185,f676,f367]) ).
fof(f680,definition,
( spl0_110
<=> c0_1(a569) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f681,plain,
( ~ c0_1(a569)
| spl0_110 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f682,plain,
( ~ spl0_31
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f184,f680,f367]) ).
fof(f684,definition,
( spl0_111
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f687,definition,
( spl0_112
<=> c0_1(a570) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f688,plain,
( ~ c0_1(a570)
| spl0_112 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f689,plain,
( ~ spl0_111
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f183,f687,f684]) ).
fof(f691,definition,
( spl0_113
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f694,definition,
( spl0_114
<=> c2_1(a571) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f696,plain,
( ~ spl0_113
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f182,f694,f691]) ).
fof(f698,definition,
( spl0_115
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f701,definition,
( spl0_116
<=> c1_1(a572) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f703,plain,
( ~ spl0_115
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f181,f701,f698]) ).
fof(f705,definition,
( spl0_117
<=> c3_1(a572) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f706,plain,
( ~ c3_1(a572)
| spl0_117 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f707,plain,
( ~ spl0_115
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f180,f705,f698]) ).
fof(f710,definition,
( spl0_118
<=> c1_1(a573) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f712,plain,
( ~ spl0_71
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f179,f710,f512]) ).
fof(f714,definition,
( spl0_119
<=> c0_1(a573) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f715,plain,
( ~ c0_1(a573)
| spl0_119 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f716,plain,
( ~ spl0_71
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f178,f714,f512]) ).
fof(f718,definition,
( spl0_120
<=> c2_1(a573) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f720,plain,
( ~ spl0_71
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f177,f718,f512]) ).
fof(f745,definition,
( spl0_126
<=> c0_1(a577) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f746,plain,
( ~ c0_1(a577)
| spl0_126 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f747,plain,
( ~ spl0_60
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f171,f745,f473]) ).
fof(f749,definition,
( spl0_127
<=> c3_1(a577) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f750,plain,
( ~ c3_1(a577)
| spl0_127 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f751,plain,
( ~ spl0_60
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f170,f749,f473]) ).
fof(f754,definition,
( spl0_128
<=> c1_1(a578) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f756,plain,
( ~ spl0_59
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f169,f754,f470]) ).
fof(f758,definition,
( spl0_129
<=> c0_1(a578) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f759,plain,
( ~ c0_1(a578)
| spl0_129 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f760,plain,
( ~ spl0_59
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f168,f758,f470]) ).
fof(f772,definition,
( spl0_132
<=> c1_1(a582) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f774,plain,
( ~ spl0_13
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f165,f772,f302]) ).
fof(f776,definition,
( spl0_133
<=> c2_1(a582) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f778,plain,
( ~ spl0_13
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f164,f776,f302]) ).
fof(f780,definition,
( spl0_134
<=> c3_1(a582) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f781,plain,
( ~ c3_1(a582)
| spl0_134 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f782,plain,
( ~ spl0_13
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f163,f780,f302]) ).
fof(f785,definition,
( spl0_135
<=> c3_1(a584) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f786,plain,
( ~ c3_1(a584)
| spl0_135 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f787,plain,
( ~ spl0_45
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f162,f785,f419]) ).
fof(f789,definition,
( spl0_136
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f792,definition,
( spl0_137
<=> c3_1(a586) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f793,plain,
( ~ c3_1(a586)
| spl0_137 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f794,plain,
( ~ spl0_136
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f161,f792,f789]) ).
fof(f796,definition,
( spl0_138
<=> c0_1(a586) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f797,plain,
( ~ c0_1(a586)
| spl0_138 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f798,plain,
( ~ spl0_136
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f160,f796,f789]) ).
fof(f801,definition,
( spl0_139
<=> c0_1(a589) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f802,plain,
( ~ c0_1(a589)
| spl0_139 ),
inference(avatar_component_clause,[],[f801]) ).
fof(f803,plain,
( ~ spl0_76
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f159,f801,f530]) ).
fof(f827,definition,
( spl0_145
<=> hskp31 ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f830,definition,
( spl0_146
<=> c1_1(a594) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f832,plain,
( ~ spl0_145
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f153,f830,f827]) ).
fof(f834,definition,
( spl0_147
<=> c3_1(a594) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f835,plain,
( ~ c3_1(a594)
| spl0_147 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f836,plain,
( ~ spl0_145
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f152,f834,f827]) ).
fof(f838,definition,
( spl0_148
<=> c0_1(a594) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f839,plain,
( ~ c0_1(a594)
| spl0_148 ),
inference(avatar_component_clause,[],[f838]) ).
fof(f840,plain,
( ~ spl0_145
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f151,f838,f827]) ).
fof(f843,definition,
( spl0_149
<=> c2_1(a596) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f845,plain,
( ~ spl0_20
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f150,f843,f327]) ).
fof(f847,definition,
( spl0_150
<=> c3_1(a596) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f848,plain,
( ~ c3_1(a596)
| spl0_150 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f849,plain,
( ~ spl0_20
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f149,f847,f327]) ).
fof(f852,definition,
( spl0_151
<=> c1_1(a537) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f854,plain,
( ~ spl0_24
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f148,f852,f341]) ).
fof(f857,definition,
( spl0_152
<=> c3_1(a544) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f858,plain,
( ~ c3_1(a544)
| spl0_152 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f859,plain,
( ~ spl0_41
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f147,f857,f403]) ).
fof(f861,definition,
( spl0_153
<=> c2_1(a544) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f863,plain,
( ~ spl0_41
| ~ spl0_153 ),
inference(avatar_split_clause,[],[f146,f861,f403]) ).
fof(f866,definition,
( spl0_154
<=> c0_1(a551) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f867,plain,
( ~ c0_1(a551)
| spl0_154 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f868,plain,
( ~ spl0_65
| ~ spl0_154 ),
inference(avatar_split_clause,[],[f145,f866,f491]) ).
fof(f871,definition,
( spl0_155
<=> c2_1(a555) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f873,plain,
( ~ spl0_63
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f144,f871,f484]) ).
fof(f886,definition,
( spl0_158
<=> c3_1(a559) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f887,plain,
( ~ c3_1(a559)
| spl0_158 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f888,plain,
( ~ spl0_75
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f141,f886,f526]) ).
fof(f891,definition,
( spl0_159
<=> c2_1(a561) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f893,plain,
( ~ spl0_48
| ~ spl0_159 ),
inference(avatar_split_clause,[],[f140,f891,f431]) ).
fof(f895,definition,
( spl0_160
<=> c3_1(a561) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f896,plain,
( ~ c3_1(a561)
| spl0_160 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f897,plain,
( ~ spl0_48
| ~ spl0_160 ),
inference(avatar_split_clause,[],[f139,f895,f431]) ).
fof(f900,definition,
( spl0_161
<=> c0_1(a562) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f901,plain,
( ~ c0_1(a562)
| spl0_161 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f902,plain,
( ~ spl0_23
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f138,f900,f337]) ).
fof(f904,definition,
( spl0_162
<=> c3_1(a562) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f905,plain,
( ~ c3_1(a562)
| spl0_162 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f906,plain,
( ~ spl0_23
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f137,f904,f337]) ).
fof(f923,definition,
( spl0_166
<=> c1_1(a568) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f925,plain,
( ~ spl0_33
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f133,f923,f374]) ).
fof(f927,definition,
( spl0_167
<=> c0_1(a568) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f928,plain,
( ~ c0_1(a568)
| spl0_167 ),
inference(avatar_component_clause,[],[f927]) ).
fof(f929,plain,
( ~ spl0_33
| ~ spl0_167 ),
inference(avatar_split_clause,[],[f132,f927,f374]) ).
fof(f932,definition,
( spl0_168
<=> c3_1(a574) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f933,plain,
( ~ c3_1(a574)
| spl0_168 ),
inference(avatar_component_clause,[],[f932]) ).
fof(f934,plain,
( ~ spl0_70
| ~ spl0_168 ),
inference(avatar_split_clause,[],[f131,f932,f509]) ).
fof(f937,definition,
( spl0_169
<=> c2_1(a583) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f939,plain,
( ~ spl0_46
| ~ spl0_169 ),
inference(avatar_split_clause,[],[f130,f937,f423]) ).
fof(f941,definition,
( spl0_170
<=> hskp52 ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f944,definition,
( spl0_171
<=> c0_1(a595) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f945,plain,
( ~ c0_1(a595)
| spl0_171 ),
inference(avatar_component_clause,[],[f944]) ).
fof(f946,plain,
( ~ spl0_170
| ~ spl0_171 ),
inference(avatar_split_clause,[],[f129,f944,f941]) ).
fof(f948,definition,
( spl0_172
<=> c0_1(a535) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f949,plain,
( c0_1(a535)
| ~ spl0_172 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f950,plain,
( spl0_172
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f128,f415,f948]) ).
fof(f952,definition,
( spl0_173
<=> c1_1(a535) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f954,plain,
( spl0_173
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f127,f415,f952]) ).
fof(f964,definition,
( spl0_176
<=> c1_1(a545) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f966,plain,
( spl0_176
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f124,f359,f964]) ).
fof(f968,definition,
( spl0_177
<=> c2_1(a546) ),
introduced(definition,[new_symbols(definition,[spl0_177])],[avatar_definition]) ).
fof(f970,plain,
( spl0_177
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f123,f399,f968]) ).
fof(f972,definition,
( spl0_178
<=> c3_1(a548) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f973,plain,
( c3_1(a548)
| ~ spl0_178 ),
inference(avatar_component_clause,[],[f972]) ).
fof(f974,plain,
( spl0_178
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f122,f438,f972]) ).
fof(f976,definition,
( spl0_179
<=> c3_1(a550) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f978,plain,
( spl0_179
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f121,f494,f976]) ).
fof(f980,definition,
( spl0_180
<=> c0_1(a550) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f981,plain,
( c0_1(a550)
| ~ spl0_180 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f982,plain,
( spl0_180
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f120,f494,f980]) ).
fof(f984,definition,
( spl0_181
<=> c3_1(a558) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f985,plain,
( c3_1(a558)
| ~ spl0_181 ),
inference(avatar_component_clause,[],[f984]) ).
fof(f986,plain,
( spl0_181
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f119,f309,f984]) ).
fof(f988,definition,
( spl0_182
<=> c1_1(a560) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f990,plain,
( spl0_182
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f118,f523,f988]) ).
fof(f1008,definition,
( spl0_187
<=> c1_1(a570) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f1010,plain,
( spl0_187
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f113,f684,f1008]) ).
fof(f1012,definition,
( spl0_188
<=> c3_1(a570) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f1013,plain,
( c3_1(a570)
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1014,plain,
( spl0_188
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f112,f684,f1012]) ).
fof(f1016,definition,
( spl0_189
<=> c3_1(a571) ),
introduced(definition,[new_symbols(definition,[spl0_189])],[avatar_definition]) ).
fof(f1017,plain,
( c3_1(a571)
| ~ spl0_189 ),
inference(avatar_component_clause,[],[f1016]) ).
fof(f1018,plain,
( spl0_189
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f111,f691,f1016]) ).
fof(f1020,definition,
( spl0_190
<=> c0_1(a571) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f1021,plain,
( c0_1(a571)
| ~ spl0_190 ),
inference(avatar_component_clause,[],[f1020]) ).
fof(f1022,plain,
( spl0_190
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f110,f691,f1020]) ).
fof(f1024,definition,
( spl0_191
<=> c0_1(a572) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f1025,plain,
( c0_1(a572)
| ~ spl0_191 ),
inference(avatar_component_clause,[],[f1024]) ).
fof(f1026,plain,
( spl0_191
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f109,f698,f1024]) ).
fof(f1032,definition,
( spl0_193
<=> c1_1(a577) ),
introduced(definition,[new_symbols(definition,[spl0_193])],[avatar_definition]) ).
fof(f1034,plain,
( spl0_193
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f107,f473,f1032]) ).
fof(f1036,definition,
( spl0_194
<=> c3_1(a578) ),
introduced(definition,[new_symbols(definition,[spl0_194])],[avatar_definition]) ).
fof(f1037,plain,
( c3_1(a578)
| ~ spl0_194 ),
inference(avatar_component_clause,[],[f1036]) ).
fof(f1038,plain,
( spl0_194
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f106,f470,f1036]) ).
fof(f1044,definition,
( spl0_196
<=> c1_1(a584) ),
introduced(definition,[new_symbols(definition,[spl0_196])],[avatar_definition]) ).
fof(f1046,plain,
( spl0_196
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f104,f419,f1044]) ).
fof(f1048,definition,
( spl0_197
<=> c0_1(a584) ),
introduced(definition,[new_symbols(definition,[spl0_197])],[avatar_definition]) ).
fof(f1049,plain,
( c0_1(a584)
| ~ spl0_197 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1050,plain,
( spl0_197
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f103,f419,f1048]) ).
fof(f1052,definition,
( spl0_198
<=> c1_1(a586) ),
introduced(definition,[new_symbols(definition,[spl0_198])],[avatar_definition]) ).
fof(f1054,plain,
( spl0_198
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f102,f789,f1052]) ).
fof(f1056,definition,
( spl0_199
<=> c3_1(a589) ),
introduced(definition,[new_symbols(definition,[spl0_199])],[avatar_definition]) ).
fof(f1057,plain,
( c3_1(a589)
| ~ spl0_199 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1058,plain,
( spl0_199
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f101,f530,f1056]) ).
fof(f1060,definition,
( spl0_200
<=> c2_1(a589) ),
introduced(definition,[new_symbols(definition,[spl0_200])],[avatar_definition]) ).
fof(f1062,plain,
( spl0_200
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f100,f530,f1060]) ).
fof(f1068,definition,
( spl0_202
<=> c0_1(a596) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f1069,plain,
( c0_1(a596)
| ~ spl0_202 ),
inference(avatar_component_clause,[],[f1068]) ).
fof(f1070,plain,
( spl0_202
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f98,f327,f1068]) ).
fof(f1072,definition,
( spl0_203
<=> c0_1(a536) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f1073,plain,
( c0_1(a536)
| ~ spl0_203 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1075,plain,
( spl0_203
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f97,f448,f1072]) ).
fof(f1077,definition,
( spl0_204
<=> c2_1(a536) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f1079,plain,
( spl0_204
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f96,f448,f1077]) ).
fof(f1081,definition,
( spl0_205
<=> c1_1(a536) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f1083,plain,
( spl0_205
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f95,f448,f1081]) ).
fof(f1085,definition,
( spl0_206
<=> c3_1(a537) ),
introduced(definition,[new_symbols(definition,[spl0_206])],[avatar_definition]) ).
fof(f1086,plain,
( c3_1(a537)
| ~ spl0_206 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1087,plain,
( spl0_206
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f94,f341,f1085]) ).
fof(f1089,definition,
( spl0_207
<=> c0_1(a537) ),
introduced(definition,[new_symbols(definition,[spl0_207])],[avatar_definition]) ).
fof(f1090,plain,
( c0_1(a537)
| ~ spl0_207 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1091,plain,
( spl0_207
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f93,f341,f1089]) ).
fof(f1093,definition,
( spl0_208
<=> c3_1(a538) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f1094,plain,
( c3_1(a538)
| ~ spl0_208 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1096,plain,
( spl0_208
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f92,f410,f1093]) ).
fof(f1098,definition,
( spl0_209
<=> c1_1(a538) ),
introduced(definition,[new_symbols(definition,[spl0_209])],[avatar_definition]) ).
fof(f1100,plain,
( spl0_209
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f91,f410,f1098]) ).
fof(f1102,definition,
( spl0_210
<=> c2_1(a538) ),
introduced(definition,[new_symbols(definition,[spl0_210])],[avatar_definition]) ).
fof(f1104,plain,
( spl0_210
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f90,f410,f1102]) ).
fof(f1106,definition,
( spl0_211
<=> c2_1(a541) ),
introduced(definition,[new_symbols(definition,[spl0_211])],[avatar_definition]) ).
fof(f1109,definition,
( spl0_212
<=> hskp36 ),
introduced(definition,[new_symbols(definition,[spl0_212])],[avatar_definition]) ).
fof(f1111,plain,
( spl0_211
| ~ spl0_212 ),
inference(avatar_split_clause,[],[f89,f1109,f1106]) ).
fof(f1113,definition,
( spl0_213
<=> c1_1(a541) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f1115,plain,
( spl0_213
| ~ spl0_212 ),
inference(avatar_split_clause,[],[f88,f1109,f1113]) ).
fof(f1117,definition,
( spl0_214
<=> c0_1(a541) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f1118,plain,
( c0_1(a541)
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f1117]) ).
fof(f1119,plain,
( spl0_214
| ~ spl0_212 ),
inference(avatar_split_clause,[],[f87,f1109,f1117]) ).
fof(f1121,definition,
( spl0_215
<=> c1_1(a544) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1123,plain,
( spl0_215
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f86,f403,f1121]) ).
fof(f1125,definition,
( spl0_216
<=> c0_1(a547) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1126,plain,
( c0_1(a547)
| ~ spl0_216 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1128,plain,
( spl0_216
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f85,f323,f1125]) ).
fof(f1130,definition,
( spl0_217
<=> c1_1(a547) ),
introduced(definition,[new_symbols(definition,[spl0_217])],[avatar_definition]) ).
fof(f1132,plain,
( spl0_217
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f84,f323,f1130]) ).
fof(f1134,definition,
( spl0_218
<=> c2_1(a547) ),
introduced(definition,[new_symbols(definition,[spl0_218])],[avatar_definition]) ).
fof(f1136,plain,
( spl0_218
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f83,f323,f1134]) ).
fof(f1138,definition,
( spl0_219
<=> c1_1(a549) ),
introduced(definition,[new_symbols(definition,[spl0_219])],[avatar_definition]) ).
fof(f1141,plain,
( spl0_219
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f82,f395,f1138]) ).
fof(f1143,definition,
( spl0_220
<=> c2_1(a549) ),
introduced(definition,[new_symbols(definition,[spl0_220])],[avatar_definition]) ).
fof(f1145,plain,
( spl0_220
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f81,f395,f1143]) ).
fof(f1147,definition,
( spl0_221
<=> c3_1(a549) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f1148,plain,
( c3_1(a549)
| ~ spl0_221 ),
inference(avatar_component_clause,[],[f1147]) ).
fof(f1149,plain,
( spl0_221
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f80,f395,f1147]) ).
fof(f1151,definition,
( spl0_222
<=> c2_1(a551) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f1153,plain,
( spl0_222
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f79,f491,f1151]) ).
fof(f1155,definition,
( spl0_223
<=> c3_1(a551) ),
introduced(definition,[new_symbols(definition,[spl0_223])],[avatar_definition]) ).
fof(f1156,plain,
( c3_1(a551)
| ~ spl0_223 ),
inference(avatar_component_clause,[],[f1155]) ).
fof(f1157,plain,
( spl0_223
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f78,f491,f1155]) ).
fof(f1159,definition,
( spl0_224
<=> c0_1(a555) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f1160,plain,
( c0_1(a555)
| ~ spl0_224 ),
inference(avatar_component_clause,[],[f1159]) ).
fof(f1161,plain,
( spl0_224
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f77,f484,f1159]) ).
fof(f1163,definition,
( spl0_225
<=> c3_1(a555) ),
introduced(definition,[new_symbols(definition,[spl0_225])],[avatar_definition]) ).
fof(f1164,plain,
( c3_1(a555)
| ~ spl0_225 ),
inference(avatar_component_clause,[],[f1163]) ).
fof(f1165,plain,
( spl0_225
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f76,f484,f1163]) ).
fof(f1183,definition,
( spl0_230
<=> c2_1(a559) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1185,plain,
( spl0_230
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f71,f526,f1183]) ).
fof(f1187,definition,
( spl0_231
<=> c0_1(a559) ),
introduced(definition,[new_symbols(definition,[spl0_231])],[avatar_definition]) ).
fof(f1188,plain,
( c0_1(a559)
| ~ spl0_231 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1189,plain,
( spl0_231
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f70,f526,f1187]) ).
fof(f1191,definition,
( spl0_232
<=> c0_1(a561) ),
introduced(definition,[new_symbols(definition,[spl0_232])],[avatar_definition]) ).
fof(f1192,plain,
( c0_1(a561)
| ~ spl0_232 ),
inference(avatar_component_clause,[],[f1191]) ).
fof(f1193,plain,
( spl0_232
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f69,f431,f1191]) ).
fof(f1195,definition,
( spl0_233
<=> c1_1(a562) ),
introduced(definition,[new_symbols(definition,[spl0_233])],[avatar_definition]) ).
fof(f1197,plain,
( spl0_233
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f68,f337,f1195]) ).
fof(f1211,definition,
( spl0_237
<=> c2_1(a568) ),
introduced(definition,[new_symbols(definition,[spl0_237])],[avatar_definition]) ).
fof(f1213,plain,
( spl0_237
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f64,f374,f1211]) ).
fof(f1215,definition,
( spl0_238
<=> c1_1(a574) ),
introduced(definition,[new_symbols(definition,[spl0_238])],[avatar_definition]) ).
fof(f1217,plain,
( spl0_238
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f63,f509,f1215]) ).
fof(f1219,definition,
( spl0_239
<=> c0_1(a574) ),
introduced(definition,[new_symbols(definition,[spl0_239])],[avatar_definition]) ).
fof(f1220,plain,
( c0_1(a574)
| ~ spl0_239 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1221,plain,
( spl0_239
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f62,f509,f1219]) ).
fof(f1223,definition,
( spl0_240
<=> c3_1(a583) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1224,plain,
( c3_1(a583)
| ~ spl0_240 ),
inference(avatar_component_clause,[],[f1223]) ).
fof(f1225,plain,
( spl0_240
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f61,f423,f1223]) ).
fof(f1231,definition,
( spl0_242
<=> c1_1(a595) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f1233,plain,
( spl0_242
| ~ spl0_170 ),
inference(avatar_split_clause,[],[f59,f941,f1231]) ).
fof(f1235,definition,
( spl0_243
<=> c2_1(a595) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f1237,plain,
( spl0_243
| ~ spl0_170 ),
inference(avatar_split_clause,[],[f58,f941,f1235]) ).
fof(f1240,plain,
( spl0_170
| spl0_145
| spl0_65 ),
inference(avatar_split_clause,[],[f57,f491,f827,f941]) ).
fof(f1242,plain,
( spl0_29
| spl0_136
| spl0_50 ),
inference(avatar_split_clause,[],[f56,f438,f789,f359]) ).
fof(f1246,plain,
( spl0_115
| spl0_113
| spl0_111 ),
inference(avatar_split_clause,[],[f55,f684,f691,f698]) ).
fof(f1249,plain,
( spl0_82
| spl0_24
| spl0_212 ),
inference(avatar_split_clause,[],[f54,f1109,f341,f557]) ).
fof(f1282,plain,
( spl0_3
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f22,f827,f268]) ).
fof(f1291,plain,
( spl0_3
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f13,f491,f268]) ).
fof(f1303,plain,
( spl0_3
| ~ spl0_170 ),
inference(avatar_split_clause,[],[f1,f941,f268]) ).
fof(f1310,definition,
( spl0_244
<=> c2_1(a594) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f1315,definition,
( spl0_245
<=> c2_1(a543) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f1323,definition,
( spl0_246
<=> c2_1(a570) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f1352,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_12 ),
inference(resolution,[],[f299,f272]) ).
fof(f1356,plain,
( c3_1(a594)
| ~ c2_1(a594)
| ~ spl0_12
| spl0_148 ),
inference(resolution,[],[f299,f839]) ).
fof(f1359,plain,
( c3_1(a543)
| ~ c2_1(a543)
| ~ spl0_12
| spl0_84 ),
inference(resolution,[],[f299,f565]) ).
fof(f1361,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f1352]) ).
fof(f1372,plain,
( ~ spl0_244
| spl0_147
| ~ spl0_12
| spl0_148 ),
inference(avatar_split_clause,[],[f1356,f838,f298,f834,f1310]) ).
fof(f1373,plain,
( spl0_21
| ~ spl0_4
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1361,f298,f271,f330]) ).
fof(f1380,plain,
( ~ c2_1(a570)
| ~ c1_1(a570)
| ~ spl0_16
| spl0_112 ),
inference(resolution,[],[f313,f688]) ).
fof(f1407,plain,
( ~ c1_1(a545)
| c3_1(a545)
| ~ spl0_25
| spl0_86 ),
inference(resolution,[],[f345,f574]) ).
fof(f1421,definition,
( spl0_251
<=> c3_1(a545) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f1422,plain,
( c3_1(a545)
| ~ spl0_251 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1430,definition,
( spl0_252
<=> c1_1(a548) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f1438,plain,
( ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_12
| ~ spl0_28 ),
inference(resolution,[],[f356,f299]) ).
fof(f1439,plain,
( ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_12
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f1438]) ).
fof(f1441,plain,
( spl0_6
| ~ spl0_12
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f1439,f355,f298,f278]) ).
fof(f1450,plain,
( c1_1(a550)
| ~ c3_1(a550)
| ~ spl0_5
| ~ spl0_180 ),
inference(resolution,[],[f981,f276]) ).
fof(f1453,plain,
( ~ spl0_179
| spl0_92
| ~ spl0_5
| ~ spl0_180 ),
inference(avatar_split_clause,[],[f1450,f980,f275,f600,f976]) ).
fof(f1454,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_25 ),
inference(resolution,[],[f263,f345]) ).
fof(f1457,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_25 ),
inference(duplicate_literal_removal,[],[f1454]) ).
fof(f1458,plain,
( spl0_32
| ~ spl0_1
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1457,f344,f262,f370]) ).
fof(f1463,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_30 ),
inference(resolution,[],[f364,f263]) ).
fof(f1465,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_30 ),
inference(resolution,[],[f364,f276]) ).
fof(f1469,plain,
( ~ c3_1(a548)
| c2_1(a548)
| ~ spl0_30
| spl0_90 ),
inference(resolution,[],[f364,f592]) ).
fof(f1475,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) )
| ~ spl0_5
| ~ spl0_30 ),
inference(duplicate_literal_removal,[],[f1465]) ).
fof(f1476,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_30 ),
inference(duplicate_literal_removal,[],[f1463]) ).
fof(f1481,plain,
( spl0_91
| ~ spl0_178
| ~ spl0_30
| spl0_90 ),
inference(avatar_split_clause,[],[f1469,f591,f363,f972,f595]) ).
fof(f1485,plain,
( spl0_2
| ~ spl0_5
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f1475,f363,f275,f265]) ).
fof(f1486,plain,
( spl0_10
| ~ spl0_1
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f1476,f363,f262,f291]) ).
fof(f1496,definition,
( spl0_254
<=> c2_1(a586) ),
introduced(definition,[new_symbols(definition,[spl0_254])],[avatar_definition]) ).
fof(f1515,definition,
( spl0_255
<=> c1_1(a571) ),
introduced(definition,[new_symbols(definition,[spl0_255])],[avatar_definition]) ).
fof(f1522,plain,
( ~ c3_1(a545)
| c2_1(a545)
| ~ spl0_30
| spl0_86 ),
inference(resolution,[],[f574,f364]) ).
fof(f1525,plain,
( ~ c3_1(a545)
| spl0_251 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1526,plain,
( spl0_87
| ~ spl0_251
| ~ spl0_30
| spl0_86 ),
inference(avatar_split_clause,[],[f1522,f573,f363,f1421,f577]) ).
fof(f1532,definition,
( spl0_256
<=> c2_1(a562) ),
introduced(definition,[new_symbols(definition,[spl0_256])],[avatar_definition]) ).
fof(f1553,plain,
( c1_1(a537)
| ~ c2_1(a537)
| ~ spl0_28
| ~ spl0_207 ),
inference(resolution,[],[f1090,f356]) ).
fof(f1555,plain,
( c1_1(a537)
| ~ c3_1(a537)
| ~ spl0_5
| ~ spl0_207 ),
inference(resolution,[],[f1090,f276]) ).
fof(f1558,plain,
( ~ spl0_206
| spl0_151
| ~ spl0_5
| ~ spl0_207 ),
inference(avatar_split_clause,[],[f1555,f1089,f275,f852,f1085]) ).
fof(f1560,definition,
( spl0_258
<=> c2_1(a537) ),
introduced(definition,[new_symbols(definition,[spl0_258])],[avatar_definition]) ).
fof(f1581,definition,
( spl0_259
<=> c1_1(a551) ),
introduced(definition,[new_symbols(definition,[spl0_259])],[avatar_definition]) ).
fof(f1602,plain,
( c2_1(a537)
| ~ c3_1(a537)
| ~ spl0_7
| ~ spl0_207 ),
inference(resolution,[],[f282,f1090]) ).
fof(f1603,plain,
( c2_1(a571)
| ~ c3_1(a571)
| ~ spl0_7
| ~ spl0_190 ),
inference(resolution,[],[f282,f1021]) ).
fof(f1605,plain,
( ~ spl0_189
| spl0_114
| ~ spl0_7
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f1603,f1020,f281,f694,f1016]) ).
fof(f1606,plain,
( ~ spl0_206
| spl0_258
| ~ spl0_7
| ~ spl0_207 ),
inference(avatar_split_clause,[],[f1602,f1089,f281,f1560,f1085]) ).
fof(f1612,plain,
( ~ spl0_245
| spl0_83
| ~ spl0_12
| spl0_84 ),
inference(avatar_split_clause,[],[f1359,f564,f298,f560,f1315]) ).
fof(f1615,plain,
( c3_1(a584)
| ~ c1_1(a584)
| ~ spl0_22
| ~ spl0_197 ),
inference(resolution,[],[f1049,f334]) ).
fof(f1635,plain,
( c1_1(a582)
| c2_1(a582)
| ~ spl0_8
| spl0_134 ),
inference(resolution,[],[f286,f781]) ).
fof(f1643,plain,
( spl0_133
| spl0_132
| ~ spl0_8
| spl0_134 ),
inference(avatar_split_clause,[],[f1635,f780,f285,f772,f776]) ).
fof(f1676,plain,
( c1_1(a572)
| c2_1(a572)
| ~ spl0_8
| spl0_117 ),
inference(resolution,[],[f706,f286]) ).
fof(f1680,definition,
( spl0_261
<=> c2_1(a572) ),
introduced(definition,[new_symbols(definition,[spl0_261])],[avatar_definition]) ).
fof(f1684,plain,
( spl0_261
| spl0_116
| ~ spl0_8
| spl0_117 ),
inference(avatar_split_clause,[],[f1676,f705,f285,f701,f1680]) ).
fof(f1743,plain,
( c1_1(a551)
| ~ c3_1(a551)
| ~ spl0_11
| spl0_154 ),
inference(resolution,[],[f296,f867]) ).
fof(f1747,plain,
( c1_1(a548)
| ~ c3_1(a548)
| ~ spl0_11
| spl0_90 ),
inference(resolution,[],[f296,f592]) ).
fof(f1754,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_11
| ~ spl0_17 ),
inference(resolution,[],[f316,f296]) ).
fof(f1760,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_11
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1754]) ).
fof(f1764,plain,
( spl0_9
| ~ spl0_11
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1760,f315,f295,f288]) ).
fof(f1765,plain,
( c1_1(a558)
| ~ c3_1(a558)
| ~ spl0_11
| spl0_99 ),
inference(resolution,[],[f632,f296]) ).
fof(f1768,definition,
( spl0_262
<=> c2_1(a558) ),
introduced(definition,[new_symbols(definition,[spl0_262])],[avatar_definition]) ).
fof(f1774,plain,
( ~ c3_1(a578)
| c2_1(a578)
| ~ spl0_30
| spl0_129 ),
inference(resolution,[],[f759,f364]) ).
fof(f1776,definition,
( spl0_263
<=> c2_1(a578) ),
introduced(definition,[new_symbols(definition,[spl0_263])],[avatar_definition]) ).
fof(f1779,plain,
( spl0_263
| ~ spl0_194
| ~ spl0_30
| spl0_129 ),
inference(avatar_split_clause,[],[f1774,f758,f363,f1036,f1776]) ).
fof(f1782,definition,
( spl0_264
<=> c2_1(a577) ),
introduced(definition,[new_symbols(definition,[spl0_264])],[avatar_definition]) ).
fof(f1794,definition,
( spl0_265
<=> c1_1(a596) ),
introduced(definition,[new_symbols(definition,[spl0_265])],[avatar_definition]) ).
fof(f1841,plain,
( c2_1(a586)
| ~ c1_1(a586)
| ~ spl0_32
| spl0_137 ),
inference(resolution,[],[f371,f793]) ).
fof(f1857,definition,
( spl0_266
<=> c2_1(a584) ),
introduced(definition,[new_symbols(definition,[spl0_266])],[avatar_definition]) ).
fof(f1861,plain,
( ~ spl0_198
| spl0_254
| ~ spl0_32
| spl0_137 ),
inference(avatar_split_clause,[],[f1841,f792,f370,f1496,f1052]) ).
fof(f1866,plain,
( ~ c3_1(a569)
| c2_1(a569)
| ~ spl0_30
| spl0_110 ),
inference(resolution,[],[f681,f364]) ).
fof(f1869,definition,
( spl0_267
<=> c3_1(a569) ),
introduced(definition,[new_symbols(definition,[spl0_267])],[avatar_definition]) ).
fof(f1878,plain,
( c3_1(a584)
| c2_1(a584)
| ~ spl0_34
| ~ spl0_197 ),
inference(resolution,[],[f378,f1049]) ).
fof(f1915,plain,
( c1_1(a551)
| ~ c2_1(a551)
| ~ spl0_38
| spl0_154 ),
inference(resolution,[],[f392,f867]) ).
fof(f1921,plain,
( c1_1(a558)
| ~ c2_1(a558)
| ~ spl0_38
| spl0_99 ),
inference(resolution,[],[f392,f632]) ).
fof(f1933,plain,
( c1_1(a552)
| c2_1(a552)
| ~ spl0_8
| spl0_95 ),
inference(resolution,[],[f614,f286]) ).
fof(f1937,plain,
( spl0_93
| spl0_94
| ~ spl0_8
| spl0_95 ),
inference(avatar_split_clause,[],[f1933,f613,f285,f609,f605]) ).
fof(f1942,plain,
( ~ spl0_223
| spl0_259
| ~ spl0_11
| spl0_154 ),
inference(avatar_split_clause,[],[f1743,f866,f295,f1581,f1155]) ).
fof(f1956,plain,
( ~ c2_1(a541)
| ~ c1_1(a541)
| ~ spl0_4
| ~ spl0_214 ),
inference(resolution,[],[f272,f1118]) ).
fof(f1958,plain,
( ~ c2_1(a584)
| ~ c1_1(a584)
| ~ spl0_4
| ~ spl0_197 ),
inference(resolution,[],[f272,f1049]) ).
fof(f1967,plain,
( spl0_251
| ~ spl0_176
| ~ spl0_25
| spl0_86 ),
inference(avatar_split_clause,[],[f1407,f573,f344,f964,f1421]) ).
fof(f1969,plain,
( ~ spl0_178
| spl0_252
| ~ spl0_11
| spl0_90 ),
inference(avatar_split_clause,[],[f1747,f591,f295,f1430,f972]) ).
fof(f1980,definition,
( spl0_270
<=> c2_1(a560) ),
introduced(definition,[new_symbols(definition,[spl0_270])],[avatar_definition]) ).
fof(f2069,plain,
( ~ c1_1(a537)
| ~ c2_1(a537)
| ~ spl0_14
| ~ spl0_206 ),
inference(resolution,[],[f306,f1086]) ).
fof(f2127,plain,
( ~ c1_1(a562)
| c3_1(a562)
| ~ spl0_25
| spl0_161 ),
inference(resolution,[],[f345,f901]) ).
fof(f2130,plain,
( ~ c1_1(a586)
| c3_1(a586)
| ~ spl0_25
| spl0_138 ),
inference(resolution,[],[f345,f797]) ).
fof(f2144,plain,
( spl0_137
| ~ spl0_198
| ~ spl0_25
| spl0_138 ),
inference(avatar_split_clause,[],[f2130,f796,f344,f1052,f792]) ).
fof(f2148,plain,
( spl0_162
| ~ spl0_233
| ~ spl0_25
| spl0_161 ),
inference(avatar_split_clause,[],[f2127,f900,f344,f1195,f904]) ).
fof(f2156,plain,
( ~ c2_1(a559)
| c1_1(a559)
| ~ spl0_6
| spl0_158 ),
inference(resolution,[],[f887,f279]) ).
fof(f2158,definition,
( spl0_273
<=> c1_1(a559) ),
introduced(definition,[new_symbols(definition,[spl0_273])],[avatar_definition]) ).
fof(f2161,plain,
( spl0_273
| ~ spl0_230
| ~ spl0_6
| spl0_158 ),
inference(avatar_split_clause,[],[f2156,f886,f278,f1183,f2158]) ).
fof(f2180,plain,
( c2_1(a537)
| ~ c1_1(a537)
| ~ spl0_10
| ~ spl0_206 ),
inference(resolution,[],[f292,f1086]) ).
fof(f2183,plain,
( c2_1(a570)
| ~ c1_1(a570)
| ~ spl0_10
| ~ spl0_188 ),
inference(resolution,[],[f292,f1013]) ).
fof(f2184,plain,
( c2_1(a548)
| ~ c1_1(a548)
| ~ spl0_10
| ~ spl0_178 ),
inference(resolution,[],[f292,f973]) ).
fof(f2185,plain,
( c2_1(a545)
| ~ c1_1(a545)
| ~ spl0_10
| ~ spl0_251 ),
inference(resolution,[],[f292,f1422]) ).
fof(f2191,plain,
( ~ spl0_176
| spl0_87
| ~ spl0_10
| ~ spl0_251 ),
inference(avatar_split_clause,[],[f2185,f1421,f291,f577,f964]) ).
fof(f2192,plain,
( ~ spl0_252
| spl0_91
| ~ spl0_10
| ~ spl0_178 ),
inference(avatar_split_clause,[],[f2184,f972,f291,f595,f1430]) ).
fof(f2193,plain,
( ~ spl0_187
| spl0_246
| ~ spl0_10
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f2183,f1012,f291,f1323,f1008]) ).
fof(f2205,plain,
( ~ spl0_187
| ~ spl0_246
| ~ spl0_16
| spl0_112 ),
inference(avatar_split_clause,[],[f1380,f687,f312,f1323,f1008]) ).
fof(f2215,plain,
( ~ spl0_222
| spl0_259
| ~ spl0_38
| spl0_154 ),
inference(avatar_split_clause,[],[f1915,f866,f391,f1581,f1151]) ).
fof(f2218,plain,
( ~ spl0_262
| spl0_100
| ~ spl0_38
| spl0_99 ),
inference(avatar_split_clause,[],[f1921,f631,f391,f635,f1768]) ).
fof(f2231,definition,
( spl0_274
<=> c2_1(a574) ),
introduced(definition,[new_symbols(definition,[spl0_274])],[avatar_definition]) ).
fof(f2238,definition,
( spl0_275
<=> c3_1(a595) ),
introduced(definition,[new_symbols(definition,[spl0_275])],[avatar_definition]) ).
fof(f2250,plain,
( c2_1(a574)
| ~ c1_1(a574)
| ~ spl0_1
| ~ spl0_239 ),
inference(resolution,[],[f263,f1220]) ).
fof(f2255,plain,
( c2_1(a596)
| ~ c1_1(a596)
| ~ spl0_1
| ~ spl0_202 ),
inference(resolution,[],[f263,f1069]) ).
fof(f2265,plain,
( ~ spl0_238
| spl0_274
| ~ spl0_1
| ~ spl0_239 ),
inference(avatar_split_clause,[],[f2250,f1219,f262,f2231,f1215]) ).
fof(f2297,plain,
( c1_1(a551)
| ~ c2_1(a551)
| ~ spl0_9
| ~ spl0_223 ),
inference(resolution,[],[f289,f1156]) ).
fof(f2311,plain,
( ~ spl0_222
| spl0_259
| ~ spl0_9
| ~ spl0_223 ),
inference(avatar_split_clause,[],[f2297,f1155,f288,f1581,f1151]) ).
fof(f2318,plain,
( ~ c1_1(a551)
| ~ c2_1(a551)
| ~ spl0_14
| ~ spl0_223 ),
inference(resolution,[],[f306,f1156]) ).
fof(f2319,plain,
( ~ c1_1(a549)
| ~ c2_1(a549)
| ~ spl0_14
| ~ spl0_221 ),
inference(resolution,[],[f306,f1148]) ).
fof(f2321,plain,
( ~ c1_1(a570)
| ~ c2_1(a570)
| ~ spl0_14
| ~ spl0_188 ),
inference(resolution,[],[f306,f1013]) ).
fof(f2325,plain,
( ~ spl0_220
| ~ spl0_219
| ~ spl0_14
| ~ spl0_221 ),
inference(avatar_split_clause,[],[f2319,f1147,f305,f1138,f1143]) ).
fof(f2383,plain,
( c1_1(a559)
| ~ c2_1(a559)
| ~ spl0_28
| ~ spl0_231 ),
inference(resolution,[],[f356,f1188]) ).
fof(f2387,plain,
( c1_1(a572)
| ~ c2_1(a572)
| ~ spl0_28
| ~ spl0_191 ),
inference(resolution,[],[f356,f1025]) ).
fof(f2393,plain,
( ~ spl0_196
| ~ spl0_266
| ~ spl0_4
| ~ spl0_197 ),
inference(avatar_split_clause,[],[f1958,f1048,f271,f1857,f1044]) ).
fof(f2405,plain,
( ~ spl0_196
| spl0_135
| ~ spl0_22
| ~ spl0_197 ),
inference(avatar_split_clause,[],[f1615,f1048,f333,f785,f1044]) ).
fof(f2440,plain,
( ~ c2_1(a559)
| ~ c1_1(a559)
| ~ spl0_4
| ~ spl0_231 ),
inference(resolution,[],[f272,f1188]) ).
fof(f2441,plain,
( ~ spl0_273
| ~ spl0_230
| ~ spl0_4
| ~ spl0_231 ),
inference(avatar_split_clause,[],[f2440,f1187,f271,f1183,f2158]) ).
fof(f2449,plain,
( ! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(resolution,[],[f296,f282]) ).
fof(f2455,plain,
( c1_1(a578)
| ~ c3_1(a578)
| ~ spl0_11
| spl0_129 ),
inference(resolution,[],[f296,f759]) ).
fof(f2464,plain,
( ! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f2449]) ).
fof(f2473,plain,
( ~ spl0_194
| spl0_128
| ~ spl0_11
| spl0_129 ),
inference(avatar_split_clause,[],[f2455,f758,f295,f754,f1036]) ).
fof(f2475,plain,
( spl0_2
| ~ spl0_7
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f2464,f295,f281,f265]) ).
fof(f2512,plain,
( ~ c1_1(a559)
| ~ c2_1(a559)
| ~ spl0_21
| spl0_158 ),
inference(resolution,[],[f331,f887]) ).
fof(f2530,plain,
( ~ spl0_230
| ~ spl0_273
| ~ spl0_21
| spl0_158 ),
inference(avatar_split_clause,[],[f2512,f886,f330,f2158,f1183]) ).
fof(f2535,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_11
| ~ spl0_36 ),
inference(resolution,[],[f385,f296]) ).
fof(f2536,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_11
| ~ spl0_36 ),
inference(duplicate_literal_removal,[],[f2535]) ).
fof(f2544,plain,
( c1_1(a568)
| ~ c2_1(a568)
| ~ spl0_38
| spl0_167 ),
inference(resolution,[],[f392,f928]) ).
fof(f2552,plain,
( c1_1(a594)
| ~ c2_1(a594)
| ~ spl0_38
| spl0_148 ),
inference(resolution,[],[f392,f839]) ).
fof(f2555,plain,
( c1_1(a543)
| ~ c2_1(a543)
| ~ spl0_38
| spl0_84 ),
inference(resolution,[],[f392,f565]) ).
fof(f2581,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22
| ~ spl0_49 ),
inference(resolution,[],[f435,f334]) ).
fof(f2587,plain,
( c3_1(a562)
| c2_1(a562)
| ~ spl0_49
| spl0_161 ),
inference(resolution,[],[f435,f901]) ).
fof(f2590,plain,
( c3_1(a577)
| c2_1(a577)
| ~ spl0_49
| spl0_126 ),
inference(resolution,[],[f435,f746]) ).
fof(f2592,plain,
( c3_1(a560)
| c2_1(a560)
| ~ spl0_49
| spl0_101 ),
inference(resolution,[],[f435,f641]) ).
fof(f2593,plain,
( c3_1(a545)
| c2_1(a545)
| ~ spl0_49
| spl0_86 ),
inference(resolution,[],[f435,f574]) ).
fof(f2594,plain,
( c3_1(a594)
| c2_1(a594)
| ~ spl0_49
| spl0_148 ),
inference(resolution,[],[f435,f839]) ).
fof(f2596,plain,
( c3_1(a569)
| c2_1(a569)
| ~ spl0_49
| spl0_110 ),
inference(resolution,[],[f435,f681]) ).
fof(f2600,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22
| ~ spl0_49 ),
inference(duplicate_literal_removal,[],[f2581]) ).
fof(f2607,plain,
( spl0_87
| spl0_251
| ~ spl0_49
| spl0_86 ),
inference(avatar_split_clause,[],[f2593,f573,f434,f1421,f577]) ).
fof(f2611,plain,
( spl0_256
| spl0_162
| ~ spl0_49
| spl0_161 ),
inference(avatar_split_clause,[],[f2587,f900,f434,f904,f1532]) ).
fof(f2613,plain,
( spl0_32
| ~ spl0_22
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f2600,f434,f333,f370]) ).
fof(f2615,plain,
( c1_1(a561)
| c2_1(a561)
| ~ spl0_8
| spl0_160 ),
inference(resolution,[],[f896,f286]) ).
fof(f2618,definition,
( spl0_278
<=> c1_1(a561) ),
introduced(definition,[new_symbols(definition,[spl0_278])],[avatar_definition]) ).
fof(f2620,plain,
( spl0_159
| spl0_278
| ~ spl0_8
| spl0_160 ),
inference(avatar_split_clause,[],[f2615,f895,f285,f2618,f891]) ).
fof(f2627,plain,
( c2_1(a561)
| c1_1(a561)
| ~ spl0_36
| ~ spl0_232 ),
inference(resolution,[],[f1192,f385]) ).
fof(f2653,plain,
( c2_1(a594)
| c1_1(a594)
| ~ spl0_51
| spl0_148 ),
inference(resolution,[],[f442,f839]) ).
fof(f2654,plain,
( c2_1(a573)
| c1_1(a573)
| ~ spl0_51
| spl0_119 ),
inference(resolution,[],[f442,f715]) ).
fof(f2655,plain,
( c2_1(a569)
| c1_1(a569)
| ~ spl0_51
| spl0_110 ),
inference(resolution,[],[f442,f681]) ).
fof(f2656,plain,
( c2_1(a543)
| c1_1(a543)
| ~ spl0_51
| spl0_84 ),
inference(resolution,[],[f442,f565]) ).
fof(f2667,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_52 ),
inference(resolution,[],[f445,f272]) ).
fof(f2670,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_17
| ~ spl0_52 ),
inference(resolution,[],[f445,f316]) ).
fof(f2675,plain,
( ~ c1_1(a595)
| ~ c3_1(a595)
| ~ spl0_52
| spl0_171 ),
inference(resolution,[],[f445,f945]) ).
fof(f2681,plain,
( ~ c1_1(a570)
| ~ c3_1(a570)
| ~ spl0_52
| spl0_112 ),
inference(resolution,[],[f445,f688]) ).
fof(f2689,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_17
| ~ spl0_52 ),
inference(duplicate_literal_removal,[],[f2670]) ).
fof(f2692,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4
| ~ spl0_52 ),
inference(duplicate_literal_removal,[],[f2667]) ).
fof(f2694,plain,
( ~ spl0_188
| ~ spl0_187
| ~ spl0_52
| spl0_112 ),
inference(avatar_split_clause,[],[f2681,f687,f444,f1008,f1012]) ).
fof(f2701,plain,
( spl0_14
| ~ spl0_17
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f2689,f444,f315,f305]) ).
fof(f2702,plain,
( spl0_14
| ~ spl0_4
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f2692,f444,f271,f305]) ).
fof(f2703,plain,
( c2_1(a554)
| c1_1(a554)
| ~ spl0_51
| spl0_98 ),
inference(resolution,[],[f627,f442]) ).
fof(f2715,plain,
( c2_1(a555)
| ~ c3_1(a555)
| ~ spl0_7
| ~ spl0_224 ),
inference(resolution,[],[f1160,f282]) ).
fof(f2722,definition,
( spl0_280
<=> c1_1(a555) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f2734,plain,
( spl0_278
| spl0_159
| ~ spl0_36
| ~ spl0_232 ),
inference(avatar_split_clause,[],[f2627,f1191,f384,f891,f2618]) ).
fof(f2805,plain,
( c2_1(a571)
| ~ c1_1(a571)
| ~ spl0_10
| ~ spl0_189 ),
inference(resolution,[],[f1017,f292]) ).
fof(f2806,plain,
( ~ spl0_255
| spl0_114
| ~ spl0_10
| ~ spl0_189 ),
inference(avatar_split_clause,[],[f2805,f1016,f291,f694,f1515]) ).
fof(f2808,plain,
( c2_1(a572)
| c1_1(a572)
| ~ spl0_36
| ~ spl0_191 ),
inference(resolution,[],[f1025,f385]) ).
fof(f2809,plain,
( c3_1(a572)
| c1_1(a572)
| ~ spl0_42
| ~ spl0_191 ),
inference(resolution,[],[f1025,f407]) ).
fof(f2810,plain,
( spl0_116
| spl0_117
| ~ spl0_42
| ~ spl0_191 ),
inference(avatar_split_clause,[],[f2809,f1024,f406,f705,f701]) ).
fof(f2811,plain,
( spl0_116
| spl0_261
| ~ spl0_36
| ~ spl0_191 ),
inference(avatar_split_clause,[],[f2808,f1024,f384,f1680,f701]) ).
fof(f2820,definition,
( spl0_282
<=> c1_1(a589) ),
introduced(definition,[new_symbols(definition,[spl0_282])],[avatar_definition]) ).
fof(f2830,plain,
( c2_1(a555)
| ~ c1_1(a555)
| ~ spl0_10
| ~ spl0_225 ),
inference(resolution,[],[f1164,f292]) ).
fof(f2831,plain,
( ~ spl0_280
| spl0_155
| ~ spl0_10
| ~ spl0_225 ),
inference(avatar_split_clause,[],[f2830,f1163,f291,f871,f2722]) ).
fof(f2866,plain,
( ~ c2_1(a551)
| ~ c1_1(a551)
| ~ spl0_16
| spl0_154 ),
inference(resolution,[],[f313,f867]) ).
fof(f2882,plain,
( ~ spl0_259
| ~ spl0_222
| ~ spl0_16
| spl0_154 ),
inference(avatar_split_clause,[],[f2866,f866,f312,f1151,f1581]) ).
fof(f2886,plain,
( c3_1(a559)
| ~ c1_1(a559)
| ~ spl0_22
| ~ spl0_231 ),
inference(resolution,[],[f334,f1188]) ).
fof(f2899,plain,
( ~ spl0_273
| spl0_158
| ~ spl0_22
| ~ spl0_231 ),
inference(avatar_split_clause,[],[f2886,f1187,f333,f886,f2158]) ).
fof(f2910,plain,
( ~ c1_1(a577)
| c3_1(a577)
| ~ spl0_25
| spl0_126 ),
inference(resolution,[],[f345,f746]) ).
fof(f2911,plain,
( ~ c1_1(a560)
| c3_1(a560)
| ~ spl0_25
| spl0_101 ),
inference(resolution,[],[f345,f641]) ).
fof(f2918,plain,
( spl0_102
| ~ spl0_182
| ~ spl0_25
| spl0_101 ),
inference(avatar_split_clause,[],[f2911,f640,f344,f988,f644]) ).
fof(f2919,plain,
( spl0_127
| ~ spl0_193
| ~ spl0_25
| spl0_126 ),
inference(avatar_split_clause,[],[f2910,f745,f344,f1032,f749]) ).
fof(f2927,plain,
( c2_1(a544)
| ~ c1_1(a544)
| ~ spl0_32
| spl0_152 ),
inference(resolution,[],[f371,f858]) ).
fof(f2933,plain,
( c2_1(a545)
| ~ c1_1(a545)
| ~ spl0_32
| spl0_251 ),
inference(resolution,[],[f371,f1525]) ).
fof(f2943,plain,
( ~ spl0_176
| spl0_87
| ~ spl0_32
| spl0_251 ),
inference(avatar_split_clause,[],[f2933,f1421,f370,f577,f964]) ).
fof(f2946,plain,
( ~ spl0_215
| spl0_153
| ~ spl0_32
| spl0_152 ),
inference(avatar_split_clause,[],[f2927,f857,f370,f861,f1121]) ).
fof(f2950,plain,
( ~ spl0_225
| spl0_155
| ~ spl0_7
| ~ spl0_224 ),
inference(avatar_split_clause,[],[f2715,f1159,f281,f871,f1163]) ).
fof(f2955,plain,
( ~ spl0_222
| ~ spl0_259
| ~ spl0_14
| ~ spl0_223 ),
inference(avatar_split_clause,[],[f2318,f1155,f305,f1581,f1151]) ).
fof(f2957,plain,
( ~ spl0_246
| ~ spl0_187
| ~ spl0_14
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f2321,f1012,f305,f1008,f1323]) ).
fof(f2961,plain,
( ~ spl0_230
| spl0_273
| ~ spl0_28
| ~ spl0_231 ),
inference(avatar_split_clause,[],[f2383,f1187,f355,f2158,f1183]) ).
fof(f2967,plain,
( ~ spl0_237
| spl0_166
| ~ spl0_38
| spl0_167 ),
inference(avatar_split_clause,[],[f2544,f927,f391,f923,f1211]) ).
fof(f2969,plain,
( ~ spl0_244
| spl0_146
| ~ spl0_38
| spl0_148 ),
inference(avatar_split_clause,[],[f2552,f838,f391,f830,f1310]) ).
fof(f2971,plain,
( spl0_244
| spl0_147
| ~ spl0_49
| spl0_148 ),
inference(avatar_split_clause,[],[f2594,f838,f434,f834,f1310]) ).
fof(f2973,plain,
( spl0_108
| spl0_267
| ~ spl0_49
| spl0_110 ),
inference(avatar_split_clause,[],[f2596,f680,f434,f1869,f672]) ).
fof(f2977,plain,
( spl0_264
| spl0_127
| ~ spl0_49
| spl0_126 ),
inference(avatar_split_clause,[],[f2590,f745,f434,f749,f1782]) ).
fof(f2978,plain,
( spl0_270
| spl0_102
| ~ spl0_49
| spl0_101 ),
inference(avatar_split_clause,[],[f2592,f640,f434,f644,f1980]) ).
fof(f2984,plain,
( ~ spl0_265
| spl0_149
| ~ spl0_1
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f2255,f1068,f262,f843,f1794]) ).
fof(f2987,plain,
( c2_1(a584)
| ~ c1_1(a584)
| ~ spl0_32
| spl0_135 ),
inference(resolution,[],[f786,f371]) ).
fof(f2988,plain,
( ~ spl0_196
| spl0_266
| ~ spl0_32
| spl0_135 ),
inference(avatar_split_clause,[],[f2987,f785,f370,f1857,f1044]) ).
fof(f2993,plain,
( c2_1(a535)
| ~ c1_1(a535)
| ~ spl0_1
| ~ spl0_172 ),
inference(resolution,[],[f949,f263]) ).
fof(f2996,plain,
( ~ spl0_173
| spl0_77
| ~ spl0_1
| ~ spl0_172 ),
inference(avatar_split_clause,[],[f2993,f948,f262,f535,f952]) ).
fof(f2997,plain,
( ~ spl0_213
| ~ spl0_211
| ~ spl0_4
| ~ spl0_214 ),
inference(avatar_split_clause,[],[f1956,f1117,f271,f1106,f1113]) ).
fof(f3039,plain,
( ~ spl0_275
| ~ spl0_242
| ~ spl0_52
| spl0_171 ),
inference(avatar_split_clause,[],[f2675,f944,f444,f1231,f2238]) ).
fof(f3043,plain,
( ~ spl0_245
| spl0_85
| ~ spl0_38
| spl0_84 ),
inference(avatar_split_clause,[],[f2555,f564,f391,f568,f1315]) ).
fof(f3055,plain,
( c2_1(a583)
| ~ c1_1(a583)
| ~ spl0_10
| ~ spl0_240 ),
inference(resolution,[],[f1224,f292]) ).
fof(f3057,definition,
( spl0_283
<=> c1_1(a583) ),
introduced(definition,[new_symbols(definition,[spl0_283])],[avatar_definition]) ).
fof(f3060,plain,
( ~ spl0_283
| spl0_169
| ~ spl0_10
| ~ spl0_240 ),
inference(avatar_split_clause,[],[f3055,f1223,f291,f937,f3057]) ).
fof(f3079,plain,
( ~ c2_1(a546)
| c1_1(a546)
| ~ spl0_6
| spl0_89 ),
inference(resolution,[],[f279,f587]) ).
fof(f3088,plain,
( spl0_88
| ~ spl0_177
| ~ spl0_6
| spl0_89 ),
inference(avatar_split_clause,[],[f3079,f586,f278,f968,f582]) ).
fof(f3099,plain,
( c1_1(a578)
| ~ c2_1(a578)
| ~ spl0_9
| ~ spl0_194 ),
inference(resolution,[],[f289,f1037]) ).
fof(f3105,plain,
( ~ spl0_263
| spl0_128
| ~ spl0_9
| ~ spl0_194 ),
inference(avatar_split_clause,[],[f3099,f1036,f288,f754,f1776]) ).
fof(f3111,plain,
( spl0_2
| ~ spl0_11
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f2536,f384,f295,f265]) ).
fof(f3114,plain,
( spl0_96
| spl0_97
| ~ spl0_51
| spl0_98 ),
inference(avatar_split_clause,[],[f2703,f626,f441,f622,f618]) ).
fof(f3128,plain,
( ~ spl0_258
| ~ spl0_151
| ~ spl0_14
| ~ spl0_206 ),
inference(avatar_split_clause,[],[f2069,f1085,f305,f852,f1560]) ).
fof(f3129,plain,
( ~ spl0_151
| spl0_258
| ~ spl0_10
| ~ spl0_206 ),
inference(avatar_split_clause,[],[f2180,f1085,f291,f1560,f852]) ).
fof(f3130,plain,
( ~ spl0_258
| spl0_151
| ~ spl0_28
| ~ spl0_207 ),
inference(avatar_split_clause,[],[f1553,f1089,f355,f852,f1560]) ).
fof(f3138,plain,
( c1_1(a589)
| ~ c2_1(a589)
| ~ spl0_9
| ~ spl0_199 ),
inference(resolution,[],[f1057,f289]) ).
fof(f3140,plain,
( ~ spl0_200
| spl0_282
| ~ spl0_9
| ~ spl0_199 ),
inference(avatar_split_clause,[],[f3138,f1056,f288,f2820,f1060]) ).
fof(f3141,plain,
( c1_1(a537)
| ~ c2_1(a537)
| ~ spl0_9
| ~ spl0_206 ),
inference(resolution,[],[f1086,f289]) ).
fof(f3143,plain,
( ~ spl0_258
| spl0_151
| ~ spl0_9
| ~ spl0_206 ),
inference(avatar_split_clause,[],[f3141,f1085,f288,f852,f1560]) ).
fof(f3170,plain,
( ~ c1_1(a538)
| ~ c2_1(a538)
| ~ spl0_14
| ~ spl0_208 ),
inference(resolution,[],[f306,f1094]) ).
fof(f3172,plain,
( ~ c1_1(a589)
| ~ c2_1(a589)
| ~ spl0_14
| ~ spl0_199 ),
inference(resolution,[],[f306,f1057]) ).
fof(f3178,plain,
( ~ spl0_200
| ~ spl0_282
| ~ spl0_14
| ~ spl0_199 ),
inference(avatar_split_clause,[],[f3172,f1056,f305,f2820,f1060]) ).
fof(f3179,plain,
( ~ spl0_210
| ~ spl0_209
| ~ spl0_14
| ~ spl0_208 ),
inference(avatar_split_clause,[],[f3170,f1093,f305,f1098,f1102]) ).
fof(f3212,plain,
( spl0_266
| spl0_135
| ~ spl0_34
| ~ spl0_197 ),
inference(avatar_split_clause,[],[f1878,f1048,f377,f785,f1857]) ).
fof(f3233,plain,
( c2_1(a584)
| ~ c1_1(a584)
| ~ spl0_1
| ~ spl0_197 ),
inference(resolution,[],[f1049,f263]) ).
fof(f3234,plain,
( ~ spl0_196
| spl0_266
| ~ spl0_1
| ~ spl0_197 ),
inference(avatar_split_clause,[],[f3233,f1048,f262,f1857,f1044]) ).
fof(f3241,plain,
( c1_1(a596)
| c2_1(a596)
| ~ spl0_8
| spl0_150 ),
inference(resolution,[],[f286,f848]) ).
fof(f3247,plain,
( c1_1(a594)
| c2_1(a594)
| ~ spl0_8
| spl0_147 ),
inference(resolution,[],[f286,f835]) ).
fof(f3249,plain,
( c1_1(a543)
| c2_1(a543)
| ~ spl0_8
| spl0_83 ),
inference(resolution,[],[f286,f561]) ).
fof(f3252,plain,
( spl0_245
| spl0_85
| ~ spl0_8
| spl0_83 ),
inference(avatar_split_clause,[],[f3249,f560,f285,f568,f1315]) ).
fof(f3254,plain,
( spl0_244
| spl0_146
| ~ spl0_8
| spl0_147 ),
inference(avatar_split_clause,[],[f3247,f834,f285,f830,f1310]) ).
fof(f3256,plain,
( spl0_149
| spl0_265
| ~ spl0_8
| spl0_150 ),
inference(avatar_split_clause,[],[f3241,f847,f285,f1794,f843]) ).
fof(f3258,plain,
( c3_1(a595)
| ~ c2_1(a595)
| ~ spl0_12
| spl0_171 ),
inference(resolution,[],[f299,f945]) ).
fof(f3275,plain,
( ~ spl0_243
| spl0_275
| ~ spl0_12
| spl0_171 ),
inference(avatar_split_clause,[],[f3258,f944,f298,f2238,f1235]) ).
fof(f3279,plain,
( ~ c2_1(a537)
| ~ c3_1(a537)
| ~ spl0_17
| ~ spl0_207 ),
inference(resolution,[],[f316,f1090]) ).
fof(f3290,plain,
( ~ spl0_206
| ~ spl0_258
| ~ spl0_17
| ~ spl0_207 ),
inference(avatar_split_clause,[],[f3279,f1089,f315,f1560,f1085]) ).
fof(f3297,plain,
( ~ c1_1(a562)
| ~ c2_1(a562)
| ~ spl0_21
| spl0_162 ),
inference(resolution,[],[f331,f905]) ).
fof(f3299,plain,
( ~ c1_1(a586)
| ~ c2_1(a586)
| ~ spl0_21
| spl0_137 ),
inference(resolution,[],[f331,f793]) ).
fof(f3300,plain,
( ~ c1_1(a584)
| ~ c2_1(a584)
| ~ spl0_21
| spl0_135 ),
inference(resolution,[],[f331,f786]) ).
fof(f3301,plain,
( ~ c1_1(a560)
| ~ c2_1(a560)
| ~ spl0_21
| spl0_102 ),
inference(resolution,[],[f331,f645]) ).
fof(f3310,plain,
( ~ spl0_270
| ~ spl0_182
| ~ spl0_21
| spl0_102 ),
inference(avatar_split_clause,[],[f3301,f644,f330,f988,f1980]) ).
fof(f3311,plain,
( ~ spl0_266
| ~ spl0_196
| ~ spl0_21
| spl0_135 ),
inference(avatar_split_clause,[],[f3300,f785,f330,f1044,f1857]) ).
fof(f3312,plain,
( ~ spl0_254
| ~ spl0_198
| ~ spl0_21
| spl0_137 ),
inference(avatar_split_clause,[],[f3299,f792,f330,f1052,f1496]) ).
fof(f3313,plain,
( ~ spl0_256
| ~ spl0_233
| ~ spl0_21
| spl0_162 ),
inference(avatar_split_clause,[],[f3297,f904,f330,f1195,f1532]) ).
fof(f3362,plain,
( ~ c1_1(a577)
| ~ c2_1(a577)
| ~ spl0_21
| spl0_127 ),
inference(resolution,[],[f750,f331]) ).
fof(f3364,plain,
( ~ spl0_264
| ~ spl0_193
| ~ spl0_21
| spl0_127 ),
inference(avatar_split_clause,[],[f3362,f749,f330,f1032,f1782]) ).
fof(f3371,plain,
( ~ c1_1(a574)
| ~ c2_1(a574)
| ~ spl0_21
| spl0_168 ),
inference(resolution,[],[f933,f331]) ).
fof(f3374,plain,
( ~ spl0_274
| ~ spl0_238
| ~ spl0_21
| spl0_168 ),
inference(avatar_split_clause,[],[f3371,f932,f330,f1215,f2231]) ).
fof(f3380,plain,
( c1_1(a583)
| c2_1(a583)
| ~ spl0_2
| ~ spl0_240 ),
inference(resolution,[],[f266,f1224]) ).
fof(f3382,plain,
( c1_1(a555)
| c2_1(a555)
| ~ spl0_2
| ~ spl0_225 ),
inference(resolution,[],[f266,f1164]) ).
fof(f3385,plain,
( c1_1(a537)
| c2_1(a537)
| ~ spl0_2
| ~ spl0_206 ),
inference(resolution,[],[f266,f1086]) ).
fof(f3390,plain,
( c1_1(a558)
| c2_1(a558)
| ~ spl0_2
| ~ spl0_181 ),
inference(resolution,[],[f266,f985]) ).
fof(f3392,plain,
( c1_1(a548)
| c2_1(a548)
| ~ spl0_2
| ~ spl0_178 ),
inference(resolution,[],[f266,f973]) ).
fof(f3396,plain,
( spl0_91
| spl0_252
| ~ spl0_2
| ~ spl0_178 ),
inference(avatar_split_clause,[],[f3392,f972,f265,f1430,f595]) ).
fof(f3398,plain,
( spl0_262
| spl0_100
| ~ spl0_2
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f3390,f984,f265,f635,f1768]) ).
fof(f3400,plain,
( spl0_258
| spl0_151
| ~ spl0_2
| ~ spl0_206 ),
inference(avatar_split_clause,[],[f3385,f1085,f265,f852,f1560]) ).
fof(f3401,plain,
( spl0_155
| spl0_280
| ~ spl0_2
| ~ spl0_225 ),
inference(avatar_split_clause,[],[f3382,f1163,f265,f2722,f871]) ).
fof(f3404,plain,
( spl0_169
| spl0_283
| ~ spl0_2
| ~ spl0_240 ),
inference(avatar_split_clause,[],[f3380,f1223,f265,f3057,f937]) ).
fof(f3421,plain,
( ~ spl0_181
| spl0_100
| ~ spl0_11
| spl0_99 ),
inference(avatar_split_clause,[],[f1765,f631,f295,f635,f984]) ).
fof(f3464,plain,
( ~ spl0_261
| spl0_116
| ~ spl0_28
| ~ spl0_191 ),
inference(avatar_split_clause,[],[f2387,f1024,f355,f701,f1680]) ).
fof(f3466,plain,
( spl0_108
| ~ spl0_267
| ~ spl0_30
| spl0_110 ),
inference(avatar_split_clause,[],[f1866,f680,f363,f1869,f672]) ).
fof(f3468,plain,
( spl0_109
| spl0_108
| ~ spl0_51
| spl0_110 ),
inference(avatar_split_clause,[],[f2655,f680,f441,f672,f676]) ).
fof(f3469,plain,
( spl0_85
| spl0_245
| ~ spl0_51
| spl0_84 ),
inference(avatar_split_clause,[],[f2656,f564,f441,f1315,f568]) ).
fof(f3471,plain,
( spl0_146
| spl0_244
| ~ spl0_51
| spl0_148 ),
inference(avatar_split_clause,[],[f2653,f838,f441,f1310,f830]) ).
fof(f3472,plain,
( spl0_118
| spl0_120
| ~ spl0_51
| spl0_119 ),
inference(avatar_split_clause,[],[f2654,f714,f441,f718,f710]) ).
fof(f3486,plain,
( ~ c2_1(a574)
| ~ c1_1(a574)
| ~ spl0_4
| ~ spl0_239 ),
inference(resolution,[],[f272,f1220]) ).
fof(f3489,plain,
( ~ c2_1(a547)
| ~ c1_1(a547)
| ~ spl0_4
| ~ spl0_216 ),
inference(resolution,[],[f272,f1126]) ).
fof(f3490,plain,
( ~ c2_1(a536)
| ~ c1_1(a536)
| ~ spl0_4
| ~ spl0_203 ),
inference(resolution,[],[f272,f1073]) ).
fof(f3494,plain,
( ~ spl0_205
| ~ spl0_204
| ~ spl0_4
| ~ spl0_203 ),
inference(avatar_split_clause,[],[f3490,f1072,f271,f1077,f1081]) ).
fof(f3495,plain,
( ~ spl0_217
| ~ spl0_218
| ~ spl0_4
| ~ spl0_216 ),
inference(avatar_split_clause,[],[f3489,f1125,f271,f1134,f1130]) ).
fof(f3496,plain,
( ~ spl0_238
| ~ spl0_274
| ~ spl0_4
| ~ spl0_239 ),
inference(avatar_split_clause,[],[f3486,f1219,f271,f2231,f1215]) ).
fof(f3501,plain,
( c1_1(a555)
| ~ c3_1(a555)
| ~ spl0_5
| ~ spl0_224 ),
inference(resolution,[],[f276,f1160]) ).
fof(f3505,plain,
( c1_1(a571)
| ~ c3_1(a571)
| ~ spl0_5
| ~ spl0_190 ),
inference(resolution,[],[f276,f1021]) ).
fof(f3507,plain,
( ~ spl0_189
| spl0_255
| ~ spl0_5
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f3505,f1020,f275,f1515,f1016]) ).
fof(f3509,plain,
( ~ spl0_225
| spl0_280
| ~ spl0_5
| ~ spl0_224 ),
inference(avatar_split_clause,[],[f3501,f1159,f275,f2722,f1163]) ).
fof(f3523,plain,
( c1_1(a589)
| ~ c3_1(a589)
| ~ spl0_11
| spl0_139 ),
inference(resolution,[],[f296,f802]) ).
fof(f3534,plain,
( ~ spl0_199
| spl0_282
| ~ spl0_11
| spl0_139 ),
inference(avatar_split_clause,[],[f3523,f801,f295,f2820,f1056]) ).
fof(f3544,plain,
( ~ c2_1(a595)
| ~ c1_1(a595)
| ~ spl0_16
| spl0_171 ),
inference(resolution,[],[f313,f945]) ).
fof(f3547,plain,
( ~ c2_1(a589)
| ~ c1_1(a589)
| ~ spl0_16
| spl0_139 ),
inference(resolution,[],[f313,f802]) ).
fof(f3559,plain,
( ~ spl0_282
| ~ spl0_200
| ~ spl0_16
| spl0_139 ),
inference(avatar_split_clause,[],[f3547,f801,f312,f1060,f2820]) ).
fof(f3560,plain,
( ~ spl0_242
| ~ spl0_243
| ~ spl0_16
| spl0_171 ),
inference(avatar_split_clause,[],[f3544,f944,f312,f1235,f1231]) ).
fof(f3564,plain,
( c3_1(a574)
| ~ c1_1(a574)
| ~ spl0_22
| ~ spl0_239 ),
inference(resolution,[],[f334,f1220]) ).
fof(f3565,plain,
( c3_1(a561)
| ~ c1_1(a561)
| ~ spl0_22
| ~ spl0_232 ),
inference(resolution,[],[f334,f1192]) ).
fof(f3579,plain,
( ~ spl0_278
| spl0_160
| ~ spl0_22
| ~ spl0_232 ),
inference(avatar_split_clause,[],[f3565,f1191,f333,f895,f2618]) ).
fof(f3581,plain,
( ~ spl0_238
| spl0_168
| ~ spl0_22
| ~ spl0_239 ),
inference(avatar_split_clause,[],[f3564,f1219,f333,f932,f1215]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f273]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f283]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f293]) ).
cnf(s4,plain,
( spl0_1
| ~ spl0_3
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f300]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_10
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f307]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f317]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_9
| spl0_14
| spl0_19 ),
inference(sat_conversion,[],[f325]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_20
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f335]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_12
| spl0_14
| spl0_23 ),
inference(sat_conversion,[],[f339]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_4
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f346]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_16
| spl0_23
| spl0_28 ),
inference(sat_conversion,[],[f357]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_14
| spl0_25
| spl0_29 ),
inference(sat_conversion,[],[f361]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_10
| spl0_23
| spl0_30 ),
inference(sat_conversion,[],[f365]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_9
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f372]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_7
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f379]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_5
| spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f393]) ).
cnf(s20,plain,
( ~ spl0_3
| spl0_10
| spl0_25
| spl0_39 ),
inference(sat_conversion,[],[f397]) ).
cnf(s21,plain,
( spl0_2
| ~ spl0_3
| spl0_21
| spl0_40 ),
inference(sat_conversion,[],[f401]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_28
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f408]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_21
| spl0_36
| spl0_43 ),
inference(sat_conversion,[],[f412]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_8
| spl0_14
| spl0_24 ),
inference(sat_conversion,[],[f413]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_4
| spl0_8
| spl0_44 ),
inference(sat_conversion,[],[f417]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_11
| spl0_25
| spl0_45 ),
inference(sat_conversion,[],[f421]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_5
| spl0_8
| spl0_46 ),
inference(sat_conversion,[],[f425]) ).
cnf(s29,plain,
( spl0_1
| ~ spl0_3
| spl0_48
| spl0_49 ),
inference(sat_conversion,[],[f436]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_50
| spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f446]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_22
| spl0_49
| spl0_53 ),
inference(sat_conversion,[],[f450]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_8
| spl0_19
| spl0_30 ),
inference(sat_conversion,[],[f458]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_22
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f475]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_52
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f489]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_28
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f496]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_36
| spl0_70
| spl0_71 ),
inference(sat_conversion,[],[f514]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_30
| spl0_74
| spl0_75 ),
inference(sat_conversion,[],[f528]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_51
| spl0_76 ),
inference(sat_conversion,[],[f532]) ).
cnf(s45,plain,
( ~ spl0_44
| ~ spl0_77 ),
inference(sat_conversion,[],[f537]) ).
cnf(s50,plain,
( ~ spl0_82
| ~ spl0_83 ),
inference(sat_conversion,[],[f562]) ).
cnf(s51,plain,
( ~ spl0_82
| ~ spl0_84 ),
inference(sat_conversion,[],[f566]) ).
cnf(s52,plain,
( ~ spl0_82
| ~ spl0_85 ),
inference(sat_conversion,[],[f570]) ).
cnf(s53,plain,
( ~ spl0_29
| ~ spl0_86 ),
inference(sat_conversion,[],[f575]) ).
cnf(s54,plain,
( ~ spl0_29
| ~ spl0_87 ),
inference(sat_conversion,[],[f579]) ).
cnf(s55,plain,
( ~ spl0_40
| ~ spl0_88 ),
inference(sat_conversion,[],[f584]) ).
cnf(s56,plain,
( ~ spl0_40
| ~ spl0_89 ),
inference(sat_conversion,[],[f588]) ).
cnf(s57,plain,
( ~ spl0_50
| ~ spl0_90 ),
inference(sat_conversion,[],[f593]) ).
cnf(s58,plain,
( ~ spl0_50
| ~ spl0_91 ),
inference(sat_conversion,[],[f597]) ).
cnf(s59,plain,
( ~ spl0_66
| ~ spl0_92 ),
inference(sat_conversion,[],[f602]) ).
cnf(s60,plain,
( ~ spl0_37
| ~ spl0_93 ),
inference(sat_conversion,[],[f607]) ).
cnf(s61,plain,
( ~ spl0_37
| ~ spl0_94 ),
inference(sat_conversion,[],[f611]) ).
cnf(s62,plain,
( ~ spl0_37
| ~ spl0_95 ),
inference(sat_conversion,[],[f615]) ).
cnf(s63,plain,
( ~ spl0_64
| ~ spl0_96 ),
inference(sat_conversion,[],[f620]) ).
cnf(s64,plain,
( ~ spl0_64
| ~ spl0_97 ),
inference(sat_conversion,[],[f624]) ).
cnf(s65,plain,
( ~ spl0_64
| ~ spl0_98 ),
inference(sat_conversion,[],[f628]) ).
cnf(s66,plain,
( ~ spl0_15
| ~ spl0_99 ),
inference(sat_conversion,[],[f633]) ).
cnf(s67,plain,
( ~ spl0_15
| ~ spl0_100 ),
inference(sat_conversion,[],[f637]) ).
cnf(s68,plain,
( ~ spl0_74
| ~ spl0_101 ),
inference(sat_conversion,[],[f642]) ).
cnf(s69,plain,
( ~ spl0_74
| ~ spl0_102 ),
inference(sat_conversion,[],[f646]) ).
cnf(s75,plain,
( ~ spl0_31
| ~ spl0_108 ),
inference(sat_conversion,[],[f674]) ).
cnf(s76,plain,
( ~ spl0_31
| ~ spl0_109 ),
inference(sat_conversion,[],[f678]) ).
cnf(s77,plain,
( ~ spl0_31
| ~ spl0_110 ),
inference(sat_conversion,[],[f682]) ).
cnf(s78,plain,
( ~ spl0_111
| ~ spl0_112 ),
inference(sat_conversion,[],[f689]) ).
cnf(s79,plain,
( ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f696]) ).
cnf(s80,plain,
( ~ spl0_115
| ~ spl0_116 ),
inference(sat_conversion,[],[f703]) ).
cnf(s81,plain,
( ~ spl0_115
| ~ spl0_117 ),
inference(sat_conversion,[],[f707]) ).
cnf(s82,plain,
( ~ spl0_71
| ~ spl0_118 ),
inference(sat_conversion,[],[f712]) ).
cnf(s83,plain,
( ~ spl0_71
| ~ spl0_119 ),
inference(sat_conversion,[],[f716]) ).
cnf(s84,plain,
( ~ spl0_71
| ~ spl0_120 ),
inference(sat_conversion,[],[f720]) ).
cnf(s90,plain,
( ~ spl0_60
| ~ spl0_126 ),
inference(sat_conversion,[],[f747]) ).
cnf(s91,plain,
( ~ spl0_60
| ~ spl0_127 ),
inference(sat_conversion,[],[f751]) ).
cnf(s92,plain,
( ~ spl0_59
| ~ spl0_128 ),
inference(sat_conversion,[],[f756]) ).
cnf(s93,plain,
( ~ spl0_59
| ~ spl0_129 ),
inference(sat_conversion,[],[f760]) ).
cnf(s96,plain,
( ~ spl0_13
| ~ spl0_132 ),
inference(sat_conversion,[],[f774]) ).
cnf(s97,plain,
( ~ spl0_13
| ~ spl0_133 ),
inference(sat_conversion,[],[f778]) ).
cnf(s98,plain,
( ~ spl0_13
| ~ spl0_134 ),
inference(sat_conversion,[],[f782]) ).
cnf(s99,plain,
( ~ spl0_45
| ~ spl0_135 ),
inference(sat_conversion,[],[f787]) ).
cnf(s100,plain,
( ~ spl0_136
| ~ spl0_137 ),
inference(sat_conversion,[],[f794]) ).
cnf(s101,plain,
( ~ spl0_136
| ~ spl0_138 ),
inference(sat_conversion,[],[f798]) ).
cnf(s102,plain,
( ~ spl0_76
| ~ spl0_139 ),
inference(sat_conversion,[],[f803]) ).
cnf(s108,plain,
( ~ spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f832]) ).
cnf(s109,plain,
( ~ spl0_145
| ~ spl0_147 ),
inference(sat_conversion,[],[f836]) ).
cnf(s110,plain,
( ~ spl0_145
| ~ spl0_148 ),
inference(sat_conversion,[],[f840]) ).
cnf(s111,plain,
( ~ spl0_20
| ~ spl0_149 ),
inference(sat_conversion,[],[f845]) ).
cnf(s112,plain,
( ~ spl0_20
| ~ spl0_150 ),
inference(sat_conversion,[],[f849]) ).
cnf(s113,plain,
( ~ spl0_24
| ~ spl0_151 ),
inference(sat_conversion,[],[f854]) ).
cnf(s114,plain,
( ~ spl0_41
| ~ spl0_152 ),
inference(sat_conversion,[],[f859]) ).
cnf(s115,plain,
( ~ spl0_41
| ~ spl0_153 ),
inference(sat_conversion,[],[f863]) ).
cnf(s116,plain,
( ~ spl0_65
| ~ spl0_154 ),
inference(sat_conversion,[],[f868]) ).
cnf(s117,plain,
( ~ spl0_63
| ~ spl0_155 ),
inference(sat_conversion,[],[f873]) ).
cnf(s120,plain,
( ~ spl0_75
| ~ spl0_158 ),
inference(sat_conversion,[],[f888]) ).
cnf(s121,plain,
( ~ spl0_48
| ~ spl0_159 ),
inference(sat_conversion,[],[f893]) ).
cnf(s122,plain,
( ~ spl0_48
| ~ spl0_160 ),
inference(sat_conversion,[],[f897]) ).
cnf(s123,plain,
( ~ spl0_23
| ~ spl0_161 ),
inference(sat_conversion,[],[f902]) ).
cnf(s124,plain,
( ~ spl0_23
| ~ spl0_162 ),
inference(sat_conversion,[],[f906]) ).
cnf(s128,plain,
( ~ spl0_33
| ~ spl0_166 ),
inference(sat_conversion,[],[f925]) ).
cnf(s129,plain,
( ~ spl0_33
| ~ spl0_167 ),
inference(sat_conversion,[],[f929]) ).
cnf(s130,plain,
( ~ spl0_70
| ~ spl0_168 ),
inference(sat_conversion,[],[f934]) ).
cnf(s131,plain,
( ~ spl0_46
| ~ spl0_169 ),
inference(sat_conversion,[],[f939]) ).
cnf(s132,plain,
( ~ spl0_170
| ~ spl0_171 ),
inference(sat_conversion,[],[f946]) ).
cnf(s133,plain,
( ~ spl0_44
| spl0_172 ),
inference(sat_conversion,[],[f950]) ).
cnf(s134,plain,
( ~ spl0_44
| spl0_173 ),
inference(sat_conversion,[],[f954]) ).
cnf(s137,plain,
( ~ spl0_29
| spl0_176 ),
inference(sat_conversion,[],[f966]) ).
cnf(s138,plain,
( ~ spl0_40
| spl0_177 ),
inference(sat_conversion,[],[f970]) ).
cnf(s139,plain,
( ~ spl0_50
| spl0_178 ),
inference(sat_conversion,[],[f974]) ).
cnf(s140,plain,
( ~ spl0_66
| spl0_179 ),
inference(sat_conversion,[],[f978]) ).
cnf(s141,plain,
( ~ spl0_66
| spl0_180 ),
inference(sat_conversion,[],[f982]) ).
cnf(s142,plain,
( ~ spl0_15
| spl0_181 ),
inference(sat_conversion,[],[f986]) ).
cnf(s143,plain,
( ~ spl0_74
| spl0_182 ),
inference(sat_conversion,[],[f990]) ).
cnf(s148,plain,
( ~ spl0_111
| spl0_187 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s149,plain,
( ~ spl0_111
| spl0_188 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s150,plain,
( ~ spl0_113
| spl0_189 ),
inference(sat_conversion,[],[f1018]) ).
cnf(s151,plain,
( ~ spl0_113
| spl0_190 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s152,plain,
( ~ spl0_115
| spl0_191 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s154,plain,
( ~ spl0_60
| spl0_193 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s155,plain,
( ~ spl0_59
| spl0_194 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s157,plain,
( ~ spl0_45
| spl0_196 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s158,plain,
( ~ spl0_45
| spl0_197 ),
inference(sat_conversion,[],[f1050]) ).
cnf(s159,plain,
( ~ spl0_136
| spl0_198 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s160,plain,
( ~ spl0_76
| spl0_199 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s161,plain,
( ~ spl0_76
| spl0_200 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s163,plain,
( ~ spl0_20
| spl0_202 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s164,plain,
( ~ spl0_53
| spl0_203 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s165,plain,
( ~ spl0_53
| spl0_204 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s166,plain,
( ~ spl0_53
| spl0_205 ),
inference(sat_conversion,[],[f1083]) ).
cnf(s167,plain,
( ~ spl0_24
| spl0_206 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s168,plain,
( ~ spl0_24
| spl0_207 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s169,plain,
( ~ spl0_43
| spl0_208 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s170,plain,
( ~ spl0_43
| spl0_209 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s171,plain,
( ~ spl0_43
| spl0_210 ),
inference(sat_conversion,[],[f1104]) ).
cnf(s172,plain,
( spl0_211
| ~ spl0_212 ),
inference(sat_conversion,[],[f1111]) ).
cnf(s173,plain,
( ~ spl0_212
| spl0_213 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s174,plain,
( ~ spl0_212
| spl0_214 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s175,plain,
( ~ spl0_41
| spl0_215 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s176,plain,
( ~ spl0_19
| spl0_216 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s177,plain,
( ~ spl0_19
| spl0_217 ),
inference(sat_conversion,[],[f1132]) ).
cnf(s178,plain,
( ~ spl0_19
| spl0_218 ),
inference(sat_conversion,[],[f1136]) ).
cnf(s179,plain,
( ~ spl0_39
| spl0_219 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s180,plain,
( ~ spl0_39
| spl0_220 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s181,plain,
( ~ spl0_39
| spl0_221 ),
inference(sat_conversion,[],[f1149]) ).
cnf(s182,plain,
( ~ spl0_65
| spl0_222 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s183,plain,
( ~ spl0_65
| spl0_223 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s184,plain,
( ~ spl0_63
| spl0_224 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s185,plain,
( ~ spl0_63
| spl0_225 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s190,plain,
( ~ spl0_75
| spl0_230 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s191,plain,
( ~ spl0_75
| spl0_231 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s192,plain,
( ~ spl0_48
| spl0_232 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s193,plain,
( ~ spl0_23
| spl0_233 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s197,plain,
( ~ spl0_33
| spl0_237 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s198,plain,
( ~ spl0_70
| spl0_238 ),
inference(sat_conversion,[],[f1217]) ).
cnf(s199,plain,
( ~ spl0_70
| spl0_239 ),
inference(sat_conversion,[],[f1221]) ).
cnf(s200,plain,
( ~ spl0_46
| spl0_240 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s202,plain,
( ~ spl0_170
| spl0_242 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s203,plain,
( ~ spl0_170
| spl0_243 ),
inference(sat_conversion,[],[f1237]) ).
cnf(s204,plain,
( spl0_65
| spl0_145
| spl0_170 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s205,plain,
( spl0_29
| spl0_50
| spl0_136 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s206,plain,
( spl0_111
| spl0_113
| spl0_115 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s207,plain,
( spl0_24
| spl0_82
| spl0_212 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s239,plain,
( spl0_3
| ~ spl0_145 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s248,plain,
( spl0_3
| ~ spl0_65 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s260,plain,
( spl0_3
| ~ spl0_170 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s269,plain,
( ~ spl0_12
| spl0_147
| spl0_148
| ~ spl0_244 ),
inference(sat_conversion,[],[f1372]) ).
cnf(s270,plain,
( ~ spl0_4
| ~ spl0_12
| spl0_21 ),
inference(sat_conversion,[],[f1373]) ).
cnf(s278,plain,
( spl0_6
| ~ spl0_12
| ~ spl0_28 ),
inference(sat_conversion,[],[f1441]) ).
cnf(s280,plain,
( ~ spl0_5
| spl0_92
| ~ spl0_179
| ~ spl0_180 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s281,plain,
( ~ spl0_1
| ~ spl0_25
| spl0_32 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s283,plain,
( ~ spl0_30
| spl0_90
| spl0_91
| ~ spl0_178 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s286,plain,
( spl0_2
| ~ spl0_5
| ~ spl0_30 ),
inference(sat_conversion,[],[f1485]) ).
cnf(s287,plain,
( ~ spl0_1
| spl0_10
| ~ spl0_30 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s301,plain,
( ~ spl0_30
| spl0_86
| spl0_87
| ~ spl0_251 ),
inference(sat_conversion,[],[f1526]) ).
cnf(s309,plain,
( ~ spl0_5
| spl0_151
| ~ spl0_206
| ~ spl0_207 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s319,plain,
( ~ spl0_7
| spl0_114
| ~ spl0_189
| ~ spl0_190 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s320,plain,
( ~ spl0_7
| ~ spl0_206
| ~ spl0_207
| spl0_258 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s326,plain,
( ~ spl0_12
| spl0_83
| spl0_84
| ~ spl0_245 ),
inference(sat_conversion,[],[f1612]) ).
cnf(s332,plain,
( ~ spl0_8
| spl0_132
| spl0_133
| spl0_134 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s351,plain,
( ~ spl0_8
| spl0_116
| spl0_117
| spl0_261 ),
inference(sat_conversion,[],[f1684]) ).
cnf(s375,plain,
( spl0_9
| ~ spl0_11
| ~ spl0_17 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s378,plain,
( ~ spl0_30
| spl0_129
| ~ spl0_194
| spl0_263 ),
inference(sat_conversion,[],[f1779]) ).
cnf(s398,plain,
( ~ spl0_32
| spl0_137
| ~ spl0_198
| spl0_254 ),
inference(sat_conversion,[],[f1861]) ).
cnf(s413,plain,
( ~ spl0_8
| spl0_93
| spl0_94
| spl0_95 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s419,plain,
( ~ spl0_11
| spl0_154
| ~ spl0_223
| spl0_259 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s429,plain,
( ~ spl0_25
| spl0_86
| ~ spl0_176
| spl0_251 ),
inference(sat_conversion,[],[f1967]) ).
cnf(s431,plain,
( ~ spl0_11
| spl0_90
| ~ spl0_178
| spl0_252 ),
inference(sat_conversion,[],[f1969]) ).
cnf(s488,plain,
( ~ spl0_25
| spl0_137
| spl0_138
| ~ spl0_198 ),
inference(sat_conversion,[],[f2144]) ).
cnf(s490,plain,
( ~ spl0_25
| spl0_161
| spl0_162
| ~ spl0_233 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s496,plain,
( ~ spl0_6
| spl0_158
| ~ spl0_230
| spl0_273 ),
inference(sat_conversion,[],[f2161]) ).
cnf(s502,plain,
( ~ spl0_10
| spl0_87
| ~ spl0_176
| ~ spl0_251 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s503,plain,
( ~ spl0_10
| spl0_91
| ~ spl0_178
| ~ spl0_252 ),
inference(sat_conversion,[],[f2192]) ).
cnf(s504,plain,
( ~ spl0_10
| ~ spl0_187
| ~ spl0_188
| spl0_246 ),
inference(sat_conversion,[],[f2193]) ).
cnf(s517,plain,
( ~ spl0_16
| spl0_112
| ~ spl0_187
| ~ spl0_246 ),
inference(sat_conversion,[],[f2205]) ).
cnf(s527,plain,
( ~ spl0_38
| spl0_154
| ~ spl0_222
| spl0_259 ),
inference(sat_conversion,[],[f2215]) ).
cnf(s530,plain,
( ~ spl0_38
| spl0_99
| spl0_100
| ~ spl0_262 ),
inference(sat_conversion,[],[f2218]) ).
cnf(s546,plain,
( ~ spl0_1
| ~ spl0_238
| ~ spl0_239
| spl0_274 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s570,plain,
( ~ spl0_9
| ~ spl0_222
| ~ spl0_223
| spl0_259 ),
inference(sat_conversion,[],[f2311]) ).
cnf(s575,plain,
( ~ spl0_14
| ~ spl0_219
| ~ spl0_220
| ~ spl0_221 ),
inference(sat_conversion,[],[f2325]) ).
cnf(s592,plain,
( ~ spl0_4
| ~ spl0_196
| ~ spl0_197
| ~ spl0_266 ),
inference(sat_conversion,[],[f2393]) ).
cnf(s604,plain,
( ~ spl0_22
| spl0_135
| ~ spl0_196
| ~ spl0_197 ),
inference(sat_conversion,[],[f2405]) ).
cnf(s620,plain,
( ~ spl0_4
| ~ spl0_230
| ~ spl0_231
| ~ spl0_273 ),
inference(sat_conversion,[],[f2441]) ).
cnf(s627,plain,
( ~ spl0_11
| spl0_128
| spl0_129
| ~ spl0_194 ),
inference(sat_conversion,[],[f2473]) ).
cnf(s629,plain,
( spl0_2
| ~ spl0_7
| ~ spl0_11 ),
inference(sat_conversion,[],[f2475]) ).
cnf(s652,plain,
( ~ spl0_21
| spl0_158
| ~ spl0_230
| ~ spl0_273 ),
inference(sat_conversion,[],[f2530]) ).
cnf(s663,plain,
( ~ spl0_49
| spl0_86
| spl0_87
| spl0_251 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s667,plain,
( ~ spl0_49
| spl0_161
| spl0_162
| spl0_256 ),
inference(sat_conversion,[],[f2611]) ).
cnf(s669,plain,
( ~ spl0_22
| spl0_32
| ~ spl0_49 ),
inference(sat_conversion,[],[f2613]) ).
cnf(s670,plain,
( ~ spl0_8
| spl0_159
| spl0_160
| spl0_278 ),
inference(sat_conversion,[],[f2620]) ).
cnf(s677,plain,
( ~ spl0_52
| spl0_112
| ~ spl0_187
| ~ spl0_188 ),
inference(sat_conversion,[],[f2694]) ).
cnf(s683,plain,
( spl0_14
| ~ spl0_17
| ~ spl0_52 ),
inference(sat_conversion,[],[f2701]) ).
cnf(s684,plain,
( ~ spl0_4
| spl0_14
| ~ spl0_52 ),
inference(sat_conversion,[],[f2702]) ).
cnf(s694,plain,
( ~ spl0_36
| spl0_159
| ~ spl0_232
| spl0_278 ),
inference(sat_conversion,[],[f2734]) ).
cnf(s748,plain,
( ~ spl0_10
| spl0_114
| ~ spl0_189
| ~ spl0_255 ),
inference(sat_conversion,[],[f2806]) ).
cnf(s749,plain,
( ~ spl0_42
| spl0_116
| spl0_117
| ~ spl0_191 ),
inference(sat_conversion,[],[f2810]) ).
cnf(s750,plain,
( ~ spl0_36
| spl0_116
| ~ spl0_191
| spl0_261 ),
inference(sat_conversion,[],[f2811]) ).
cnf(s756,plain,
( ~ spl0_10
| spl0_155
| ~ spl0_225
| ~ spl0_280 ),
inference(sat_conversion,[],[f2831]) ).
cnf(s767,plain,
( ~ spl0_16
| spl0_154
| ~ spl0_222
| ~ spl0_259 ),
inference(sat_conversion,[],[f2882]) ).
cnf(s772,plain,
( ~ spl0_22
| spl0_158
| ~ spl0_231
| ~ spl0_273 ),
inference(sat_conversion,[],[f2899]) ).
cnf(s773,plain,
( ~ spl0_25
| spl0_101
| spl0_102
| ~ spl0_182 ),
inference(sat_conversion,[],[f2918]) ).
cnf(s774,plain,
( ~ spl0_25
| spl0_126
| spl0_127
| ~ spl0_193 ),
inference(sat_conversion,[],[f2919]) ).
cnf(s780,plain,
( ~ spl0_32
| spl0_87
| ~ spl0_176
| spl0_251 ),
inference(sat_conversion,[],[f2943]) ).
cnf(s783,plain,
( ~ spl0_32
| spl0_152
| spl0_153
| ~ spl0_215 ),
inference(sat_conversion,[],[f2946]) ).
cnf(s786,plain,
( ~ spl0_7
| spl0_155
| ~ spl0_224
| ~ spl0_225 ),
inference(sat_conversion,[],[f2950]) ).
cnf(s791,plain,
( ~ spl0_14
| ~ spl0_222
| ~ spl0_223
| ~ spl0_259 ),
inference(sat_conversion,[],[f2955]) ).
cnf(s793,plain,
( ~ spl0_14
| ~ spl0_187
| ~ spl0_188
| ~ spl0_246 ),
inference(sat_conversion,[],[f2957]) ).
cnf(s797,plain,
( ~ spl0_28
| ~ spl0_230
| ~ spl0_231
| spl0_273 ),
inference(sat_conversion,[],[f2961]) ).
cnf(s803,plain,
( ~ spl0_38
| spl0_166
| spl0_167
| ~ spl0_237 ),
inference(sat_conversion,[],[f2967]) ).
cnf(s805,plain,
( ~ spl0_38
| spl0_146
| spl0_148
| ~ spl0_244 ),
inference(sat_conversion,[],[f2969]) ).
cnf(s807,plain,
( ~ spl0_49
| spl0_147
| spl0_148
| spl0_244 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s809,plain,
( ~ spl0_49
| spl0_108
| spl0_110
| spl0_267 ),
inference(sat_conversion,[],[f2973]) ).
cnf(s813,plain,
( ~ spl0_49
| spl0_126
| spl0_127
| spl0_264 ),
inference(sat_conversion,[],[f2977]) ).
cnf(s814,plain,
( ~ spl0_49
| spl0_101
| spl0_102
| spl0_270 ),
inference(sat_conversion,[],[f2978]) ).
cnf(s820,plain,
( ~ spl0_1
| spl0_149
| ~ spl0_202
| ~ spl0_265 ),
inference(sat_conversion,[],[f2984]) ).
cnf(s821,plain,
( ~ spl0_32
| spl0_135
| ~ spl0_196
| spl0_266 ),
inference(sat_conversion,[],[f2988]) ).
cnf(s823,plain,
( ~ spl0_1
| spl0_77
| ~ spl0_172
| ~ spl0_173 ),
inference(sat_conversion,[],[f2996]) ).
cnf(s824,plain,
( ~ spl0_4
| ~ spl0_211
| ~ spl0_213
| ~ spl0_214 ),
inference(sat_conversion,[],[f2997]) ).
cnf(s869,plain,
( ~ spl0_52
| spl0_171
| ~ spl0_242
| ~ spl0_275 ),
inference(sat_conversion,[],[f3039]) ).
cnf(s873,plain,
( ~ spl0_38
| spl0_84
| spl0_85
| ~ spl0_245 ),
inference(sat_conversion,[],[f3043]) ).
cnf(s883,plain,
( ~ spl0_10
| spl0_169
| ~ spl0_240
| ~ spl0_283 ),
inference(sat_conversion,[],[f3060]) ).
cnf(s889,plain,
( ~ spl0_6
| spl0_88
| spl0_89
| ~ spl0_177 ),
inference(sat_conversion,[],[f3088]) ).
cnf(s895,plain,
( ~ spl0_9
| spl0_128
| ~ spl0_194
| ~ spl0_263 ),
inference(sat_conversion,[],[f3105]) ).
cnf(s900,plain,
( spl0_2
| ~ spl0_11
| ~ spl0_36 ),
inference(sat_conversion,[],[f3111]) ).
cnf(s903,plain,
( ~ spl0_51
| spl0_96
| spl0_97
| spl0_98 ),
inference(sat_conversion,[],[f3114]) ).
cnf(s918,plain,
( ~ spl0_14
| ~ spl0_151
| ~ spl0_206
| ~ spl0_258 ),
inference(sat_conversion,[],[f3128]) ).
cnf(s919,plain,
( ~ spl0_10
| ~ spl0_151
| ~ spl0_206
| spl0_258 ),
inference(sat_conversion,[],[f3129]) ).
cnf(s920,plain,
( ~ spl0_28
| spl0_151
| ~ spl0_207
| ~ spl0_258 ),
inference(sat_conversion,[],[f3130]) ).
cnf(s926,plain,
( ~ spl0_9
| ~ spl0_199
| ~ spl0_200
| spl0_282 ),
inference(sat_conversion,[],[f3140]) ).
cnf(s927,plain,
( ~ spl0_9
| spl0_151
| ~ spl0_206
| ~ spl0_258 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s933,plain,
( ~ spl0_14
| ~ spl0_199
| ~ spl0_200
| ~ spl0_282 ),
inference(sat_conversion,[],[f3178]) ).
cnf(s934,plain,
( ~ spl0_14
| ~ spl0_208
| ~ spl0_209
| ~ spl0_210 ),
inference(sat_conversion,[],[f3179]) ).
cnf(s967,plain,
( ~ spl0_34
| spl0_135
| ~ spl0_197
| spl0_266 ),
inference(sat_conversion,[],[f3212]) ).
cnf(s982,plain,
( ~ spl0_1
| ~ spl0_196
| ~ spl0_197
| spl0_266 ),
inference(sat_conversion,[],[f3234]) ).
cnf(s984,plain,
( ~ spl0_8
| spl0_83
| spl0_85
| spl0_245 ),
inference(sat_conversion,[],[f3252]) ).
cnf(s986,plain,
( ~ spl0_8
| spl0_146
| spl0_147
| spl0_244 ),
inference(sat_conversion,[],[f3254]) ).
cnf(s988,plain,
( ~ spl0_8
| spl0_149
| spl0_150
| spl0_265 ),
inference(sat_conversion,[],[f3256]) ).
cnf(s992,plain,
( ~ spl0_12
| spl0_171
| ~ spl0_243
| spl0_275 ),
inference(sat_conversion,[],[f3275]) ).
cnf(s995,plain,
( ~ spl0_17
| ~ spl0_206
| ~ spl0_207
| ~ spl0_258 ),
inference(sat_conversion,[],[f3290]) ).
cnf(s998,plain,
( ~ spl0_21
| spl0_102
| ~ spl0_182
| ~ spl0_270 ),
inference(sat_conversion,[],[f3310]) ).
cnf(s999,plain,
( ~ spl0_21
| spl0_135
| ~ spl0_196
| ~ spl0_266 ),
inference(sat_conversion,[],[f3311]) ).
cnf(s1000,plain,
( ~ spl0_21
| spl0_137
| ~ spl0_198
| ~ spl0_254 ),
inference(sat_conversion,[],[f3312]) ).
cnf(s1001,plain,
( ~ spl0_21
| spl0_162
| ~ spl0_233
| ~ spl0_256 ),
inference(sat_conversion,[],[f3313]) ).
cnf(s1044,plain,
( ~ spl0_21
| spl0_127
| ~ spl0_193
| ~ spl0_264 ),
inference(sat_conversion,[],[f3364]) ).
cnf(s1047,plain,
( ~ spl0_21
| spl0_168
| ~ spl0_238
| ~ spl0_274 ),
inference(sat_conversion,[],[f3374]) ).
cnf(s1049,plain,
( ~ spl0_2
| spl0_91
| ~ spl0_178
| spl0_252 ),
inference(sat_conversion,[],[f3396]) ).
cnf(s1051,plain,
( ~ spl0_2
| spl0_100
| ~ spl0_181
| spl0_262 ),
inference(sat_conversion,[],[f3398]) ).
cnf(s1053,plain,
( ~ spl0_2
| spl0_151
| ~ spl0_206
| spl0_258 ),
inference(sat_conversion,[],[f3400]) ).
cnf(s1054,plain,
( ~ spl0_2
| spl0_155
| ~ spl0_225
| spl0_280 ),
inference(sat_conversion,[],[f3401]) ).
cnf(s1056,plain,
( ~ spl0_2
| spl0_169
| ~ spl0_240
| spl0_283 ),
inference(sat_conversion,[],[f3404]) ).
cnf(s1074,plain,
( ~ spl0_11
| spl0_99
| spl0_100
| ~ spl0_181 ),
inference(sat_conversion,[],[f3421]) ).
cnf(s1118,plain,
( ~ spl0_28
| spl0_116
| ~ spl0_191
| ~ spl0_261 ),
inference(sat_conversion,[],[f3464]) ).
cnf(s1120,plain,
( ~ spl0_30
| spl0_108
| spl0_110
| ~ spl0_267 ),
inference(sat_conversion,[],[f3466]) ).
cnf(s1122,plain,
( ~ spl0_51
| spl0_108
| spl0_109
| spl0_110 ),
inference(sat_conversion,[],[f3468]) ).
cnf(s1123,plain,
( ~ spl0_51
| spl0_84
| spl0_85
| spl0_245 ),
inference(sat_conversion,[],[f3469]) ).
cnf(s1125,plain,
( ~ spl0_51
| spl0_146
| spl0_148
| spl0_244 ),
inference(sat_conversion,[],[f3471]) ).
cnf(s1126,plain,
( ~ spl0_51
| spl0_118
| spl0_119
| spl0_120 ),
inference(sat_conversion,[],[f3472]) ).
cnf(s1137,plain,
( ~ spl0_4
| ~ spl0_203
| ~ spl0_204
| ~ spl0_205 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s1138,plain,
( ~ spl0_4
| ~ spl0_216
| ~ spl0_217
| ~ spl0_218 ),
inference(sat_conversion,[],[f3495]) ).
cnf(s1139,plain,
( ~ spl0_4
| ~ spl0_238
| ~ spl0_239
| ~ spl0_274 ),
inference(sat_conversion,[],[f3496]) ).
cnf(s1141,plain,
( ~ spl0_5
| ~ spl0_189
| ~ spl0_190
| spl0_255 ),
inference(sat_conversion,[],[f3507]) ).
cnf(s1143,plain,
( ~ spl0_5
| ~ spl0_224
| ~ spl0_225
| spl0_280 ),
inference(sat_conversion,[],[f3509]) ).
cnf(s1149,plain,
( ~ spl0_11
| spl0_139
| ~ spl0_199
| spl0_282 ),
inference(sat_conversion,[],[f3534]) ).
cnf(s1156,plain,
( ~ spl0_16
| spl0_139
| ~ spl0_200
| ~ spl0_282 ),
inference(sat_conversion,[],[f3559]) ).
cnf(s1157,plain,
( ~ spl0_16
| spl0_171
| ~ spl0_242
| ~ spl0_243 ),
inference(sat_conversion,[],[f3560]) ).
cnf(s1163,plain,
( ~ spl0_22
| spl0_160
| ~ spl0_232
| ~ spl0_278 ),
inference(sat_conversion,[],[f3579]) ).
cnf(s1164,plain,
( ~ spl0_22
| spl0_168
| ~ spl0_238
| ~ spl0_239 ),
inference(sat_conversion,[],[f3581]) ).
cnf(s1166,plain,
spl0_3,
inference(rat,[],[s204,s239,s248,s260]) ).
cnf(s1167,plain,
( ~ spl0_19
| ~ spl0_4 ),
inference(rat,[],[s1138,s176,s177,s178]) ).
cnf(s1171,plain,
( ~ spl0_53
| ~ spl0_4 ),
inference(rat,[],[s1137,s164,s165,s166]) ).
cnf(s1175,plain,
( ~ spl0_60
| ~ spl0_49
| ~ spl0_21 ),
inference(rat,[],[s813,s1044,s90,s91,s154]) ).
cnf(s1178,plain,
( ~ spl0_37
| ~ spl0_8 ),
inference(rat,[],[s413,s60,s61,s62]) ).
cnf(s1179,plain,
( ~ spl0_23
| ~ spl0_49
| ~ spl0_21 ),
inference(rat,[],[s667,s1001,s123,s124,s193]) ).
cnf(s1181,plain,
( ~ spl0_31
| ~ spl0_30
| ~ spl0_49 ),
inference(rat,[],[s809,s1120,s75,s77]) ).
cnf(s1184,plain,
( ~ spl0_45
| ~ spl0_32
| ~ spl0_4 ),
inference(rat,[],[s821,s592,s99,s157,s158]) ).
cnf(s1185,plain,
( ~ spl0_41
| ~ spl0_215
| ~ spl0_32 ),
inference(rat,[],[s783,s114,s115]) ).
cnf(s1189,plain,
( ~ spl0_50
| ~ spl0_30 ),
inference(rat,[],[s283,s57,s58,s139]) ).
cnf(s1190,plain,
( ~ spl0_136
| ~ spl0_25 ),
inference(rat,[],[s488,s100,s101,s159]) ).
cnf(s1191,plain,
( ~ spl0_49
| ~ spl0_65
| spl0_28
| ~ spl0_21
| spl0_11
| spl0_5
| ~ spl0_4 ),
inference(rat,[],[s502,s780,s54,s137,s205,s1190,s1189,s26,s1184,s16,s1181,s3,s33,s1178,s19,s527,s570,s767,s13,s1179,s1167,s183,s182,s116,s1166]) ).
cnf(s1193,plain,
( ~ spl0_45
| ~ spl0_22 ),
inference(rat,[],[s604,s99,s157,s158]) ).
cnf(s1197,plain,
( ~ spl0_212
| ~ spl0_4 ),
inference(rat,[],[s824,s172,s173,s174]) ).
cnf(s1198,plain,
( ~ spl0_82
| ~ spl0_38
| ~ spl0_8 ),
inference(rat,[],[s984,s873,s50,s51,s52]) ).
cnf(s1200,plain,
( ~ spl0_170
| ~ spl0_16 ),
inference(rat,[],[s1157,s132,s202,s203]) ).
cnf(s1201,plain,
( ~ spl0_49
| spl0_28
| ~ spl0_12
| spl0_11
| spl0_5
| ~ spl0_4 ),
inference(rat,[],[s269,s807,s109,s110,s204,s1200,s13,s1191,s1179,s270,s1166]) ).
cnf(s1202,plain,
( spl0_6
| spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s301,s429,s53,s54,s137,s205,s1189,s33,s1190,s670,s26,s1163,s1193,s121,s122,s192,s31,s29,s1201,s278,s4,s629,s2,s1167,s1171,s1,s1166]) ).
cnf(s1203,plain,
( ~ spl0_24
| ~ spl0_7
| ~ spl0_28 ),
inference(rat,[],[s920,s320,s113,s167,s168]) ).
cnf(s1204,plain,
( spl0_24
| ~ spl0_12
| spl0_11
| ~ spl0_49
| ~ spl0_4 ),
inference(rat,[],[s780,s502,s54,s137,s205,s1190,s26,s1184,s16,s3,s926,s933,s160,s161,s1189,s1181,s44,s24,s33,s1123,s984,s326,s50,s51,s52,s207,s1167,s1197,s1166]) ).
cnf(s1205,plain,
( ~ spl0_33
| ~ spl0_38 ),
inference(rat,[],[s803,s128,s129,s197]) ).
cnf(s1206,plain,
( ~ spl0_45
| ~ spl0_34
| ~ spl0_4 ),
inference(rat,[],[s967,s592,s99,s157,s158]) ).
cnf(s1211,plain,
( ~ spl0_75
| ~ spl0_28
| ~ spl0_4 ),
inference(rat,[],[s620,s797,s190,s191]) ).
cnf(s1212,plain,
( spl0_30
| spl0_75
| spl0_7
| spl0_11
| spl0_5
| ~ spl0_4 ),
inference(rat,[],[s773,s68,s69,s143,s43,s26,s1206,s17,s1205,s19,s1178,s33,s1167,s1166]) ).
cnf(s1214,plain,
( ~ spl0_29
| ~ spl0_30
| ~ spl0_49 ),
inference(rat,[],[s301,s663,s53,s54]) ).
cnf(s1215,plain,
( spl0_11
| ~ spl0_49
| spl0_5
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s895,s378,s92,s93,s155,s35,s16,s1193,s398,s26,s1000,s1190,s100,s159,s205,s1214,s1189,s1181,s1212,s1211,s1203,s1204,s1175,s1201,s270,s4,s1166]) ).
cnf(s1217,plain,
( ~ spl0_75
| ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s496,s620,s120,s190,s191]) ).
cnf(s1218,plain,
( ~ spl0_40
| ~ spl0_6 ),
inference(rat,[],[s889,s55,s56,s138]) ).
cnf(s1219,plain,
( ~ spl0_74
| ~ spl0_49
| ~ spl0_21 ),
inference(rat,[],[s814,s998,s68,s69,s143]) ).
cnf(s1220,plain,
( ~ spl0_59
| ~ spl0_11 ),
inference(rat,[],[s627,s92,s93,s155]) ).
cnf(s1221,plain,
( ~ spl0_49
| ~ spl0_21
| spl0_75
| spl0_5
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s669,s398,s35,s1000,s1220,s100,s159,s205,s1214,s1189,s43,s1219,s1175,s1215,s1166]) ).
cnf(s1222,plain,
( ~ spl0_25
| ~ spl0_30 ),
inference(rat,[],[s301,s429,s53,s54,s137,s205,s1190,s1189]) ).
cnf(s1223,plain,
( ~ spl0_76
| ~ spl0_14
| ~ spl0_11 ),
inference(rat,[],[s1149,s933,s102,s160,s161]) ).
cnf(s1224,plain,
( ~ spl0_31
| ~ spl0_51 ),
inference(rat,[],[s1122,s75,s76,s77]) ).
cnf(s1225,plain,
( ~ spl0_145
| ~ spl0_51
| ~ spl0_12 ),
inference(rat,[],[s1125,s269,s108,s109,s110]) ).
cnf(s1227,plain,
( ~ spl0_15
| ~ spl0_11 ),
inference(rat,[],[s1074,s66,s67,s142]) ).
cnf(s1230,plain,
( ~ spl0_64
| ~ spl0_51 ),
inference(rat,[],[s903,s63,s64,s65]) ).
cnf(s1232,plain,
( ~ spl0_71
| ~ spl0_51 ),
inference(rat,[],[s1126,s82,s83,s84]) ).
cnf(s1233,plain,
( ~ spl0_70
| ~ spl0_22 ),
inference(rat,[],[s1164,s130,s198,s199]) ).
cnf(s1234,plain,
( spl0_49
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s684,s1223,s30,s44,s1232,s41,s1233,s26,s1222,s1189,s33,s694,s670,s1163,s1193,s121,s122,s192,s31,s29,s1167,s1171,s1166]) ).
cnf(s1235,plain,
( spl0_11
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s309,s113,s167,s168,s1204,s1215,s4,s1234,s1166]) ).
cnf(s1236,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s21,s1221,s1218,s1217,s1202,s1234,s1,s1166]) ).
cnf(s1237,plain,
( ~ spl0_13
| ~ spl0_8 ),
inference(rat,[],[s332,s96,s97,s98]) ).
cnf(s1238,plain,
( ~ spl0_14
| spl0_36
| ~ spl0_11
| ~ spl0_49 ),
inference(rat,[],[s934,s169,s170,s171,s23,s1175,s35,s1233,s41,s1232,s44,s1223,s1220,s1166]) ).
cnf(s1239,plain,
( ~ spl0_50
| ~ spl0_10
| ~ spl0_11 ),
inference(rat,[],[s503,s431,s57,s58,s139]) ).
cnf(s1240,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s756,s1143,s117,s184,s185,s37,s1230,s30,s1239,s5,s684,s1238,s1237,s33,s286,s1236,s900,s1235,s1234,s1167,s1,s1166]) ).
cnf(s1243,plain,
( ~ spl0_65
| ~ spl0_38
| ~ spl0_14 ),
inference(rat,[],[s527,s791,s116,s182,s183]) ).
cnf(s1244,plain,
( ~ spl0_50
| ~ spl0_10
| ~ spl0_2 ),
inference(rat,[],[s503,s1049,s58,s139]) ).
cnf(s1245,plain,
( ~ spl0_170
| ~ spl0_52
| ~ spl0_12 ),
inference(rat,[],[s869,s992,s132,s202,s203]) ).
cnf(s1246,plain,
( ~ spl0_10
| spl0_51
| ~ spl0_14
| spl0_145
| spl0_5
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s1056,s883,s131,s200,s27,s1178,s19,s1243,s204,s1245,s30,s1244,s1166]) ).
cnf(s1251,plain,
( ~ spl0_38
| spl0_154
| ~ spl0_222
| spl0_17
| ~ spl0_2 ),
inference(rat,[],[s1051,s530,s66,s67,s142,s6,s767,s527,s1166]) ).
cnf(s1252,plain,
( ~ spl0_46
| ~ spl0_10
| ~ spl0_2 ),
inference(rat,[],[s1056,s883,s131,s200]) ).
cnf(s1253,plain,
( ~ spl0_52
| ~ spl0_38
| spl0_14
| spl0_145
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s1251,s116,s182,s204,s1245,s683]) ).
cnf(s1254,plain,
( ~ spl0_10
| spl0_14
| spl0_145
| spl0_5
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s756,s1054,s117,s185,s37,s1230,s30,s1253,s19,s1178,s27,s1252,s1244,s1166]) ).
cnf(s1256,plain,
( ~ spl0_145
| ~ spl0_8
| ~ spl0_12 ),
inference(rat,[],[s986,s269,s108,s109,s110]) ).
cnf(s1257,plain,
( ~ spl0_39
| ~ spl0_14 ),
inference(rat,[],[s575,s179,s180,s181]) ).
cnf(s1258,plain,
( ~ spl0_10
| spl0_51
| ~ spl0_14
| ~ spl0_2
| spl0_5
| ~ spl0_12 ),
inference(rat,[],[s27,s1256,s1252,s1246,s1166]) ).
cnf(s1259,plain,
( spl0_10
| spl0_30
| spl0_39 ),
inference(rat,[],[s490,s123,s124,s193,s20,s15,s1166]) ).
cnf(s1260,plain,
( ~ spl0_10
| ~ spl0_14
| ~ spl0_12
| ~ spl0_2
| spl0_5 ),
inference(rat,[],[s756,s1054,s117,s185,s37,s1245,s204,s1243,s19,s1178,s27,s1225,s1230,s1252,s1258,s1166]) ).
cnf(s1261,plain,
( spl0_10
| spl0_39 ),
inference(rat,[],[s1222,s1259,s20,s1166]) ).
cnf(s1262,plain,
( ~ spl0_14
| spl0_5
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s1261,s1260,s1257]) ).
cnf(s1263,plain,
( ~ spl0_10
| spl0_5
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s1256,s27,s1254,s1252,s1262,s1166]) ).
cnf(s1264,plain,
( spl0_5
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s927,s1053,s113,s167,s24,s3,s1237,s5,s1263,s1262,s1166]) ).
cnf(s1265,plain,
( ~ spl0_24
| ~ spl0_5 ),
inference(rat,[],[s309,s113,s167,s168]) ).
cnf(s1266,plain,
( ~ spl0_10
| ~ spl0_25
| ~ spl0_2 ),
inference(rat,[],[s429,s502,s53,s54,s137,s205,s1244,s1190]) ).
cnf(s1267,plain,
( ~ spl0_25
| ~ spl0_2 ),
inference(rat,[],[s490,s123,s124,s193,s15,s1266,s1222,s1166]) ).
cnf(s1268,plain,
( ~ spl0_4
| spl0_65
| spl0_82
| ~ spl0_38
| spl0_15
| spl0_1 ),
inference(rat,[],[s805,s807,s108,s109,s110,s204,s1200,s6,s995,s1053,s113,s167,s168,s207,s1234,s1197,s1240,s1166]) ).
cnf(s1269,plain,
( ~ spl0_14
| spl0_5
| spl0_1 ),
inference(rat,[],[s805,s1125,s108,s110,s204,s1200,s6,s995,s1053,s113,s167,s168,s11,s1268,s1243,s1198,s19,s1178,s27,s1252,s1261,s44,s1257,s1223,s1267,s1227,s4,s1264,s1240,s1166]) ).
cnf(s1270,plain,
( spl0_251
| spl0_5
| spl0_1 ),
inference(rat,[],[s1156,s1149,s102,s160,s161,s44,s1224,s16,s6,s927,s995,s1053,s113,s167,s168,s11,s1234,s663,s780,s1227,s4,s1264,s137,s54,s53,s14,s1269,s1267,s1240,s1166]) ).
cnf(s1271,plain,
( spl0_5
| spl0_1 ),
inference(rat,[],[s927,s1053,s113,s167,s24,s3,s1237,s5,s502,s1270,s54,s137,s14,s1269,s1267,s1240,s1166]) ).
cnf(s1272,plain,
( ~ spl0_65
| ~ spl0_14
| ~ spl0_11 ),
inference(rat,[],[s419,s791,s116,s182,s183]) ).
cnf(s1273,plain,
( spl0_151
| ~ spl0_206
| ~ spl0_9
| ~ spl0_2 ),
inference(rat,[],[s927,s1053]) ).
cnf(s1274,plain,
( ~ spl0_206
| ~ spl0_9
| ~ spl0_14
| ~ spl0_2 ),
inference(rat,[],[s918,s919,s1273,s1261,s1257]) ).
cnf(s1275,plain,
( ~ spl0_63
| ~ spl0_10
| ~ spl0_5 ),
inference(rat,[],[s756,s1143,s117,s184,s185]) ).
cnf(s1284,plain,
( ~ spl0_115
| ~ spl0_28
| ~ spl0_36 ),
inference(rat,[],[s750,s1118,s80,s152]) ).
cnf(s1285,plain,
( ~ spl0_113
| ~ spl0_7 ),
inference(rat,[],[s319,s79,s150,s151]) ).
cnf(s1286,plain,
( ~ spl0_111
| ~ spl0_52 ),
inference(rat,[],[s677,s78,s148,s149]) ).
cnf(s1287,plain,
( ~ spl0_113
| ~ spl0_10
| ~ spl0_5 ),
inference(rat,[],[s1141,s748,s79,s150,s151]) ).
cnf(s1288,plain,
( ~ spl0_66
| ~ spl0_5 ),
inference(rat,[],[s280,s59,s140,s141]) ).
cnf(s1289,plain,
( ~ spl0_14
| spl0_1 ),
inference(rat,[],[s1286,s206,s37,s1284,s1287,s1275,s1230,s38,s1261,s44,s1272,s1238,s1257,s1223,s1234,s1235,s11,s1265,s1267,s1240,s1288,s1271,s1166]) ).
cnf(s1290,plain,
spl0_1,
inference(rat,[],[s502,s5,s663,s1237,s53,s54,s137,s24,s14,s1289,s1234,s11,s1265,s1271,s1267,s1240,s1166]) ).
cnf(s1291,plain,
( ~ spl0_5
| spl0_71
| spl0_64
| spl0_65
| spl0_59
| ~ spl0_10 ),
inference(rat,[],[s774,s11,s90,s91,s154,s1139,s35,s546,s1233,s198,s199,s41,s1284,s206,s1286,s37,s38,s1287,s1275,s1288,s1265,s1166,s1290]) ).
cnf(s1292,plain,
( ~ spl0_2
| spl0_212
| ~ spl0_11
| ~ spl0_14 ),
inference(rat,[],[s805,s1125,s108,s110,s204,s1200,s6,s375,s1274,s167,s207,s1198,s19,s1178,s27,s1252,s1227,s1291,s1232,s1230,s44,s1223,s1272,s1220,s1261,s1257,s1166]) ).
cnf(s1293,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_14 ),
inference(rat,[],[s1233,s31,s41,s1238,s900,s1292,s1197,s1171,s1232,s44,s1223,s1166]) ).
cnf(s1294,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_14 ),
inference(rat,[],[s805,s1125,s108,s110,s204,s1200,s6,s375,s19,s1274,s1178,s167,s27,s11,s1252,s1267,s1227,s1291,s1232,s1230,s44,s1223,s1272,s1220,s1261,s1257,s1293,s1166]) ).
cnf(s1295,plain,
( ~ spl0_11
| ~ spl0_14 ),
inference(rat,[],[s1047,s21,s546,s1218,s130,s198,s199,s2,s41,s629,s900,s1294,s1291,s1232,s1230,s44,s1272,s1223,s1220,s1261,s1257,s1166,s1290]) ).
cnf(s1296,plain,
( spl0_25
| spl0_24
| spl0_11 ),
inference(rat,[],[s592,s982,s157,s158,s26,s11,s1290,s1166]) ).
cnf(s1297,plain,
( ~ spl0_41
| ~ spl0_32 ),
inference(rat,[],[s1185,s175]) ).
cnf(s1298,plain,
( ~ spl0_115
| ~ spl0_8
| spl0_41 ),
inference(rat,[],[s1118,s22,s351,s749,s80,s81,s152,s1166]) ).
cnf(s1299,plain,
( ~ spl0_111
| ~ spl0_14 ),
inference(rat,[],[s504,s793,s148,s149,s1261,s1257]) ).
cnf(s1300,plain,
~ spl0_44,
inference(rat,[],[s823,s45,s133,s134,s1290]) ).
cnf(s1301,plain,
( spl0_8
| spl0_30 ),
inference(rat,[],[s1167,s25,s33,s1300,s1166]) ).
cnf(s1302,plain,
( ~ spl0_5
| ~ spl0_14 ),
inference(rat,[],[s1301,s1298,s1297,s281,s1222,s206,s1296,s1287,s1265,s1261,s1257,s1295,s1299,s1290]) ).
cnf(s1303,plain,
( ~ spl0_45
| ~ spl0_4 ),
inference(rat,[],[s592,s982,s157,s158,s1290]) ).
cnf(s1304,plain,
( ~ spl0_4
| ~ spl0_14 ),
inference(rat,[],[s1217,s1212,s2,s1285,s206,s1298,s1297,s1301,s281,s1222,s26,s1303,s1295,s1299,s1302,s1166,s1290]) ).
cnf(s1305,plain,
( ~ spl0_20
| ~ spl0_8 ),
inference(rat,[],[s988,s820,s111,s112,s163,s1290]) ).
cnf(s1306,plain,
( ~ spl0_45
| spl0_20 ),
inference(rat,[],[s999,s9,s982,s1193,s99,s157,s158,s1166,s1290]) ).
cnf(s1307,plain,
( ~ spl0_70
| ~ spl0_21 ),
inference(rat,[],[s1047,s546,s130,s198,s199,s1290]) ).
cnf(s1309,plain,
( ~ spl0_75
| ~ spl0_28
| ~ spl0_21 ),
inference(rat,[],[s652,s797,s120,s190,s191]) ).
cnf(s1310,plain,
( ~ spl0_74
| ~ spl0_25 ),
inference(rat,[],[s773,s68,s69,s143]) ).
cnf(s1311,plain,
~ spl0_14,
inference(rat,[],[s496,s652,s120,s190,s43,s1310,s21,s1218,s2,s1285,s206,s1298,s1297,s281,s1267,s1222,s26,s1306,s1305,s25,s1304,s1302,s1299,s1295,s1166,s1290,s1300]) ).
cnf(s1313,plain,
( ~ spl0_10
| spl0_52
| ~ spl0_2
| ~ spl0_11 ),
inference(rat,[],[s756,s1054,s117,s185,s37,s1230,s30,s1239,s1166]) ).
cnf(s1314,plain,
spl0_10,
inference(rat,[],[s1237,s1301,s5,s287,s1166,s1311,s1290]) ).
cnf(s1315,plain,
( ~ spl0_4
| ~ spl0_11 ),
inference(rat,[],[s1139,s546,s198,s199,s41,s1232,s900,s30,s1313,s684,s1239,s1290,s1166,s1314,s1311]) ).
cnf(s1316,plain,
( ~ spl0_2
| ~ spl0_11 ),
inference(rat,[],[s1156,s1149,s102,s160,s161,s44,s1224,s16,s780,s1273,s502,s6,s113,s167,s54,s137,s683,s11,s14,s1313,s1267,s1227,s1315,s1166,s1314,s1311]) ).
cnf(s1317,plain,
( spl0_51
| ~ spl0_11 ),
inference(rat,[],[s1156,s6,s1149,s683,s102,s160,s161,s30,s44,s1227,s1239,s1166,s1311,s1314]) ).
cnf(s1318,plain,
~ spl0_11,
inference(rat,[],[s9,s1307,s1233,s41,s1232,s1317,s900,s1316,s1305,s25,s1315,s1166,s1300]) ).
cnf(s1319,plain,
( ~ spl0_63
| spl0_6 ),
inference(rat,[],[s2,s786,s1275,s117,s184,s185,s1166,s1314]) ).
cnf(s1320,plain,
~ spl0_4,
inference(rat,[],[s490,s123,s124,s193,s13,s1156,s926,s102,s160,s161,s44,s1230,s37,s1319,s1217,s1211,s43,s1310,s1222,s26,s8,s684,s1303,s1167,s1166,s1318,s1311]) ).
cnf(s1321,plain,
spl0_8,
inference(rat,[],[s25,s1300,s1166,s1320]) ).
cnf(s1322,plain,
~ spl0_37,
inference(rat,[],[s1178,s1321]) ).
cnf(s1324,plain,
~ spl0_20,
inference(rat,[],[s1305,s1321]) ).
cnf(s1325,plain,
~ spl0_45,
inference(rat,[],[s1306,s1324]) ).
cnf(s1326,plain,
spl0_25,
inference(rat,[],[s26,s1318,s1166,s1325]) ).
cnf(s1328,plain,
~ spl0_30,
inference(rat,[],[s1222,s1326]) ).
cnf(s1330,plain,
spl0_32,
inference(rat,[],[s281,s1290,s1326]) ).
cnf(s1331,plain,
~ spl0_74,
inference(rat,[],[s1310,s1326]) ).
cnf(s1332,plain,
~ spl0_41,
inference(rat,[],[s1297,s1330]) ).
cnf(s1333,plain,
spl0_75,
inference(rat,[],[s43,s1328,s1166,s1331]) ).
cnf(s1334,plain,
~ spl0_115,
inference(rat,[],[s1298,s1321,s1332]) ).
cnf(s1335,plain,
spl0_231,
inference(rat,[],[s191,s1333]) ).
cnf(s1336,plain,
spl0_230,
inference(rat,[],[s190,s1333]) ).
cnf(s1337,plain,
~ spl0_158,
inference(rat,[],[s120,s1333]) ).
cnf(s1350,plain,
~ spl0_28,
inference(rat,[],[s772,s9,s797,s1309,s1337,s1335,s1166,s1324,s1336,s1333]) ).
cnf(s1353,plain,
~ spl0_23,
inference(rat,[],[s490,s123,s124,s193,s1326]) ).
cnf(s1354,plain,
spl0_12,
inference(rat,[],[s10,s1166,s1311,s1353]) ).
cnf(s1355,plain,
spl0_16,
inference(rat,[],[s13,s1350,s1166,s1353]) ).
cnf(s1357,plain,
~ spl0_145,
inference(rat,[],[s1256,s1321,s1354]) ).
cnf(s1358,plain,
~ spl0_170,
inference(rat,[],[s1200,s1355]) ).
cnf(s1361,plain,
spl0_65,
inference(rat,[],[s204,s1358,s1357]) ).
cnf(s1367,plain,
spl0_222,
inference(rat,[],[s182,s1361]) ).
cnf(s1368,plain,
~ spl0_154,
inference(rat,[],[s116,s1361]) ).
cnf(s1372,plain,
~ spl0_259,
inference(rat,[],[s767,s1355,s1367,s1368]) ).
cnf(s1377,plain,
~ spl0_38,
inference(rat,[],[s527,s1368,s1367,s1372]) ).
cnf(s1379,plain,
spl0_5,
inference(rat,[],[s19,s1322,s1166,s1377]) ).
cnf(s1385,plain,
~ spl0_113,
inference(rat,[],[s1287,s1314,s1379]) ).
cnf(s1387,plain,
spl0_111,
inference(rat,[],[s206,s1334,s1385]) ).
cnf(s1388,plain,
spl0_188,
inference(rat,[],[s149,s1387]) ).
cnf(s1389,plain,
spl0_187,
inference(rat,[],[s148,s1387]) ).
cnf(s1390,plain,
~ spl0_112,
inference(rat,[],[s78,s1387]) ).
cnf(s1391,plain,
spl0_246,
inference(rat,[],[s504,s1314,s1388,s1389]) ).
cnf(s1392,plain,
$false,
inference(rat,[],[s517,s1390,s1355,s1389,s1391]) ).
fof(f3583,plain,
$false,
inference(avatar_sat_refutation,[],[s1392]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN439-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n007.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 15:59:10 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.54/1.17 % (2525564)Input is clausal, will run a generic CNF schedule.
% 3.54/1.17 % (2525573)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2308636235:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.54/1.17 % (2525572)lrs+10_1_sil=8000:sp=occurrence:random_seed=719603433:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.54/1.17 % (2525574)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2403673993:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.54/1.17 % (2525569)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1988833536:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.54/1.17 % (2525571)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1066790336:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.54/1.17 % (2525570)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2252724583:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.54/1.17 % (2525575)dis-21_1_sil=8000:lcm=predicate:random_seed=3032140042:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.54/1.17 % (2525573)Instruction limit reached!
% 3.54/1.17 % (2525573)------------------------------
% 3.54/1.17 % (2525573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.17 % (2525573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.17 % (2525573)CaDiCaL version: 2.1.3
% 3.54/1.17 % (2525573)Termination reason: Instruction limit
% 3.54/1.17 % (2525573)Termination phase: Saturation
% 3.54/1.17 % (2525573)Time elapsed: 0.042 s
% 3.54/1.17 % (2525573)Peak memory usage: 90 MB
% 3.54/1.17 % (2525573)Instructions burned: 114 (million)
% 3.54/1.17 % (2525575)First to succeed.
% 3.54/1.17 % (2525575)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2525564"
% 3.54/1.17 % (2525572)Instruction limit reached!
% 3.54/1.17 % (2525572)------------------------------
% 3.54/1.17 % (2525572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.17 % (2525572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.17 % (2525572)CaDiCaL version: 2.1.3
% 3.54/1.17 % (2525572)Termination reason: Instruction limit
% 3.54/1.17 % (2525572)Termination phase: Saturation
% 3.54/1.17 % (2525572)Time elapsed: 0.070 s
% 3.54/1.17 % (2525572)Peak memory usage: 90 MB
% 3.54/1.17 % (2525572)Instructions burned: 107 (million)
% 3.54/1.17 % (2525574)Instruction limit reached!
% 3.54/1.17 % (2525574)------------------------------
% 3.54/1.17 % (2525574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.17 % (2525574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.17 % (2525574)CaDiCaL version: 2.1.3
% 3.54/1.17 % (2525574)Termination reason: Instruction limit
% 3.54/1.17 % (2525574)Termination phase: Saturation
% 3.54/1.17 % (2525574)Time elapsed: 0.117 s
% 3.54/1.17 % (2525574)Peak memory usage: 91 MB
% 3.54/1.17 % (2525574)Instructions burned: 181 (million)
% 3.54/1.17 % (2525583)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1309086822:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.54/1.17 % (2525583)Instruction limit reached!
% 3.54/1.17 % (2525583)------------------------------
% 3.54/1.17 % (2525583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.17 % (2525583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.17 % (2525583)CaDiCaL version: 2.1.3
% 3.54/1.17 % (2525583)Termination reason: Instruction limit
% 3.54/1.17 % (2525583)Termination phase: Saturation
% 3.54/1.17 % (2525583)Time elapsed: 0.051 s
% 3.54/1.17 % (2525583)Peak memory usage: 90 MB
% 3.54/1.17 % (2525583)Instructions burned: 145 (million)
% 3.54/1.17 % (2525584)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3294437229:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.54/1.17 % (2525584)Refutation not found, incomplete strategy
% 3.54/1.17 % (2525584)------------------------------
% 3.54/1.17 % (2525584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.17 % (2525584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.17 % (2525584)CaDiCaL version: 2.1.3
% 3.54/1.17 % (2525584)Termination reason: Refutation not found, incomplete strategy
% 3.54/1.17 % (2525584)Time elapsed: 0.031 s
% 3.54/1.17 % (2525584)Peak memory usage: 90 MB
% 3.54/1.17 % (2525584)Instructions burned: 51 (million)
% 3.54/1.17 % (2525585)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=446586213:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.54/1.17 % (2525575)Refutation found. Thanks to Tanya!
% 3.54/1.17 % SZS status Unsatisfiable for theBenchmark
% 3.54/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 4.09/1.37 % (2525575)------------------------------
% 4.09/1.37 % (2525575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.09/1.37 % (2525575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.09/1.37 % (2525575)CaDiCaL version: 2.1.3
% 4.09/1.37 % (2525575)Termination reason: Refutation
% 4.09/1.37 % (2525575)Time elapsed: 0.062 s
% 4.09/1.37 % (2525575)Peak memory usage: 91 MB
% 4.09/1.37 % (2525575)Instructions burned: 98 (million)
% 4.09/1.37 % (2525575)------------------------------
% 4.09/1.37 % (2525575)------------------------------
% 4.09/1.37 % (2525564)Success in time 0.493 s
% 4.09/1.37 % Vampire exiting
%------------------------------------------------------------------------------