%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN460-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:52:50 PM UTC 2026
% Result : Unsatisfiable 3.27s 1.18s
% Output : Refutation 4.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 221
% Syntax : Number of formulae : 694 ( 19 unt; 126 def)
% Number of atoms : 2087 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2460 (1067 ~;1267 |; 0 &)
% ( 126 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 154 ( 153 usr; 150 prp; 0-1 aty)
% Number of functors : 22 ( 22 usr; 22 con; 0-0 aty)
% Number of variables : 115 ( 0 sgn 115 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,negated_conjecture,
( ~ hskp55
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
fof(f5,negated_conjecture,
( ~ hskp54
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
fof(f38,negated_conjecture,
( ~ hskp21
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f60,negated_conjecture,
( hskp29
| hskp30
| hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
fof(f64,negated_conjecture,
( hskp21
| hskp54
| hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp58
| c0_1(a2252) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
fof(f70,negated_conjecture,
( ~ hskp55
| c1_1(a2241) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp55
| c0_1(a2241) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp55
| c2_1(a2241) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp54
| c1_1(a2240) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp54
| c3_1(a2240) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp54
| c0_1(a2240) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
fof(f79,negated_conjecture,
( ~ hskp52
| c1_1(a2234) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp52
| c3_1(a2234) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp52
| c2_1(a2234) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f91,negated_conjecture,
( ~ hskp47
| c2_1(a2226) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp47
| c0_1(a2226) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f95,negated_conjecture,
( ~ hskp45
| c2_1(a2216) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ hskp45
| c3_1(a2216) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ hskp45
| c0_1(a2216) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f100,negated_conjecture,
( ~ hskp43
| c3_1(a2208) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ hskp43
| c0_1(a2208) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ hskp42
| c1_1(a2207) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ hskp42
| c0_1(a2207) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f106,negated_conjecture,
( ~ hskp40
| c2_1(a2204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ hskp40
| c3_1(a2204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f109,negated_conjecture,
( ~ hskp38
| c1_1(a2200) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f118,negated_conjecture,
( ~ hskp33
| c1_1(a2188) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ hskp32
| c0_1(a2186) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ hskp31
| c1_1(a2185) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ hskp31
| c3_1(a2185) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ hskp30
| c0_1(a2184) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ hskp29
| c2_1(a2183) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ hskp29
| c3_1(a2183) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f137,negated_conjecture,
( ~ hskp21
| c2_1(a2239) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f140,negated_conjecture,
( ~ hskp18
| c0_1(a2222) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
( ~ hskp18
| c3_1(a2222) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause141) ).
fof(f143,negated_conjecture,
( ~ hskp15
| c1_1(a2217) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause143) ).
fof(f155,negated_conjecture,
( ~ hskp2
| c3_1(a2187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
( ~ hskp2
| c1_1(a2187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause156) ).
fof(f158,negated_conjecture,
( ~ c2_1(a2252)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
( ~ c1_1(a2252)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause159) ).
fof(f165,negated_conjecture,
( ~ c1_1(a2226)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause165) ).
fof(f168,negated_conjecture,
( ~ c2_1(a2208)
| ~ hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
( ~ c3_1(a2207)
| ~ hskp42 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f171,negated_conjecture,
( ~ c1_1(a2204)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause171) ).
fof(f174,negated_conjecture,
( ~ c0_1(a2200)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
( ~ c2_1(a2200)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f180,negated_conjecture,
( ~ c3_1(a2188)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
( ~ c2_1(a2188)
| ~ hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
( ~ c3_1(a2186)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
( ~ c2_1(a2186)
| ~ hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
( ~ c2_1(a2185)
| ~ hskp31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
( ~ c3_1(a2184)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
( ~ c1_1(a2184)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
( ~ c0_1(a2183)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause187) ).
fof(f197,negated_conjecture,
( ~ c0_1(a2239)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause197) ).
fof(f198,negated_conjecture,
( ~ c3_1(a2239)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause198) ).
fof(f200,negated_conjecture,
( ~ c0_1(a2233)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
( ~ c1_1(a2233)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
( ~ c3_1(a2233)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
( ~ c2_1(a2222)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause203) ).
fof(f209,negated_conjecture,
( ~ c3_1(a2217)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause209) ).
fof(f210,negated_conjecture,
( ~ c0_1(a2217)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause210) ).
fof(f218,negated_conjecture,
( ~ c2_1(a2206)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ c0_1(a2206)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause219) ).
fof(f220,negated_conjecture,
( ~ c3_1(a2206)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause220) ).
fof(f236,negated_conjecture,
( ~ c2_1(a2187)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause236) ).
fof(f239,negated_conjecture,
( ~ c0_1(a2181)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause239) ).
fof(f240,negated_conjecture,
( ~ c1_1(a2181)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause240) ).
fof(f241,negated_conjecture,
( ~ c2_1(a2181)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause241) ).
fof(f243,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| hskp32
| hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause243) ).
fof(f244,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| hskp42
| hskp43 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause244) ).
fof(f245,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp18
| c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp58
| c1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause246) ).
fof(f253,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c0_1(X0)
| hskp19
| hskp52 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause253) ).
fof(f256,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause256) ).
fof(f258,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp45
| hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause258) ).
fof(f264,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| c2_1(X0)
| hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause264) ).
fof(f266,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause266) ).
fof(f269,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause269) ).
fof(f270,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp32 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause270) ).
fof(f281,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X0)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause281) ).
fof(f282,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| c0_1(X0)
| c2_1(X1)
| hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause282) ).
fof(f284,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X0)
| hskp33 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause284) ).
fof(f286,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| c1_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause286) ).
fof(f287,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X2)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause287) ).
fof(f288,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X2)
| c0_1(X0)
| c1_1(X0)
| c3_1(X1)
| c3_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause288) ).
fof(f289,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c1_1(X1)
| c0_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause289) ).
fof(f291,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X2)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause291) ).
fof(f292,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause292) ).
fof(f293,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X2)
| c2_1(X0)
| c2_1(X1)
| c2_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause293) ).
fof(f294,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X2)
| ~ c1_1(X2)
| c3_1(X0)
| c3_1(X1)
| c0_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause294) ).
fof(f295,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X2)
| c0_1(X1)
| c2_1(X1)
| c2_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause295) ).
fof(f296,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c0_1(X0)
| c3_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause296) ).
fof(f298,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f299,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f301,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f302,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f307,definition,
( spl0_4
<=> ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f308,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f309,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f296,f307,f304,f301,f298]) ).
fof(f311,definition,
( spl0_5
<=> ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f312,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f314,definition,
( spl0_6
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f315,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f316,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f295,f301,f304,f314,f311]) ).
fof(f318,definition,
( spl0_7
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f319,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f320,plain,
( spl0_4
| spl0_1
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f294,f318,f304,f298,f307]) ).
fof(f322,definition,
( spl0_8
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f323,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f325,definition,
( spl0_9
<=> ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f326,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f327,plain,
( spl0_6
| spl0_8
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f293,f325,f304,f322,f314]) ).
fof(f329,definition,
( spl0_10
<=> ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f330,plain,
( ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X2) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,definition,
( spl0_11
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f333,plain,
( ! [X1] :
( c1_1(X1)
| c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f335,definition,
( spl0_12
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f336,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( spl0_10
| spl0_11
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f292,f335,f304,f332,f329]) ).
fof(f339,definition,
( spl0_13
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f340,plain,
( ! [X1] :
( c1_1(X1)
| ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,definition,
( spl0_14
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f343,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f344,plain,
( spl0_12
| spl0_13
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f291,f342,f304,f339,f335]) ).
fof(f346,definition,
( spl0_15
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f347,plain,
( ! [X1] :
( c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f349,definition,
( spl0_16
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f350,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f352,plain,
( spl0_1
| spl0_13
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f289,f346,f304,f339,f298]) ).
fof(f354,definition,
( spl0_17
<=> ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f355,plain,
( ! [X2] :
( c1_1(X2)
| ~ c0_1(X2)
| c3_1(X2) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f356,plain,
( spl0_17
| spl0_14
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f288,f339,f304,f342,f354]) ).
fof(f358,definition,
( spl0_18
<=> ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f359,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f361,definition,
( spl0_19
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f362,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( spl0_18
| spl0_10
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f287,f361,f304,f329,f358]) ).
fof(f365,definition,
( spl0_20
<=> ! [X2] :
( c1_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f366,plain,
( ! [X2] :
( c1_1(X2)
| c3_1(X2)
| c2_1(X2) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f368,definition,
( spl0_21
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f369,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f371,definition,
( spl0_22
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f372,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f373,plain,
( spl0_20
| spl0_21
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f286,f371,f304,f368,f365]) ).
fof(f375,definition,
( spl0_23
<=> ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f376,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f379,definition,
( spl0_24
<=> hskp33 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f382,definition,
( spl0_25
<=> ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f383,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f385,definition,
( spl0_26
<=> ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f386,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f387,plain,
( spl0_24
| spl0_25
| ~ spl0_3
| spl0_26 ),
inference(avatar_split_clause,[],[f284,f385,f304,f382,f379]) ).
fof(f393,definition,
( spl0_28
<=> hskp40 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f396,definition,
( spl0_29
<=> ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f397,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f398,plain,
( spl0_28
| spl0_22
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f282,f396,f304,f371,f393]) ).
fof(f400,definition,
( spl0_30
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f402,plain,
( spl0_30
| spl0_9
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f281,f371,f304,f325,f400]) ).
fof(f447,definition,
( spl0_42
<=> hskp32 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f449,plain,
( spl0_42
| spl0_16
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f270,f332,f304,f349,f447]) ).
fof(f450,plain,
( spl0_24
| spl0_17
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f269,f314,f304,f354,f379]) ).
fof(f460,definition,
( spl0_45
<=> hskp38 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f462,plain,
( spl0_45
| spl0_18
| spl0_7
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f266,f304,f318,f358,f460]) ).
fof(f468,definition,
( spl0_47
<=> hskp47 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f470,plain,
( spl0_47
| spl0_20
| spl0_5
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f264,f304,f311,f365,f468]) ).
fof(f493,definition,
( spl0_54
<=> hskp31 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f496,definition,
( spl0_55
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f510,definition,
( spl0_59
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f513,definition,
( spl0_60
<=> hskp45 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f515,plain,
( spl0_59
| spl0_60
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f258,f346,f304,f513,f510]) ).
fof(f518,definition,
( spl0_61
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f520,plain,
( spl0_61
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f256,f329,f304,f518]) ).
fof(f533,definition,
( spl0_65
<=> hskp52 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f536,definition,
( spl0_66
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f538,plain,
( spl0_65
| spl0_66
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f253,f298,f304,f536,f533]) ).
fof(f570,definition,
( spl0_75
<=> hskp58 ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f572,plain,
( spl0_75
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f246,f332,f304,f570]) ).
fof(f573,plain,
( spl0_55
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f245,f361,f304,f496]) ).
fof(f575,definition,
( spl0_76
<=> hskp43 ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f578,definition,
( spl0_77
<=> hskp42 ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f580,plain,
( spl0_76
| spl0_77
| spl0_21
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f244,f304,f368,f578,f575]) ).
fof(f582,definition,
( spl0_78
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f584,plain,
( spl0_78
| spl0_42
| spl0_21
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f243,f304,f368,f447,f582]) ).
fof(f594,definition,
( spl0_81
<=> c2_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f596,plain,
( ~ spl0_61
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f241,f594,f518]) ).
fof(f598,definition,
( spl0_82
<=> c1_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f599,plain,
( ~ c1_1(a2181)
| spl0_82 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f600,plain,
( ~ spl0_61
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f240,f598,f518]) ).
fof(f602,definition,
( spl0_83
<=> c0_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f604,plain,
( ~ spl0_61
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f239,f602,f518]) ).
fof(f616,definition,
( spl0_86
<=> c2_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f618,plain,
( ~ spl0_78
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f236,f616,f582]) ).
fof(f692,definition,
( spl0_104
<=> c3_1(a2206) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f693,plain,
( ~ c3_1(a2206)
| spl0_104 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f694,plain,
( ~ spl0_30
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f220,f692,f400]) ).
fof(f696,definition,
( spl0_105
<=> c0_1(a2206) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f698,plain,
( ~ spl0_30
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f219,f696,f400]) ).
fof(f700,definition,
( spl0_106
<=> c2_1(a2206) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f702,plain,
( ~ spl0_30
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f218,f700,f400]) ).
fof(f741,definition,
( spl0_116
<=> c0_1(a2217) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f743,plain,
( ~ spl0_59
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f210,f741,f510]) ).
fof(f745,definition,
( spl0_117
<=> c3_1(a2217) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f746,plain,
( ~ c3_1(a2217)
| spl0_117 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f747,plain,
( ~ spl0_59
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f209,f745,f510]) ).
fof(f772,definition,
( spl0_123
<=> c2_1(a2222) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f774,plain,
( ~ spl0_55
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f203,f772,f496]) ).
fof(f777,definition,
( spl0_124
<=> c3_1(a2233) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f779,plain,
( ~ spl0_66
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f202,f777,f536]) ).
fof(f781,definition,
( spl0_125
<=> c1_1(a2233) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f782,plain,
( ~ c1_1(a2233)
| spl0_125 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f783,plain,
( ~ spl0_66
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f201,f781,f536]) ).
fof(f785,definition,
( spl0_126
<=> c0_1(a2233) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f787,plain,
( ~ spl0_66
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f200,f785,f536]) ).
fof(f794,definition,
( spl0_128
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f797,definition,
( spl0_129
<=> c3_1(a2239) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f798,plain,
( ~ c3_1(a2239)
| spl0_129 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f799,plain,
( ~ spl0_128
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f198,f797,f794]) ).
fof(f801,definition,
( spl0_130
<=> c0_1(a2239) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f803,plain,
( ~ spl0_128
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f197,f801,f794]) ).
fof(f847,definition,
( spl0_140
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f850,definition,
( spl0_141
<=> c0_1(a2183) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f852,plain,
( ~ spl0_140
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f187,f850,f847]) ).
fof(f854,definition,
( spl0_142
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f857,definition,
( spl0_143
<=> c1_1(a2184) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f858,plain,
( ~ c1_1(a2184)
| spl0_143 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f859,plain,
( ~ spl0_142
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f186,f857,f854]) ).
fof(f861,definition,
( spl0_144
<=> c3_1(a2184) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f862,plain,
( ~ c3_1(a2184)
| spl0_144 ),
inference(avatar_component_clause,[],[f861]) ).
fof(f863,plain,
( ~ spl0_142
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f185,f861,f854]) ).
fof(f866,definition,
( spl0_145
<=> c2_1(a2185) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f868,plain,
( ~ spl0_54
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f184,f866,f493]) ).
fof(f871,definition,
( spl0_146
<=> c2_1(a2186) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f873,plain,
( ~ spl0_42
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f183,f871,f447]) ).
fof(f875,definition,
( spl0_147
<=> c3_1(a2186) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f876,plain,
( ~ c3_1(a2186)
| spl0_147 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f877,plain,
( ~ spl0_42
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f182,f875,f447]) ).
fof(f880,definition,
( spl0_148
<=> c2_1(a2188) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f882,plain,
( ~ spl0_24
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f181,f880,f379]) ).
fof(f884,definition,
( spl0_149
<=> c3_1(a2188) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f886,plain,
( ~ spl0_24
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f180,f884,f379]) ).
fof(f913,definition,
( spl0_156
<=> c2_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f915,plain,
( ~ spl0_45
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f175,f913,f460]) ).
fof(f917,definition,
( spl0_157
<=> c0_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f919,plain,
( ~ spl0_45
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f174,f917,f460]) ).
fof(f931,definition,
( spl0_160
<=> c1_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f932,plain,
( ~ c1_1(a2204)
| spl0_160 ),
inference(avatar_component_clause,[],[f931]) ).
fof(f933,plain,
( ~ spl0_28
| ~ spl0_160 ),
inference(avatar_split_clause,[],[f171,f931,f393]) ).
fof(f941,definition,
( spl0_162
<=> c3_1(a2207) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f942,plain,
( ~ c3_1(a2207)
| spl0_162 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f943,plain,
( ~ spl0_77
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f169,f941,f578]) ).
fof(f946,definition,
( spl0_163
<=> c2_1(a2208) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f948,plain,
( ~ spl0_76
| ~ spl0_163 ),
inference(avatar_split_clause,[],[f168,f946,f575]) ).
fof(f961,definition,
( spl0_166
<=> c1_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f962,plain,
( ~ c1_1(a2226)
| spl0_166 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f963,plain,
( ~ spl0_47
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f165,f961,f468]) ).
fof(f990,definition,
( spl0_172
<=> c1_1(a2252) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f991,plain,
( ~ c1_1(a2252)
| spl0_172 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f992,plain,
( ~ spl0_75
| ~ spl0_172 ),
inference(avatar_split_clause,[],[f159,f990,f570]) ).
fof(f994,definition,
( spl0_173
<=> c2_1(a2252) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f996,plain,
( ~ spl0_75
| ~ spl0_173 ),
inference(avatar_split_clause,[],[f158,f994,f570]) ).
fof(f1002,definition,
( spl0_175
<=> c1_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1003,plain,
( c1_1(a2187)
| ~ spl0_175 ),
inference(avatar_component_clause,[],[f1002]) ).
fof(f1004,plain,
( spl0_175
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f156,f582,f1002]) ).
fof(f1006,definition,
( spl0_176
<=> c3_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f1007,plain,
( c3_1(a2187)
| ~ spl0_176 ),
inference(avatar_component_clause,[],[f1006]) ).
fof(f1008,plain,
( spl0_176
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f155,f582,f1006]) ).
fof(f1054,definition,
( spl0_188
<=> c1_1(a2217) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f1055,plain,
( c1_1(a2217)
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1056,plain,
( spl0_188
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f143,f510,f1054]) ).
fof(f1062,definition,
( spl0_190
<=> c3_1(a2222) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f1063,plain,
( c3_1(a2222)
| ~ spl0_190 ),
inference(avatar_component_clause,[],[f1062]) ).
fof(f1064,plain,
( spl0_190
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f141,f496,f1062]) ).
fof(f1066,definition,
( spl0_191
<=> c0_1(a2222) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f1068,plain,
( spl0_191
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f140,f496,f1066]) ).
fof(f1078,definition,
( spl0_194
<=> c2_1(a2239) ),
introduced(definition,[new_symbols(definition,[spl0_194])],[avatar_definition]) ).
fof(f1080,plain,
( spl0_194
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f137,f794,f1078]) ).
fof(f1131,definition,
( spl0_207
<=> c3_1(a2183) ),
introduced(definition,[new_symbols(definition,[spl0_207])],[avatar_definition]) ).
fof(f1132,plain,
( c3_1(a2183)
| ~ spl0_207 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1133,plain,
( spl0_207
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f124,f847,f1131]) ).
fof(f1135,definition,
( spl0_208
<=> c2_1(a2183) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f1137,plain,
( spl0_208
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f123,f847,f1135]) ).
fof(f1139,definition,
( spl0_209
<=> c0_1(a2184) ),
introduced(definition,[new_symbols(definition,[spl0_209])],[avatar_definition]) ).
fof(f1141,plain,
( spl0_209
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f122,f854,f1139]) ).
fof(f1143,definition,
( spl0_210
<=> c3_1(a2185) ),
introduced(definition,[new_symbols(definition,[spl0_210])],[avatar_definition]) ).
fof(f1145,plain,
( spl0_210
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f121,f493,f1143]) ).
fof(f1147,definition,
( spl0_211
<=> c1_1(a2185) ),
introduced(definition,[new_symbols(definition,[spl0_211])],[avatar_definition]) ).
fof(f1148,plain,
( c1_1(a2185)
| ~ spl0_211 ),
inference(avatar_component_clause,[],[f1147]) ).
fof(f1149,plain,
( spl0_211
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f120,f493,f1147]) ).
fof(f1151,definition,
( spl0_212
<=> c0_1(a2186) ),
introduced(definition,[new_symbols(definition,[spl0_212])],[avatar_definition]) ).
fof(f1153,plain,
( spl0_212
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f119,f447,f1151]) ).
fof(f1155,definition,
( spl0_213
<=> c1_1(a2188) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f1156,plain,
( c1_1(a2188)
| ~ spl0_213 ),
inference(avatar_component_clause,[],[f1155]) ).
fof(f1157,plain,
( spl0_213
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f118,f379,f1155]) ).
fof(f1191,definition,
( spl0_222
<=> c1_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f1192,plain,
( c1_1(a2200)
| ~ spl0_222 ),
inference(avatar_component_clause,[],[f1191]) ).
fof(f1193,plain,
( spl0_222
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f109,f460,f1191]) ).
fof(f1199,definition,
( spl0_224
<=> c3_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f1200,plain,
( c3_1(a2204)
| ~ spl0_224 ),
inference(avatar_component_clause,[],[f1199]) ).
fof(f1201,plain,
( spl0_224
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f107,f393,f1199]) ).
fof(f1203,definition,
( spl0_225
<=> c2_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_225])],[avatar_definition]) ).
fof(f1205,plain,
( spl0_225
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f106,f393,f1203]) ).
fof(f1215,definition,
( spl0_228
<=> c0_1(a2207) ),
introduced(definition,[new_symbols(definition,[spl0_228])],[avatar_definition]) ).
fof(f1217,plain,
( spl0_228
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f103,f578,f1215]) ).
fof(f1219,definition,
( spl0_229
<=> c1_1(a2207) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f1220,plain,
( c1_1(a2207)
| ~ spl0_229 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1221,plain,
( spl0_229
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f102,f578,f1219]) ).
fof(f1223,definition,
( spl0_230
<=> c0_1(a2208) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1225,plain,
( spl0_230
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f101,f575,f1223]) ).
fof(f1227,definition,
( spl0_231
<=> c3_1(a2208) ),
introduced(definition,[new_symbols(definition,[spl0_231])],[avatar_definition]) ).
fof(f1228,plain,
( c3_1(a2208)
| ~ spl0_231 ),
inference(avatar_component_clause,[],[f1227]) ).
fof(f1229,plain,
( spl0_231
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f100,f575,f1227]) ).
fof(f1239,definition,
( spl0_234
<=> c0_1(a2216) ),
introduced(definition,[new_symbols(definition,[spl0_234])],[avatar_definition]) ).
fof(f1242,plain,
( spl0_234
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f97,f513,f1239]) ).
fof(f1244,definition,
( spl0_235
<=> c3_1(a2216) ),
introduced(definition,[new_symbols(definition,[spl0_235])],[avatar_definition]) ).
fof(f1245,plain,
( c3_1(a2216)
| ~ spl0_235 ),
inference(avatar_component_clause,[],[f1244]) ).
fof(f1246,plain,
( spl0_235
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f96,f513,f1244]) ).
fof(f1248,definition,
( spl0_236
<=> c2_1(a2216) ),
introduced(definition,[new_symbols(definition,[spl0_236])],[avatar_definition]) ).
fof(f1250,plain,
( spl0_236
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f95,f513,f1248]) ).
fof(f1260,definition,
( spl0_239
<=> c0_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_239])],[avatar_definition]) ).
fof(f1262,plain,
( spl0_239
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f92,f468,f1260]) ).
fof(f1264,definition,
( spl0_240
<=> c2_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1266,plain,
( spl0_240
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f91,f468,f1264]) ).
fof(f1305,definition,
( spl0_250
<=> c2_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_250])],[avatar_definition]) ).
fof(f1308,plain,
( spl0_250
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f81,f533,f1305]) ).
fof(f1310,definition,
( spl0_251
<=> c3_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f1311,plain,
( c3_1(a2234)
| ~ spl0_251 ),
inference(avatar_component_clause,[],[f1310]) ).
fof(f1312,plain,
( spl0_251
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f80,f533,f1310]) ).
fof(f1314,definition,
( spl0_252
<=> c1_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f1315,plain,
( c1_1(a2234)
| ~ spl0_252 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1316,plain,
( spl0_252
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f79,f533,f1314]) ).
fof(f1331,definition,
( spl0_256
<=> c0_1(a2240) ),
introduced(definition,[new_symbols(definition,[spl0_256])],[avatar_definition]) ).
fof(f1334,definition,
( spl0_257
<=> hskp54 ),
introduced(definition,[new_symbols(definition,[spl0_257])],[avatar_definition]) ).
fof(f1336,plain,
( spl0_256
| ~ spl0_257 ),
inference(avatar_split_clause,[],[f75,f1334,f1331]) ).
fof(f1338,definition,
( spl0_258
<=> c3_1(a2240) ),
introduced(definition,[new_symbols(definition,[spl0_258])],[avatar_definition]) ).
fof(f1339,plain,
( c3_1(a2240)
| ~ spl0_258 ),
inference(avatar_component_clause,[],[f1338]) ).
fof(f1340,plain,
( spl0_258
| ~ spl0_257 ),
inference(avatar_split_clause,[],[f74,f1334,f1338]) ).
fof(f1342,definition,
( spl0_259
<=> c1_1(a2240) ),
introduced(definition,[new_symbols(definition,[spl0_259])],[avatar_definition]) ).
fof(f1343,plain,
( c1_1(a2240)
| ~ spl0_259 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1344,plain,
( spl0_259
| ~ spl0_257 ),
inference(avatar_split_clause,[],[f73,f1334,f1342]) ).
fof(f1346,definition,
( spl0_260
<=> c2_1(a2241) ),
introduced(definition,[new_symbols(definition,[spl0_260])],[avatar_definition]) ).
fof(f1349,definition,
( spl0_261
<=> hskp55 ),
introduced(definition,[new_symbols(definition,[spl0_261])],[avatar_definition]) ).
fof(f1351,plain,
( spl0_260
| ~ spl0_261 ),
inference(avatar_split_clause,[],[f72,f1349,f1346]) ).
fof(f1353,definition,
( spl0_262
<=> c0_1(a2241) ),
introduced(definition,[new_symbols(definition,[spl0_262])],[avatar_definition]) ).
fof(f1355,plain,
( spl0_262
| ~ spl0_261 ),
inference(avatar_split_clause,[],[f71,f1349,f1353]) ).
fof(f1357,definition,
( spl0_263
<=> c1_1(a2241) ),
introduced(definition,[new_symbols(definition,[spl0_263])],[avatar_definition]) ).
fof(f1358,plain,
( c1_1(a2241)
| ~ spl0_263 ),
inference(avatar_component_clause,[],[f1357]) ).
fof(f1359,plain,
( spl0_263
| ~ spl0_261 ),
inference(avatar_split_clause,[],[f70,f1349,f1357]) ).
fof(f1378,definition,
( spl0_268
<=> c0_1(a2252) ),
introduced(definition,[new_symbols(definition,[spl0_268])],[avatar_definition]) ).
fof(f1380,plain,
( spl0_268
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f65,f570,f1378]) ).
fof(f1384,plain,
( spl0_261
| spl0_257
| spl0_128 ),
inference(avatar_split_clause,[],[f64,f794,f1334,f1349]) ).
fof(f1396,plain,
( spl0_54
| spl0_142
| spl0_140 ),
inference(avatar_split_clause,[],[f60,f847,f854,f493]) ).
fof(f1419,plain,
( spl0_3
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f38,f794,f304]) ).
fof(f1452,plain,
( spl0_3
| ~ spl0_257 ),
inference(avatar_split_clause,[],[f5,f1334,f304]) ).
fof(f1453,plain,
( spl0_3
| ~ spl0_261 ),
inference(avatar_split_clause,[],[f4,f1349,f304]) ).
fof(f1468,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_8
| ~ spl0_11 ),
inference(resolution,[],[f333,f323]) ).
fof(f1473,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_8
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f1468]) ).
fof(f1474,plain,
( spl0_22
| ~ spl0_8
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1473,f332,f322,f371]) ).
fof(f1496,definition,
( spl0_271
<=> c2_1(a2233) ),
introduced(definition,[new_symbols(definition,[spl0_271])],[avatar_definition]) ).
fof(f1520,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f347,f330]) ).
fof(f1527,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_10
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f1520]) ).
fof(f1606,plain,
( c2_1(a2181)
| ~ c3_1(a2181)
| ~ spl0_11
| spl0_82 ),
inference(resolution,[],[f599,f333]) ).
fof(f1608,definition,
( spl0_277
<=> c3_1(a2181) ),
introduced(definition,[new_symbols(definition,[spl0_277])],[avatar_definition]) ).
fof(f1611,plain,
( ~ spl0_277
| spl0_81
| ~ spl0_11
| spl0_82 ),
inference(avatar_split_clause,[],[f1606,f598,f332,f594,f1608]) ).
fof(f1618,plain,
( c0_1(a2239)
| ~ c2_1(a2239)
| ~ spl0_1
| spl0_129 ),
inference(resolution,[],[f299,f798]) ).
fof(f1619,plain,
( c0_1(a2217)
| ~ c2_1(a2217)
| ~ spl0_1
| spl0_117 ),
inference(resolution,[],[f299,f746]) ).
fof(f1632,definition,
( spl0_278
<=> c2_1(a2217) ),
introduced(definition,[new_symbols(definition,[spl0_278])],[avatar_definition]) ).
fof(f1635,plain,
( ~ spl0_278
| spl0_116
| ~ spl0_1
| spl0_117 ),
inference(avatar_split_clause,[],[f1619,f745,f298,f741,f1632]) ).
fof(f1638,plain,
( ~ spl0_194
| spl0_130
| ~ spl0_1
| spl0_129 ),
inference(avatar_split_clause,[],[f1618,f797,f298,f801,f1078]) ).
fof(f1643,definition,
( spl0_279
<=> c2_1(a2240) ),
introduced(definition,[new_symbols(definition,[spl0_279])],[avatar_definition]) ).
fof(f1646,plain,
( c2_1(a2240)
| ~ c0_1(a2240)
| ~ spl0_8
| ~ spl0_259 ),
inference(resolution,[],[f1343,f323]) ).
fof(f1649,plain,
( ~ spl0_256
| spl0_279
| ~ spl0_8
| ~ spl0_259 ),
inference(avatar_split_clause,[],[f1646,f1342,f322,f1643,f1331]) ).
fof(f1692,plain,
( c2_1(a2181)
| c0_1(a2181)
| ~ spl0_18
| spl0_82 ),
inference(resolution,[],[f359,f599]) ).
fof(f1695,plain,
( spl0_83
| spl0_81
| ~ spl0_18
| spl0_82 ),
inference(avatar_split_clause,[],[f1692,f598,f358,f594,f602]) ).
fof(f1763,definition,
( spl0_284
<=> c0_1(a2204) ),
introduced(definition,[new_symbols(definition,[spl0_284])],[avatar_definition]) ).
fof(f1797,plain,
( ~ c2_1(a2240)
| ~ c0_1(a2240)
| ~ spl0_10
| ~ spl0_259 ),
inference(resolution,[],[f330,f1343]) ).
fof(f1802,plain,
( ~ spl0_256
| ~ spl0_279
| ~ spl0_10
| ~ spl0_259 ),
inference(avatar_split_clause,[],[f1797,f1342,f329,f1643,f1331]) ).
fof(f1850,plain,
( spl0_2
| ~ spl0_10
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1527,f346,f329,f301]) ).
fof(f1929,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_6
| ~ spl0_20 ),
inference(resolution,[],[f366,f315]) ).
fof(f1939,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_6
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f1929]) ).
fof(f1945,plain,
( spl0_23
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1939,f365,f314,f375]) ).
fof(f1953,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_6
| ~ spl0_21 ),
inference(resolution,[],[f369,f315]) ).
fof(f1964,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_6
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f1953]) ).
fof(f1968,plain,
( spl0_23
| ~ spl0_6
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1964,f368,f314,f375]) ).
fof(f1974,plain,
( c2_1(a2240)
| ~ c0_1(a2240)
| ~ spl0_22
| ~ spl0_258 ),
inference(resolution,[],[f372,f1339]) ).
fof(f1996,plain,
( c0_1(a2206)
| c2_1(a2206)
| ~ spl0_23
| spl0_104 ),
inference(resolution,[],[f376,f693]) ).
fof(f2006,plain,
( spl0_106
| spl0_105
| ~ spl0_23
| spl0_104 ),
inference(avatar_split_clause,[],[f1996,f692,f375,f696,f700]) ).
fof(f2044,definition,
( spl0_290
<=> c0_1(a2185) ),
introduced(definition,[new_symbols(definition,[spl0_290])],[avatar_definition]) ).
fof(f2058,definition,
( spl0_291
<=> c0_1(a2234) ),
introduced(definition,[new_symbols(definition,[spl0_291])],[avatar_definition]) ).
fof(f2067,plain,
( c0_1(a2234)
| ~ c3_1(a2234)
| ~ spl0_4
| ~ spl0_252 ),
inference(resolution,[],[f308,f1315]) ).
fof(f2104,plain,
( c2_1(a2233)
| c0_1(a2233)
| ~ spl0_18
| spl0_125 ),
inference(resolution,[],[f782,f359]) ).
fof(f2105,plain,
( spl0_126
| spl0_271
| ~ spl0_18
| spl0_125 ),
inference(avatar_split_clause,[],[f2104,f781,f358,f1496,f785]) ).
fof(f2112,plain,
( ~ c2_1(a2216)
| ~ c0_1(a2216)
| ~ spl0_2
| ~ spl0_235 ),
inference(resolution,[],[f302,f1245]) ).
fof(f2114,plain,
( ~ c2_1(a2204)
| ~ c0_1(a2204)
| ~ spl0_2
| ~ spl0_224 ),
inference(resolution,[],[f302,f1200]) ).
fof(f2124,plain,
( ~ spl0_284
| ~ spl0_225
| ~ spl0_2
| ~ spl0_224 ),
inference(avatar_split_clause,[],[f2114,f1199,f301,f1203,f1763]) ).
fof(f2127,plain,
( ~ spl0_234
| ~ spl0_236
| ~ spl0_2
| ~ spl0_235 ),
inference(avatar_split_clause,[],[f2112,f1244,f301,f1248,f1239]) ).
fof(f2158,plain,
( c2_1(a2240)
| ~ c3_1(a2240)
| ~ spl0_9
| ~ spl0_259 ),
inference(resolution,[],[f326,f1343]) ).
fof(f2163,plain,
( c2_1(a2185)
| ~ c3_1(a2185)
| ~ spl0_9
| ~ spl0_211 ),
inference(resolution,[],[f326,f1148]) ).
fof(f2166,plain,
( ~ spl0_210
| spl0_145
| ~ spl0_9
| ~ spl0_211 ),
inference(avatar_split_clause,[],[f2163,f1147,f325,f866,f1143]) ).
fof(f2167,plain,
( ~ spl0_258
| spl0_279
| ~ spl0_9
| ~ spl0_259 ),
inference(avatar_split_clause,[],[f2158,f1342,f325,f1643,f1338]) ).
fof(f2177,plain,
( ~ c3_1(a2204)
| ~ c2_1(a2204)
| ~ spl0_15
| spl0_160 ),
inference(resolution,[],[f347,f932]) ).
fof(f2191,plain,
( ~ spl0_225
| ~ spl0_224
| ~ spl0_15
| spl0_160 ),
inference(avatar_split_clause,[],[f2177,f931,f346,f1199,f1203]) ).
fof(f2244,plain,
( c3_1(a2233)
| c2_1(a2233)
| ~ spl0_20
| spl0_125 ),
inference(resolution,[],[f366,f782]) ).
fof(f2254,plain,
( c2_1(a2208)
| ~ c0_1(a2208)
| ~ spl0_22
| ~ spl0_231 ),
inference(resolution,[],[f372,f1228]) ).
fof(f2258,plain,
( c2_1(a2222)
| ~ c0_1(a2222)
| ~ spl0_22
| ~ spl0_190 ),
inference(resolution,[],[f372,f1063]) ).
fof(f2277,definition,
( spl0_294
<=> c2_1(a2207) ),
introduced(definition,[new_symbols(definition,[spl0_294])],[avatar_definition]) ).
fof(f2286,plain,
( ~ c2_1(a2207)
| ~ c0_1(a2207)
| ~ spl0_10
| ~ spl0_229 ),
inference(resolution,[],[f1220,f330]) ).
fof(f2287,plain,
( ~ spl0_228
| ~ spl0_294
| ~ spl0_10
| ~ spl0_229 ),
inference(avatar_split_clause,[],[f2286,f1219,f329,f2277,f1215]) ).
fof(f2296,plain,
( c2_1(a2207)
| c3_1(a2207)
| ~ spl0_19
| ~ spl0_229 ),
inference(resolution,[],[f362,f1220]) ).
fof(f2299,plain,
( c2_1(a2188)
| c3_1(a2188)
| ~ spl0_19
| ~ spl0_213 ),
inference(resolution,[],[f362,f1156]) ).
fof(f2301,plain,
( c2_1(a2217)
| c3_1(a2217)
| ~ spl0_19
| ~ spl0_188 ),
inference(resolution,[],[f362,f1055]) ).
fof(f2365,plain,
( c2_1(a2187)
| ~ c3_1(a2187)
| ~ spl0_9
| ~ spl0_175 ),
inference(resolution,[],[f1003,f326]) ).
fof(f2369,definition,
( spl0_296
<=> c0_1(a2187) ),
introduced(definition,[new_symbols(definition,[spl0_296])],[avatar_definition]) ).
fof(f2374,plain,
( ~ spl0_176
| spl0_86
| ~ spl0_9
| ~ spl0_175 ),
inference(avatar_split_clause,[],[f2365,f1002,f325,f616,f1006]) ).
fof(f2376,plain,
( c2_1(a2187)
| ~ c0_1(a2187)
| ~ spl0_22
| ~ spl0_176 ),
inference(resolution,[],[f1007,f372]) ).
fof(f2378,plain,
( c0_1(a2187)
| c2_1(a2187)
| ~ spl0_5
| ~ spl0_176 ),
inference(resolution,[],[f1007,f312]) ).
fof(f2379,plain,
( spl0_86
| spl0_296
| ~ spl0_5
| ~ spl0_176 ),
inference(avatar_split_clause,[],[f2378,f1006,f311,f2369,f616]) ).
fof(f2386,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_7
| ~ spl0_20 ),
inference(resolution,[],[f319,f366]) ).
fof(f2400,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_7
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f2386]) ).
fof(f2405,plain,
( spl0_12
| ~ spl0_7
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2400,f365,f318,f335]) ).
fof(f2453,plain,
( ~ c2_1(a2233)
| c0_1(a2233)
| ~ spl0_13
| spl0_125 ),
inference(resolution,[],[f340,f782]) ).
fof(f2475,plain,
( c3_1(a2233)
| c0_1(a2233)
| ~ spl0_21
| spl0_125 ),
inference(resolution,[],[f369,f782]) ).
fof(f2492,plain,
( ~ c2_1(a2234)
| ~ c3_1(a2234)
| ~ spl0_25
| ~ spl0_252 ),
inference(resolution,[],[f383,f1315]) ).
fof(f2506,plain,
( ~ spl0_251
| ~ spl0_250
| ~ spl0_25
| ~ spl0_252 ),
inference(avatar_split_clause,[],[f2492,f1314,f382,f1305,f1310]) ).
fof(f2533,plain,
( ~ spl0_251
| spl0_291
| ~ spl0_4
| ~ spl0_252 ),
inference(avatar_split_clause,[],[f2067,f1314,f307,f2058,f1310]) ).
fof(f2556,plain,
( spl0_126
| spl0_124
| ~ spl0_21
| spl0_125 ),
inference(avatar_split_clause,[],[f2475,f781,f368,f777,f785]) ).
fof(f2583,plain,
( spl0_126
| ~ spl0_271
| ~ spl0_13
| spl0_125 ),
inference(avatar_split_clause,[],[f2453,f781,f339,f1496,f785]) ).
fof(f2596,plain,
( c3_1(a2181)
| c0_1(a2181)
| ~ spl0_21
| spl0_82 ),
inference(resolution,[],[f599,f369]) ).
fof(f2597,plain,
( spl0_83
| spl0_277
| ~ spl0_21
| spl0_82 ),
inference(avatar_split_clause,[],[f2596,f598,f368,f1608,f602]) ).
fof(f2608,plain,
( ~ c3_1(a2226)
| ~ c2_1(a2226)
| ~ spl0_15
| spl0_166 ),
inference(resolution,[],[f962,f347]) ).
fof(f2611,definition,
( spl0_298
<=> c3_1(a2226) ),
introduced(definition,[new_symbols(definition,[spl0_298])],[avatar_definition]) ).
fof(f2616,plain,
( ~ spl0_240
| ~ spl0_298
| ~ spl0_15
| spl0_166 ),
inference(avatar_split_clause,[],[f2608,f961,f346,f2611,f1264]) ).
fof(f2622,plain,
( c2_1(a2200)
| c3_1(a2200)
| ~ spl0_19
| ~ spl0_222 ),
inference(resolution,[],[f1192,f362]) ).
fof(f2624,plain,
( c2_1(a2200)
| c0_1(a2200)
| ~ spl0_6
| ~ spl0_222 ),
inference(resolution,[],[f1192,f315]) ).
fof(f2627,plain,
( spl0_157
| spl0_156
| ~ spl0_6
| ~ spl0_222 ),
inference(avatar_split_clause,[],[f2624,f1191,f314,f913,f917]) ).
fof(f2629,definition,
( spl0_299
<=> c3_1(a2200) ),
introduced(definition,[new_symbols(definition,[spl0_299])],[avatar_definition]) ).
fof(f2664,plain,
( ~ c2_1(a2241)
| ~ c0_1(a2241)
| ~ spl0_10
| ~ spl0_263 ),
inference(resolution,[],[f330,f1358]) ).
fof(f2665,plain,
( ~ c2_1(a2234)
| ~ c0_1(a2234)
| ~ spl0_10
| ~ spl0_252 ),
inference(resolution,[],[f330,f1315]) ).
fof(f2678,plain,
( ~ spl0_291
| ~ spl0_250
| ~ spl0_10
| ~ spl0_252 ),
inference(avatar_split_clause,[],[f2665,f1314,f329,f1305,f2058]) ).
fof(f2679,plain,
( ~ spl0_262
| ~ spl0_260
| ~ spl0_10
| ~ spl0_263 ),
inference(avatar_split_clause,[],[f2664,f1357,f329,f1346,f1353]) ).
fof(f2688,plain,
( ~ c2_1(a2204)
| c0_1(a2204)
| ~ spl0_13
| spl0_160 ),
inference(resolution,[],[f340,f932]) ).
fof(f2699,plain,
( spl0_284
| ~ spl0_225
| ~ spl0_13
| spl0_160 ),
inference(avatar_split_clause,[],[f2688,f931,f339,f1203,f1763]) ).
fof(f2721,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_17
| ~ spl0_19 ),
inference(resolution,[],[f355,f362]) ).
fof(f2726,plain,
( ~ c0_1(a2226)
| c3_1(a2226)
| ~ spl0_17
| spl0_166 ),
inference(resolution,[],[f355,f962]) ).
fof(f2735,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_17
| ~ spl0_19 ),
inference(duplicate_literal_removal,[],[f2721]) ).
fof(f2742,plain,
( spl0_298
| ~ spl0_239
| ~ spl0_17
| spl0_166 ),
inference(avatar_split_clause,[],[f2726,f961,f354,f1260,f2611]) ).
fof(f2746,plain,
( spl0_12
| ~ spl0_17
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2735,f361,f354,f335]) ).
fof(f2775,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0) )
| ~ spl0_21
| ~ spl0_26 ),
inference(resolution,[],[f386,f369]) ).
fof(f2785,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_21
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f2775]) ).
fof(f2797,plain,
( spl0_1
| ~ spl0_21
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f2785,f385,f368,f298]) ).
fof(f2810,plain,
( spl0_271
| spl0_124
| ~ spl0_20
| spl0_125 ),
inference(avatar_split_clause,[],[f2244,f781,f365,f777,f1496]) ).
fof(f2841,plain,
( c0_1(a2200)
| ~ c3_1(a2200)
| ~ spl0_4
| ~ spl0_222 ),
inference(resolution,[],[f308,f1192]) ).
fof(f2844,plain,
( c0_1(a2185)
| ~ c3_1(a2185)
| ~ spl0_4
| ~ spl0_211 ),
inference(resolution,[],[f308,f1148]) ).
fof(f2848,plain,
( ~ spl0_210
| spl0_290
| ~ spl0_4
| ~ spl0_211 ),
inference(avatar_split_clause,[],[f2844,f1147,f307,f2044,f1143]) ).
fof(f2850,plain,
( ~ spl0_299
| spl0_157
| ~ spl0_4
| ~ spl0_222 ),
inference(avatar_split_clause,[],[f2841,f1191,f307,f917,f2629]) ).
fof(f2866,plain,
( c3_1(a2233)
| c2_1(a2233)
| ~ spl0_20
| spl0_125 ),
inference(resolution,[],[f366,f782]) ).
fof(f2870,plain,
( spl0_271
| spl0_124
| ~ spl0_20
| spl0_125 ),
inference(avatar_split_clause,[],[f2866,f781,f365,f777,f1496]) ).
fof(f2878,plain,
( c0_1(a2234)
| ~ c2_1(a2234)
| ~ spl0_29
| ~ spl0_251 ),
inference(resolution,[],[f397,f1311]) ).
fof(f2882,plain,
( c0_1(a2183)
| ~ c2_1(a2183)
| ~ spl0_29
| ~ spl0_207 ),
inference(resolution,[],[f397,f1132]) ).
fof(f2901,plain,
( ~ spl0_250
| spl0_291
| ~ spl0_29
| ~ spl0_251 ),
inference(avatar_split_clause,[],[f2878,f1310,f396,f2058,f1305]) ).
fof(f2913,plain,
( ~ c0_1(a2184)
| c3_1(a2184)
| ~ spl0_17
| spl0_143 ),
inference(resolution,[],[f858,f355]) ).
fof(f2914,plain,
( c3_1(a2184)
| c2_1(a2184)
| ~ spl0_20
| spl0_143 ),
inference(resolution,[],[f858,f366]) ).
fof(f2916,definition,
( spl0_301
<=> c2_1(a2184) ),
introduced(definition,[new_symbols(definition,[spl0_301])],[avatar_definition]) ).
fof(f2919,plain,
( spl0_301
| spl0_144
| ~ spl0_20
| spl0_143 ),
inference(avatar_split_clause,[],[f2914,f857,f365,f861,f2916]) ).
fof(f2921,plain,
( spl0_144
| ~ spl0_209
| ~ spl0_17
| spl0_143 ),
inference(avatar_split_clause,[],[f2913,f857,f354,f1139,f861]) ).
fof(f2949,plain,
( spl0_149
| spl0_148
| ~ spl0_19
| ~ spl0_213 ),
inference(avatar_split_clause,[],[f2299,f1155,f361,f880,f884]) ).
fof(f2951,plain,
( spl0_117
| spl0_278
| ~ spl0_19
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f2301,f1054,f361,f1632,f745]) ).
fof(f2965,plain,
( c3_1(a2181)
| c2_1(a2181)
| ~ spl0_20
| spl0_82 ),
inference(resolution,[],[f599,f366]) ).
fof(f2966,plain,
( spl0_81
| spl0_277
| ~ spl0_20
| spl0_82 ),
inference(avatar_split_clause,[],[f2965,f598,f365,f1608,f594]) ).
fof(f2973,plain,
( ~ c0_1(a2184)
| ~ c2_1(a2184)
| ~ spl0_14
| spl0_144 ),
inference(resolution,[],[f862,f343]) ).
fof(f2974,plain,
( ~ spl0_301
| ~ spl0_209
| ~ spl0_14
| spl0_144 ),
inference(avatar_split_clause,[],[f2973,f861,f342,f1139,f2916]) ).
fof(f3021,plain,
( c2_1(a2185)
| ~ c0_1(a2185)
| ~ spl0_8
| ~ spl0_211 ),
inference(resolution,[],[f323,f1148]) ).
fof(f3029,plain,
( ~ spl0_290
| spl0_145
| ~ spl0_8
| ~ spl0_211 ),
inference(avatar_split_clause,[],[f3021,f1147,f322,f866,f2044]) ).
fof(f3035,plain,
( ~ spl0_256
| spl0_279
| ~ spl0_22
| ~ spl0_258 ),
inference(avatar_split_clause,[],[f1974,f1338,f371,f1643,f1331]) ).
fof(f3038,plain,
( ~ spl0_230
| spl0_163
| ~ spl0_22
| ~ spl0_231 ),
inference(avatar_split_clause,[],[f2254,f1227,f371,f946,f1223]) ).
fof(f3040,plain,
( ~ spl0_191
| spl0_123
| ~ spl0_22
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f2258,f1062,f371,f772,f1066]) ).
fof(f3041,plain,
( ~ spl0_296
| spl0_86
| ~ spl0_22
| ~ spl0_176 ),
inference(avatar_split_clause,[],[f2376,f1006,f371,f616,f2369]) ).
fof(f3046,plain,
( spl0_299
| spl0_156
| ~ spl0_19
| ~ spl0_222 ),
inference(avatar_split_clause,[],[f2622,f1191,f361,f913,f2629]) ).
fof(f3047,plain,
( spl0_162
| spl0_294
| ~ spl0_19
| ~ spl0_229 ),
inference(avatar_split_clause,[],[f2296,f1219,f361,f2277,f941]) ).
fof(f3058,plain,
( c2_1(a2207)
| ~ c0_1(a2207)
| ~ spl0_8
| ~ spl0_229 ),
inference(resolution,[],[f1220,f323]) ).
fof(f3059,plain,
( c3_1(a2207)
| ~ c0_1(a2207)
| ~ spl0_7
| ~ spl0_229 ),
inference(resolution,[],[f1220,f319]) ).
fof(f3060,plain,
( ~ spl0_228
| spl0_162
| ~ spl0_7
| ~ spl0_229 ),
inference(avatar_split_clause,[],[f3059,f1219,f318,f941,f1215]) ).
fof(f3061,plain,
( ~ spl0_228
| spl0_294
| ~ spl0_8
| ~ spl0_229 ),
inference(avatar_split_clause,[],[f3058,f1219,f322,f2277,f1215]) ).
fof(f3064,plain,
( ~ spl0_208
| spl0_141
| ~ spl0_29
| ~ spl0_207 ),
inference(avatar_split_clause,[],[f2882,f1131,f396,f850,f1135]) ).
fof(f3072,plain,
( ~ c0_1(a2207)
| c2_1(a2207)
| ~ spl0_12
| spl0_162 ),
inference(resolution,[],[f336,f942]) ).
fof(f3074,plain,
( ~ c0_1(a2186)
| c2_1(a2186)
| ~ spl0_12
| spl0_147 ),
inference(resolution,[],[f336,f876]) ).
fof(f3090,plain,
( spl0_146
| ~ spl0_212
| ~ spl0_12
| spl0_147 ),
inference(avatar_split_clause,[],[f3074,f875,f335,f1151,f871]) ).
fof(f3091,plain,
( spl0_294
| ~ spl0_228
| ~ spl0_12
| spl0_162 ),
inference(avatar_split_clause,[],[f3072,f941,f335,f1215,f2277]) ).
fof(f3094,plain,
( ~ c0_1(a2252)
| c2_1(a2252)
| ~ spl0_16
| spl0_172 ),
inference(resolution,[],[f350,f991]) ).
fof(f3107,plain,
( spl0_173
| ~ spl0_268
| ~ spl0_16
| spl0_172 ),
inference(avatar_split_clause,[],[f3094,f990,f349,f1378,f994]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f309]) ).
cnf(s2,plain,
( spl0_2
| ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f316]) ).
cnf(s3,plain,
( spl0_1
| ~ spl0_3
| spl0_4
| spl0_7 ),
inference(sat_conversion,[],[f320]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_6
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f327]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f337]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f344]) ).
cnf(s8,plain,
( spl0_1
| ~ spl0_3
| spl0_13
| spl0_15 ),
inference(sat_conversion,[],[f352]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_13
| spl0_14
| spl0_17 ),
inference(sat_conversion,[],[f356]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_10
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f363]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_20
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f373]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_24
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f387]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_22
| spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f398]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_9
| spl0_22
| spl0_30 ),
inference(sat_conversion,[],[f402]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_11
| spl0_16
| spl0_42 ),
inference(sat_conversion,[],[f449]) ).
cnf(s28,plain,
( ~ spl0_3
| spl0_6
| spl0_17
| spl0_24 ),
inference(sat_conversion,[],[f450]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_7
| spl0_18
| spl0_45 ),
inference(sat_conversion,[],[f462]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_5
| spl0_20
| spl0_47 ),
inference(sat_conversion,[],[f470]) ).
cnf(s39,plain,
( ~ spl0_3
| spl0_15
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f515]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_10
| spl0_61 ),
inference(sat_conversion,[],[f520]) ).
cnf(s44,plain,
( spl0_1
| ~ spl0_3
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f538]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_11
| spl0_75 ),
inference(sat_conversion,[],[f572]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_19
| spl0_55 ),
inference(sat_conversion,[],[f573]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_21
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f580]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_21
| spl0_42
| spl0_78 ),
inference(sat_conversion,[],[f584]) ).
cnf(s56,plain,
( ~ spl0_61
| ~ spl0_81 ),
inference(sat_conversion,[],[f596]) ).
cnf(s57,plain,
( ~ spl0_61
| ~ spl0_82 ),
inference(sat_conversion,[],[f600]) ).
cnf(s58,plain,
( ~ spl0_61
| ~ spl0_83 ),
inference(sat_conversion,[],[f604]) ).
cnf(s61,plain,
( ~ spl0_78
| ~ spl0_86 ),
inference(sat_conversion,[],[f618]) ).
cnf(s77,plain,
( ~ spl0_30
| ~ spl0_104 ),
inference(sat_conversion,[],[f694]) ).
cnf(s78,plain,
( ~ spl0_30
| ~ spl0_105 ),
inference(sat_conversion,[],[f698]) ).
cnf(s79,plain,
( ~ spl0_30
| ~ spl0_106 ),
inference(sat_conversion,[],[f702]) ).
cnf(s87,plain,
( ~ spl0_59
| ~ spl0_116 ),
inference(sat_conversion,[],[f743]) ).
cnf(s88,plain,
( ~ spl0_59
| ~ spl0_117 ),
inference(sat_conversion,[],[f747]) ).
cnf(s94,plain,
( ~ spl0_55
| ~ spl0_123 ),
inference(sat_conversion,[],[f774]) ).
cnf(s95,plain,
( ~ spl0_66
| ~ spl0_124 ),
inference(sat_conversion,[],[f779]) ).
cnf(s96,plain,
( ~ spl0_66
| ~ spl0_125 ),
inference(sat_conversion,[],[f783]) ).
cnf(s97,plain,
( ~ spl0_66
| ~ spl0_126 ),
inference(sat_conversion,[],[f787]) ).
cnf(s99,plain,
( ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f799]) ).
cnf(s100,plain,
( ~ spl0_128
| ~ spl0_130 ),
inference(sat_conversion,[],[f803]) ).
cnf(s110,plain,
( ~ spl0_140
| ~ spl0_141 ),
inference(sat_conversion,[],[f852]) ).
cnf(s111,plain,
( ~ spl0_142
| ~ spl0_143 ),
inference(sat_conversion,[],[f859]) ).
cnf(s112,plain,
( ~ spl0_142
| ~ spl0_144 ),
inference(sat_conversion,[],[f863]) ).
cnf(s113,plain,
( ~ spl0_54
| ~ spl0_145 ),
inference(sat_conversion,[],[f868]) ).
cnf(s114,plain,
( ~ spl0_42
| ~ spl0_146 ),
inference(sat_conversion,[],[f873]) ).
cnf(s115,plain,
( ~ spl0_42
| ~ spl0_147 ),
inference(sat_conversion,[],[f877]) ).
cnf(s116,plain,
( ~ spl0_24
| ~ spl0_148 ),
inference(sat_conversion,[],[f882]) ).
cnf(s117,plain,
( ~ spl0_24
| ~ spl0_149 ),
inference(sat_conversion,[],[f886]) ).
cnf(s122,plain,
( ~ spl0_45
| ~ spl0_156 ),
inference(sat_conversion,[],[f915]) ).
cnf(s123,plain,
( ~ spl0_45
| ~ spl0_157 ),
inference(sat_conversion,[],[f919]) ).
cnf(s126,plain,
( ~ spl0_28
| ~ spl0_160 ),
inference(sat_conversion,[],[f933]) ).
cnf(s128,plain,
( ~ spl0_77
| ~ spl0_162 ),
inference(sat_conversion,[],[f943]) ).
cnf(s129,plain,
( ~ spl0_76
| ~ spl0_163 ),
inference(sat_conversion,[],[f948]) ).
cnf(s132,plain,
( ~ spl0_47
| ~ spl0_166 ),
inference(sat_conversion,[],[f963]) ).
cnf(s138,plain,
( ~ spl0_75
| ~ spl0_172 ),
inference(sat_conversion,[],[f992]) ).
cnf(s139,plain,
( ~ spl0_75
| ~ spl0_173 ),
inference(sat_conversion,[],[f996]) ).
cnf(s141,plain,
( ~ spl0_78
| spl0_175 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s142,plain,
( ~ spl0_78
| spl0_176 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s154,plain,
( ~ spl0_59
| spl0_188 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s156,plain,
( ~ spl0_55
| spl0_190 ),
inference(sat_conversion,[],[f1064]) ).
cnf(s157,plain,
( ~ spl0_55
| spl0_191 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s160,plain,
( ~ spl0_128
| spl0_194 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s173,plain,
( ~ spl0_140
| spl0_207 ),
inference(sat_conversion,[],[f1133]) ).
cnf(s174,plain,
( ~ spl0_140
| spl0_208 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s175,plain,
( ~ spl0_142
| spl0_209 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s176,plain,
( ~ spl0_54
| spl0_210 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s177,plain,
( ~ spl0_54
| spl0_211 ),
inference(sat_conversion,[],[f1149]) ).
cnf(s178,plain,
( ~ spl0_42
| spl0_212 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s179,plain,
( ~ spl0_24
| spl0_213 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s188,plain,
( ~ spl0_45
| spl0_222 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s190,plain,
( ~ spl0_28
| spl0_224 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s191,plain,
( ~ spl0_28
| spl0_225 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s194,plain,
( ~ spl0_77
| spl0_228 ),
inference(sat_conversion,[],[f1217]) ).
cnf(s195,plain,
( ~ spl0_77
| spl0_229 ),
inference(sat_conversion,[],[f1221]) ).
cnf(s196,plain,
( ~ spl0_76
| spl0_230 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s197,plain,
( ~ spl0_76
| spl0_231 ),
inference(sat_conversion,[],[f1229]) ).
cnf(s200,plain,
( ~ spl0_60
| spl0_234 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s201,plain,
( ~ spl0_60
| spl0_235 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s202,plain,
( ~ spl0_60
| spl0_236 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s205,plain,
( ~ spl0_47
| spl0_239 ),
inference(sat_conversion,[],[f1262]) ).
cnf(s206,plain,
( ~ spl0_47
| spl0_240 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s216,plain,
( ~ spl0_65
| spl0_250 ),
inference(sat_conversion,[],[f1308]) ).
cnf(s217,plain,
( ~ spl0_65
| spl0_251 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s218,plain,
( ~ spl0_65
| spl0_252 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s222,plain,
( spl0_256
| ~ spl0_257 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s223,plain,
( ~ spl0_257
| spl0_258 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s224,plain,
( ~ spl0_257
| spl0_259 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s225,plain,
( spl0_260
| ~ spl0_261 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s226,plain,
( ~ spl0_261
| spl0_262 ),
inference(sat_conversion,[],[f1355]) ).
cnf(s227,plain,
( ~ spl0_261
| spl0_263 ),
inference(sat_conversion,[],[f1359]) ).
cnf(s232,plain,
( ~ spl0_75
| spl0_268 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s233,plain,
( spl0_128
| spl0_257
| spl0_261 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s237,plain,
( spl0_54
| spl0_140
| spl0_142 ),
inference(sat_conversion,[],[f1396]) ).
cnf(s259,plain,
( spl0_3
| ~ spl0_128 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s292,plain,
( spl0_3
| ~ spl0_257 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s293,plain,
( spl0_3
| ~ spl0_261 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s298,plain,
( ~ spl0_8
| ~ spl0_11
| spl0_22 ),
inference(sat_conversion,[],[f1474]) ).
cnf(s322,plain,
( ~ spl0_11
| spl0_81
| spl0_82
| ~ spl0_277 ),
inference(sat_conversion,[],[f1611]) ).
cnf(s326,plain,
( ~ spl0_1
| spl0_116
| spl0_117
| ~ spl0_278 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s327,plain,
( ~ spl0_1
| spl0_129
| spl0_130
| ~ spl0_194 ),
inference(sat_conversion,[],[f1638]) ).
cnf(s330,plain,
( ~ spl0_8
| ~ spl0_256
| ~ spl0_259
| spl0_279 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s336,plain,
( ~ spl0_18
| spl0_81
| spl0_82
| spl0_83 ),
inference(sat_conversion,[],[f1695]) ).
cnf(s372,plain,
( ~ spl0_10
| ~ spl0_256
| ~ spl0_259
| ~ spl0_279 ),
inference(sat_conversion,[],[f1802]) ).
cnf(s386,plain,
( spl0_2
| ~ spl0_10
| ~ spl0_15 ),
inference(sat_conversion,[],[f1850]) ).
cnf(s409,plain,
( ~ spl0_6
| ~ spl0_20
| spl0_23 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s413,plain,
( ~ spl0_6
| ~ spl0_21
| spl0_23 ),
inference(sat_conversion,[],[f1968]) ).
cnf(s422,plain,
( ~ spl0_23
| spl0_104
| spl0_105
| spl0_106 ),
inference(sat_conversion,[],[f2006]) ).
cnf(s462,plain,
( ~ spl0_18
| spl0_125
| spl0_126
| spl0_271 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s466,plain,
( ~ spl0_2
| ~ spl0_224
| ~ spl0_225
| ~ spl0_284 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s467,plain,
( ~ spl0_2
| ~ spl0_234
| ~ spl0_235
| ~ spl0_236 ),
inference(sat_conversion,[],[f2127]) ).
cnf(s492,plain,
( ~ spl0_9
| spl0_145
| ~ spl0_210
| ~ spl0_211 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s493,plain,
( ~ spl0_9
| ~ spl0_258
| ~ spl0_259
| spl0_279 ),
inference(sat_conversion,[],[f2167]) ).
cnf(s500,plain,
( ~ spl0_15
| spl0_160
| ~ spl0_224
| ~ spl0_225 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s528,plain,
( ~ spl0_10
| ~ spl0_228
| ~ spl0_229
| ~ spl0_294 ),
inference(sat_conversion,[],[f2287]) ).
cnf(s571,plain,
( ~ spl0_9
| spl0_86
| ~ spl0_175
| ~ spl0_176 ),
inference(sat_conversion,[],[f2374]) ).
cnf(s573,plain,
( ~ spl0_5
| spl0_86
| ~ spl0_176
| spl0_296 ),
inference(sat_conversion,[],[f2379]) ).
cnf(s581,plain,
( ~ spl0_7
| spl0_12
| ~ spl0_20 ),
inference(sat_conversion,[],[f2405]) ).
cnf(s606,plain,
( ~ spl0_25
| ~ spl0_250
| ~ spl0_251
| ~ spl0_252 ),
inference(sat_conversion,[],[f2506]) ).
cnf(s621,plain,
( ~ spl0_4
| ~ spl0_251
| ~ spl0_252
| spl0_291 ),
inference(sat_conversion,[],[f2533]) ).
cnf(s644,plain,
( ~ spl0_21
| spl0_124
| spl0_125
| spl0_126 ),
inference(sat_conversion,[],[f2556]) ).
cnf(s674,plain,
( ~ spl0_13
| spl0_125
| spl0_126
| ~ spl0_271 ),
inference(sat_conversion,[],[f2583]) ).
cnf(s686,plain,
( ~ spl0_21
| spl0_82
| spl0_83
| spl0_277 ),
inference(sat_conversion,[],[f2597]) ).
cnf(s691,plain,
( ~ spl0_15
| spl0_166
| ~ spl0_240
| ~ spl0_298 ),
inference(sat_conversion,[],[f2616]) ).
cnf(s692,plain,
( ~ spl0_6
| spl0_156
| spl0_157
| ~ spl0_222 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s706,plain,
( ~ spl0_10
| ~ spl0_250
| ~ spl0_252
| ~ spl0_291 ),
inference(sat_conversion,[],[f2678]) ).
cnf(s707,plain,
( ~ spl0_10
| ~ spl0_260
| ~ spl0_262
| ~ spl0_263 ),
inference(sat_conversion,[],[f2679]) ).
cnf(s709,plain,
( ~ spl0_13
| spl0_160
| ~ spl0_225
| spl0_284 ),
inference(sat_conversion,[],[f2699]) ).
cnf(s719,plain,
( ~ spl0_17
| spl0_166
| ~ spl0_239
| spl0_298 ),
inference(sat_conversion,[],[f2742]) ).
cnf(s722,plain,
( spl0_12
| ~ spl0_17
| ~ spl0_19 ),
inference(sat_conversion,[],[f2746]) ).
cnf(s740,plain,
( spl0_1
| ~ spl0_21
| ~ spl0_26 ),
inference(sat_conversion,[],[f2797]) ).
cnf(s754,plain,
( ~ spl0_20
| spl0_124
| spl0_125
| spl0_271 ),
inference(sat_conversion,[],[f2810]) ).
cnf(s765,plain,
( ~ spl0_4
| ~ spl0_210
| ~ spl0_211
| spl0_290 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s767,plain,
( ~ spl0_4
| spl0_157
| ~ spl0_222
| ~ spl0_299 ),
inference(sat_conversion,[],[f2850]) ).
cnf(s774,plain,
( ~ spl0_20
| spl0_124
| spl0_125
| spl0_271 ),
inference(sat_conversion,[],[f2870]) ).
cnf(s784,plain,
( ~ spl0_29
| ~ spl0_250
| ~ spl0_251
| spl0_291 ),
inference(sat_conversion,[],[f2901]) ).
cnf(s795,plain,
( ~ spl0_20
| spl0_143
| spl0_144
| spl0_301 ),
inference(sat_conversion,[],[f2919]) ).
cnf(s796,plain,
( ~ spl0_17
| spl0_143
| spl0_144
| ~ spl0_209 ),
inference(sat_conversion,[],[f2921]) ).
cnf(s828,plain,
( ~ spl0_19
| spl0_148
| spl0_149
| ~ spl0_213 ),
inference(sat_conversion,[],[f2949]) ).
cnf(s830,plain,
( ~ spl0_19
| spl0_117
| ~ spl0_188
| spl0_278 ),
inference(sat_conversion,[],[f2951]) ).
cnf(s842,plain,
( ~ spl0_20
| spl0_81
| spl0_82
| spl0_277 ),
inference(sat_conversion,[],[f2966]) ).
cnf(s845,plain,
( ~ spl0_14
| spl0_144
| ~ spl0_209
| ~ spl0_301 ),
inference(sat_conversion,[],[f2974]) ).
cnf(s855,plain,
( ~ spl0_8
| spl0_145
| ~ spl0_211
| ~ spl0_290 ),
inference(sat_conversion,[],[f3029]) ).
cnf(s860,plain,
( ~ spl0_22
| ~ spl0_256
| ~ spl0_258
| spl0_279 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s863,plain,
( ~ spl0_22
| spl0_163
| ~ spl0_230
| ~ spl0_231 ),
inference(sat_conversion,[],[f3038]) ).
cnf(s865,plain,
( ~ spl0_22
| spl0_123
| ~ spl0_190
| ~ spl0_191 ),
inference(sat_conversion,[],[f3040]) ).
cnf(s866,plain,
( ~ spl0_22
| spl0_86
| ~ spl0_176
| ~ spl0_296 ),
inference(sat_conversion,[],[f3041]) ).
cnf(s871,plain,
( ~ spl0_19
| spl0_156
| ~ spl0_222
| spl0_299 ),
inference(sat_conversion,[],[f3046]) ).
cnf(s872,plain,
( ~ spl0_19
| spl0_162
| ~ spl0_229
| spl0_294 ),
inference(sat_conversion,[],[f3047]) ).
cnf(s877,plain,
( ~ spl0_7
| spl0_162
| ~ spl0_228
| ~ spl0_229 ),
inference(sat_conversion,[],[f3060]) ).
cnf(s878,plain,
( ~ spl0_8
| ~ spl0_228
| ~ spl0_229
| spl0_294 ),
inference(sat_conversion,[],[f3061]) ).
cnf(s882,plain,
( ~ spl0_29
| spl0_141
| ~ spl0_207
| ~ spl0_208 ),
inference(sat_conversion,[],[f3064]) ).
cnf(s886,plain,
( ~ spl0_12
| spl0_146
| spl0_147
| ~ spl0_212 ),
inference(sat_conversion,[],[f3090]) ).
cnf(s887,plain,
( ~ spl0_12
| spl0_162
| ~ spl0_228
| spl0_294 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s890,plain,
( ~ spl0_16
| spl0_172
| spl0_173
| ~ spl0_268 ),
inference(sat_conversion,[],[f3107]) ).
cnf(s891,plain,
spl0_3,
inference(rat,[],[s233,s259,s292,s293]) ).
cnf(s892,plain,
( ~ spl0_45
| ~ spl0_6 ),
inference(rat,[],[s692,s122,s123,s188]) ).
cnf(s893,plain,
( spl0_11
| spl0_10 ),
inference(rat,[],[s886,s114,s115,s178,s27,s890,s138,s139,s232,s5,s51,s891]) ).
cnf(s894,plain,
( ~ spl0_42
| ~ spl0_12 ),
inference(rat,[],[s886,s114,s115,s178]) ).
cnf(s899,plain,
( ~ spl0_77
| ~ spl0_7 ),
inference(rat,[],[s877,s128,s194,s195]) ).
cnf(s900,plain,
( spl0_10
| spl0_77 ),
inference(rat,[],[s863,s129,s196,s197,s53,s11,s842,s686,s322,s893,s56,s57,s58,s41,s891]) ).
cnf(s901,plain,
( spl0_21
| spl0_9
| spl0_77
| ~ spl0_6 ),
inference(rat,[],[s422,s409,s77,s78,s79,s11,s16,s863,s129,s196,s197,s53,s891]) ).
cnf(s902,plain,
( ~ spl0_30
| ~ spl0_23 ),
inference(rat,[],[s422,s77,s78,s79]) ).
cnf(s904,plain,
( ~ spl0_66
| ~ spl0_21 ),
inference(rat,[],[s644,s95,s96,s97]) ).
cnf(s905,plain,
( ~ spl0_65
| ~ spl0_10
| ~ spl0_4 ),
inference(rat,[],[s706,s621,s216,s217,s218]) ).
cnf(s906,plain,
( spl0_77
| spl0_2
| spl0_1 ),
inference(rat,[],[s863,s129,s196,s197,s11,s53,s774,s674,s904,s95,s96,s97,s44,s905,s8,s386,s900,s1,s891]) ).
cnf(s907,plain,
( ~ spl0_61
| ~ spl0_18 ),
inference(rat,[],[s336,s56,s57,s58]) ).
cnf(s908,plain,
( ~ spl0_18
| spl0_2
| spl0_1 ),
inference(rat,[],[s462,s674,s96,s97,s44,s8,s905,s386,s41,s907,s1,s891]) ).
cnf(s909,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s11,s904,s774,s674,s95,s96,s97,s44,s8,s865,s905,s386,s94,s156,s157,s10,s52,s871,s767,s122,s123,s188,s31,s908,s899,s906,s1,s891]) ).
cnf(s910,plain,
( spl0_21
| ~ spl0_7 ),
inference(rat,[],[s890,s138,s139,s232,s27,s51,s298,s4,s901,s571,s61,s141,s142,s54,s894,s581,s11,s863,s129,s196,s197,s53,s899,s891]) ).
cnf(s911,plain,
( ~ spl0_28
| spl0_1 ),
inference(rat,[],[s8,s709,s500,s466,s126,s190,s191,s909,s891]) ).
cnf(s912,plain,
( ~ spl0_7
| spl0_1 ),
inference(rat,[],[s865,s94,s156,s157,s52,s828,s116,s117,s179,s15,s13,s784,s606,s706,s216,s217,s218,s44,s904,s740,s900,s910,s899,s911,s891]) ).
cnf(s913,plain,
( spl0_10
| spl0_1 ),
inference(rat,[],[s767,s871,s122,s123,s188,s10,s31,s907,s41,s3,s912,s891]) ).
cnf(s916,plain,
( ~ spl0_142
| ~ spl0_17 ),
inference(rat,[],[s796,s111,s112,s175]) ).
cnf(s917,plain,
( ~ spl0_140
| ~ spl0_29 ),
inference(rat,[],[s882,s110,s173,s174]) ).
cnf(s918,plain,
( ~ spl0_54
| ~ spl0_9 ),
inference(rat,[],[s492,s113,s176,s177]) ).
cnf(s919,plain,
( ~ spl0_142
| ~ spl0_14
| ~ spl0_20 ),
inference(rat,[],[s795,s845,s111,s112,s175]) ).
cnf(s920,plain,
( ~ spl0_77
| spl0_1 ),
inference(rat,[],[s902,s409,s16,s4,s918,s237,s919,s917,s6,s674,s754,s15,s11,s865,s94,s156,s157,s52,s887,s878,s872,s528,s128,s194,s195,s911,s97,s96,s95,s904,s44,s905,s913,s3,s912,s891]) ).
cnf(s921,plain,
( ~ spl0_142
| spl0_1 ),
inference(rat,[],[s9,s919,s916,s674,s754,s11,s863,s196,s197,s129,s53,s920,s904,s95,s97,s96,s44,s905,s913,s3,s912,s891]) ).
cnf(s922,plain,
spl0_1,
inference(rat,[],[s4,s901,s855,s765,s918,s113,s176,s177,s237,s921,s917,s15,s863,s129,s196,s197,s53,s920,s904,s44,s905,s913,s3,s912,s911,s891]) ).
cnf(s929,plain,
( ~ spl0_261
| ~ spl0_10 ),
inference(rat,[],[s707,s225,s226,s227]) ).
cnf(s931,plain,
~ spl0_128,
inference(rat,[],[s327,s99,s100,s160,s922]) ).
cnf(s932,plain,
( ~ spl0_10
| spl0_6 ),
inference(rat,[],[s4,s493,s330,s372,s222,s223,s224,s233,s929,s891,s931]) ).
cnf(s933,plain,
( spl0_10
| ~ spl0_20 ),
inference(rat,[],[s842,s322,s56,s57,s893,s41,s891]) ).
cnf(s934,plain,
~ spl0_20,
inference(rat,[],[s16,s860,s493,s372,s902,s222,s223,s224,s409,s233,s932,s929,s933,s891,s931]) ).
cnf(s935,plain,
( ~ spl0_24
| ~ spl0_19 ),
inference(rat,[],[s828,s116,s117,s179]) ).
cnf(s938,plain,
( ~ spl0_60
| ~ spl0_2 ),
inference(rat,[],[s467,s200,s201,s202]) ).
cnf(s939,plain,
( spl0_6
| spl0_21 ),
inference(rat,[],[s326,s830,s87,s88,s154,s39,s938,s691,s719,s132,s205,s206,s33,s2,s573,s866,s61,s142,s54,s894,s722,s28,s935,s10,s907,s41,s932,s11,s922,s891,s934]) ).
cnf(s940,plain,
spl0_21,
inference(rat,[],[s372,s860,s222,s223,s224,s233,s929,s41,s907,s31,s892,s939,s11,s910,s931,s891,s934]) ).
cnf(s942,plain,
spl0_10,
inference(rat,[],[s686,s322,s56,s57,s58,s893,s41,s940,s891]) ).
cnf(s943,plain,
~ spl0_261,
inference(rat,[],[s929,s942]) ).
cnf(s944,plain,
spl0_6,
inference(rat,[],[s932,s942]) ).
cnf(s945,plain,
spl0_257,
inference(rat,[],[s233,s931,s943]) ).
cnf(s947,plain,
spl0_23,
inference(rat,[],[s413,s940,s944]) ).
cnf(s948,plain,
spl0_259,
inference(rat,[],[s224,s945]) ).
cnf(s949,plain,
spl0_258,
inference(rat,[],[s223,s945]) ).
cnf(s950,plain,
spl0_256,
inference(rat,[],[s222,s945]) ).
cnf(s951,plain,
~ spl0_30,
inference(rat,[],[s902,s947]) ).
cnf(s952,plain,
~ spl0_279,
inference(rat,[],[s372,s948,s942,s950]) ).
cnf(s954,plain,
~ spl0_9,
inference(rat,[],[s493,s948,s949,s952]) ).
cnf(s955,plain,
~ spl0_22,
inference(rat,[],[s860,s949,s950,s952]) ).
cnf(s956,plain,
$false,
inference(rat,[],[s16,s951,s891,s955,s954]) ).
fof(f3108,plain,
$false,
inference(avatar_sat_refutation,[],[s956]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN460-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n009.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 16:06:30 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.27/1.17 % (3191132)Input is clausal, will run a generic CNF schedule.
% 3.27/1.17 % (3191225)lrs+10_1_sil=8000:sp=occurrence:random_seed=803664599:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.27/1.17 % (3191225)Instruction limit reached!
% 3.27/1.17 % (3191225)------------------------------
% 3.27/1.17 % (3191225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.17 % (3191225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.17 % (3191225)CaDiCaL version: 2.1.3
% 3.27/1.17 % (3191225)Termination reason: Instruction limit
% 3.27/1.17 % (3191225)Termination phase: Saturation
% 3.27/1.17 % (3191225)Time elapsed: 0.039 s
% 3.27/1.17 % (3191225)Peak memory usage: 90 MB
% 3.27/1.17 % (3191225)Instructions burned: 107 (million)
% 3.27/1.17 % (3191230)dis-21_1_sil=8000:lcm=predicate:random_seed=3061180671:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.27/1.17 % (3191228)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=530672860:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.27/1.17 % (3191221)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3331590896:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.27/1.17 % (3191220)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=3884108185:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.27/1.17 % (3191223)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1981163581:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.27/1.17 % (3191226)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=124682951:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.27/1.17 % (3191230)First to succeed.
% 3.27/1.17 % (3191230)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3191132"
% 3.27/1.17 % (3191226)Instruction limit reached!
% 3.27/1.17 % (3191226)------------------------------
% 3.27/1.17 % (3191226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.17 % (3191226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.17 % (3191226)CaDiCaL version: 2.1.3
% 3.27/1.17 % (3191226)Termination reason: Instruction limit
% 3.27/1.17 % (3191226)Termination phase: Saturation
% 3.27/1.17 % (3191226)Time elapsed: 0.109 s
% 3.27/1.17 % (3191226)Peak memory usage: 90 MB
% 3.27/1.17 % (3191226)Instructions burned: 114 (million)
% 3.27/1.17 % (3191228)Instruction limit reached!
% 3.27/1.17 % (3191228)------------------------------
% 3.27/1.17 % (3191228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.17 % (3191228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.17 % (3191228)CaDiCaL version: 2.1.3
% 3.27/1.17 % (3191228)Termination reason: Instruction limit
% 3.27/1.17 % (3191228)Termination phase: Saturation
% 3.27/1.17 % (3191228)Time elapsed: 0.152 s
% 3.27/1.17 % (3191228)Peak memory usage: 91 MB
% 3.27/1.17 % (3191228)Instructions burned: 181 (million)
% 3.27/1.17 % (3191269)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=953942767:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.27/1.18 % (3191296)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3189610336:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 3.27/1.18 % (3191269)Instruction limit reached!
% 3.27/1.18 % (3191269)------------------------------
% 3.27/1.18 % (3191269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.18 % (3191269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.18 % (3191269)CaDiCaL version: 2.1.3
% 3.27/1.18 % (3191269)Termination reason: Instruction limit
% 3.27/1.18 % (3191269)Termination phase: Saturation
% 3.27/1.18 % (3191269)Time elapsed: 0.094 s
% 3.27/1.18 % (3191269)Peak memory usage: 90 MB
% 3.27/1.18 % (3191269)Instructions burned: 143 (million)
% 3.27/1.18 % (3191298)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1633623946:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 3.27/1.18 % (3191230)Refutation found. Thanks to Tanya!
% 3.27/1.18 % SZS status Unsatisfiable for theBenchmark
% 3.27/1.18 % SZS output start Proof for theBenchmark
% See solution above
% 4.05/1.37 % (3191230)------------------------------
% 4.05/1.37 % (3191230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.05/1.37 % (3191230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.05/1.37 % (3191230)CaDiCaL version: 2.1.3
% 4.05/1.37 % (3191230)Termination reason: Refutation
% 4.05/1.37 % (3191230)Time elapsed: 0.048 s
% 4.05/1.37 % (3191230)Peak memory usage: 90 MB
% 4.05/1.37 % (3191230)Instructions burned: 71 (million)
% 4.05/1.37 % (3191230)------------------------------
% 4.05/1.37 % (3191230)------------------------------
% 4.05/1.37 % (3191132)Success in time 0.494 s
% 4.05/1.37 % Vampire exiting
%------------------------------------------------------------------------------