%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN440-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:51:04 PM UTC 2026
% Result : Unsatisfiable 0.65s 0.99s
% Output : Refutation 2.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 343
% Syntax : Number of formulae : 1101 ( 18 unt; 194 def)
% Number of atoms : 3284 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 3962 (1779 ~;1989 |; 0 &)
% ( 194 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 237 ( 236 usr; 233 prp; 0-1 aty)
% Number of functors : 37 ( 37 usr; 37 con; 0-0 aty)
% Number of variables : 145 ( 0 sgn 145 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,negated_conjecture,
( ~ hskp66
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f3,negated_conjecture,
( ~ hskp65
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
fof(f4,negated_conjecture,
( ~ hskp64
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f71,negated_conjecture,
( hskp16
| hskp17
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f74,negated_conjecture,
( hskp33
| hskp60
| hskp61 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( hskp64
| hskp65
| hskp66 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp66
| c1_1(a675) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp66
| c3_1(a675) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp65
| c2_1(a674) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp65
| c0_1(a674) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp64
| c3_1(a673) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp64
| c1_1(a673) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f85,negated_conjecture,
( ~ hskp61
| c2_1(a670) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ hskp60
| c0_1(a669) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ hskp60
| c1_1(a669) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f90,negated_conjecture,
( ~ hskp58
| c3_1(a663) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f93,negated_conjecture,
( ~ hskp56
| c2_1(a658) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ hskp56
| c3_1(a658) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ hskp55
| c3_1(a653) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ hskp55
| c1_1(a653) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ hskp54
| c3_1(a651) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ hskp54
| c2_1(a651) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ hskp53
| c3_1(a648) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ hskp53
| c0_1(a648) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ hskp52
| c0_1(a647) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f117,negated_conjecture,
( ~ hskp43
| c0_1(a619) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ hskp42
| c1_1(a618) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ hskp41
| c2_1(a617) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ hskp41
| c3_1(a617) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ hskp40
| c2_1(a614) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ hskp40
| c1_1(a614) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ hskp40
| c0_1(a614) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f126,negated_conjecture,
( ~ hskp38
| c1_1(a608) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ hskp38
| c3_1(a608) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ hskp38
| c0_1(a608) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( ~ hskp37
| c1_1(a607) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ hskp37
| c0_1(a607) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f133,negated_conjecture,
( ~ hskp35
| c2_1(a602) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f136,negated_conjecture,
( ~ hskp33
| c0_1(a599) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( ~ hskp33
| c3_1(a599) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f142,negated_conjecture,
( ~ hskp26
| c3_1(a652) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
( ~ hskp25
| c3_1(a646) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
( ~ hskp24
| c3_1(a643) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
( ~ hskp23
| c2_1(a642) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
( ~ hskp23
| c3_1(a642) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f152,negated_conjecture,
( ~ hskp17
| c3_1(a628) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( ~ hskp16
| c2_1(a627) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
( ~ hskp16
| c0_1(a627) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( ~ hskp14
| c3_1(a624) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
( ~ hskp11
| c0_1(a616) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
( ~ hskp11
| c1_1(a616) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
( ~ hskp10
| c0_1(a615) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
( ~ hskp10
| c3_1(a615) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( ~ hskp9
| c1_1(a613) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( ~ hskp9
| c2_1(a613) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f164,negated_conjecture,
( ~ hskp6
| c2_1(a609) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
( ~ hskp5
| c2_1(a606) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause165) ).
fof(f166,negated_conjecture,
( ~ hskp3
| c0_1(a603) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f168,negated_conjecture,
( ~ hskp1
| c0_1(a598) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( ~ hskp1
| c2_1(a598) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
( ~ hskp0
| c0_1(a597) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
( ~ c2_1(a675)
| ~ hskp66 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
( ~ c1_1(a674)
| ~ hskp65 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
( ~ c0_1(a673)
| ~ hskp64 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f177,negated_conjecture,
( ~ c1_1(a670)
| ~ hskp61 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
( ~ c0_1(a670)
| ~ hskp61 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
( ~ c2_1(a669)
| ~ hskp60 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f181,negated_conjecture,
( ~ c0_1(a663)
| ~ hskp58 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( ~ c1_1(a663)
| ~ hskp58 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f184,negated_conjecture,
( ~ c1_1(a658)
| ~ hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
( ~ c2_1(a653)
| ~ hskp55 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
( ~ c0_1(a651)
| ~ hskp54 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
( ~ c2_1(a648)
| ~ hskp53 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
( ~ c2_1(a647)
| ~ hskp52 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
( ~ c1_1(a647)
| ~ hskp52 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f199,negated_conjecture,
( ~ c3_1(a619)
| ~ hskp43 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
( ~ c1_1(a619)
| ~ hskp43 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
( ~ c2_1(a618)
| ~ hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ c3_1(a618)
| ~ hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ c1_1(a617)
| ~ hskp41 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause203) ).
fof(f205,negated_conjecture,
( ~ c2_1(a607)
| ~ hskp37 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause205) ).
fof(f207,negated_conjecture,
( ~ c3_1(a602)
| ~ hskp35 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause207) ).
fof(f210,negated_conjecture,
( ~ c2_1(a599)
| ~ hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause210) ).
fof(f217,negated_conjecture,
( ~ c1_1(a660)
| ~ hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
( ~ c3_1(a660)
| ~ hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ c0_1(a660)
| ~ hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause219) ).
fof(f225,negated_conjecture,
( ~ c1_1(a652)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause225) ).
fof(f226,negated_conjecture,
( ~ c2_1(a652)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause226) ).
fof(f227,negated_conjecture,
( ~ c2_1(a646)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause227) ).
fof(f228,negated_conjecture,
( ~ c0_1(a646)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause228) ).
fof(f229,negated_conjecture,
( ~ c0_1(a643)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause229) ).
fof(f230,negated_conjecture,
( ~ c1_1(a643)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause230) ).
fof(f231,negated_conjecture,
( ~ c0_1(a642)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause231) ).
fof(f242,negated_conjecture,
( ~ c2_1(a628)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause242) ).
fof(f243,negated_conjecture,
( ~ c1_1(a628)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause243) ).
fof(f244,negated_conjecture,
( ~ c3_1(a627)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
( ~ c2_1(a625)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
( ~ c1_1(a625)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause246) ).
fof(f247,negated_conjecture,
( ~ c0_1(a625)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause247) ).
fof(f248,negated_conjecture,
( ~ c1_1(a624)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause248) ).
fof(f249,negated_conjecture,
( ~ c2_1(a624)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause249) ).
fof(f253,negated_conjecture,
( ~ c0_1(a620)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause253) ).
fof(f254,negated_conjecture,
( ~ c3_1(a620)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause254) ).
fof(f255,negated_conjecture,
( ~ c1_1(a620)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause255) ).
fof(f256,negated_conjecture,
( ~ c2_1(a616)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause256) ).
fof(f257,negated_conjecture,
( ~ c2_1(a615)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause257) ).
fof(f258,negated_conjecture,
( ~ c3_1(a613)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause258) ).
fof(f263,negated_conjecture,
( ~ c0_1(a609)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause263) ).
fof(f264,negated_conjecture,
( ~ c1_1(a609)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause264) ).
fof(f265,negated_conjecture,
( ~ c0_1(a606)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause265) ).
fof(f266,negated_conjecture,
( ~ c3_1(a606)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause266) ).
fof(f270,negated_conjecture,
( ~ c1_1(a603)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause270) ).
fof(f274,negated_conjecture,
( ~ c1_1(a598)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause274) ).
fof(f275,negated_conjecture,
( ~ c3_1(a597)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause275) ).
fof(f276,negated_conjecture,
( ~ c1_1(a597)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause276) ).
fof(f280,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp0
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause280) ).
fof(f281,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c2_1(X0)
| hskp40
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause281) ).
fof(f284,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c2_1(X0)
| hskp25
| hskp52 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause284) ).
fof(f285,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp53
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause285) ).
fof(f286,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c0_1(X0)
| hskp37
| hskp54 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause286) ).
fof(f287,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp26
| hskp55 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause287) ).
fof(f288,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp3
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause288) ).
fof(f289,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause289) ).
fof(f291,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp43
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause291) ).
fof(f293,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp14
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause293) ).
fof(f294,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp23
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause294) ).
fof(f295,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp58
| hskp41 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause295) ).
fof(f297,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| c0_1(X0)
| c0_1(X1)
| c2_1(X0)
| c3_1(X1)
| c1_1(X1)
| c3_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause297) ).
fof(f298,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp5
| hskp37 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause298) ).
fof(f299,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c2_1(X0)
| c0_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X0)
| c3_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause299) ).
fof(f300,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| c0_1(X0)
| c1_1(X0)
| hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause300) ).
fof(f301,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X0)
| c3_1(X0)
| c0_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause301) ).
fof(f302,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| hskp38 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause302) ).
fof(f303,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause303) ).
fof(f305,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| hskp55 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause305) ).
fof(f306,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c2_1(X1)
| c1_1(X1)
| hskp56 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause306) ).
fof(f307,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c2_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause307) ).
fof(f312,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c2_1(X0)
| c1_1(X0)
| c2_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause312) ).
fof(f313,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| c1_1(X1)
| hskp55 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause313) ).
fof(f314,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c0_1(X1)
| c2_1(X0)
| c2_1(X1)
| hskp41 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause314) ).
fof(f318,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| hskp35 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause318) ).
fof(f320,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c2_1(X0)
| ~ c2_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause320) ).
fof(f321,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X2)
| c1_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause321) ).
fof(f322,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X1)
| ~ c0_1(X1)
| c3_1(X2)
| c0_1(X2)
| c2_1(X2)
| c1_1(X0)
| c2_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause322) ).
fof(f324,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X2)
| c1_1(X0)
| c0_1(X1)
| c2_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause324) ).
fof(f325,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X2)
| c0_1(X0)
| c1_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause325) ).
fof(f326,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X2)
| ~ c1_1(X2)
| c1_1(X0)
| c1_1(X1)
| c0_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause326) ).
fof(f327,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| ~ c0_1(X2)
| c3_1(X0)
| c0_1(X1)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause327) ).
fof(f328,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X2)
| ~ c0_1(X2)
| ~ c1_1(X2)
| c3_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause328) ).
fof(f330,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| ~ c1_1(X2)
| ~ c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f331,plain,
( ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,definition,
( spl0_2
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f334,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f336,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f339,definition,
( spl0_4
<=> ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f340,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f341,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f328,f339,f336,f333,f330]) ).
fof(f343,definition,
( spl0_5
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| ~ c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f344,plain,
( ! [X2] :
( c2_1(X2)
| ~ c3_1(X2)
| ~ c0_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f346,definition,
( spl0_6
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f347,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f349,definition,
( spl0_7
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f350,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f351,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f327,f349,f336,f346,f343]) ).
fof(f353,definition,
( spl0_8
<=> ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f354,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f356,definition,
( spl0_9
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f357,plain,
( ! [X1] :
( c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,definition,
( spl0_10
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f360,plain,
( ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f361,plain,
( spl0_8
| spl0_9
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f326,f359,f336,f356,f353]) ).
fof(f363,definition,
( spl0_11
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f364,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f366,definition,
( spl0_12
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f367,plain,
( ! [X1] :
( c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f368,plain,
( spl0_11
| spl0_12
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f325,f346,f336,f366,f363]) ).
fof(f370,definition,
( spl0_13
<=> ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f371,plain,
( ! [X2] :
( c1_1(X2)
| ~ c0_1(X2)
| c2_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f372,plain,
( spl0_13
| spl0_6
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f324,f366,f336,f346,f370]) ).
fof(f374,definition,
( spl0_14
<=> ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f375,plain,
( ! [X2] :
( c2_1(X2)
| c0_1(X2)
| c3_1(X2) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f378,definition,
( spl0_15
<=> ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f379,plain,
( ! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f380,plain,
( spl0_14
| spl0_5
| spl0_15
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f322,f336,f378,f343,f374]) ).
fof(f382,definition,
( spl0_16
<=> ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f383,plain,
( ! [X2] :
( c1_1(X2)
| c0_1(X2)
| c3_1(X2) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f385,definition,
( spl0_17
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f386,plain,
( ! [X1] :
( c1_1(X1)
| ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f387,plain,
( spl0_16
| spl0_17
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f321,f359,f336,f385,f382]) ).
fof(f389,definition,
( spl0_18
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f390,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f392,definition,
( spl0_19
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f393,plain,
( ! [X0] :
( c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f394,plain,
( spl0_18
| spl0_9
| spl0_19
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f320,f336,f392,f356,f389]) ).
fof(f399,definition,
( spl0_21
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f400,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f403,definition,
( spl0_22
<=> hskp35 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f405,plain,
( spl0_22
| spl0_4
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f318,f343,f336,f339,f403]) ).
fof(f411,definition,
( spl0_24
<=> ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f412,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f419,definition,
( spl0_26
<=> hskp41 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f422,definition,
( spl0_27
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f423,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f425,definition,
( spl0_28
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f426,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( spl0_26
| spl0_27
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f314,f425,f336,f422,f419]) ).
fof(f429,definition,
( spl0_29
<=> hskp55 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f431,plain,
( spl0_29
| spl0_15
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f313,f385,f336,f378,f429]) ).
fof(f433,definition,
( spl0_30
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f435,plain,
( spl0_30
| spl0_27
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f312,f363,f336,f422,f433]) ).
fof(f440,definition,
( spl0_32
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f441,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f444,definition,
( spl0_33
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f447,definition,
( spl0_34
<=> ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f448,plain,
( ! [X1] :
( c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f454,definition,
( spl0_36
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f455,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f462,definition,
( spl0_38
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f465,definition,
( spl0_39
<=> ! [X1] :
( c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f466,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( spl0_38
| spl0_39
| spl0_24
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f307,f336,f411,f465,f462]) ).
fof(f469,definition,
( spl0_40
<=> hskp56 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f471,plain,
( spl0_40
| spl0_11
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f306,f454,f336,f363,f469]) ).
fof(f473,definition,
( spl0_41
<=> ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f474,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f475,plain,
( spl0_29
| spl0_11
| ~ spl0_3
| spl0_41 ),
inference(avatar_split_clause,[],[f305,f473,f336,f363,f429]) ).
fof(f480,definition,
( spl0_43
<=> ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f481,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f484,definition,
( spl0_44
<=> hskp42 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f486,plain,
( spl0_44
| spl0_17
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f303,f370,f336,f385,f484]) ).
fof(f488,definition,
( spl0_45
<=> hskp38 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f490,plain,
( spl0_45
| spl0_18
| ~ spl0_3
| spl0_43 ),
inference(avatar_split_clause,[],[f302,f480,f336,f389,f488]) ).
fof(f491,plain,
( ~ spl0_3
| spl0_8
| spl0_41 ),
inference(avatar_split_clause,[],[f301,f473,f353,f336]) ).
fof(f492,plain,
( spl0_44
| spl0_16
| spl0_17
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f300,f336,f385,f382,f484]) ).
fof(f493,plain,
( spl0_39
| spl0_41
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f299,f336,f473,f465]) ).
fof(f495,definition,
( spl0_46
<=> hskp37 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f497,plain,
( spl0_46
| spl0_30
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f298,f339,f336,f433,f495]) ).
fof(f498,plain,
( spl0_16
| spl0_14
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f297,f336,f374,f382]) ).
fof(f507,definition,
( spl0_49
<=> hskp58 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f509,plain,
( spl0_26
| spl0_49
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f295,f343,f336,f507,f419]) ).
fof(f511,definition,
( spl0_50
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f514,definition,
( spl0_51
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f516,plain,
( spl0_50
| spl0_51
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f294,f359,f336,f514,f511]) ).
fof(f518,definition,
( spl0_52
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f521,definition,
( spl0_53
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f523,plain,
( spl0_52
| spl0_53
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f293,f366,f336,f521,f518]) ).
fof(f532,definition,
( spl0_56
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f535,definition,
( spl0_57
<=> hskp43 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f537,plain,
( spl0_56
| spl0_57
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f291,f425,f336,f535,f532]) ).
fof(f546,definition,
( spl0_60
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f548,plain,
( spl0_60
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f289,f399,f336,f546]) ).
fof(f550,definition,
( spl0_61
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f553,definition,
( spl0_62
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f555,plain,
( spl0_61
| spl0_62
| ~ spl0_3
| spl0_34 ),
inference(avatar_split_clause,[],[f288,f447,f336,f553,f550]) ).
fof(f557,definition,
( spl0_63
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f559,plain,
( spl0_29
| spl0_63
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f287,f370,f336,f557,f429]) ).
fof(f561,definition,
( spl0_64
<=> hskp54 ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f563,plain,
( spl0_64
| spl0_46
| ~ spl0_3
| spl0_41 ),
inference(avatar_split_clause,[],[f286,f473,f336,f495,f561]) ).
fof(f565,definition,
( spl0_65
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f568,definition,
( spl0_66
<=> hskp53 ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f570,plain,
( spl0_65
| spl0_66
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f285,f385,f336,f568,f565]) ).
fof(f572,definition,
( spl0_67
<=> hskp52 ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f575,definition,
( spl0_68
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f577,plain,
( spl0_67
| spl0_68
| ~ spl0_3
| spl0_32 ),
inference(avatar_split_clause,[],[f284,f440,f336,f575,f572]) ).
fof(f596,definition,
( spl0_74
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f599,definition,
( spl0_75
<=> hskp40 ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f601,plain,
( spl0_74
| spl0_75
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f281,f454,f336,f599,f596]) ).
fof(f603,definition,
( spl0_76
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f606,definition,
( spl0_77
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f608,plain,
( spl0_76
| spl0_77
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f280,f385,f336,f606,f603]) ).
fof(f624,definition,
( spl0_82
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f632,definition,
( spl0_84
<=> c1_1(a597) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f633,plain,
( ~ c1_1(a597)
| spl0_84 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f634,plain,
( ~ spl0_77
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f276,f632,f606]) ).
fof(f636,definition,
( spl0_85
<=> c3_1(a597) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f638,plain,
( ~ spl0_77
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f275,f636,f606]) ).
fof(f641,definition,
( spl0_86
<=> c1_1(a598) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f642,plain,
( ~ c1_1(a598)
| spl0_86 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f643,plain,
( ~ spl0_76
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f274,f641,f603]) ).
fof(f661,definition,
( spl0_91
<=> c1_1(a603) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f662,plain,
( ~ c1_1(a603)
| spl0_91 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f663,plain,
( ~ spl0_62
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f270,f661,f553]) ).
fof(f681,definition,
( spl0_96
<=> c3_1(a606) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f683,plain,
( ~ spl0_30
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f266,f681,f433]) ).
fof(f685,definition,
( spl0_97
<=> c0_1(a606) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f687,plain,
( ~ spl0_30
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f265,f685,f433]) ).
fof(f690,definition,
( spl0_98
<=> c1_1(a609) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f691,plain,
( ~ c1_1(a609)
| spl0_98 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f692,plain,
( ~ spl0_60
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f264,f690,f546]) ).
fof(f694,definition,
( spl0_99
<=> c0_1(a609) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f696,plain,
( ~ spl0_60
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f263,f694,f546]) ).
fof(f717,definition,
( spl0_104
<=> c3_1(a613) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f719,plain,
( ~ spl0_82
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f258,f717,f624]) ).
fof(f722,definition,
( spl0_105
<=> c2_1(a615) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f723,plain,
( ~ c2_1(a615)
| spl0_105 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f724,plain,
( ~ spl0_74
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f257,f722,f596]) ).
fof(f727,definition,
( spl0_106
<=> c2_1(a616) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f729,plain,
( ~ spl0_38
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f256,f727,f462]) ).
fof(f732,definition,
( spl0_107
<=> c1_1(a620) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f733,plain,
( ~ c1_1(a620)
| spl0_107 ),
inference(avatar_component_clause,[],[f732]) ).
fof(f734,plain,
( ~ spl0_56
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f255,f732,f532]) ).
fof(f736,definition,
( spl0_108
<=> c3_1(a620) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f738,plain,
( ~ spl0_56
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f254,f736,f532]) ).
fof(f740,definition,
( spl0_109
<=> c0_1(a620) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f742,plain,
( ~ spl0_56
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f253,f740,f532]) ).
fof(f758,definition,
( spl0_113
<=> c2_1(a624) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f760,plain,
( ~ spl0_53
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f249,f758,f521]) ).
fof(f762,definition,
( spl0_114
<=> c1_1(a624) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f763,plain,
( ~ c1_1(a624)
| spl0_114 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f764,plain,
( ~ spl0_53
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f248,f762,f521]) ).
fof(f767,definition,
( spl0_115
<=> c0_1(a625) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f769,plain,
( ~ spl0_52
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f247,f767,f518]) ).
fof(f771,definition,
( spl0_116
<=> c1_1(a625) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f772,plain,
( ~ c1_1(a625)
| spl0_116 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f773,plain,
( ~ spl0_52
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f246,f771,f518]) ).
fof(f775,definition,
( spl0_117
<=> c2_1(a625) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f777,plain,
( ~ spl0_52
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f245,f775,f518]) ).
fof(f780,definition,
( spl0_118
<=> c3_1(a627) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f782,plain,
( ~ spl0_33
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f244,f780,f444]) ).
fof(f785,definition,
( spl0_119
<=> c1_1(a628) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f786,plain,
( ~ c1_1(a628)
| spl0_119 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f787,plain,
( ~ spl0_65
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f243,f785,f565]) ).
fof(f789,definition,
( spl0_120
<=> c2_1(a628) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f790,plain,
( ~ c2_1(a628)
| spl0_120 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f791,plain,
( ~ spl0_65
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f242,f789,f565]) ).
fof(f843,definition,
( spl0_133
<=> c0_1(a642) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f845,plain,
( ~ spl0_51
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f231,f843,f514]) ).
fof(f848,definition,
( spl0_134
<=> c1_1(a643) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f849,plain,
( ~ c1_1(a643)
| spl0_134 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f850,plain,
( ~ spl0_50
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f230,f848,f511]) ).
fof(f852,definition,
( spl0_135
<=> c0_1(a643) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f854,plain,
( ~ spl0_50
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f229,f852,f511]) ).
fof(f857,definition,
( spl0_136
<=> c0_1(a646) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f859,plain,
( ~ spl0_68
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f228,f857,f575]) ).
fof(f861,definition,
( spl0_137
<=> c2_1(a646) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f862,plain,
( ~ c2_1(a646)
| spl0_137 ),
inference(avatar_component_clause,[],[f861]) ).
fof(f863,plain,
( ~ spl0_68
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f227,f861,f575]) ).
fof(f866,definition,
( spl0_138
<=> c2_1(a652) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f867,plain,
( ~ c2_1(a652)
| spl0_138 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f868,plain,
( ~ spl0_63
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f226,f866,f557]) ).
fof(f870,definition,
( spl0_139
<=> c1_1(a652) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f871,plain,
( ~ c1_1(a652)
| spl0_139 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f872,plain,
( ~ spl0_63
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f225,f870,f557]) ).
fof(f901,definition,
( spl0_147
<=> c0_1(a660) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f903,plain,
( ~ spl0_61
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f219,f901,f550]) ).
fof(f905,definition,
( spl0_148
<=> c3_1(a660) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f907,plain,
( ~ spl0_61
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f218,f905,f550]) ).
fof(f909,definition,
( spl0_149
<=> c1_1(a660) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f910,plain,
( ~ c1_1(a660)
| spl0_149 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f911,plain,
( ~ spl0_61
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f217,f909,f550]) ).
fof(f940,definition,
( spl0_156
<=> hskp33 ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f943,definition,
( spl0_157
<=> c2_1(a599) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f944,plain,
( ~ c2_1(a599)
| spl0_157 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f945,plain,
( ~ spl0_156
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f210,f943,f940]) ).
fof(f959,definition,
( spl0_161
<=> c3_1(a602) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f961,plain,
( ~ spl0_22
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f207,f959,f403]) ).
fof(f969,definition,
( spl0_163
<=> c2_1(a607) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f970,plain,
( ~ c2_1(a607)
| spl0_163 ),
inference(avatar_component_clause,[],[f969]) ).
fof(f971,plain,
( ~ spl0_46
| ~ spl0_163 ),
inference(avatar_split_clause,[],[f205,f969,f495]) ).
fof(f979,definition,
( spl0_165
<=> c1_1(a617) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f980,plain,
( ~ c1_1(a617)
| spl0_165 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f981,plain,
( ~ spl0_26
| ~ spl0_165 ),
inference(avatar_split_clause,[],[f203,f979,f419]) ).
fof(f984,definition,
( spl0_166
<=> c3_1(a618) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f986,plain,
( ~ spl0_44
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f202,f984,f484]) ).
fof(f988,definition,
( spl0_167
<=> c2_1(a618) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f989,plain,
( ~ c2_1(a618)
| spl0_167 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f990,plain,
( ~ spl0_44
| ~ spl0_167 ),
inference(avatar_split_clause,[],[f201,f988,f484]) ).
fof(f993,definition,
( spl0_168
<=> c1_1(a619) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f994,plain,
( ~ c1_1(a619)
| spl0_168 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f995,plain,
( ~ spl0_57
| ~ spl0_168 ),
inference(avatar_split_clause,[],[f200,f993,f535]) ).
fof(f997,definition,
( spl0_169
<=> c3_1(a619) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f999,plain,
( ~ spl0_57
| ~ spl0_169 ),
inference(avatar_split_clause,[],[f199,f997,f535]) ).
fof(f1045,definition,
( spl0_179
<=> c1_1(a647) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f1046,plain,
( ~ c1_1(a647)
| spl0_179 ),
inference(avatar_component_clause,[],[f1045]) ).
fof(f1047,plain,
( ~ spl0_67
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f189,f1045,f572]) ).
fof(f1049,definition,
( spl0_180
<=> c2_1(a647) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f1050,plain,
( ~ c2_1(a647)
| spl0_180 ),
inference(avatar_component_clause,[],[f1049]) ).
fof(f1051,plain,
( ~ spl0_67
| ~ spl0_180 ),
inference(avatar_split_clause,[],[f188,f1049,f572]) ).
fof(f1054,definition,
( spl0_181
<=> c2_1(a648) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1055,plain,
( ~ c2_1(a648)
| spl0_181 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1056,plain,
( ~ spl0_66
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f187,f1054,f568]) ).
fof(f1059,definition,
( spl0_182
<=> c0_1(a651) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f1061,plain,
( ~ spl0_64
| ~ spl0_182 ),
inference(avatar_split_clause,[],[f186,f1059,f561]) ).
fof(f1064,definition,
( spl0_183
<=> c2_1(a653) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1066,plain,
( ~ spl0_29
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f185,f1064,f429]) ).
fof(f1069,definition,
( spl0_184
<=> c1_1(a658) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f1070,plain,
( ~ c1_1(a658)
| spl0_184 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1071,plain,
( ~ spl0_40
| ~ spl0_184 ),
inference(avatar_split_clause,[],[f184,f1069,f469]) ).
fof(f1079,definition,
( spl0_186
<=> c1_1(a663) ),
introduced(definition,[new_symbols(definition,[spl0_186])],[avatar_definition]) ).
fof(f1080,plain,
( ~ c1_1(a663)
| spl0_186 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1081,plain,
( ~ spl0_49
| ~ spl0_186 ),
inference(avatar_split_clause,[],[f182,f1079,f507]) ).
fof(f1083,definition,
( spl0_187
<=> c0_1(a663) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f1085,plain,
( ~ spl0_49
| ~ spl0_187 ),
inference(avatar_split_clause,[],[f181,f1083,f507]) ).
fof(f1094,definition,
( spl0_190
<=> hskp60 ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f1097,definition,
( spl0_191
<=> c2_1(a669) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f1098,plain,
( ~ c2_1(a669)
| spl0_191 ),
inference(avatar_component_clause,[],[f1097]) ).
fof(f1099,plain,
( ~ spl0_190
| ~ spl0_191 ),
inference(avatar_split_clause,[],[f179,f1097,f1094]) ).
fof(f1101,definition,
( spl0_192
<=> hskp61 ),
introduced(definition,[new_symbols(definition,[spl0_192])],[avatar_definition]) ).
fof(f1104,definition,
( spl0_193
<=> c0_1(a670) ),
introduced(definition,[new_symbols(definition,[spl0_193])],[avatar_definition]) ).
fof(f1106,plain,
( ~ spl0_192
| ~ spl0_193 ),
inference(avatar_split_clause,[],[f178,f1104,f1101]) ).
fof(f1108,definition,
( spl0_194
<=> c1_1(a670) ),
introduced(definition,[new_symbols(definition,[spl0_194])],[avatar_definition]) ).
fof(f1109,plain,
( ~ c1_1(a670)
| spl0_194 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1110,plain,
( ~ spl0_192
| ~ spl0_194 ),
inference(avatar_split_clause,[],[f177,f1108,f1101]) ).
fof(f1126,definition,
( spl0_198
<=> hskp64 ),
introduced(definition,[new_symbols(definition,[spl0_198])],[avatar_definition]) ).
fof(f1129,definition,
( spl0_199
<=> c0_1(a673) ),
introduced(definition,[new_symbols(definition,[spl0_199])],[avatar_definition]) ).
fof(f1131,plain,
( ~ spl0_198
| ~ spl0_199 ),
inference(avatar_split_clause,[],[f173,f1129,f1126]) ).
fof(f1133,definition,
( spl0_200
<=> hskp65 ),
introduced(definition,[new_symbols(definition,[spl0_200])],[avatar_definition]) ).
fof(f1136,definition,
( spl0_201
<=> c1_1(a674) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f1137,plain,
( ~ c1_1(a674)
| spl0_201 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1138,plain,
( ~ spl0_200
| ~ spl0_201 ),
inference(avatar_split_clause,[],[f172,f1136,f1133]) ).
fof(f1140,definition,
( spl0_202
<=> hskp66 ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f1143,definition,
( spl0_203
<=> c2_1(a675) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f1144,plain,
( ~ c2_1(a675)
| spl0_203 ),
inference(avatar_component_clause,[],[f1143]) ).
fof(f1145,plain,
( ~ spl0_202
| ~ spl0_203 ),
inference(avatar_split_clause,[],[f171,f1143,f1140]) ).
fof(f1147,definition,
( spl0_204
<=> c0_1(a597) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f1149,plain,
( spl0_204
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f170,f606,f1147]) ).
fof(f1151,definition,
( spl0_205
<=> c2_1(a598) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f1153,plain,
( spl0_205
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f169,f603,f1151]) ).
fof(f1155,definition,
( spl0_206
<=> c0_1(a598) ),
introduced(definition,[new_symbols(definition,[spl0_206])],[avatar_definition]) ).
fof(f1157,plain,
( spl0_206
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f168,f603,f1155]) ).
fof(f1163,definition,
( spl0_208
<=> c0_1(a603) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f1165,plain,
( spl0_208
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f166,f553,f1163]) ).
fof(f1167,definition,
( spl0_209
<=> c2_1(a606) ),
introduced(definition,[new_symbols(definition,[spl0_209])],[avatar_definition]) ).
fof(f1168,plain,
( c2_1(a606)
| ~ spl0_209 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1169,plain,
( spl0_209
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f165,f433,f1167]) ).
fof(f1171,definition,
( spl0_210
<=> c2_1(a609) ),
introduced(definition,[new_symbols(definition,[spl0_210])],[avatar_definition]) ).
fof(f1172,plain,
( c2_1(a609)
| ~ spl0_210 ),
inference(avatar_component_clause,[],[f1171]) ).
fof(f1173,plain,
( spl0_210
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f164,f546,f1171]) ).
fof(f1183,definition,
( spl0_213
<=> c2_1(a613) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f1184,plain,
( c2_1(a613)
| ~ spl0_213 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1185,plain,
( spl0_213
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f161,f624,f1183]) ).
fof(f1187,definition,
( spl0_214
<=> c1_1(a613) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f1188,plain,
( c1_1(a613)
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1189,plain,
( spl0_214
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f160,f624,f1187]) ).
fof(f1191,definition,
( spl0_215
<=> c3_1(a615) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1193,plain,
( spl0_215
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f159,f596,f1191]) ).
fof(f1195,definition,
( spl0_216
<=> c0_1(a615) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1197,plain,
( spl0_216
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f158,f596,f1195]) ).
fof(f1199,definition,
( spl0_217
<=> c1_1(a616) ),
introduced(definition,[new_symbols(definition,[spl0_217])],[avatar_definition]) ).
fof(f1200,plain,
( c1_1(a616)
| ~ spl0_217 ),
inference(avatar_component_clause,[],[f1199]) ).
fof(f1201,plain,
( spl0_217
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f157,f462,f1199]) ).
fof(f1203,definition,
( spl0_218
<=> c0_1(a616) ),
introduced(definition,[new_symbols(definition,[spl0_218])],[avatar_definition]) ).
fof(f1205,plain,
( spl0_218
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f156,f462,f1203]) ).
fof(f1207,definition,
( spl0_219
<=> c3_1(a624) ),
introduced(definition,[new_symbols(definition,[spl0_219])],[avatar_definition]) ).
fof(f1209,plain,
( spl0_219
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f155,f521,f1207]) ).
fof(f1211,definition,
( spl0_220
<=> c0_1(a627) ),
introduced(definition,[new_symbols(definition,[spl0_220])],[avatar_definition]) ).
fof(f1213,plain,
( spl0_220
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f154,f444,f1211]) ).
fof(f1215,definition,
( spl0_221
<=> c2_1(a627) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f1216,plain,
( c2_1(a627)
| ~ spl0_221 ),
inference(avatar_component_clause,[],[f1215]) ).
fof(f1217,plain,
( spl0_221
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f153,f444,f1215]) ).
fof(f1219,definition,
( spl0_222
<=> c3_1(a628) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f1221,plain,
( spl0_222
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f152,f565,f1219]) ).
fof(f1243,definition,
( spl0_228
<=> c3_1(a642) ),
introduced(definition,[new_symbols(definition,[spl0_228])],[avatar_definition]) ).
fof(f1245,plain,
( spl0_228
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f146,f514,f1243]) ).
fof(f1247,definition,
( spl0_229
<=> c2_1(a642) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f1248,plain,
( c2_1(a642)
| ~ spl0_229 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1249,plain,
( spl0_229
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f145,f514,f1247]) ).
fof(f1251,definition,
( spl0_230
<=> c3_1(a643) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1253,plain,
( spl0_230
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f144,f511,f1251]) ).
fof(f1255,definition,
( spl0_231
<=> c3_1(a646) ),
introduced(definition,[new_symbols(definition,[spl0_231])],[avatar_definition]) ).
fof(f1257,plain,
( spl0_231
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f143,f575,f1255]) ).
fof(f1259,definition,
( spl0_232
<=> c3_1(a652) ),
introduced(definition,[new_symbols(definition,[spl0_232])],[avatar_definition]) ).
fof(f1261,plain,
( spl0_232
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f142,f557,f1259]) ).
fof(f1279,definition,
( spl0_237
<=> c3_1(a599) ),
introduced(definition,[new_symbols(definition,[spl0_237])],[avatar_definition]) ).
fof(f1281,plain,
( spl0_237
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f137,f940,f1279]) ).
fof(f1283,definition,
( spl0_238
<=> c0_1(a599) ),
introduced(definition,[new_symbols(definition,[spl0_238])],[avatar_definition]) ).
fof(f1285,plain,
( spl0_238
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f136,f940,f1283]) ).
fof(f1295,definition,
( spl0_241
<=> c2_1(a602) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1296,plain,
( c2_1(a602)
| ~ spl0_241 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1297,plain,
( spl0_241
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f133,f403,f1295]) ).
fof(f1307,definition,
( spl0_244
<=> c0_1(a607) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f1309,plain,
( spl0_244
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f130,f495,f1307]) ).
fof(f1311,definition,
( spl0_245
<=> c1_1(a607) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f1312,plain,
( c1_1(a607)
| ~ spl0_245 ),
inference(avatar_component_clause,[],[f1311]) ).
fof(f1313,plain,
( spl0_245
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f129,f495,f1311]) ).
fof(f1315,definition,
( spl0_246
<=> c0_1(a608) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f1318,plain,
( spl0_246
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f128,f488,f1315]) ).
fof(f1320,definition,
( spl0_247
<=> c3_1(a608) ),
introduced(definition,[new_symbols(definition,[spl0_247])],[avatar_definition]) ).
fof(f1322,plain,
( spl0_247
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f127,f488,f1320]) ).
fof(f1324,definition,
( spl0_248
<=> c1_1(a608) ),
introduced(definition,[new_symbols(definition,[spl0_248])],[avatar_definition]) ).
fof(f1325,plain,
( c1_1(a608)
| ~ spl0_248 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1326,plain,
( spl0_248
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f126,f488,f1324]) ).
fof(f1336,definition,
( spl0_251
<=> c0_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f1339,plain,
( spl0_251
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f123,f599,f1336]) ).
fof(f1341,definition,
( spl0_252
<=> c1_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f1342,plain,
( c1_1(a614)
| ~ spl0_252 ),
inference(avatar_component_clause,[],[f1341]) ).
fof(f1343,plain,
( spl0_252
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f122,f599,f1341]) ).
fof(f1345,definition,
( spl0_253
<=> c2_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_253])],[avatar_definition]) ).
fof(f1346,plain,
( c2_1(a614)
| ~ spl0_253 ),
inference(avatar_component_clause,[],[f1345]) ).
fof(f1347,plain,
( spl0_253
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f121,f599,f1345]) ).
fof(f1349,definition,
( spl0_254
<=> c3_1(a617) ),
introduced(definition,[new_symbols(definition,[spl0_254])],[avatar_definition]) ).
fof(f1351,plain,
( spl0_254
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f120,f419,f1349]) ).
fof(f1353,definition,
( spl0_255
<=> c2_1(a617) ),
introduced(definition,[new_symbols(definition,[spl0_255])],[avatar_definition]) ).
fof(f1354,plain,
( c2_1(a617)
| ~ spl0_255 ),
inference(avatar_component_clause,[],[f1353]) ).
fof(f1355,plain,
( spl0_255
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f119,f419,f1353]) ).
fof(f1357,definition,
( spl0_256
<=> c1_1(a618) ),
introduced(definition,[new_symbols(definition,[spl0_256])],[avatar_definition]) ).
fof(f1358,plain,
( c1_1(a618)
| ~ spl0_256 ),
inference(avatar_component_clause,[],[f1357]) ).
fof(f1359,plain,
( spl0_256
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f118,f484,f1357]) ).
fof(f1361,definition,
( spl0_257
<=> c0_1(a619) ),
introduced(definition,[new_symbols(definition,[spl0_257])],[avatar_definition]) ).
fof(f1363,plain,
( spl0_257
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f117,f535,f1361]) ).
fof(f1426,definition,
( spl0_273
<=> c0_1(a647) ),
introduced(definition,[new_symbols(definition,[spl0_273])],[avatar_definition]) ).
fof(f1428,plain,
( spl0_273
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f101,f572,f1426]) ).
fof(f1430,definition,
( spl0_274
<=> c0_1(a648) ),
introduced(definition,[new_symbols(definition,[spl0_274])],[avatar_definition]) ).
fof(f1432,plain,
( spl0_274
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f100,f568,f1430]) ).
fof(f1434,definition,
( spl0_275
<=> c3_1(a648) ),
introduced(definition,[new_symbols(definition,[spl0_275])],[avatar_definition]) ).
fof(f1436,plain,
( spl0_275
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f99,f568,f1434]) ).
fof(f1438,definition,
( spl0_276
<=> c2_1(a651) ),
introduced(definition,[new_symbols(definition,[spl0_276])],[avatar_definition]) ).
fof(f1439,plain,
( c2_1(a651)
| ~ spl0_276 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1440,plain,
( spl0_276
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f98,f561,f1438]) ).
fof(f1442,definition,
( spl0_277
<=> c3_1(a651) ),
introduced(definition,[new_symbols(definition,[spl0_277])],[avatar_definition]) ).
fof(f1444,plain,
( spl0_277
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f97,f561,f1442]) ).
fof(f1446,definition,
( spl0_278
<=> c1_1(a653) ),
introduced(definition,[new_symbols(definition,[spl0_278])],[avatar_definition]) ).
fof(f1447,plain,
( c1_1(a653)
| ~ spl0_278 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1448,plain,
( spl0_278
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f96,f429,f1446]) ).
fof(f1450,definition,
( spl0_279
<=> c3_1(a653) ),
introduced(definition,[new_symbols(definition,[spl0_279])],[avatar_definition]) ).
fof(f1452,plain,
( spl0_279
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f95,f429,f1450]) ).
fof(f1454,definition,
( spl0_280
<=> c3_1(a658) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f1456,plain,
( spl0_280
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f94,f469,f1454]) ).
fof(f1458,definition,
( spl0_281
<=> c2_1(a658) ),
introduced(definition,[new_symbols(definition,[spl0_281])],[avatar_definition]) ).
fof(f1459,plain,
( c2_1(a658)
| ~ spl0_281 ),
inference(avatar_component_clause,[],[f1458]) ).
fof(f1460,plain,
( spl0_281
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f93,f469,f1458]) ).
fof(f1470,definition,
( spl0_284
<=> c3_1(a663) ),
introduced(definition,[new_symbols(definition,[spl0_284])],[avatar_definition]) ).
fof(f1472,plain,
( spl0_284
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f90,f507,f1470]) ).
fof(f1482,definition,
( spl0_287
<=> c1_1(a669) ),
introduced(definition,[new_symbols(definition,[spl0_287])],[avatar_definition]) ).
fof(f1483,plain,
( c1_1(a669)
| ~ spl0_287 ),
inference(avatar_component_clause,[],[f1482]) ).
fof(f1484,plain,
( spl0_287
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f87,f1094,f1482]) ).
fof(f1486,definition,
( spl0_288
<=> c0_1(a669) ),
introduced(definition,[new_symbols(definition,[spl0_288])],[avatar_definition]) ).
fof(f1488,plain,
( spl0_288
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f86,f1094,f1486]) ).
fof(f1490,definition,
( spl0_289
<=> c2_1(a670) ),
introduced(definition,[new_symbols(definition,[spl0_289])],[avatar_definition]) ).
fof(f1491,plain,
( c2_1(a670)
| ~ spl0_289 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1492,plain,
( spl0_289
| ~ spl0_192 ),
inference(avatar_split_clause,[],[f85,f1101,f1490]) ).
fof(f1506,definition,
( spl0_293
<=> c1_1(a673) ),
introduced(definition,[new_symbols(definition,[spl0_293])],[avatar_definition]) ).
fof(f1507,plain,
( c1_1(a673)
| ~ spl0_293 ),
inference(avatar_component_clause,[],[f1506]) ).
fof(f1508,plain,
( spl0_293
| ~ spl0_198 ),
inference(avatar_split_clause,[],[f81,f1126,f1506]) ).
fof(f1510,definition,
( spl0_294
<=> c3_1(a673) ),
introduced(definition,[new_symbols(definition,[spl0_294])],[avatar_definition]) ).
fof(f1512,plain,
( spl0_294
| ~ spl0_198 ),
inference(avatar_split_clause,[],[f80,f1126,f1510]) ).
fof(f1514,definition,
( spl0_295
<=> c0_1(a674) ),
introduced(definition,[new_symbols(definition,[spl0_295])],[avatar_definition]) ).
fof(f1516,plain,
( spl0_295
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f79,f1133,f1514]) ).
fof(f1518,definition,
( spl0_296
<=> c2_1(a674) ),
introduced(definition,[new_symbols(definition,[spl0_296])],[avatar_definition]) ).
fof(f1520,plain,
( spl0_296
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f78,f1133,f1518]) ).
fof(f1522,definition,
( spl0_297
<=> c3_1(a675) ),
introduced(definition,[new_symbols(definition,[spl0_297])],[avatar_definition]) ).
fof(f1524,plain,
( spl0_297
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f77,f1140,f1522]) ).
fof(f1526,definition,
( spl0_298
<=> c1_1(a675) ),
introduced(definition,[new_symbols(definition,[spl0_298])],[avatar_definition]) ).
fof(f1527,plain,
( c1_1(a675)
| ~ spl0_298 ),
inference(avatar_component_clause,[],[f1526]) ).
fof(f1528,plain,
( spl0_298
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f76,f1140,f1526]) ).
fof(f1532,plain,
( spl0_202
| spl0_200
| spl0_198 ),
inference(avatar_split_clause,[],[f75,f1126,f1133,f1140]) ).
fof(f1536,plain,
( spl0_192
| spl0_190
| spl0_156 ),
inference(avatar_split_clause,[],[f74,f940,f1094,f1101]) ).
fof(f1543,plain,
( spl0_82
| spl0_65
| spl0_33 ),
inference(avatar_split_clause,[],[f71,f444,f565,f624]) ).
fof(f1614,plain,
( spl0_3
| ~ spl0_198 ),
inference(avatar_split_clause,[],[f4,f1126,f336]) ).
fof(f1615,plain,
( spl0_3
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f3,f1133,f336]) ).
fof(f1616,plain,
( spl0_3
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f2,f1140,f336]) ).
fof(f1630,definition,
( spl0_299
<=> c0_1(a617) ),
introduced(definition,[new_symbols(definition,[spl0_299])],[avatar_definition]) ).
fof(f1635,plain,
( c0_1(a617)
| ~ c3_1(a617)
| ~ spl0_6
| ~ spl0_255 ),
inference(resolution,[],[f347,f1354]) ).
fof(f1638,plain,
( c0_1(a613)
| ~ c2_1(a613)
| ~ spl0_8
| ~ spl0_214 ),
inference(resolution,[],[f354,f1188]) ).
fof(f1647,definition,
( spl0_301
<=> c0_1(a613) ),
introduced(definition,[new_symbols(definition,[spl0_301])],[avatar_definition]) ).
fof(f1651,plain,
( ~ c2_1(a663)
| ~ c3_1(a663)
| ~ spl0_10
| spl0_186 ),
inference(resolution,[],[f360,f1080]) ).
fof(f1652,plain,
( ~ c2_1(a617)
| ~ c3_1(a617)
| ~ spl0_10
| spl0_165 ),
inference(resolution,[],[f360,f980]) ).
fof(f1657,definition,
( spl0_302
<=> c2_1(a663) ),
introduced(definition,[new_symbols(definition,[spl0_302])],[avatar_definition]) ).
fof(f1684,plain,
( ! [X0] :
( c0_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_8
| ~ spl0_16 ),
inference(resolution,[],[f383,f354]) ).
fof(f1688,plain,
( ! [X0] :
( c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_8
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f1684]) ).
fof(f1693,plain,
( spl0_41
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1688,f382,f353,f473]) ).
fof(f1700,definition,
( spl0_303
<=> c2_1(a603) ),
introduced(definition,[new_symbols(definition,[spl0_303])],[avatar_definition]) ).
fof(f1738,definition,
( spl0_306
<=> c0_1(a652) ),
introduced(definition,[new_symbols(definition,[spl0_306])],[avatar_definition]) ).
fof(f1746,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_8
| ~ spl0_17 ),
inference(resolution,[],[f386,f354]) ).
fof(f1747,plain,
( ~ c3_1(a663)
| c0_1(a663)
| ~ spl0_17
| spl0_186 ),
inference(resolution,[],[f386,f1080]) ).
fof(f1748,plain,
( ~ c3_1(a617)
| c0_1(a617)
| ~ spl0_17
| spl0_165 ),
inference(resolution,[],[f386,f980]) ).
fof(f1749,plain,
( ~ c3_1(a652)
| c0_1(a652)
| ~ spl0_17
| spl0_139 ),
inference(resolution,[],[f386,f871]) ).
fof(f1754,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_8
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1746]) ).
fof(f1763,definition,
( spl0_307
<=> c2_1(a597) ),
introduced(definition,[new_symbols(definition,[spl0_307])],[avatar_definition]) ).
fof(f1764,plain,
( ~ c2_1(a597)
| spl0_307 ),
inference(avatar_component_clause,[],[f1763]) ).
fof(f1768,plain,
( c0_1(a618)
| c3_1(a618)
| ~ spl0_14
| spl0_167 ),
inference(resolution,[],[f989,f375]) ).
fof(f1771,definition,
( spl0_308
<=> c0_1(a618) ),
introduced(definition,[new_symbols(definition,[spl0_308])],[avatar_definition]) ).
fof(f1773,plain,
( spl0_166
| spl0_308
| ~ spl0_14
| spl0_167 ),
inference(avatar_split_clause,[],[f1768,f988,f374,f1771,f984]) ).
fof(f1787,plain,
( c2_1(a625)
| c0_1(a625)
| ~ spl0_18
| spl0_116 ),
inference(resolution,[],[f390,f772]) ).
fof(f1789,plain,
( spl0_115
| spl0_117
| ~ spl0_18
| spl0_116 ),
inference(avatar_split_clause,[],[f1787,f771,f389,f775,f767]) ).
fof(f1800,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_8
| ~ spl0_19 ),
inference(resolution,[],[f393,f354]) ).
fof(f1809,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_8
| ~ spl0_19 ),
inference(duplicate_literal_removal,[],[f1800]) ).
fof(f1818,plain,
( spl0_41
| ~ spl0_8
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1809,f392,f353,f473]) ).
fof(f1865,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_15
| ~ spl0_27 ),
inference(resolution,[],[f423,f379]) ).
fof(f1870,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_15
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f1865]) ).
fof(f1874,plain,
( spl0_5
| ~ spl0_15
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1870,f422,f378,f343]) ).
fof(f1929,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_11
| ~ spl0_21 ),
inference(resolution,[],[f364,f400]) ).
fof(f1934,plain,
( c2_1(a624)
| ~ c3_1(a624)
| ~ spl0_11
| spl0_114 ),
inference(resolution,[],[f364,f763]) ).
fof(f1938,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_11
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f1929]) ).
fof(f1943,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1938,f399,f363,f343]) ).
fof(f1947,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_15
| ~ spl0_28 ),
inference(resolution,[],[f426,f379]) ).
fof(f1955,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_15
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f1947]) ).
fof(f1962,plain,
( spl0_5
| ~ spl0_15
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f1955,f425,f378,f343]) ).
fof(f1964,plain,
( spl0_187
| ~ spl0_284
| ~ spl0_17
| spl0_186 ),
inference(avatar_split_clause,[],[f1747,f1079,f385,f1470,f1083]) ).
fof(f1965,plain,
( spl0_306
| ~ spl0_232
| ~ spl0_17
| spl0_139 ),
inference(avatar_split_clause,[],[f1749,f870,f385,f1259,f1738]) ).
fof(f1983,definition,
( spl0_314
<=> c0_1(a628) ),
introduced(definition,[new_symbols(definition,[spl0_314])],[avatar_definition]) ).
fof(f1996,definition,
( spl0_316
<=> c3_1(a670) ),
introduced(definition,[new_symbols(definition,[spl0_316])],[avatar_definition]) ).
fof(f2004,definition,
( spl0_317
<=> c3_1(a669) ),
introduced(definition,[new_symbols(definition,[spl0_317])],[avatar_definition]) ).
fof(f2010,plain,
( ~ c3_1(a614)
| ~ c0_1(a614)
| ~ spl0_21
| ~ spl0_252 ),
inference(resolution,[],[f1342,f400]) ).
fof(f2013,definition,
( spl0_318
<=> c3_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_318])],[avatar_definition]) ).
fof(f2042,plain,
( ~ c3_1(a648)
| ~ c0_1(a648)
| ~ spl0_5
| spl0_181 ),
inference(resolution,[],[f344,f1055]) ).
fof(f2043,plain,
( ~ c3_1(a599)
| ~ c0_1(a599)
| ~ spl0_5
| spl0_157 ),
inference(resolution,[],[f344,f944]) ).
fof(f2045,plain,
( ~ c3_1(a652)
| ~ c0_1(a652)
| ~ spl0_5
| spl0_138 ),
inference(resolution,[],[f344,f867]) ).
fof(f2057,plain,
( ~ spl0_306
| ~ spl0_232
| ~ spl0_5
| spl0_138 ),
inference(avatar_split_clause,[],[f2045,f866,f343,f1259,f1738]) ).
fof(f2058,plain,
( ~ spl0_238
| ~ spl0_237
| ~ spl0_5
| spl0_157 ),
inference(avatar_split_clause,[],[f2043,f943,f343,f1279,f1283]) ).
fof(f2061,plain,
( ~ spl0_274
| ~ spl0_275
| ~ spl0_5
| spl0_181 ),
inference(avatar_split_clause,[],[f2042,f1054,f343,f1434,f1430]) ).
fof(f2093,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_12
| ~ spl0_21 ),
inference(resolution,[],[f367,f400]) ).
fof(f2100,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_12
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f2093]) ).
fof(f2110,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_13
| ~ spl0_28 ),
inference(resolution,[],[f371,f426]) ).
fof(f2111,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_21 ),
inference(resolution,[],[f371,f400]) ).
fof(f2115,plain,
( ~ c0_1(a603)
| c2_1(a603)
| ~ spl0_13
| spl0_91 ),
inference(resolution,[],[f371,f662]) ).
fof(f2118,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_13
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f2111]) ).
fof(f2119,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_13
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f2110]) ).
fof(f2128,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_17
| ~ spl0_28 ),
inference(resolution,[],[f386,f426]) ).
fof(f2136,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_17
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f2128]) ).
fof(f2141,plain,
( spl0_34
| ~ spl0_17
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f2136,f425,f385,f447]) ).
fof(f2150,plain,
( ~ c2_1(a674)
| ~ c0_1(a674)
| ~ spl0_12
| spl0_201 ),
inference(resolution,[],[f1137,f367]) ).
fof(f2158,plain,
( ~ spl0_295
| ~ spl0_296
| ~ spl0_12
| spl0_201 ),
inference(avatar_split_clause,[],[f2150,f1136,f366,f1518,f1514]) ).
fof(f2164,definition,
( spl0_320
<=> c0_1(a675) ),
introduced(definition,[new_symbols(definition,[spl0_320])],[avatar_definition]) ).
fof(f2219,plain,
( ~ c3_1(a670)
| c0_1(a670)
| ~ spl0_17
| spl0_194 ),
inference(resolution,[],[f1109,f386]) ).
fof(f2222,plain,
( ~ c2_1(a670)
| ~ c3_1(a670)
| ~ spl0_10
| spl0_194 ),
inference(resolution,[],[f1109,f360]) ).
fof(f2224,plain,
( spl0_193
| ~ spl0_316
| ~ spl0_17
| spl0_194 ),
inference(avatar_split_clause,[],[f2219,f1108,f385,f1996,f1104]) ).
fof(f2231,plain,
( ~ c0_1(a597)
| c3_1(a597)
| ~ spl0_32
| spl0_307 ),
inference(resolution,[],[f441,f1764]) ).
fof(f2241,plain,
( ~ c0_1(a647)
| c2_1(a647)
| ~ spl0_13
| spl0_179 ),
inference(resolution,[],[f1046,f371]) ).
fof(f2245,definition,
( spl0_322
<=> c3_1(a647) ),
introduced(definition,[new_symbols(definition,[spl0_322])],[avatar_definition]) ).
fof(f2251,plain,
( spl0_180
| ~ spl0_273
| ~ spl0_13
| spl0_179 ),
inference(avatar_split_clause,[],[f2241,f1045,f370,f1426,f1049]) ).
fof(f2263,plain,
( c0_1(a646)
| ~ c3_1(a646)
| ~ spl0_34
| spl0_137 ),
inference(resolution,[],[f448,f862]) ).
fof(f2264,plain,
( c0_1(a628)
| ~ c3_1(a628)
| ~ spl0_34
| spl0_120 ),
inference(resolution,[],[f448,f790]) ).
fof(f2271,plain,
( ~ spl0_231
| spl0_136
| ~ spl0_34
| spl0_137 ),
inference(avatar_split_clause,[],[f2263,f861,f447,f857,f1255]) ).
fof(f2275,plain,
( spl0_85
| ~ spl0_204
| ~ spl0_32
| spl0_307 ),
inference(avatar_split_clause,[],[f2231,f1763,f440,f1147,f636]) ).
fof(f2285,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_13
| ~ spl0_36 ),
inference(resolution,[],[f455,f371]) ).
fof(f2289,plain,
( c3_1(a669)
| c2_1(a669)
| ~ spl0_36
| ~ spl0_287 ),
inference(resolution,[],[f455,f1483]) ).
fof(f2291,plain,
( c3_1(a618)
| c2_1(a618)
| ~ spl0_36
| ~ spl0_256 ),
inference(resolution,[],[f455,f1358]) ).
fof(f2296,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_36 ),
inference(duplicate_literal_removal,[],[f2285]) ).
fof(f2303,plain,
( spl0_167
| spl0_166
| ~ spl0_36
| ~ spl0_256 ),
inference(avatar_split_clause,[],[f2291,f1357,f454,f984,f988]) ).
fof(f2307,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_27
| ~ spl0_39 ),
inference(resolution,[],[f466,f423]) ).
fof(f2311,plain,
( c3_1(a647)
| c2_1(a647)
| ~ spl0_39
| spl0_179 ),
inference(resolution,[],[f466,f1046]) ).
fof(f2317,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_27
| ~ spl0_39 ),
inference(duplicate_literal_removal,[],[f2307]) ).
fof(f2322,plain,
( spl0_180
| spl0_322
| ~ spl0_39
| spl0_179 ),
inference(avatar_split_clause,[],[f2311,f1045,f465,f2245,f1049]) ).
fof(f2336,plain,
( c0_1(a606)
| c3_1(a606)
| ~ spl0_41
| ~ spl0_209 ),
inference(resolution,[],[f474,f1168]) ).
fof(f2345,plain,
( spl0_96
| spl0_97
| ~ spl0_41
| ~ spl0_209 ),
inference(avatar_split_clause,[],[f2336,f1167,f473,f685,f681]) ).
fof(f2351,plain,
( spl0_6
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1754,f385,f353,f346]) ).
fof(f2352,plain,
( ~ spl0_219
| spl0_113
| ~ spl0_11
| spl0_114 ),
inference(avatar_split_clause,[],[f1934,f762,f363,f758,f1207]) ).
fof(f2355,plain,
( spl0_299
| ~ spl0_254
| ~ spl0_17
| spl0_165 ),
inference(avatar_split_clause,[],[f1748,f979,f385,f1349,f1630]) ).
fof(f2375,plain,
( spl0_4
| ~ spl0_12
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f2100,f399,f366,f339]) ).
fof(f2376,plain,
( ~ spl0_254
| spl0_299
| ~ spl0_6
| ~ spl0_255 ),
inference(avatar_split_clause,[],[f1635,f1353,f346,f1630,f1349]) ).
fof(f2397,definition,
( spl0_323
<=> c3_1(a609) ),
introduced(definition,[new_symbols(definition,[spl0_323])],[avatar_definition]) ).
fof(f2414,plain,
( ~ c3_1(a643)
| c0_1(a643)
| ~ spl0_17
| spl0_134 ),
inference(resolution,[],[f849,f386]) ).
fof(f2433,definition,
( spl0_325
<=> c3_1(a607) ),
introduced(definition,[new_symbols(definition,[spl0_325])],[avatar_definition]) ).
fof(f2444,plain,
( ~ c0_1(a619)
| c2_1(a619)
| ~ spl0_13
| spl0_168 ),
inference(resolution,[],[f994,f371]) ).
fof(f2448,definition,
( spl0_326
<=> c2_1(a619) ),
introduced(definition,[new_symbols(definition,[spl0_326])],[avatar_definition]) ).
fof(f2452,plain,
( spl0_326
| ~ spl0_257
| ~ spl0_13
| spl0_168 ),
inference(avatar_split_clause,[],[f2444,f993,f370,f1361,f2448]) ).
fof(f2482,plain,
( c3_1(a614)
| ~ c0_1(a614)
| ~ spl0_2
| ~ spl0_253 ),
inference(resolution,[],[f334,f1346]) ).
fof(f2486,plain,
( c3_1(a613)
| ~ c0_1(a613)
| ~ spl0_2
| ~ spl0_213 ),
inference(resolution,[],[f334,f1184]) ).
fof(f2496,plain,
( ~ spl0_301
| spl0_104
| ~ spl0_2
| ~ spl0_213 ),
inference(avatar_split_clause,[],[f2486,f1183,f333,f717,f1647]) ).
fof(f2529,plain,
( ~ spl0_251
| spl0_318
| ~ spl0_2
| ~ spl0_253 ),
inference(avatar_split_clause,[],[f2482,f1345,f333,f2013,f1336]) ).
fof(f2531,plain,
( ~ spl0_213
| spl0_301
| ~ spl0_8
| ~ spl0_214 ),
inference(avatar_split_clause,[],[f1638,f1187,f353,f1647,f1183]) ).
fof(f2586,plain,
( c0_1(a670)
| ~ c3_1(a670)
| ~ spl0_6
| ~ spl0_289 ),
inference(resolution,[],[f347,f1491]) ).
fof(f2588,plain,
( c0_1(a651)
| ~ c3_1(a651)
| ~ spl0_6
| ~ spl0_276 ),
inference(resolution,[],[f347,f1439]) ).
fof(f2594,plain,
( c0_1(a642)
| ~ c3_1(a642)
| ~ spl0_6
| ~ spl0_229 ),
inference(resolution,[],[f347,f1248]) ).
fof(f2596,plain,
( c0_1(a609)
| ~ c3_1(a609)
| ~ spl0_6
| ~ spl0_210 ),
inference(resolution,[],[f347,f1172]) ).
fof(f2604,plain,
( ~ spl0_323
| spl0_99
| ~ spl0_6
| ~ spl0_210 ),
inference(avatar_split_clause,[],[f2596,f1171,f346,f694,f2397]) ).
fof(f2607,plain,
( ~ spl0_228
| spl0_133
| ~ spl0_6
| ~ spl0_229 ),
inference(avatar_split_clause,[],[f2594,f1247,f346,f843,f1243]) ).
fof(f2614,plain,
( ~ spl0_277
| spl0_182
| ~ spl0_6
| ~ spl0_276 ),
inference(avatar_split_clause,[],[f2588,f1438,f346,f1059,f1442]) ).
fof(f2618,plain,
( ~ spl0_316
| spl0_193
| ~ spl0_6
| ~ spl0_289 ),
inference(avatar_split_clause,[],[f2586,f1490,f346,f1104,f1996]) ).
fof(f2621,plain,
( ~ spl0_316
| ~ spl0_289
| ~ spl0_10
| spl0_194 ),
inference(avatar_split_clause,[],[f2222,f1108,f359,f1490,f1996]) ).
fof(f2627,plain,
( spl0_32
| ~ spl0_27
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f2317,f465,f422,f440]) ).
fof(f2648,plain,
( ~ spl0_254
| ~ spl0_255
| ~ spl0_10
| spl0_165 ),
inference(avatar_split_clause,[],[f1652,f979,f359,f1353,f1349]) ).
fof(f2666,plain,
( spl0_303
| ~ spl0_208
| ~ spl0_13
| spl0_91 ),
inference(avatar_split_clause,[],[f2115,f661,f370,f1163,f1700]) ).
fof(f2717,plain,
( c0_1(a658)
| ~ c3_1(a658)
| ~ spl0_6
| ~ spl0_281 ),
inference(resolution,[],[f1459,f347]) ).
fof(f2720,definition,
( spl0_332
<=> c0_1(a658) ),
introduced(definition,[new_symbols(definition,[spl0_332])],[avatar_definition]) ).
fof(f2722,plain,
( ~ spl0_280
| spl0_332
| ~ spl0_6
| ~ spl0_281 ),
inference(avatar_split_clause,[],[f2717,f1458,f346,f2720,f1454]) ).
fof(f2736,plain,
( ~ c2_1(a614)
| ~ c0_1(a614)
| ~ spl0_1
| ~ spl0_252 ),
inference(resolution,[],[f331,f1342]) ).
fof(f2744,plain,
( ~ spl0_251
| ~ spl0_253
| ~ spl0_1
| ~ spl0_252 ),
inference(avatar_split_clause,[],[f2736,f1341,f330,f1345,f1336]) ).
fof(f2775,plain,
( spl0_5
| ~ spl0_13
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f2118,f399,f370,f343]) ).
fof(f2776,plain,
( ~ spl0_251
| ~ spl0_318
| ~ spl0_21
| ~ spl0_252 ),
inference(avatar_split_clause,[],[f2010,f1341,f399,f2013,f1336]) ).
fof(f2793,plain,
( c0_1(a670)
| ~ c2_1(a670)
| ~ spl0_9
| spl0_194 ),
inference(resolution,[],[f357,f1109]) ).
fof(f2794,plain,
( c0_1(a658)
| ~ c2_1(a658)
| ~ spl0_9
| spl0_184 ),
inference(resolution,[],[f357,f1070]) ).
fof(f2801,plain,
( c0_1(a609)
| ~ c2_1(a609)
| ~ spl0_9
| spl0_98 ),
inference(resolution,[],[f357,f691]) ).
fof(f2819,plain,
( ~ spl0_210
| spl0_99
| ~ spl0_9
| spl0_98 ),
inference(avatar_split_clause,[],[f2801,f690,f356,f694,f1171]) ).
fof(f2823,definition,
( spl0_338
<=> c0_1(a602) ),
introduced(definition,[new_symbols(definition,[spl0_338])],[avatar_definition]) ).
fof(f2828,plain,
( ~ spl0_281
| spl0_332
| ~ spl0_9
| spl0_184 ),
inference(avatar_split_clause,[],[f2794,f1069,f356,f2720,f1458]) ).
fof(f2829,plain,
( ~ spl0_289
| spl0_193
| ~ spl0_9
| spl0_194 ),
inference(avatar_split_clause,[],[f2793,f1108,f356,f1104,f1490]) ).
fof(f2833,plain,
( ~ spl0_284
| ~ spl0_302
| ~ spl0_10
| spl0_186 ),
inference(avatar_split_clause,[],[f1651,f1079,f359,f1657,f1470]) ).
fof(f2848,plain,
( c3_1(a602)
| ~ c0_1(a602)
| ~ spl0_2
| ~ spl0_241 ),
inference(resolution,[],[f334,f1296]) ).
fof(f2850,plain,
( c3_1(a627)
| ~ c0_1(a627)
| ~ spl0_2
| ~ spl0_221 ),
inference(resolution,[],[f334,f1216]) ).
fof(f2859,plain,
( ~ spl0_220
| spl0_118
| ~ spl0_2
| ~ spl0_221 ),
inference(avatar_split_clause,[],[f2850,f1215,f333,f780,f1211]) ).
fof(f2863,plain,
( ~ spl0_338
| spl0_161
| ~ spl0_2
| ~ spl0_241 ),
inference(avatar_split_clause,[],[f2848,f1295,f333,f959,f2823]) ).
fof(f2870,plain,
( ~ c2_1(a658)
| ~ c3_1(a658)
| ~ spl0_10
| spl0_184 ),
inference(resolution,[],[f360,f1070]) ).
fof(f2876,plain,
( ~ c2_1(a609)
| ~ c3_1(a609)
| ~ spl0_10
| spl0_98 ),
inference(resolution,[],[f360,f691]) ).
fof(f2886,plain,
( ~ spl0_323
| ~ spl0_210
| ~ spl0_10
| spl0_98 ),
inference(avatar_split_clause,[],[f2876,f690,f359,f1171,f2397]) ).
fof(f2888,plain,
( ~ spl0_280
| ~ spl0_281
| ~ spl0_10
| spl0_184 ),
inference(avatar_split_clause,[],[f2870,f1069,f359,f1458,f1454]) ).
fof(f2905,plain,
( spl0_32
| ~ spl0_13
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f2296,f454,f370,f440]) ).
fof(f2906,plain,
( spl0_191
| spl0_317
| ~ spl0_36
| ~ spl0_287 ),
inference(avatar_split_clause,[],[f2289,f1482,f454,f2004,f1097]) ).
fof(f2913,plain,
( spl0_5
| ~ spl0_13
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f2119,f425,f370,f343]) ).
fof(f2924,plain,
( ~ c3_1(a617)
| ~ c0_1(a617)
| ~ spl0_4
| ~ spl0_255 ),
inference(resolution,[],[f340,f1354]) ).
fof(f2939,plain,
( ~ c3_1(a669)
| ~ c0_1(a669)
| ~ spl0_5
| spl0_191 ),
inference(resolution,[],[f344,f1098]) ).
fof(f2942,plain,
( ~ c3_1(a607)
| ~ c0_1(a607)
| ~ spl0_5
| spl0_163 ),
inference(resolution,[],[f344,f970]) ).
fof(f2946,plain,
( ~ c3_1(a628)
| ~ c0_1(a628)
| ~ spl0_5
| spl0_120 ),
inference(resolution,[],[f344,f790]) ).
fof(f2949,plain,
( ~ c3_1(a615)
| ~ c0_1(a615)
| ~ spl0_5
| spl0_105 ),
inference(resolution,[],[f344,f723]) ).
fof(f2964,plain,
( ~ spl0_216
| ~ spl0_215
| ~ spl0_5
| spl0_105 ),
inference(avatar_split_clause,[],[f2949,f722,f343,f1191,f1195]) ).
fof(f2970,plain,
( ~ spl0_314
| ~ spl0_222
| ~ spl0_5
| spl0_120 ),
inference(avatar_split_clause,[],[f2946,f789,f343,f1219,f1983]) ).
fof(f2971,plain,
( ~ spl0_244
| ~ spl0_325
| ~ spl0_5
| spl0_163 ),
inference(avatar_split_clause,[],[f2942,f969,f343,f2433,f1307]) ).
fof(f2973,plain,
( ~ spl0_288
| ~ spl0_317
| ~ spl0_5
| spl0_191 ),
inference(avatar_split_clause,[],[f2939,f1097,f343,f2004,f1486]) ).
fof(f2980,plain,
( ~ c3_1(a614)
| ~ c0_1(a614)
| ~ spl0_4
| ~ spl0_253 ),
inference(resolution,[],[f1346,f340]) ).
fof(f2982,plain,
( ~ spl0_251
| ~ spl0_318
| ~ spl0_4
| ~ spl0_253 ),
inference(avatar_split_clause,[],[f2980,f1345,f339,f2013,f1336]) ).
fof(f2987,plain,
( c2_1(a628)
| ~ c3_1(a628)
| ~ spl0_11
| spl0_119 ),
inference(resolution,[],[f364,f786]) ).
fof(f2999,plain,
( ~ spl0_222
| spl0_120
| ~ spl0_11
| spl0_119 ),
inference(avatar_split_clause,[],[f2987,f785,f363,f789,f1219]) ).
fof(f3003,plain,
( spl0_135
| ~ spl0_230
| ~ spl0_17
| spl0_134 ),
inference(avatar_split_clause,[],[f2414,f848,f385,f1251,f852]) ).
fof(f3010,plain,
( ~ spl0_222
| spl0_314
| ~ spl0_34
| spl0_120 ),
inference(avatar_split_clause,[],[f2264,f789,f447,f1983,f1219]) ).
fof(f3031,plain,
( ~ c2_1(a598)
| ~ c0_1(a598)
| ~ spl0_12
| spl0_86 ),
inference(resolution,[],[f367,f642]) ).
fof(f3037,plain,
( ~ spl0_206
| ~ spl0_205
| ~ spl0_12
| spl0_86 ),
inference(avatar_split_clause,[],[f3031,f641,f366,f1151,f1155]) ).
fof(f3086,plain,
( c0_1(a660)
| c3_1(a660)
| ~ spl0_16
| spl0_149 ),
inference(resolution,[],[f383,f910]) ).
fof(f3090,plain,
( c0_1(a620)
| c3_1(a620)
| ~ spl0_16
| spl0_107 ),
inference(resolution,[],[f383,f733]) ).
fof(f3091,plain,
( spl0_108
| spl0_109
| ~ spl0_16
| spl0_107 ),
inference(avatar_split_clause,[],[f3090,f732,f382,f740,f736]) ).
fof(f3096,plain,
( spl0_148
| spl0_147
| ~ spl0_16
| spl0_149 ),
inference(avatar_split_clause,[],[f3086,f909,f382,f901,f905]) ).
fof(f3137,plain,
( ~ c3_1(a669)
| ~ c0_1(a669)
| ~ spl0_21
| ~ spl0_287 ),
inference(resolution,[],[f400,f1483]) ).
fof(f3142,plain,
( ~ c3_1(a614)
| ~ c0_1(a614)
| ~ spl0_21
| ~ spl0_252 ),
inference(resolution,[],[f400,f1342]) ).
fof(f3158,plain,
( ~ spl0_251
| ~ spl0_318
| ~ spl0_21
| ~ spl0_252 ),
inference(avatar_split_clause,[],[f3142,f1341,f399,f2013,f1336]) ).
fof(f3162,plain,
( ~ spl0_288
| ~ spl0_317
| ~ spl0_21
| ~ spl0_287 ),
inference(avatar_split_clause,[],[f3137,f1482,f399,f2004,f1486]) ).
fof(f3174,plain,
( c2_1(a653)
| ~ c3_1(a653)
| ~ spl0_28
| ~ spl0_278 ),
inference(resolution,[],[f426,f1447]) ).
fof(f3197,plain,
( ~ spl0_279
| spl0_183
| ~ spl0_28
| ~ spl0_278 ),
inference(avatar_split_clause,[],[f3174,f1446,f425,f1064,f1450]) ).
fof(f3202,plain,
( ~ c0_1(a669)
| c3_1(a669)
| ~ spl0_32
| spl0_191 ),
inference(resolution,[],[f441,f1098]) ).
fof(f3205,plain,
( ~ c0_1(a607)
| c3_1(a607)
| ~ spl0_32
| spl0_163 ),
inference(resolution,[],[f441,f970]) ).
fof(f3224,plain,
( spl0_325
| ~ spl0_244
| ~ spl0_32
| spl0_163 ),
inference(avatar_split_clause,[],[f3205,f969,f440,f1307,f2433]) ).
fof(f3227,plain,
( spl0_317
| ~ spl0_288
| ~ spl0_32
| spl0_191 ),
inference(avatar_split_clause,[],[f3202,f1097,f440,f1486,f2004]) ).
fof(f3258,plain,
( ~ c2_1(a597)
| ~ c0_1(a597)
| ~ spl0_12
| spl0_84 ),
inference(resolution,[],[f633,f367]) ).
fof(f3262,plain,
( ~ spl0_204
| ~ spl0_307
| ~ spl0_12
| spl0_84 ),
inference(avatar_split_clause,[],[f3258,f632,f366,f1763,f1147]) ).
fof(f3263,plain,
( ~ c2_1(a603)
| ~ c0_1(a603)
| ~ spl0_12
| spl0_91 ),
inference(resolution,[],[f662,f367]) ).
fof(f3266,plain,
( ~ spl0_208
| ~ spl0_303
| ~ spl0_12
| spl0_91 ),
inference(avatar_split_clause,[],[f3263,f661,f366,f1700,f1163]) ).
fof(f3269,plain,
( c0_1(a609)
| c3_1(a609)
| ~ spl0_16
| spl0_98 ),
inference(resolution,[],[f691,f383]) ).
fof(f3270,plain,
( spl0_323
| spl0_99
| ~ spl0_16
| spl0_98 ),
inference(avatar_split_clause,[],[f3269,f690,f382,f694,f2397]) ).
fof(f3293,plain,
( ~ c2_1(a619)
| ~ c0_1(a619)
| ~ spl0_12
| spl0_168 ),
inference(resolution,[],[f994,f367]) ).
fof(f3296,plain,
( ~ spl0_257
| ~ spl0_326
| ~ spl0_12
| spl0_168 ),
inference(avatar_split_clause,[],[f3293,f993,f366,f2448,f1361]) ).
fof(f3297,plain,
( ~ c3_1(a647)
| ~ c0_1(a647)
| ~ spl0_5
| spl0_180 ),
inference(resolution,[],[f1050,f344]) ).
fof(f3298,plain,
( ~ spl0_273
| ~ spl0_322
| ~ spl0_5
| spl0_180 ),
inference(avatar_split_clause,[],[f3297,f1049,f343,f2245,f1426]) ).
fof(f3313,plain,
( ~ c3_1(a658)
| ~ c0_1(a658)
| ~ spl0_4
| ~ spl0_281 ),
inference(resolution,[],[f1459,f340]) ).
fof(f3314,plain,
( ~ spl0_332
| ~ spl0_280
| ~ spl0_4
| ~ spl0_281 ),
inference(avatar_split_clause,[],[f3313,f1458,f339,f1454,f2720]) ).
fof(f3341,plain,
( c2_1(a663)
| c0_1(a663)
| ~ spl0_18
| spl0_186 ),
inference(resolution,[],[f390,f1080]) ).
fof(f3345,plain,
( c2_1(a628)
| c0_1(a628)
| ~ spl0_18
| spl0_119 ),
inference(resolution,[],[f390,f786]) ).
fof(f3352,plain,
( spl0_314
| spl0_120
| ~ spl0_18
| spl0_119 ),
inference(avatar_split_clause,[],[f3345,f785,f389,f789,f1983]) ).
fof(f3353,plain,
( spl0_187
| spl0_302
| ~ spl0_18
| spl0_186 ),
inference(avatar_split_clause,[],[f3341,f1079,f389,f1657,f1083]) ).
fof(f3360,plain,
( c3_1(a670)
| ~ c2_1(a670)
| ~ spl0_19
| spl0_194 ),
inference(resolution,[],[f393,f1109]) ).
fof(f3363,plain,
( c3_1(a619)
| ~ c2_1(a619)
| ~ spl0_19
| spl0_168 ),
inference(resolution,[],[f393,f994]) ).
fof(f3366,plain,
( c3_1(a609)
| ~ c2_1(a609)
| ~ spl0_19
| spl0_98 ),
inference(resolution,[],[f393,f691]) ).
fof(f3372,plain,
( ~ spl0_210
| spl0_323
| ~ spl0_19
| spl0_98 ),
inference(avatar_split_clause,[],[f3366,f690,f392,f2397,f1171]) ).
fof(f3373,plain,
( ~ spl0_326
| spl0_169
| ~ spl0_19
| spl0_168 ),
inference(avatar_split_clause,[],[f3363,f993,f392,f997,f2448]) ).
fof(f3374,plain,
( ~ spl0_289
| spl0_316
| ~ spl0_19
| spl0_194 ),
inference(avatar_split_clause,[],[f3360,f1108,f392,f1996,f1490]) ).
fof(f3408,plain,
( c2_1(a669)
| ~ c0_1(a669)
| ~ spl0_27
| ~ spl0_287 ),
inference(resolution,[],[f423,f1483]) ).
fof(f3412,plain,
( c2_1(a618)
| ~ c0_1(a618)
| ~ spl0_27
| ~ spl0_256 ),
inference(resolution,[],[f423,f1358]) ).
fof(f3414,plain,
( c2_1(a607)
| ~ c0_1(a607)
| ~ spl0_27
| ~ spl0_245 ),
inference(resolution,[],[f423,f1312]) ).
fof(f3423,plain,
( ~ spl0_244
| spl0_163
| ~ spl0_27
| ~ spl0_245 ),
inference(avatar_split_clause,[],[f3414,f1311,f422,f969,f1307]) ).
fof(f3424,plain,
( ~ spl0_308
| spl0_167
| ~ spl0_27
| ~ spl0_256 ),
inference(avatar_split_clause,[],[f3412,f1357,f422,f988,f1771]) ).
fof(f3428,plain,
( ~ spl0_288
| spl0_191
| ~ spl0_27
| ~ spl0_287 ),
inference(avatar_split_clause,[],[f3408,f1482,f422,f1097,f1486]) ).
fof(f3430,plain,
( c0_1(a670)
| c3_1(a670)
| ~ spl0_41
| ~ spl0_289 ),
inference(resolution,[],[f474,f1491]) ).
fof(f3440,plain,
( c0_1(a602)
| c3_1(a602)
| ~ spl0_41
| ~ spl0_241 ),
inference(resolution,[],[f474,f1296]) ).
fof(f3446,plain,
( c0_1(a609)
| c3_1(a609)
| ~ spl0_41
| ~ spl0_210 ),
inference(resolution,[],[f474,f1172]) ).
fof(f3451,plain,
( spl0_323
| spl0_99
| ~ spl0_41
| ~ spl0_210 ),
inference(avatar_split_clause,[],[f3446,f1171,f473,f694,f2397]) ).
fof(f3452,plain,
( spl0_161
| spl0_338
| ~ spl0_41
| ~ spl0_241 ),
inference(avatar_split_clause,[],[f3440,f1295,f473,f2823,f959]) ).
fof(f3457,plain,
( spl0_316
| spl0_193
| ~ spl0_41
| ~ spl0_289 ),
inference(avatar_split_clause,[],[f3430,f1490,f473,f1104,f1996]) ).
fof(f3482,plain,
( c2_1(a608)
| ~ c0_1(a608)
| ~ spl0_27
| ~ spl0_248 ),
inference(resolution,[],[f1325,f423]) ).
fof(f3487,definition,
( spl0_342
<=> c2_1(a608) ),
introduced(definition,[new_symbols(definition,[spl0_342])],[avatar_definition]) ).
fof(f3492,plain,
( ~ spl0_246
| spl0_342
| ~ spl0_27
| ~ spl0_248 ),
inference(avatar_split_clause,[],[f3482,f1324,f422,f3487,f1315]) ).
fof(f3510,plain,
( ~ c3_1(a675)
| ~ c0_1(a675)
| ~ spl0_5
| spl0_203 ),
inference(resolution,[],[f1144,f344]) ).
fof(f3511,plain,
( ~ spl0_320
| ~ spl0_297
| ~ spl0_5
| spl0_203 ),
inference(avatar_split_clause,[],[f3510,f1143,f343,f1522,f2164]) ).
fof(f3512,plain,
( c2_1(a616)
| ~ c0_1(a616)
| ~ spl0_27
| ~ spl0_217 ),
inference(resolution,[],[f1200,f423]) ).
fof(f3514,plain,
( ~ spl0_218
| spl0_106
| ~ spl0_27
| ~ spl0_217 ),
inference(avatar_split_clause,[],[f3512,f1199,f422,f727,f1203]) ).
fof(f3538,plain,
( ~ c2_1(a608)
| ~ c3_1(a608)
| ~ spl0_24
| ~ spl0_248 ),
inference(resolution,[],[f412,f1325]) ).
fof(f3547,plain,
( ~ spl0_247
| ~ spl0_342
| ~ spl0_24
| ~ spl0_248 ),
inference(avatar_split_clause,[],[f3538,f1324,f411,f3487,f1320]) ).
fof(f3555,plain,
( c0_1(a675)
| ~ c3_1(a675)
| ~ spl0_43
| ~ spl0_298 ),
inference(resolution,[],[f481,f1527]) ).
fof(f3556,plain,
( c0_1(a673)
| ~ c3_1(a673)
| ~ spl0_43
| ~ spl0_293 ),
inference(resolution,[],[f481,f1507]) ).
fof(f3574,plain,
( ~ spl0_294
| spl0_199
| ~ spl0_43
| ~ spl0_293 ),
inference(avatar_split_clause,[],[f3556,f1506,f480,f1129,f1510]) ).
fof(f3575,plain,
( ~ spl0_297
| spl0_320
| ~ spl0_43
| ~ spl0_298 ),
inference(avatar_split_clause,[],[f3555,f1526,f480,f2164,f1522]) ).
fof(f3587,plain,
( ~ spl0_299
| ~ spl0_254
| ~ spl0_4
| ~ spl0_255 ),
inference(avatar_split_clause,[],[f2924,f1353,f339,f1349,f1630]) ).
fof(f3601,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_7
| ~ spl0_12 ),
inference(resolution,[],[f350,f367]) ).
fof(f3619,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_7
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f3601]) ).
fof(f3627,plain,
( spl0_2
| ~ spl0_7
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f3619,f366,f349,f333]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f341]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f351]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f361]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_6
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f368]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_6
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f372]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_5
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f380]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_10
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f387]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_9
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f394]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_4
| spl0_5
| spl0_22 ),
inference(sat_conversion,[],[f405]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f427]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_15
| spl0_17
| spl0_29 ),
inference(sat_conversion,[],[f431]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_11
| spl0_27
| spl0_30 ),
inference(sat_conversion,[],[f435]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_24
| spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f467]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_11
| spl0_36
| spl0_40 ),
inference(sat_conversion,[],[f471]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_11
| spl0_29
| spl0_41 ),
inference(sat_conversion,[],[f475]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_13
| spl0_17
| spl0_44 ),
inference(sat_conversion,[],[f486]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_18
| spl0_43
| spl0_45 ),
inference(sat_conversion,[],[f490]) ).
cnf(s28,plain,
( ~ spl0_3
| spl0_8
| spl0_41 ),
inference(sat_conversion,[],[f491]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_16
| spl0_17
| spl0_44 ),
inference(sat_conversion,[],[f492]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_39
| spl0_41 ),
inference(sat_conversion,[],[f493]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_4
| spl0_30
| spl0_46 ),
inference(sat_conversion,[],[f497]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_14
| spl0_16 ),
inference(sat_conversion,[],[f498]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_5
| spl0_26
| spl0_49 ),
inference(sat_conversion,[],[f509]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_10
| spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f516]) ).
cnf(s36,plain,
( ~ spl0_3
| spl0_12
| spl0_52
| spl0_53 ),
inference(sat_conversion,[],[f523]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_28
| spl0_56
| spl0_57 ),
inference(sat_conversion,[],[f537]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_21
| spl0_60 ),
inference(sat_conversion,[],[f548]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_34
| spl0_61
| spl0_62 ),
inference(sat_conversion,[],[f555]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_13
| spl0_29
| spl0_63 ),
inference(sat_conversion,[],[f559]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_41
| spl0_46
| spl0_64 ),
inference(sat_conversion,[],[f563]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_17
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f570]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_32
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f577]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_36
| spl0_74
| spl0_75 ),
inference(sat_conversion,[],[f601]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_17
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f608]) ).
cnf(s53,plain,
( ~ spl0_77
| ~ spl0_84 ),
inference(sat_conversion,[],[f634]) ).
cnf(s54,plain,
( ~ spl0_77
| ~ spl0_85 ),
inference(sat_conversion,[],[f638]) ).
cnf(s55,plain,
( ~ spl0_76
| ~ spl0_86 ),
inference(sat_conversion,[],[f643]) ).
cnf(s59,plain,
( ~ spl0_62
| ~ spl0_91 ),
inference(sat_conversion,[],[f663]) ).
cnf(s63,plain,
( ~ spl0_30
| ~ spl0_96 ),
inference(sat_conversion,[],[f683]) ).
cnf(s64,plain,
( ~ spl0_30
| ~ spl0_97 ),
inference(sat_conversion,[],[f687]) ).
cnf(s65,plain,
( ~ spl0_60
| ~ spl0_98 ),
inference(sat_conversion,[],[f692]) ).
cnf(s66,plain,
( ~ spl0_60
| ~ spl0_99 ),
inference(sat_conversion,[],[f696]) ).
cnf(s71,plain,
( ~ spl0_82
| ~ spl0_104 ),
inference(sat_conversion,[],[f719]) ).
cnf(s72,plain,
( ~ spl0_74
| ~ spl0_105 ),
inference(sat_conversion,[],[f724]) ).
cnf(s73,plain,
( ~ spl0_38
| ~ spl0_106 ),
inference(sat_conversion,[],[f729]) ).
cnf(s74,plain,
( ~ spl0_56
| ~ spl0_107 ),
inference(sat_conversion,[],[f734]) ).
cnf(s75,plain,
( ~ spl0_56
| ~ spl0_108 ),
inference(sat_conversion,[],[f738]) ).
cnf(s76,plain,
( ~ spl0_56
| ~ spl0_109 ),
inference(sat_conversion,[],[f742]) ).
cnf(s80,plain,
( ~ spl0_53
| ~ spl0_113 ),
inference(sat_conversion,[],[f760]) ).
cnf(s81,plain,
( ~ spl0_53
| ~ spl0_114 ),
inference(sat_conversion,[],[f764]) ).
cnf(s82,plain,
( ~ spl0_52
| ~ spl0_115 ),
inference(sat_conversion,[],[f769]) ).
cnf(s83,plain,
( ~ spl0_52
| ~ spl0_116 ),
inference(sat_conversion,[],[f773]) ).
cnf(s84,plain,
( ~ spl0_52
| ~ spl0_117 ),
inference(sat_conversion,[],[f777]) ).
cnf(s85,plain,
( ~ spl0_33
| ~ spl0_118 ),
inference(sat_conversion,[],[f782]) ).
cnf(s86,plain,
( ~ spl0_65
| ~ spl0_119 ),
inference(sat_conversion,[],[f787]) ).
cnf(s87,plain,
( ~ spl0_65
| ~ spl0_120 ),
inference(sat_conversion,[],[f791]) ).
cnf(s98,plain,
( ~ spl0_51
| ~ spl0_133 ),
inference(sat_conversion,[],[f845]) ).
cnf(s99,plain,
( ~ spl0_50
| ~ spl0_134 ),
inference(sat_conversion,[],[f850]) ).
cnf(s100,plain,
( ~ spl0_50
| ~ spl0_135 ),
inference(sat_conversion,[],[f854]) ).
cnf(s101,plain,
( ~ spl0_68
| ~ spl0_136 ),
inference(sat_conversion,[],[f859]) ).
cnf(s102,plain,
( ~ spl0_68
| ~ spl0_137 ),
inference(sat_conversion,[],[f863]) ).
cnf(s103,plain,
( ~ spl0_63
| ~ spl0_138 ),
inference(sat_conversion,[],[f868]) ).
cnf(s104,plain,
( ~ spl0_63
| ~ spl0_139 ),
inference(sat_conversion,[],[f872]) ).
cnf(s110,plain,
( ~ spl0_61
| ~ spl0_147 ),
inference(sat_conversion,[],[f903]) ).
cnf(s111,plain,
( ~ spl0_61
| ~ spl0_148 ),
inference(sat_conversion,[],[f907]) ).
cnf(s112,plain,
( ~ spl0_61
| ~ spl0_149 ),
inference(sat_conversion,[],[f911]) ).
cnf(s119,plain,
( ~ spl0_156
| ~ spl0_157 ),
inference(sat_conversion,[],[f945]) ).
cnf(s122,plain,
( ~ spl0_22
| ~ spl0_161 ),
inference(sat_conversion,[],[f961]) ).
cnf(s124,plain,
( ~ spl0_46
| ~ spl0_163 ),
inference(sat_conversion,[],[f971]) ).
cnf(s126,plain,
( ~ spl0_26
| ~ spl0_165 ),
inference(sat_conversion,[],[f981]) ).
cnf(s127,plain,
( ~ spl0_44
| ~ spl0_166 ),
inference(sat_conversion,[],[f986]) ).
cnf(s128,plain,
( ~ spl0_44
| ~ spl0_167 ),
inference(sat_conversion,[],[f990]) ).
cnf(s129,plain,
( ~ spl0_57
| ~ spl0_168 ),
inference(sat_conversion,[],[f995]) ).
cnf(s130,plain,
( ~ spl0_57
| ~ spl0_169 ),
inference(sat_conversion,[],[f999]) ).
cnf(s140,plain,
( ~ spl0_67
| ~ spl0_179 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s141,plain,
( ~ spl0_67
| ~ spl0_180 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s142,plain,
( ~ spl0_66
| ~ spl0_181 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s143,plain,
( ~ spl0_64
| ~ spl0_182 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s144,plain,
( ~ spl0_29
| ~ spl0_183 ),
inference(sat_conversion,[],[f1066]) ).
cnf(s145,plain,
( ~ spl0_40
| ~ spl0_184 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s147,plain,
( ~ spl0_49
| ~ spl0_186 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s148,plain,
( ~ spl0_49
| ~ spl0_187 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s150,plain,
( ~ spl0_190
| ~ spl0_191 ),
inference(sat_conversion,[],[f1099]) ).
cnf(s151,plain,
( ~ spl0_192
| ~ spl0_193 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s152,plain,
( ~ spl0_192
| ~ spl0_194 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s156,plain,
( ~ spl0_198
| ~ spl0_199 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s157,plain,
( ~ spl0_200
| ~ spl0_201 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s158,plain,
( ~ spl0_202
| ~ spl0_203 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s159,plain,
( ~ spl0_77
| spl0_204 ),
inference(sat_conversion,[],[f1149]) ).
cnf(s160,plain,
( ~ spl0_76
| spl0_205 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s161,plain,
( ~ spl0_76
| spl0_206 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s163,plain,
( ~ spl0_62
| spl0_208 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s164,plain,
( ~ spl0_30
| spl0_209 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s165,plain,
( ~ spl0_60
| spl0_210 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s168,plain,
( ~ spl0_82
| spl0_213 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s169,plain,
( ~ spl0_82
| spl0_214 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s170,plain,
( ~ spl0_74
| spl0_215 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s171,plain,
( ~ spl0_74
| spl0_216 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s172,plain,
( ~ spl0_38
| spl0_217 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s173,plain,
( ~ spl0_38
| spl0_218 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s174,plain,
( ~ spl0_53
| spl0_219 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s175,plain,
( ~ spl0_33
| spl0_220 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s176,plain,
( ~ spl0_33
| spl0_221 ),
inference(sat_conversion,[],[f1217]) ).
cnf(s177,plain,
( ~ spl0_65
| spl0_222 ),
inference(sat_conversion,[],[f1221]) ).
cnf(s183,plain,
( ~ spl0_51
| spl0_228 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s184,plain,
( ~ spl0_51
| spl0_229 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s185,plain,
( ~ spl0_50
| spl0_230 ),
inference(sat_conversion,[],[f1253]) ).
cnf(s186,plain,
( ~ spl0_68
| spl0_231 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s187,plain,
( ~ spl0_63
| spl0_232 ),
inference(sat_conversion,[],[f1261]) ).
cnf(s192,plain,
( ~ spl0_156
| spl0_237 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s193,plain,
( ~ spl0_156
| spl0_238 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s196,plain,
( ~ spl0_22
| spl0_241 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s199,plain,
( ~ spl0_46
| spl0_244 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s200,plain,
( ~ spl0_46
| spl0_245 ),
inference(sat_conversion,[],[f1313]) ).
cnf(s201,plain,
( ~ spl0_45
| spl0_246 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s202,plain,
( ~ spl0_45
| spl0_247 ),
inference(sat_conversion,[],[f1322]) ).
cnf(s203,plain,
( ~ spl0_45
| spl0_248 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s206,plain,
( ~ spl0_75
| spl0_251 ),
inference(sat_conversion,[],[f1339]) ).
cnf(s207,plain,
( ~ spl0_75
| spl0_252 ),
inference(sat_conversion,[],[f1343]) ).
cnf(s208,plain,
( ~ spl0_75
| spl0_253 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s209,plain,
( ~ spl0_26
| spl0_254 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s210,plain,
( ~ spl0_26
| spl0_255 ),
inference(sat_conversion,[],[f1355]) ).
cnf(s211,plain,
( ~ spl0_44
| spl0_256 ),
inference(sat_conversion,[],[f1359]) ).
cnf(s212,plain,
( ~ spl0_57
| spl0_257 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s228,plain,
( ~ spl0_67
| spl0_273 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s229,plain,
( ~ spl0_66
| spl0_274 ),
inference(sat_conversion,[],[f1432]) ).
cnf(s230,plain,
( ~ spl0_66
| spl0_275 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s231,plain,
( ~ spl0_64
| spl0_276 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s232,plain,
( ~ spl0_64
| spl0_277 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s233,plain,
( ~ spl0_29
| spl0_278 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s234,plain,
( ~ spl0_29
| spl0_279 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s235,plain,
( ~ spl0_40
| spl0_280 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s236,plain,
( ~ spl0_40
| spl0_281 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s239,plain,
( ~ spl0_49
| spl0_284 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s242,plain,
( ~ spl0_190
| spl0_287 ),
inference(sat_conversion,[],[f1484]) ).
cnf(s243,plain,
( ~ spl0_190
| spl0_288 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s244,plain,
( ~ spl0_192
| spl0_289 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s248,plain,
( ~ spl0_198
| spl0_293 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s249,plain,
( ~ spl0_198
| spl0_294 ),
inference(sat_conversion,[],[f1512]) ).
cnf(s250,plain,
( ~ spl0_200
| spl0_295 ),
inference(sat_conversion,[],[f1516]) ).
cnf(s251,plain,
( ~ spl0_200
| spl0_296 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s252,plain,
( ~ spl0_202
| spl0_297 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s253,plain,
( ~ spl0_202
| spl0_298 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s254,plain,
( spl0_198
| spl0_200
| spl0_202 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s255,plain,
( spl0_156
| spl0_190
| spl0_192 ),
inference(sat_conversion,[],[f1536]) ).
cnf(s258,plain,
( spl0_33
| spl0_65
| spl0_82 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s325,plain,
( spl0_3
| ~ spl0_198 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s326,plain,
( spl0_3
| ~ spl0_200 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s327,plain,
( spl0_3
| ~ spl0_202 ),
inference(sat_conversion,[],[f1616]) ).
cnf(s338,plain,
( ~ spl0_8
| ~ spl0_16
| spl0_41 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s355,plain,
( ~ spl0_14
| spl0_166
| spl0_167
| spl0_308 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s357,plain,
( ~ spl0_18
| spl0_115
| spl0_116
| spl0_117 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s366,plain,
( ~ spl0_8
| ~ spl0_19
| spl0_41 ),
inference(sat_conversion,[],[f1818]) ).
cnf(s377,plain,
( spl0_5
| ~ spl0_15
| ~ spl0_27 ),
inference(sat_conversion,[],[f1874]) ).
cnf(s392,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_21 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s395,plain,
( spl0_5
| ~ spl0_15
| ~ spl0_28 ),
inference(sat_conversion,[],[f1962]) ).
cnf(s397,plain,
( ~ spl0_17
| spl0_186
| spl0_187
| ~ spl0_284 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s398,plain,
( ~ spl0_17
| spl0_139
| ~ spl0_232
| spl0_306 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s421,plain,
( ~ spl0_5
| spl0_138
| ~ spl0_232
| ~ spl0_306 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s422,plain,
( ~ spl0_5
| spl0_157
| ~ spl0_237
| ~ spl0_238 ),
inference(sat_conversion,[],[f2058]) ).
cnf(s423,plain,
( ~ spl0_5
| spl0_181
| ~ spl0_274
| ~ spl0_275 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s468,plain,
( ~ spl0_17
| ~ spl0_28
| spl0_34 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s476,plain,
( ~ spl0_12
| spl0_201
| ~ spl0_295
| ~ spl0_296 ),
inference(sat_conversion,[],[f2158]) ).
cnf(s494,plain,
( ~ spl0_17
| spl0_193
| spl0_194
| ~ spl0_316 ),
inference(sat_conversion,[],[f2224]) ).
cnf(s500,plain,
( ~ spl0_13
| spl0_179
| spl0_180
| ~ spl0_273 ),
inference(sat_conversion,[],[f2251]) ).
cnf(s506,plain,
( ~ spl0_34
| spl0_136
| spl0_137
| ~ spl0_231 ),
inference(sat_conversion,[],[f2271]) ).
cnf(s510,plain,
( ~ spl0_32
| spl0_85
| ~ spl0_204
| spl0_307 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s516,plain,
( ~ spl0_36
| spl0_166
| spl0_167
| ~ spl0_256 ),
inference(sat_conversion,[],[f2303]) ).
cnf(s521,plain,
( ~ spl0_39
| spl0_179
| spl0_180
| spl0_322 ),
inference(sat_conversion,[],[f2322]) ).
cnf(s523,plain,
( ~ spl0_41
| spl0_96
| spl0_97
| ~ spl0_209 ),
inference(sat_conversion,[],[f2345]) ).
cnf(s528,plain,
( spl0_6
| ~ spl0_8
| ~ spl0_17 ),
inference(sat_conversion,[],[f2351]) ).
cnf(s529,plain,
( ~ spl0_11
| spl0_113
| spl0_114
| ~ spl0_219 ),
inference(sat_conversion,[],[f2352]) ).
cnf(s532,plain,
( ~ spl0_17
| spl0_165
| ~ spl0_254
| spl0_299 ),
inference(sat_conversion,[],[f2355]) ).
cnf(s552,plain,
( spl0_4
| ~ spl0_12
| ~ spl0_21 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s553,plain,
( ~ spl0_6
| ~ spl0_254
| ~ spl0_255
| spl0_299 ),
inference(sat_conversion,[],[f2376]) ).
cnf(s585,plain,
( ~ spl0_13
| spl0_168
| ~ spl0_257
| spl0_326 ),
inference(sat_conversion,[],[f2452]) ).
cnf(s594,plain,
( ~ spl0_2
| spl0_104
| ~ spl0_213
| ~ spl0_301 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s606,plain,
( ~ spl0_2
| ~ spl0_251
| ~ spl0_253
| spl0_318 ),
inference(sat_conversion,[],[f2529]) ).
cnf(s608,plain,
( ~ spl0_8
| ~ spl0_213
| ~ spl0_214
| spl0_301 ),
inference(sat_conversion,[],[f2531]) ).
cnf(s623,plain,
( ~ spl0_6
| spl0_99
| ~ spl0_210
| ~ spl0_323 ),
inference(sat_conversion,[],[f2604]) ).
cnf(s624,plain,
( ~ spl0_6
| spl0_133
| ~ spl0_228
| ~ spl0_229 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s627,plain,
( ~ spl0_6
| spl0_182
| ~ spl0_276
| ~ spl0_277 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s629,plain,
( ~ spl0_6
| spl0_193
| ~ spl0_289
| ~ spl0_316 ),
inference(sat_conversion,[],[f2618]) ).
cnf(s632,plain,
( ~ spl0_10
| spl0_194
| ~ spl0_289
| ~ spl0_316 ),
inference(sat_conversion,[],[f2621]) ).
cnf(s638,plain,
( ~ spl0_27
| spl0_32
| ~ spl0_39 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s659,plain,
( ~ spl0_10
| spl0_165
| ~ spl0_254
| ~ spl0_255 ),
inference(sat_conversion,[],[f2648]) ).
cnf(s678,plain,
( ~ spl0_13
| spl0_91
| ~ spl0_208
| spl0_303 ),
inference(sat_conversion,[],[f2666]) ).
cnf(s703,plain,
( ~ spl0_6
| ~ spl0_280
| ~ spl0_281
| spl0_332 ),
inference(sat_conversion,[],[f2722]) ).
cnf(s707,plain,
( ~ spl0_1
| ~ spl0_251
| ~ spl0_252
| ~ spl0_253 ),
inference(sat_conversion,[],[f2744]) ).
cnf(s716,plain,
( spl0_5
| ~ spl0_13
| ~ spl0_21 ),
inference(sat_conversion,[],[f2775]) ).
cnf(s717,plain,
( ~ spl0_21
| ~ spl0_251
| ~ spl0_252
| ~ spl0_318 ),
inference(sat_conversion,[],[f2776]) ).
cnf(s728,plain,
( ~ spl0_9
| spl0_98
| spl0_99
| ~ spl0_210 ),
inference(sat_conversion,[],[f2819]) ).
cnf(s732,plain,
( ~ spl0_9
| spl0_184
| ~ spl0_281
| spl0_332 ),
inference(sat_conversion,[],[f2828]) ).
cnf(s733,plain,
( ~ spl0_9
| spl0_193
| spl0_194
| ~ spl0_289 ),
inference(sat_conversion,[],[f2829]) ).
cnf(s737,plain,
( ~ spl0_10
| spl0_186
| ~ spl0_284
| ~ spl0_302 ),
inference(sat_conversion,[],[f2833]) ).
cnf(s745,plain,
( ~ spl0_2
| spl0_118
| ~ spl0_220
| ~ spl0_221 ),
inference(sat_conversion,[],[f2859]) ).
cnf(s747,plain,
( ~ spl0_2
| spl0_161
| ~ spl0_241
| ~ spl0_338 ),
inference(sat_conversion,[],[f2863]) ).
cnf(s752,plain,
( ~ spl0_10
| spl0_98
| ~ spl0_210
| ~ spl0_323 ),
inference(sat_conversion,[],[f2886]) ).
cnf(s754,plain,
( ~ spl0_10
| spl0_184
| ~ spl0_280
| ~ spl0_281 ),
inference(sat_conversion,[],[f2888]) ).
cnf(s767,plain,
( ~ spl0_13
| spl0_32
| ~ spl0_36 ),
inference(sat_conversion,[],[f2905]) ).
cnf(s768,plain,
( ~ spl0_36
| spl0_191
| ~ spl0_287
| spl0_317 ),
inference(sat_conversion,[],[f2906]) ).
cnf(s776,plain,
( spl0_5
| ~ spl0_13
| ~ spl0_28 ),
inference(sat_conversion,[],[f2913]) ).
cnf(s789,plain,
( ~ spl0_5
| spl0_105
| ~ spl0_215
| ~ spl0_216 ),
inference(sat_conversion,[],[f2964]) ).
cnf(s791,plain,
( ~ spl0_5
| spl0_120
| ~ spl0_222
| ~ spl0_314 ),
inference(sat_conversion,[],[f2970]) ).
cnf(s792,plain,
( ~ spl0_5
| spl0_163
| ~ spl0_244
| ~ spl0_325 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s794,plain,
( ~ spl0_5
| spl0_191
| ~ spl0_288
| ~ spl0_317 ),
inference(sat_conversion,[],[f2973]) ).
cnf(s801,plain,
( ~ spl0_4
| ~ spl0_251
| ~ spl0_253
| ~ spl0_318 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s804,plain,
( ~ spl0_11
| spl0_119
| spl0_120
| ~ spl0_222 ),
inference(sat_conversion,[],[f2999]) ).
cnf(s807,plain,
( ~ spl0_17
| spl0_134
| spl0_135
| ~ spl0_230 ),
inference(sat_conversion,[],[f3003]) ).
cnf(s815,plain,
( ~ spl0_34
| spl0_120
| ~ spl0_222
| spl0_314 ),
inference(sat_conversion,[],[f3010]) ).
cnf(s824,plain,
( ~ spl0_12
| spl0_86
| ~ spl0_205
| ~ spl0_206 ),
inference(sat_conversion,[],[f3037]) ).
cnf(s837,plain,
( ~ spl0_16
| spl0_107
| spl0_108
| spl0_109 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s841,plain,
( ~ spl0_16
| spl0_147
| spl0_148
| spl0_149 ),
inference(sat_conversion,[],[f3096]) ).
cnf(s872,plain,
( ~ spl0_21
| ~ spl0_251
| ~ spl0_252
| ~ spl0_318 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s875,plain,
( ~ spl0_21
| ~ spl0_287
| ~ spl0_288
| ~ spl0_317 ),
inference(sat_conversion,[],[f3162]) ).
cnf(s880,plain,
( ~ spl0_28
| spl0_183
| ~ spl0_278
| ~ spl0_279 ),
inference(sat_conversion,[],[f3197]) ).
cnf(s890,plain,
( ~ spl0_32
| spl0_163
| ~ spl0_244
| spl0_325 ),
inference(sat_conversion,[],[f3224]) ).
cnf(s893,plain,
( ~ spl0_32
| spl0_191
| ~ spl0_288
| spl0_317 ),
inference(sat_conversion,[],[f3227]) ).
cnf(s926,plain,
( ~ spl0_12
| spl0_84
| ~ spl0_204
| ~ spl0_307 ),
inference(sat_conversion,[],[f3262]) ).
cnf(s927,plain,
( ~ spl0_12
| spl0_91
| ~ spl0_208
| ~ spl0_303 ),
inference(sat_conversion,[],[f3266]) ).
cnf(s928,plain,
( ~ spl0_16
| spl0_98
| spl0_99
| spl0_323 ),
inference(sat_conversion,[],[f3270]) ).
cnf(s935,plain,
( ~ spl0_12
| spl0_168
| ~ spl0_257
| ~ spl0_326 ),
inference(sat_conversion,[],[f3296]) ).
cnf(s936,plain,
( ~ spl0_5
| spl0_180
| ~ spl0_273
| ~ spl0_322 ),
inference(sat_conversion,[],[f3298]) ).
cnf(s941,plain,
( ~ spl0_4
| ~ spl0_280
| ~ spl0_281
| ~ spl0_332 ),
inference(sat_conversion,[],[f3314]) ).
cnf(s948,plain,
( ~ spl0_18
| spl0_119
| spl0_120
| spl0_314 ),
inference(sat_conversion,[],[f3352]) ).
cnf(s949,plain,
( ~ spl0_18
| spl0_186
| spl0_187
| spl0_302 ),
inference(sat_conversion,[],[f3353]) ).
cnf(s957,plain,
( ~ spl0_19
| spl0_98
| ~ spl0_210
| spl0_323 ),
inference(sat_conversion,[],[f3372]) ).
cnf(s958,plain,
( ~ spl0_19
| spl0_168
| spl0_169
| ~ spl0_326 ),
inference(sat_conversion,[],[f3373]) ).
cnf(s959,plain,
( ~ spl0_19
| spl0_194
| ~ spl0_289
| spl0_316 ),
inference(sat_conversion,[],[f3374]) ).
cnf(s968,plain,
( ~ spl0_27
| spl0_163
| ~ spl0_244
| ~ spl0_245 ),
inference(sat_conversion,[],[f3423]) ).
cnf(s969,plain,
( ~ spl0_27
| spl0_167
| ~ spl0_256
| ~ spl0_308 ),
inference(sat_conversion,[],[f3424]) ).
cnf(s972,plain,
( ~ spl0_27
| spl0_191
| ~ spl0_287
| ~ spl0_288 ),
inference(sat_conversion,[],[f3428]) ).
cnf(s974,plain,
( ~ spl0_41
| spl0_99
| ~ spl0_210
| spl0_323 ),
inference(sat_conversion,[],[f3451]) ).
cnf(s975,plain,
( ~ spl0_41
| spl0_161
| ~ spl0_241
| spl0_338 ),
inference(sat_conversion,[],[f3452]) ).
cnf(s979,plain,
( ~ spl0_41
| spl0_193
| ~ spl0_289
| spl0_316 ),
inference(sat_conversion,[],[f3457]) ).
cnf(s986,plain,
( ~ spl0_27
| ~ spl0_246
| ~ spl0_248
| spl0_342 ),
inference(sat_conversion,[],[f3492]) ).
cnf(s998,plain,
( ~ spl0_5
| spl0_203
| ~ spl0_297
| ~ spl0_320 ),
inference(sat_conversion,[],[f3511]) ).
cnf(s999,plain,
( ~ spl0_27
| spl0_106
| ~ spl0_217
| ~ spl0_218 ),
inference(sat_conversion,[],[f3514]) ).
cnf(s1009,plain,
( ~ spl0_24
| ~ spl0_247
| ~ spl0_248
| ~ spl0_342 ),
inference(sat_conversion,[],[f3547]) ).
cnf(s1017,plain,
( ~ spl0_43
| spl0_199
| ~ spl0_293
| ~ spl0_294 ),
inference(sat_conversion,[],[f3574]) ).
cnf(s1018,plain,
( ~ spl0_43
| ~ spl0_297
| ~ spl0_298
| spl0_320 ),
inference(sat_conversion,[],[f3575]) ).
cnf(s1030,plain,
( ~ spl0_4
| ~ spl0_254
| ~ spl0_255
| ~ spl0_299 ),
inference(sat_conversion,[],[f3587]) ).
cnf(s1047,plain,
( spl0_2
| ~ spl0_7
| ~ spl0_12 ),
inference(sat_conversion,[],[f3627]) ).
cnf(s1048,plain,
spl0_3,
inference(rat,[],[s254,s325,s326,s327]) ).
cnf(s1049,plain,
( spl0_8
| ~ spl0_60 ),
inference(rat,[],[s752,s974,s3,s28,s728,s65,s66,s165,s1048]) ).
cnf(s1050,plain,
( ~ spl0_10
| spl0_17
| spl0_98
| spl0_99
| ~ spl0_210
| spl0_28 ),
inference(rat,[],[s659,s126,s209,s210,s15,s969,s355,s127,s128,s211,s29,s32,s928,s752,s1048]) ).
cnf(s1056,plain,
( ~ spl0_53
| ~ spl0_11 ),
inference(rat,[],[s529,s80,s81,s174]) ).
cnf(s1057,plain,
( ~ spl0_57
| ~ spl0_19
| ~ spl0_13 ),
inference(rat,[],[s585,s958,s129,s130,s212]) ).
cnf(s1058,plain,
( spl0_6
| spl0_5
| spl0_2 ),
inference(rat,[],[s837,s74,s75,s76,s38,s1057,s9,s357,s82,s83,s84,s36,s1056,s8,s1050,s528,s1049,s728,s65,s66,s165,s40,s716,s776,s4,s5,s1047,s2,s1048]) ).
cnf(s1059,plain,
( ~ spl0_26
| ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s553,s1030,s209,s210]) ).
cnf(s1060,plain,
( ~ spl0_60
| spl0_186
| spl0_187
| ~ spl0_284
| ~ spl0_6 ),
inference(rat,[],[s8,s737,s949,s9,s928,s957,s728,s623,s65,s66,s165,s397,s1048]) ).
cnf(s1061,plain,
( spl0_5
| ~ spl0_4
| spl0_2 ),
inference(rat,[],[s703,s941,s235,s236,s23,s516,s127,s128,s211,s26,s392,s716,s40,s1060,s397,s147,s148,s239,s34,s1059,s1058,s1048]) ).
cnf(s1062,plain,
( ~ spl0_56
| ~ spl0_16 ),
inference(rat,[],[s837,s74,s75,s76]) ).
cnf(s1063,plain,
( ~ spl0_29
| ~ spl0_28 ),
inference(rat,[],[s880,s144,s233,s234]) ).
cnf(s1066,plain,
( ~ spl0_66
| ~ spl0_5 ),
inference(rat,[],[s423,s142,s229,s230]) ).
cnf(s1067,plain,
( ~ spl0_65
| ~ spl0_11 ),
inference(rat,[],[s804,s86,s87,s177]) ).
cnf(s1069,plain,
( ~ spl0_26
| ~ spl0_17
| ~ spl0_4 ),
inference(rat,[],[s532,s1030,s126,s209,s210]) ).
cnf(s1077,plain,
( ~ spl0_74
| ~ spl0_5 ),
inference(rat,[],[s789,s72,s170,s171]) ).
cnf(s1087,plain,
( ~ spl0_192
| ~ spl0_9 ),
inference(rat,[],[s733,s151,s152,s244]) ).
cnf(s1088,plain,
( ~ spl0_190
| ~ spl0_36
| ~ spl0_21 ),
inference(rat,[],[s768,s875,s150,s242,s243]) ).
cnf(s1089,plain,
( ~ spl0_156
| ~ spl0_5 ),
inference(rat,[],[s422,s119,s192,s193]) ).
cnf(s1090,plain,
( ~ spl0_192
| ~ spl0_41
| ~ spl0_17 ),
inference(rat,[],[s494,s979,s151,s152,s244]) ).
cnf(s1093,plain,
( ~ spl0_68
| ~ spl0_34 ),
inference(rat,[],[s506,s101,s102,s186]) ).
cnf(s1094,plain,
( ~ spl0_67
| ~ spl0_13 ),
inference(rat,[],[s500,s140,s141,s228]) ).
cnf(s1095,plain,
( ~ spl0_17
| ~ spl0_28
| spl0_6
| spl0_67
| spl0_156 ),
inference(rat,[],[s893,s875,s150,s242,s243,s255,s45,s40,s1090,s1093,s1049,s28,s468,s528,s1048]) ).
cnf(s1098,plain,
( spl0_8
| ~ spl0_36
| ~ spl0_41
| spl0_156 ),
inference(rat,[],[s632,s3,s979,s1087,s151,s152,s244,s255,s1088,s40,s1049,s1048]) ).
cnf(s1103,plain,
( ~ spl0_30
| ~ spl0_41 ),
inference(rat,[],[s523,s63,s64,s164]) ).
cnf(s1104,plain,
( ~ spl0_45
| ~ spl0_24
| ~ spl0_27 ),
inference(rat,[],[s986,s1009,s201,s202,s203]) ).
cnf(s1106,plain,
( ~ spl0_62
| ~ spl0_12
| ~ spl0_13 ),
inference(rat,[],[s927,s678,s59,s163]) ).
cnf(s1107,plain,
( ~ spl0_28
| spl0_6
| ~ spl0_13
| ~ spl0_5 ),
inference(rat,[],[s355,s969,s127,s128,s211,s29,s32,s841,s110,s111,s112,s41,s1106,s17,s1103,s815,s24,s4,s791,s1067,s87,s177,s44,s1095,s1063,s1066,s1089,s1094,s1048]) ).
cnf(s1108,plain,
( ~ spl0_17
| spl0_28
| spl0_6
| spl0_156
| ~ spl0_4 ),
inference(rat,[],[s972,s150,s242,s243,s255,s1090,s15,s28,s1069,s528,s1048]) ).
cnf(s1109,plain,
( spl0_6
| ~ spl0_13
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s754,s145,s235,s236,s23,s516,s127,s128,s211,s29,s8,s841,s110,s111,s112,s41,s1106,s815,s4,s791,s1067,s87,s177,s44,s1108,s1107,s1066,s1089,s1048]) ).
cnf(s1110,plain,
( ~ spl0_190
| ~ spl0_32
| ~ spl0_5 ),
inference(rat,[],[s893,s794,s150,s243]) ).
cnf(s1112,plain,
( ~ spl0_190
| ~ spl0_17
| spl0_26
| spl0_67
| ~ spl0_5 ),
inference(rat,[],[s468,s1093,s15,s45,s972,s1110,s150,s242,s243,s1048]) ).
cnf(s1117,plain,
( ~ spl0_51
| ~ spl0_6 ),
inference(rat,[],[s624,s98,s183,s184]) ).
cnf(s1118,plain,
( ~ spl0_50
| ~ spl0_17 ),
inference(rat,[],[s807,s99,s100,s185]) ).
cnf(s1129,plain,
( ~ spl0_64
| ~ spl0_6 ),
inference(rat,[],[s627,s143,s231,s232]) ).
cnf(s1130,plain,
( ~ spl0_17
| spl0_64
| spl0_26
| spl0_67
| ~ spl0_5 ),
inference(rat,[],[s1093,s468,s45,s15,s890,s968,s792,s124,s199,s200,s43,s1090,s255,s1112,s1089,s1048]) ).
cnf(s1131,plain,
( ~ spl0_192
| spl0_18
| ~ spl0_6 ),
inference(rat,[],[s959,s9,s629,s1087,s151,s152,s244,s1048]) ).
cnf(s1132,plain,
( ~ spl0_13
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s24,s1103,s1063,s17,s15,s972,s150,s242,s243,s255,s1131,s948,s791,s1067,s86,s87,s177,s44,s1130,s1129,s1059,s1109,s1094,s1066,s1089,s1048]) ).
cnf(s1133,plain,
( ~ spl0_63
| ~ spl0_17
| ~ spl0_5 ),
inference(rat,[],[s398,s421,s103,s104,s187]) ).
cnf(s1134,plain,
( ~ spl0_17
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s972,s150,s242,s243,s255,s1090,s30,s521,s936,s140,s141,s228,s1130,s1129,s15,s1108,s1063,s42,s1133,s1069,s1089,s1132,s1048]) ).
cnf(s1135,plain,
( ~ spl0_61
| ~ spl0_16 ),
inference(rat,[],[s841,s110,s111,s112]) ).
cnf(s1136,plain,
( ~ spl0_77
| ~ spl0_32
| ~ spl0_12 ),
inference(rat,[],[s926,s510,s53,s54,s159]) ).
cnf(s1137,plain,
( ~ spl0_76
| ~ spl0_12 ),
inference(rat,[],[s824,s55,s160,s161]) ).
cnf(s1140,plain,
( ~ spl0_200
| ~ spl0_12 ),
inference(rat,[],[s476,s157,s250,s251]) ).
cnf(s1141,plain,
( ~ spl0_198
| ~ spl0_43 ),
inference(rat,[],[s1017,s156,s248,s249]) ).
cnf(s1142,plain,
( ~ spl0_43
| spl0_200
| ~ spl0_5 ),
inference(rat,[],[s998,s1018,s158,s252,s253,s254,s1141]) ).
cnf(s1143,plain,
( ~ spl0_4
| spl0_2 ),
inference(rat,[],[s999,s73,s172,s173,s22,s1104,s27,s1142,s1140,s638,s1136,s49,s1137,s17,s1103,s366,s5,s3,s9,s703,s732,s754,s941,s145,s235,s236,s23,s948,s516,s791,s127,s128,s211,s1067,s86,s87,s177,s26,s44,s1134,s1132,s1066,s1061,s1048]) ).
cnf(s1144,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s1143,s1,s1048]) ).
cnf(s1145,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s606,s801,s206,s208,s48,s516,s127,s128,s211,s26,s1134,s1132,s1077,s1048]) ).
cnf(s1146,plain,
( spl0_17
| spl0_13
| ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s968,s124,s199,s200,s17,s31,s1103,s338,s1049,s40,s8,s872,s754,s606,s145,s235,s236,s206,s207,s208,s23,s48,s516,s127,s128,s211,s1067,s26,s44,s1066,s1077,s1145,s1048]) ).
cnf(s1147,plain,
( spl0_6
| ~ spl0_17
| spl0_13
| spl0_4 ),
inference(rat,[],[s40,s1049,s552,s528,s5,s1048]) ).
cnf(s1148,plain,
( ~ spl0_26
| ~ spl0_10 ),
inference(rat,[],[s659,s126,s209,s210]) ).
cnf(s1149,plain,
( spl0_13
| ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s972,s150,s242,s243,s255,s1090,s30,s521,s936,s140,s141,s228,s1130,s15,s1148,s35,s1129,s1117,s1147,s1063,s42,s1133,s1118,s1146,s1089,s1145,s1048]) ).
cnf(s1150,plain,
( spl0_6
| spl0_17
| ~ spl0_13
| spl0_4
| ~ spl0_5 ),
inference(rat,[],[s8,s1050,s1135,s65,s66,s165,s41,s40,s1106,s552,s4,s1107,s1067,s815,s791,s177,s87,s44,s1066,s1048]) ).
cnf(s1151,plain,
( spl0_17
| ~ spl0_13
| spl0_4
| ~ spl0_5 ),
inference(rat,[],[s8,s338,s754,s28,s145,s235,s236,s1103,s23,s17,s767,s972,s1110,s150,s242,s243,s255,s1131,s1150,s948,s791,s1067,s86,s87,s177,s44,s1066,s1089,s1048]) ).
cnf(s1152,plain,
( spl0_8
| ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s717,s606,s206,s207,s208,s48,s40,s1098,s1049,s28,s1077,s1089,s1048]) ).
cnf(s1153,plain,
( ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s1148,s1130,s35,s1129,s1117,s528,s1152,s1118,s1151,s1094,s1149,s1145,s1048]) ).
cnf(s1154,plain,
( ~ spl0_27
| ~ spl0_44
| spl0_5 ),
inference(rat,[],[s355,s7,s969,s377,s211,s128,s127,s1048]) ).
cnf(s1155,plain,
( ~ spl0_33
| ~ spl0_2 ),
inference(rat,[],[s745,s85,s175,s176]) ).
cnf(s1156,plain,
( spl0_11
| spl0_36
| spl0_27
| spl0_17 ),
inference(rat,[],[s338,s8,s28,s754,s1103,s145,s235,s236,s17,s23,s1048]) ).
cnf(s1157,plain,
( ~ spl0_11
| ~ spl0_2 ),
inference(rat,[],[s594,s608,s71,s168,s169,s1049,s258,s40,s1067,s392,s1153,s1155,s1048]) ).
cnf(s1158,plain,
( spl0_17
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s1156,s516,s1154,s127,s128,s211,s26,s1153,s1157,s1048]) ).
cnf(s1159,plain,
( ~ spl0_17
| ~ spl0_4
| spl0_5 ),
inference(rat,[],[s397,s147,s148,s239,s34,s1069,s1048]) ).
cnf(s1160,plain,
( spl0_17
| ~ spl0_2 ),
inference(rat,[],[s935,s585,s4,s129,s212,s623,s38,s928,s1062,s8,s1050,s65,s66,s165,s40,s716,s776,s1158,s1153,s1157,s1048]) ).
cnf(s1161,plain,
~ spl0_2,
inference(rat,[],[s968,s15,s124,s199,s200,s1148,s43,s35,s1129,s1117,s1063,s528,s24,s28,s975,s747,s122,s196,s11,s1159,s1118,s1160,s1157,s1153,s1048]) ).
cnf(s1162,plain,
spl0_1,
inference(rat,[],[s1144,s1161]) ).
cnf(s1163,plain,
~ spl0_4,
inference(rat,[],[s1143,s1161]) ).
cnf(s1164,plain,
~ spl0_75,
inference(rat,[],[s707,s206,s207,s208,s1162]) ).
cnf(s1165,plain,
( ~ spl0_44
| ~ spl0_36 ),
inference(rat,[],[s516,s127,s128,s211]) ).
cnf(s1166,plain,
( spl0_17
| ~ spl0_5 ),
inference(rat,[],[s26,s1151,s1165,s48,s1077,s1048,s1163,s1164]) ).
cnf(s1167,plain,
( spl0_13
| ~ spl0_5 ),
inference(rat,[],[s972,s150,s242,s243,s255,s1090,s30,s521,s936,s140,s141,s228,s15,s1130,s1148,s35,s1063,s1129,s1117,s42,s1147,s1089,s1118,s1133,s1166,s1048,s1163]) ).
cnf(s1168,plain,
~ spl0_5,
inference(rat,[],[s1148,s1130,s35,s1129,s1117,s528,s28,s1090,s255,s1110,s767,s1094,s1167,s1118,s1166,s48,s1089,s1077,s1048,s1164]) ).
cnf(s1169,plain,
spl0_6,
inference(rat,[],[s1058,s1161,s1168]) ).
cnf(s1171,plain,
~ spl0_51,
inference(rat,[],[s1117,s1169]) ).
cnf(s1177,plain,
( ~ spl0_28
| spl0_17 ),
inference(rat,[],[s16,s1063,s395,s1048,s1168]) ).
cnf(s1178,plain,
( ~ spl0_44
| spl0_17 ),
inference(rat,[],[s928,s623,s65,s66,s165,s40,s8,s392,s1148,s1156,s15,s1165,s1154,s1177,s1169,s1048,s1168]) ).
cnf(s1179,plain,
( spl0_44
| spl0_17 ),
inference(rat,[],[s928,s623,s65,s66,s165,s40,s716,s29,s26,s1168,s1048,s1169]) ).
cnf(s1180,plain,
spl0_17,
inference(rat,[],[s1179,s1178]) ).
cnf(s1181,plain,
~ spl0_50,
inference(rat,[],[s1118,s1180]) ).
cnf(s1182,plain,
spl0_10,
inference(rat,[],[s35,s1171,s1048,s1181]) ).
cnf(s1183,plain,
~ spl0_26,
inference(rat,[],[s1148,s1182]) ).
cnf(s1184,plain,
spl0_49,
inference(rat,[],[s34,s1168,s1048,s1183]) ).
cnf(s1185,plain,
spl0_284,
inference(rat,[],[s239,s1184]) ).
cnf(s1186,plain,
~ spl0_187,
inference(rat,[],[s148,s1184]) ).
cnf(s1187,plain,
~ spl0_186,
inference(rat,[],[s147,s1184]) ).
cnf(s1188,plain,
$false,
inference(rat,[],[s397,s1187,s1180,s1185,s1186]) ).
fof(f3628,plain,
$false,
inference(avatar_sat_refutation,[],[s1188]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN440-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:06:03 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.65/0.99 % (3735388)Input is clausal, will run a generic CNF schedule.
% 0.65/0.99 % (3735399)dis-21_1_sil=8000:lcm=predicate:random_seed=4169576483: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)
% 0.65/0.99 % (3735399)First to succeed.
% 0.65/0.99 % (3735399)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3735388"
% 0.65/0.99 % (3735397)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1143803150:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.65/0.99 % (3735394)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2920213042:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.65/0.99 % (3735395)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4220083922:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.65/0.99 % (3735393)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=1994675616:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.65/0.99 % (3735396)lrs+10_1_sil=8000:sp=occurrence:random_seed=509766489:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.65/0.99 % (3735398)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=566689505:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.65/0.99 % (3735396)Instruction limit reached!
% 0.65/0.99 % (3735396)------------------------------
% 0.65/0.99 % (3735396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.65/0.99 % (3735396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.99 % (3735396)CaDiCaL version: 2.1.3
% 0.65/0.99 % (3735396)Termination reason: Instruction limit
% 0.65/0.99 % (3735396)Termination phase: Saturation
% 0.65/0.99 % (3735396)Time elapsed: 0.069 s
% 0.65/0.99 % (3735396)Peak memory usage: 90 MB
% 0.65/0.99 % (3735396)Instructions burned: 107 (million)
% 0.65/0.99 % (3735397)Instruction limit reached!
% 0.65/0.99 % (3735397)------------------------------
% 0.65/0.99 % (3735397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.65/0.99 % (3735397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.99 % (3735397)CaDiCaL version: 2.1.3
% 0.65/0.99 % (3735397)Termination reason: Instruction limit
% 0.65/0.99 % (3735397)Termination phase: Saturation
% 0.65/0.99 % (3735397)Time elapsed: 0.075 s
% 0.65/0.99 % (3735397)Peak memory usage: 89 MB
% 0.65/0.99 % (3735397)Instructions burned: 114 (million)
% 0.65/0.99 % (3735398)Instruction limit reached!
% 0.65/0.99 % (3735398)------------------------------
% 0.65/0.99 % (3735398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.65/0.99 % (3735398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.99 % (3735398)CaDiCaL version: 2.1.3
% 0.65/0.99 % (3735398)Termination reason: Instruction limit
% 0.65/0.99 % (3735398)Termination phase: Saturation
% 0.65/0.99 % (3735398)Time elapsed: 0.116 s
% 0.65/0.99 % (3735398)Peak memory usage: 92 MB
% 0.65/0.99 % (3735398)Instructions burned: 181 (million)
% 0.65/0.99 % (3735399)Refutation found. Thanks to Tanya!
% 0.65/0.99 % SZS status Unsatisfiable for theBenchmark
% 0.65/0.99 % SZS output start Proof for theBenchmark
% See solution above
% 2.91/1.19 % (3735399)------------------------------
% 2.91/1.19 % (3735399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.91/1.19 % (3735399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.19 % (3735399)CaDiCaL version: 2.1.3
% 2.91/1.19 % (3735399)Termination reason: Refutation
% 2.91/1.19 % (3735399)Time elapsed: 0.032 s
% 2.91/1.19 % (3735399)Peak memory usage: 91 MB
% 2.91/1.19 % (3735399)Instructions burned: 92 (million)
% 2.91/1.19 % (3735399)------------------------------
% 2.91/1.19 % (3735399)------------------------------
% 2.91/1.19 % (3735388)Success in time 0.322 s
% 2.91/1.19 % Vampire exiting
%------------------------------------------------------------------------------