%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN475-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 : n015.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:54:50 PM UTC 2026
% Result : Unsatisfiable 2.21s 0.72s
% Output : Refutation 2.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 192
% Syntax : Number of formulae : 645 ( 17 unt; 109 def)
% Number of atoms : 2000 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2407 (1052 ~;1246 |; 0 &)
% ( 109 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 134 ( 133 usr; 130 prp; 0-1 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 102 ( 0 sgn 102 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp29
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f4,negated_conjecture,
( ~ hskp26
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f27,negated_conjecture,
( ~ hskp3
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
fof(f31,negated_conjecture,
( hskp29
| hskp23
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
fof(f33,negated_conjecture,
( hskp29
| hskp3
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f38,negated_conjecture,
( hskp4
| hskp21
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f40,negated_conjecture,
( ~ hskp29
| c0_1(a1040) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f41,negated_conjecture,
( ~ hskp29
| c1_1(a1040) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
fof(f43,negated_conjecture,
( ~ hskp28
| c0_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp28
| c1_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp28
| c2_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f49,negated_conjecture,
( ~ hskp26
| c3_1(a1052) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f51,negated_conjecture,
( ~ hskp24
| c1_1(a1045) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp24
| c3_1(a1045) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp23
| c0_1(a1044) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp23
| c1_1(a1044) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f56,negated_conjecture,
( ~ hskp21
| c2_1(a1041) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f59,negated_conjecture,
( ~ hskp17
| c2_1(a1032) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp17
| c3_1(a1032) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f62,negated_conjecture,
( ~ hskp15
| c2_1(a1026) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f64,negated_conjecture,
( ~ hskp13
| c3_1(a1023) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f67,negated_conjecture,
( ~ hskp11
| c3_1(a1015) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f71,negated_conjecture,
( ~ hskp8
| c0_1(a1010) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp8
| c3_1(a1010) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp7
| c2_1(a1008) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp6
| c0_1(a1006) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp6
| c3_1(a1006) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp4
| c1_1(a1004) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp4
| c2_1(a1004) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f79,negated_conjecture,
( ~ hskp2
| c0_1(a1002) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp2
| c2_1(a1002) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp1
| c2_1(a1001) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp1
| c3_1(a1001) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f85,negated_conjecture,
( ~ c0_1(a1052)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ c2_1(a1052)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f89,negated_conjecture,
( ~ c0_1(a1045)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c3_1(a1044)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f93,negated_conjecture,
( ~ c0_1(a1041)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c3_1(a1041)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f98,negated_conjecture,
( ~ c0_1(a1037)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c1_1(a1037)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c3_1(a1037)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f102,negated_conjecture,
( ~ c0_1(a1032)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f105,negated_conjecture,
( ~ c0_1(a1026)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c1_1(a1026)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f109,negated_conjecture,
( ~ c1_1(a1023)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c2_1(a1023)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f112,negated_conjecture,
( ~ c0_1(a1015)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c1_1(a1015)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f117,negated_conjecture,
( ~ c1_1(a1010)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c1_1(a1008)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c3_1(a1008)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c2_1(a1006)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c1_1(a1005)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c2_1(a1005)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c3_1(a1005)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c3_1(a1004)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f127,negated_conjecture,
( ~ c1_1(a1002)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ c1_1(a1001)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f134,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp2
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp28
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f138,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f140,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp24
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp8
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp6
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f152,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f159,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f164,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
fof(f166,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f178,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c1_1(X1)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f181,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X0)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f185,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c3_1(X2)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause185) ).
fof(f187,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f190,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c2_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f191,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c0_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause191) ).
fof(f194,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f195,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| ~ c0_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f197,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f198,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f200,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f203,definition,
( spl0_4
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f204,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f207,definition,
( spl0_5
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f208,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| ~ c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f210,definition,
( spl0_6
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f211,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f212,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f191,f203,f200,f210,f207]) ).
fof(f214,definition,
( spl0_7
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f215,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| ~ c2_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f217,definition,
( spl0_8
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f218,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f220,definition,
( spl0_9
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f221,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f222,plain,
( spl0_7
| spl0_8
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f190,f220,f200,f217,f214]) ).
fof(f224,definition,
( spl0_10
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f225,plain,
( ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f227,definition,
( spl0_11
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f228,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f231,definition,
( spl0_12
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f232,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f235,definition,
( spl0_13
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f236,plain,
( ! [X2] :
( c0_1(X2)
| c1_1(X2)
| ~ c2_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f238,definition,
( spl0_14
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f239,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( spl0_13
| spl0_14
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f187,f197,f200,f238,f235]) ).
fof(f242,definition,
( spl0_15
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f243,plain,
( ! [X2] :
( c3_1(X2)
| ~ c2_1(X2)
| c0_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f249,definition,
( spl0_17
<=> ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f250,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f252,definition,
( spl0_18
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f253,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f255,definition,
( spl0_19
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f256,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f257,plain,
( spl0_17
| spl0_18
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f185,f255,f200,f252,f249]) ).
fof(f259,definition,
( spl0_20
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f260,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f263,definition,
( spl0_21
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f264,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f265,plain,
( spl0_21
| spl0_13
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f183,f252,f200,f235,f263]) ).
fof(f267,definition,
( spl0_22
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f270,definition,
( spl0_23
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f271,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( spl0_22
| spl0_11
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f182,f270,f200,f227,f267]) ).
fof(f274,definition,
( spl0_24
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f277,definition,
( spl0_25
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f278,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f279,plain,
( spl0_24
| spl0_2
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f181,f277,f200,f197,f274]) ).
fof(f281,definition,
( spl0_26
<=> ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f282,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1)
| c2_1(X1) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f284,plain,
( spl0_24
| spl0_14
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f179,f214,f200,f238,f274]) ).
fof(f286,definition,
( spl0_27
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f288,plain,
( spl0_27
| spl0_5
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f178,f194,f200,f207,f286]) ).
fof(f297,definition,
( spl0_30
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f302,definition,
( spl0_31
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f304,plain,
( spl0_31
| spl0_17
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f174,f270,f200,f249,f302]) ).
fof(f317,definition,
( spl0_35
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f318,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f321,definition,
( spl0_36
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f323,plain,
( spl0_36
| spl0_35
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f170,f238,f200,f317,f321]) ).
fof(f329,definition,
( spl0_38
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f333,definition,
( spl0_39
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f335,plain,
( spl0_39
| spl0_15
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f167,f194,f200,f242,f333]) ).
fof(f336,plain,
( spl0_39
| spl0_10
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f166,f207,f200,f224,f333]) ).
fof(f345,definition,
( spl0_42
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f347,plain,
( spl0_42
| spl0_13
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f164,f217,f200,f235,f345]) ).
fof(f365,definition,
( spl0_47
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f367,plain,
( spl0_47
| spl0_10
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f159,f255,f200,f224,f365]) ).
fof(f371,plain,
( spl0_24
| spl0_20
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f155,f210,f200,f259,f274]) ).
fof(f373,definition,
( spl0_48
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f380,plain,
( spl0_38
| spl0_26
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f152,f317,f200,f281,f329]) ).
fof(f382,definition,
( spl0_50
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f389,definition,
( spl0_52
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f393,definition,
( spl0_53
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f397,plain,
( spl0_47
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f147,f270,f200,f365]) ).
fof(f399,definition,
( spl0_54
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f408,plain,
( spl0_38
| spl0_24
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f142,f197,f200,f274,f329]) ).
fof(f409,plain,
( spl0_52
| spl0_30
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f141,f197,f200,f297,f389]) ).
fof(f410,plain,
( spl0_27
| spl0_53
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f140,f194,f200,f393,f286]) ).
fof(f415,plain,
( spl0_54
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f138,f194,f200,f399]) ).
fof(f417,definition,
( spl0_57
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f420,definition,
( spl0_58
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f428,definition,
( spl0_60
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f430,plain,
( spl0_30
| spl0_60
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f135,f231,f200,f428,f297]) ).
fof(f432,definition,
( spl0_61
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f434,plain,
( spl0_61
| spl0_50
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f134,f242,f200,f382,f432]) ).
fof(f446,definition,
( spl0_63
<=> c1_1(a1001) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f448,plain,
( ~ spl0_61
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f128,f446,f432]) ).
fof(f451,definition,
( spl0_64
<=> c1_1(a1002) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f453,plain,
( ~ spl0_50
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f127,f451,f382]) ).
fof(f465,definition,
( spl0_67
<=> c3_1(a1004) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f466,plain,
( ~ c3_1(a1004)
| spl0_67 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( ~ spl0_42
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f124,f465,f345]) ).
fof(f470,definition,
( spl0_68
<=> c3_1(a1005) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f471,plain,
( ~ c3_1(a1005)
| spl0_68 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( ~ spl0_31
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f123,f470,f302]) ).
fof(f474,definition,
( spl0_69
<=> c2_1(a1005) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f476,plain,
( ~ spl0_31
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f122,f474,f302]) ).
fof(f478,definition,
( spl0_70
<=> c1_1(a1005) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f480,plain,
( ~ spl0_31
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f121,f478,f302]) ).
fof(f483,definition,
( spl0_71
<=> c2_1(a1006) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f485,plain,
( ~ spl0_24
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f120,f483,f274]) ).
fof(f488,definition,
( spl0_72
<=> c3_1(a1008) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f489,plain,
( ~ c3_1(a1008)
| spl0_72 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f490,plain,
( ~ spl0_47
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f119,f488,f365]) ).
fof(f492,definition,
( spl0_73
<=> c1_1(a1008) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f494,plain,
( ~ spl0_47
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f118,f492,f365]) ).
fof(f497,definition,
( spl0_74
<=> c1_1(a1010) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f499,plain,
( ~ spl0_30
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f117,f497,f297]) ).
fof(f516,definition,
( spl0_78
<=> c1_1(a1015) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f518,plain,
( ~ spl0_39
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f113,f516,f333]) ).
fof(f520,definition,
( spl0_79
<=> c0_1(a1015) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f521,plain,
( ~ c0_1(a1015)
| spl0_79 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f522,plain,
( ~ spl0_39
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f112,f520,f333]) ).
fof(f530,definition,
( spl0_81
<=> c2_1(a1023) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f532,plain,
( ~ spl0_38
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f110,f530,f329]) ).
fof(f534,definition,
( spl0_82
<=> c1_1(a1023) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f536,plain,
( ~ spl0_38
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f109,f534,f329]) ).
fof(f548,definition,
( spl0_85
<=> c1_1(a1026) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f550,plain,
( ~ spl0_27
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f106,f548,f286]) ).
fof(f552,definition,
( spl0_86
<=> c0_1(a1026) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f553,plain,
( ~ c0_1(a1026)
| spl0_86 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f554,plain,
( ~ spl0_27
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f105,f552,f286]) ).
fof(f566,definition,
( spl0_89
<=> c0_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f568,plain,
( ~ spl0_22
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f102,f566,f267]) ).
fof(f576,definition,
( spl0_91
<=> c3_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f577,plain,
( ~ c3_1(a1037)
| spl0_91 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f578,plain,
( ~ spl0_36
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f100,f576,f321]) ).
fof(f580,definition,
( spl0_92
<=> c1_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f582,plain,
( ~ spl0_36
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f99,f580,f321]) ).
fof(f584,definition,
( spl0_93
<=> c0_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f585,plain,
( ~ c0_1(a1037)
| spl0_93 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f586,plain,
( ~ spl0_36
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f98,f584,f321]) ).
fof(f602,definition,
( spl0_97
<=> c3_1(a1041) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f603,plain,
( ~ c3_1(a1041)
| spl0_97 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f604,plain,
( ~ spl0_57
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f94,f602,f417]) ).
fof(f606,definition,
( spl0_98
<=> c0_1(a1041) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f607,plain,
( ~ c0_1(a1041)
| spl0_98 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f608,plain,
( ~ spl0_57
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f93,f606,f417]) ).
fof(f620,definition,
( spl0_101
<=> c3_1(a1044) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f621,plain,
( ~ c3_1(a1044)
| spl0_101 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f622,plain,
( ~ spl0_54
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f90,f620,f399]) ).
fof(f625,definition,
( spl0_102
<=> c0_1(a1045) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f627,plain,
( ~ spl0_53
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f89,f625,f393]) ).
fof(f639,definition,
( spl0_105
<=> c2_1(a1052) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f641,plain,
( ~ spl0_52
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f86,f639,f389]) ).
fof(f643,definition,
( spl0_106
<=> c0_1(a1052) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f645,plain,
( ~ spl0_52
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f85,f643,f389]) ).
fof(f655,definition,
( spl0_109
<=> c3_1(a1001) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f656,plain,
( c3_1(a1001)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f655]) ).
fof(f657,plain,
( spl0_109
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f82,f432,f655]) ).
fof(f659,definition,
( spl0_110
<=> c2_1(a1001) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f661,plain,
( spl0_110
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f81,f432,f659]) ).
fof(f663,definition,
( spl0_111
<=> c2_1(a1002) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f665,plain,
( spl0_111
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f80,f382,f663]) ).
fof(f667,definition,
( spl0_112
<=> c0_1(a1002) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f668,plain,
( c0_1(a1002)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f669,plain,
( spl0_112
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f79,f382,f667]) ).
fof(f675,definition,
( spl0_114
<=> c2_1(a1004) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f677,plain,
( spl0_114
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f77,f345,f675]) ).
fof(f679,definition,
( spl0_115
<=> c1_1(a1004) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f681,plain,
( spl0_115
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f76,f345,f679]) ).
fof(f683,definition,
( spl0_116
<=> c3_1(a1006) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f684,plain,
( c3_1(a1006)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f685,plain,
( spl0_116
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f75,f274,f683]) ).
fof(f687,definition,
( spl0_117
<=> c0_1(a1006) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f689,plain,
( spl0_117
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f74,f274,f687]) ).
fof(f691,definition,
( spl0_118
<=> c2_1(a1008) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f693,plain,
( spl0_118
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f73,f365,f691]) ).
fof(f695,definition,
( spl0_119
<=> c3_1(a1010) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f696,plain,
( c3_1(a1010)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f697,plain,
( spl0_119
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f72,f297,f695]) ).
fof(f699,definition,
( spl0_120
<=> c0_1(a1010) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f701,plain,
( spl0_120
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f71,f297,f699]) ).
fof(f715,definition,
( spl0_124
<=> c3_1(a1015) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f716,plain,
( c3_1(a1015)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f717,plain,
( spl0_124
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f67,f333,f715]) ).
fof(f727,definition,
( spl0_127
<=> c3_1(a1023) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f728,plain,
( c3_1(a1023)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f729,plain,
( spl0_127
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f64,f329,f727]) ).
fof(f735,definition,
( spl0_129
<=> c2_1(a1026) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f737,plain,
( spl0_129
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f62,f286,f735]) ).
fof(f743,definition,
( spl0_131
<=> c3_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f744,plain,
( c3_1(a1032)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f745,plain,
( spl0_131
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f60,f267,f743]) ).
fof(f747,definition,
( spl0_132
<=> c2_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f749,plain,
( spl0_132
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f59,f267,f747]) ).
fof(f759,definition,
( spl0_135
<=> c2_1(a1041) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f761,plain,
( spl0_135
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f56,f417,f759]) ).
fof(f767,definition,
( spl0_137
<=> c1_1(a1044) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f769,plain,
( spl0_137
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f54,f399,f767]) ).
fof(f771,definition,
( spl0_138
<=> c0_1(a1044) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f772,plain,
( c0_1(a1044)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f773,plain,
( spl0_138
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f53,f399,f771]) ).
fof(f775,definition,
( spl0_139
<=> c3_1(a1045) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f776,plain,
( c3_1(a1045)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f777,plain,
( spl0_139
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f52,f393,f775]) ).
fof(f779,definition,
( spl0_140
<=> c1_1(a1045) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f781,plain,
( spl0_140
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f51,f393,f779]) ).
fof(f787,definition,
( spl0_142
<=> c3_1(a1052) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f788,plain,
( c3_1(a1052)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f789,plain,
( spl0_142
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f49,f389,f787]) ).
fof(f804,definition,
( spl0_146
<=> c2_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f807,plain,
( spl0_146
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f45,f428,f804]) ).
fof(f809,definition,
( spl0_147
<=> c1_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f811,plain,
( spl0_147
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f44,f428,f809]) ).
fof(f813,definition,
( spl0_148
<=> c0_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f814,plain,
( c0_1(a1033)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f815,plain,
( spl0_148
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f43,f428,f813]) ).
fof(f822,definition,
( spl0_150
<=> c1_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f824,plain,
( spl0_150
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f41,f420,f822]) ).
fof(f826,definition,
( spl0_151
<=> c0_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f827,plain,
( c0_1(a1040)
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f828,plain,
( spl0_151
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f40,f420,f826]) ).
fof(f830,plain,
( spl0_47
| spl0_57
| spl0_42 ),
inference(avatar_split_clause,[],[f38,f345,f417,f365]) ).
fof(f835,plain,
( spl0_52
| spl0_48
| spl0_58 ),
inference(avatar_split_clause,[],[f33,f420,f373,f389]) ).
fof(f837,plain,
( spl0_38
| spl0_54
| spl0_58 ),
inference(avatar_split_clause,[],[f31,f420,f399,f329]) ).
fof(f842,plain,
( spl0_3
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f27,f373,f200]) ).
fof(f865,plain,
( spl0_3
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f4,f389,f200]) ).
fof(f868,plain,
( spl0_3
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f1,f420,f200]) ).
fof(f870,plain,
( c2_1(a1044)
| ~ c1_1(a1044)
| ~ spl0_2
| ~ spl0_138 ),
inference(resolution,[],[f198,f772]) ).
fof(f873,definition,
( spl0_152
<=> c2_1(a1044) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f875,plain,
( ~ spl0_137
| spl0_152
| ~ spl0_2
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f870,f771,f197,f873,f767]) ).
fof(f881,plain,
( c2_1(a1040)
| ~ c1_1(a1040)
| ~ spl0_2
| ~ spl0_151 ),
inference(resolution,[],[f827,f198]) ).
fof(f884,definition,
( spl0_154
<=> c2_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f886,plain,
( ~ spl0_150
| spl0_154
| ~ spl0_2
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f881,f826,f197,f884,f822]) ).
fof(f897,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(resolution,[],[f228,f215]) ).
fof(f899,plain,
( ~ c0_1(a1044)
| ~ c2_1(a1044)
| ~ spl0_11
| spl0_101 ),
inference(resolution,[],[f228,f621]) ).
fof(f900,plain,
( ~ c0_1(a1008)
| ~ c2_1(a1008)
| ~ spl0_11
| spl0_72 ),
inference(resolution,[],[f228,f489]) ).
fof(f902,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f897]) ).
fof(f905,definition,
( spl0_155
<=> c0_1(a1008) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f906,plain,
( ~ c0_1(a1008)
| spl0_155 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f907,plain,
( ~ spl0_118
| ~ spl0_155
| ~ spl0_11
| spl0_72 ),
inference(avatar_split_clause,[],[f900,f488,f227,f905,f691]) ).
fof(f910,plain,
( ~ spl0_152
| ~ spl0_138
| ~ spl0_11
| spl0_101 ),
inference(avatar_split_clause,[],[f899,f620,f227,f771,f873]) ).
fof(f911,plain,
( spl0_14
| ~ spl0_7
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f902,f227,f214,f238]) ).
fof(f944,definition,
( spl0_157
<=> c2_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f953,definition,
( spl0_158
<=> c0_1(a1004) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f954,plain,
( c0_1(a1004)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f957,plain,
( c2_1(a1006)
| ~ c0_1(a1006)
| ~ spl0_8
| ~ spl0_116 ),
inference(resolution,[],[f218,f684]) ).
fof(f963,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7
| ~ spl0_15 ),
inference(resolution,[],[f243,f215]) ).
fof(f968,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c1_1(X0) )
| ~ spl0_7
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f963]) ).
fof(f972,plain,
( c0_1(a1008)
| ~ spl0_155 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f974,plain,
( spl0_13
| ~ spl0_7
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f968,f242,f214,f235]) ).
fof(f1004,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_15
| ~ spl0_17 ),
inference(resolution,[],[f250,f243]) ).
fof(f1010,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1004]) ).
fof(f1011,plain,
( spl0_13
| ~ spl0_15
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1010,f249,f242,f235]) ).
fof(f1017,plain,
( c0_1(a1001)
| ~ c2_1(a1001)
| ~ spl0_6
| ~ spl0_109 ),
inference(resolution,[],[f656,f211]) ).
fof(f1023,definition,
( spl0_160
<=> c0_1(a1001) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1025,plain,
( ~ spl0_110
| spl0_160
| ~ spl0_6
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f1017,f655,f210,f1023,f659]) ).
fof(f1026,plain,
( ~ c0_1(a1001)
| spl0_160 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1030,plain,
( c2_1(a1015)
| c1_1(a1015)
| ~ spl0_12
| ~ spl0_124 ),
inference(resolution,[],[f716,f232]) ).
fof(f1033,definition,
( spl0_161
<=> c2_1(a1015) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1052,plain,
( ~ c1_1(a1041)
| c0_1(a1041)
| ~ spl0_10
| spl0_97 ),
inference(resolution,[],[f603,f225]) ).
fof(f1055,definition,
( spl0_162
<=> c1_1(a1041) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1057,plain,
( spl0_98
| ~ spl0_162
| ~ spl0_10
| spl0_97 ),
inference(avatar_split_clause,[],[f1052,f602,f224,f1055,f606]) ).
fof(f1071,plain,
( ~ c1_1(a1004)
| c0_1(a1004)
| ~ spl0_10
| spl0_67 ),
inference(resolution,[],[f466,f225]) ).
fof(f1072,plain,
( spl0_158
| ~ spl0_115
| ~ spl0_10
| spl0_67 ),
inference(avatar_split_clause,[],[f1071,f465,f224,f679,f953]) ).
fof(f1094,plain,
( c2_1(a1015)
| c0_1(a1015)
| ~ spl0_18
| ~ spl0_124 ),
inference(resolution,[],[f253,f716]) ).
fof(f1106,plain,
( ~ spl0_117
| spl0_71
| ~ spl0_8
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f957,f683,f217,f483,f687]) ).
fof(f1143,plain,
( ~ c2_1(a1004)
| ~ c1_1(a1004)
| ~ spl0_23
| ~ spl0_158 ),
inference(resolution,[],[f271,f954]) ).
fof(f1157,definition,
( spl0_163
<=> c0_1(a1005) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1170,plain,
( c0_1(a1032)
| ~ c2_1(a1032)
| ~ spl0_6
| ~ spl0_131 ),
inference(resolution,[],[f744,f211]) ).
fof(f1173,definition,
( spl0_164
<=> c1_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1178,plain,
( ~ spl0_132
| spl0_89
| ~ spl0_6
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f1170,f743,f210,f566,f747]) ).
fof(f1186,plain,
( ~ spl0_115
| ~ spl0_114
| ~ spl0_23
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f1143,f953,f270,f675,f679]) ).
fof(f1204,plain,
( c2_1(a1023)
| ~ c0_1(a1023)
| ~ spl0_8
| ~ spl0_127 ),
inference(resolution,[],[f728,f218]) ).
fof(f1211,definition,
( spl0_166
<=> c0_1(a1023) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1213,plain,
( ~ spl0_166
| spl0_81
| ~ spl0_8
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1204,f727,f217,f530,f1211]) ).
fof(f1234,plain,
( c1_1(a1023)
| ~ c0_1(a1023)
| ~ spl0_1
| ~ spl0_127 ),
inference(resolution,[],[f195,f728]) ).
fof(f1237,plain,
( c1_1(a1001)
| ~ c0_1(a1001)
| ~ spl0_1
| ~ spl0_109 ),
inference(resolution,[],[f195,f656]) ).
fof(f1238,plain,
( ~ spl0_160
| spl0_63
| ~ spl0_1
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f1237,f655,f194,f446,f1023]) ).
fof(f1241,plain,
( ~ spl0_166
| spl0_82
| ~ spl0_1
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1234,f727,f194,f534,f1211]) ).
fof(f1246,plain,
( c1_1(a1032)
| ~ c2_1(a1032)
| ~ spl0_7
| ~ spl0_131 ),
inference(resolution,[],[f215,f744]) ).
fof(f1248,plain,
( c1_1(a1015)
| ~ c2_1(a1015)
| ~ spl0_7
| ~ spl0_124 ),
inference(resolution,[],[f215,f716]) ).
fof(f1250,plain,
( c1_1(a1001)
| ~ c2_1(a1001)
| ~ spl0_7
| ~ spl0_109 ),
inference(resolution,[],[f215,f656]) ).
fof(f1252,plain,
( ~ spl0_110
| spl0_63
| ~ spl0_7
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f1250,f655,f214,f446,f659]) ).
fof(f1253,plain,
( ~ spl0_161
| spl0_78
| ~ spl0_7
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1248,f715,f214,f516,f1033]) ).
fof(f1254,plain,
( ~ spl0_132
| spl0_164
| ~ spl0_7
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f1246,f743,f214,f1173,f747]) ).
fof(f1259,plain,
( ~ c1_1(a1041)
| ~ c2_1(a1041)
| ~ spl0_9
| spl0_97 ),
inference(resolution,[],[f221,f603]) ).
fof(f1262,plain,
( ~ c1_1(a1004)
| ~ c2_1(a1004)
| ~ spl0_9
| spl0_67 ),
inference(resolution,[],[f221,f466]) ).
fof(f1269,plain,
( ~ spl0_114
| ~ spl0_115
| ~ spl0_9
| spl0_67 ),
inference(avatar_split_clause,[],[f1262,f465,f220,f679,f675]) ).
fof(f1270,plain,
( ~ spl0_135
| ~ spl0_162
| ~ spl0_9
| spl0_97 ),
inference(avatar_split_clause,[],[f1259,f602,f220,f1055,f759]) ).
fof(f1276,plain,
( c1_1(a1041)
| ~ c2_1(a1041)
| ~ spl0_13
| spl0_98 ),
inference(resolution,[],[f236,f607]) ).
fof(f1278,plain,
( c1_1(a1026)
| ~ c2_1(a1026)
| ~ spl0_13
| spl0_86 ),
inference(resolution,[],[f236,f553]) ).
fof(f1283,plain,
( ~ spl0_129
| spl0_85
| ~ spl0_13
| spl0_86 ),
inference(avatar_split_clause,[],[f1278,f552,f235,f548,f735]) ).
fof(f1285,plain,
( ~ spl0_135
| spl0_162
| ~ spl0_13
| spl0_98 ),
inference(avatar_split_clause,[],[f1276,f606,f235,f1055,f759]) ).
fof(f1287,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_19 ),
inference(resolution,[],[f256,f195]) ).
fof(f1298,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_19 ),
inference(duplicate_literal_removal,[],[f1287]) ).
fof(f1305,plain,
( spl0_14
| ~ spl0_1
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1298,f255,f194,f238]) ).
fof(f1313,plain,
( c1_1(a1015)
| c0_1(a1015)
| ~ spl0_17
| ~ spl0_124 ),
inference(resolution,[],[f250,f716]) ).
fof(f1315,plain,
( c1_1(a1001)
| c0_1(a1001)
| ~ spl0_17
| ~ spl0_109 ),
inference(resolution,[],[f250,f656]) ).
fof(f1318,plain,
( spl0_160
| spl0_63
| ~ spl0_17
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f1315,f655,f249,f446,f1023]) ).
fof(f1319,plain,
( spl0_79
| spl0_78
| ~ spl0_17
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1313,f715,f249,f516,f520]) ).
fof(f1365,plain,
( c1_1(a1002)
| ~ c2_1(a1002)
| ~ spl0_14
| ~ spl0_112 ),
inference(resolution,[],[f239,f668]) ).
fof(f1370,plain,
( ~ spl0_111
| spl0_64
| ~ spl0_14
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1365,f667,f238,f451,f663]) ).
fof(f1376,plain,
( ~ c2_1(a1008)
| c1_1(a1008)
| ~ spl0_19
| spl0_72 ),
inference(resolution,[],[f256,f489]) ).
fof(f1381,plain,
( spl0_73
| ~ spl0_118
| ~ spl0_19
| spl0_72 ),
inference(avatar_split_clause,[],[f1376,f488,f255,f691,f492]) ).
fof(f1393,plain,
( c1_1(a1008)
| ~ c2_1(a1008)
| ~ spl0_14
| ~ spl0_155 ),
inference(resolution,[],[f972,f239]) ).
fof(f1395,plain,
( ~ spl0_118
| spl0_73
| ~ spl0_14
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f1393,f905,f238,f492,f691]) ).
fof(f1404,plain,
( c2_1(a1015)
| c1_1(a1015)
| ~ spl0_21
| spl0_79 ),
inference(resolution,[],[f264,f521]) ).
fof(f1407,plain,
( c2_1(a1037)
| c1_1(a1037)
| ~ spl0_21
| spl0_93 ),
inference(resolution,[],[f264,f585]) ).
fof(f1410,plain,
( spl0_78
| spl0_161
| ~ spl0_21
| spl0_79 ),
inference(avatar_split_clause,[],[f1404,f520,f263,f1033,f516]) ).
fof(f1412,definition,
( spl0_169
<=> c1_1(a1052) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1418,plain,
( ~ c2_1(a1033)
| ~ c1_1(a1033)
| ~ spl0_23
| ~ spl0_148 ),
inference(resolution,[],[f271,f814]) ).
fof(f1427,plain,
( ~ spl0_147
| ~ spl0_146
| ~ spl0_23
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f1418,f813,f270,f804,f809]) ).
fof(f1430,plain,
( c1_1(a1010)
| ~ c0_1(a1010)
| ~ spl0_1
| ~ spl0_119 ),
inference(resolution,[],[f696,f195]) ).
fof(f1431,plain,
( c2_1(a1010)
| ~ c0_1(a1010)
| ~ spl0_8
| ~ spl0_119 ),
inference(resolution,[],[f696,f218]) ).
fof(f1434,definition,
( spl0_170
<=> c2_1(a1010) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1436,plain,
( ~ spl0_120
| spl0_170
| ~ spl0_8
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1431,f695,f217,f1434,f699]) ).
fof(f1438,plain,
( ~ spl0_120
| spl0_74
| ~ spl0_1
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1430,f695,f194,f497,f699]) ).
fof(f1447,plain,
( spl0_78
| spl0_161
| ~ spl0_12
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1030,f715,f231,f1033,f516]) ).
fof(f1450,plain,
( spl0_79
| spl0_161
| ~ spl0_18
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1094,f715,f252,f1033,f520]) ).
fof(f1461,plain,
( ~ c2_1(a1040)
| ~ c1_1(a1040)
| ~ spl0_23
| ~ spl0_151 ),
inference(resolution,[],[f827,f271]) ).
fof(f1463,plain,
( ~ spl0_150
| ~ spl0_154
| ~ spl0_23
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f1461,f826,f270,f884,f822]) ).
fof(f1467,plain,
( c0_1(a1052)
| ~ c1_1(a1052)
| ~ spl0_5
| ~ spl0_142 ),
inference(resolution,[],[f208,f788]) ).
fof(f1468,plain,
( c0_1(a1045)
| ~ c1_1(a1045)
| ~ spl0_5
| ~ spl0_139 ),
inference(resolution,[],[f208,f776]) ).
fof(f1470,plain,
( c0_1(a1032)
| ~ c1_1(a1032)
| ~ spl0_5
| ~ spl0_131 ),
inference(resolution,[],[f208,f744]) ).
fof(f1477,plain,
( ~ spl0_164
| spl0_89
| ~ spl0_5
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f1470,f743,f207,f566,f1173]) ).
fof(f1481,plain,
( ~ spl0_140
| spl0_102
| ~ spl0_5
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1468,f775,f207,f625,f779]) ).
fof(f1484,plain,
( ~ spl0_169
| spl0_106
| ~ spl0_5
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1467,f787,f207,f643,f1412]) ).
fof(f1521,plain,
( c2_1(a1052)
| c1_1(a1052)
| ~ spl0_12
| ~ spl0_142 ),
inference(resolution,[],[f232,f788]) ).
fof(f1524,plain,
( c2_1(a1023)
| c1_1(a1023)
| ~ spl0_12
| ~ spl0_127 ),
inference(resolution,[],[f232,f728]) ).
fof(f1530,plain,
( spl0_82
| spl0_81
| ~ spl0_12
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1524,f727,f231,f530,f534]) ).
fof(f1531,plain,
( spl0_169
| spl0_105
| ~ spl0_12
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1521,f787,f231,f639,f1412]) ).
fof(f1546,plain,
( spl0_92
| spl0_157
| ~ spl0_21
| spl0_93 ),
inference(avatar_split_clause,[],[f1407,f584,f263,f944,f580]) ).
fof(f1553,plain,
( ~ c2_1(a1044)
| ~ c1_1(a1044)
| ~ spl0_23
| ~ spl0_138 ),
inference(resolution,[],[f772,f271]) ).
fof(f1555,plain,
( ~ spl0_137
| ~ spl0_152
| ~ spl0_23
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1553,f771,f270,f873,f767]) ).
fof(f1560,plain,
( ~ c1_1(a1032)
| ~ c2_1(a1032)
| ~ spl0_4
| ~ spl0_131 ),
inference(resolution,[],[f204,f744]) ).
fof(f1568,plain,
( ~ spl0_132
| ~ spl0_164
| ~ spl0_4
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f1560,f743,f203,f1173,f747]) ).
fof(f1578,plain,
( c1_1(a1008)
| ~ c2_1(a1008)
| ~ spl0_13
| spl0_155 ),
inference(resolution,[],[f236,f906]) ).
fof(f1580,plain,
( c1_1(a1001)
| ~ c2_1(a1001)
| ~ spl0_13
| spl0_160 ),
inference(resolution,[],[f236,f1026]) ).
fof(f1582,plain,
( c1_1(a1037)
| ~ c2_1(a1037)
| ~ spl0_13
| spl0_93 ),
inference(resolution,[],[f236,f585]) ).
fof(f1585,plain,
( ~ spl0_110
| spl0_63
| ~ spl0_13
| spl0_160 ),
inference(avatar_split_clause,[],[f1580,f1023,f235,f446,f659]) ).
fof(f1586,plain,
( ~ spl0_118
| spl0_73
| ~ spl0_13
| spl0_155 ),
inference(avatar_split_clause,[],[f1578,f905,f235,f492,f691]) ).
fof(f1608,plain,
( ~ spl0_157
| spl0_92
| ~ spl0_13
| spl0_93 ),
inference(avatar_split_clause,[],[f1582,f584,f235,f580,f944]) ).
fof(f1632,plain,
( ~ c2_1(a1008)
| c0_1(a1008)
| ~ spl0_15
| spl0_72 ),
inference(resolution,[],[f243,f489]) ).
fof(f1638,plain,
( spl0_155
| ~ spl0_118
| ~ spl0_15
| spl0_72 ),
inference(avatar_split_clause,[],[f1632,f488,f242,f691,f905]) ).
fof(f1659,plain,
( c2_1(a1052)
| c0_1(a1052)
| ~ spl0_18
| ~ spl0_142 ),
inference(resolution,[],[f253,f788]) ).
fof(f1662,plain,
( c2_1(a1023)
| c0_1(a1023)
| ~ spl0_18
| ~ spl0_127 ),
inference(resolution,[],[f253,f728]) ).
fof(f1668,plain,
( spl0_166
| spl0_81
| ~ spl0_18
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1662,f727,f252,f530,f1211]) ).
fof(f1672,plain,
( spl0_106
| spl0_105
| ~ spl0_18
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1659,f787,f252,f639,f643]) ).
fof(f1682,plain,
( c1_1(a1052)
| c0_1(a1052)
| ~ spl0_17
| ~ spl0_142 ),
inference(resolution,[],[f250,f788]) ).
fof(f1684,plain,
( c1_1(a1032)
| c0_1(a1032)
| ~ spl0_17
| ~ spl0_131 ),
inference(resolution,[],[f250,f744]) ).
fof(f1685,plain,
( c1_1(a1023)
| c0_1(a1023)
| ~ spl0_17
| ~ spl0_127 ),
inference(resolution,[],[f250,f728]) ).
fof(f1690,plain,
( spl0_166
| spl0_82
| ~ spl0_17
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1685,f727,f249,f534,f1211]) ).
fof(f1691,plain,
( spl0_89
| spl0_164
| ~ spl0_17
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f1684,f743,f249,f1173,f566]) ).
fof(f1692,plain,
( spl0_106
| spl0_169
| ~ spl0_17
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1682,f787,f249,f1412,f643]) ).
fof(f1703,plain,
( ~ c0_1(a1010)
| ~ c2_1(a1010)
| ~ spl0_25
| ~ spl0_119 ),
inference(resolution,[],[f278,f696]) ).
fof(f1708,plain,
( ~ spl0_170
| ~ spl0_120
| ~ spl0_25
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1703,f695,f277,f699,f1434]) ).
fof(f1713,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_17
| ~ spl0_26 ),
inference(resolution,[],[f282,f250]) ).
fof(f1721,plain,
( c1_1(a1037)
| c2_1(a1037)
| ~ spl0_26
| spl0_91 ),
inference(resolution,[],[f282,f577]) ).
fof(f1722,plain,
( c1_1(a1005)
| c2_1(a1005)
| ~ spl0_26
| spl0_68 ),
inference(resolution,[],[f282,f471]) ).
fof(f1725,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_17
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f1713]) ).
fof(f1727,plain,
( spl0_69
| spl0_70
| ~ spl0_26
| spl0_68 ),
inference(avatar_split_clause,[],[f1722,f470,f281,f478,f474]) ).
fof(f1728,plain,
( spl0_157
| spl0_92
| ~ spl0_26
| spl0_91 ),
inference(avatar_split_clause,[],[f1721,f576,f281,f580,f944]) ).
fof(f1731,plain,
( spl0_21
| ~ spl0_17
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1725,f281,f249,f263]) ).
fof(f1750,plain,
( c0_1(a1005)
| c2_1(a1005)
| ~ spl0_20
| spl0_68 ),
inference(resolution,[],[f260,f471]) ).
fof(f1753,plain,
( spl0_69
| spl0_163
| ~ spl0_20
| spl0_68 ),
inference(avatar_split_clause,[],[f1750,f470,f259,f1157,f474]) ).
fof(f1823,plain,
( ~ c0_1(a1008)
| c1_1(a1008)
| ~ spl0_35
| spl0_72 ),
inference(resolution,[],[f318,f489]) ).
fof(f1825,plain,
( ~ c0_1(a1005)
| c1_1(a1005)
| ~ spl0_35
| spl0_68 ),
inference(resolution,[],[f318,f471]) ).
fof(f1830,plain,
( spl0_70
| ~ spl0_163
| ~ spl0_35
| spl0_68 ),
inference(avatar_split_clause,[],[f1825,f470,f317,f1157,f478]) ).
fof(f1833,plain,
( spl0_73
| ~ spl0_155
| ~ spl0_35
| spl0_72 ),
inference(avatar_split_clause,[],[f1823,f488,f317,f905,f492]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f212]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f222]) ).
cnf(s6,plain,
( spl0_2
| ~ spl0_3
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f240]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_17
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f257]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_13
| spl0_18
| spl0_21 ),
inference(sat_conversion,[],[f265]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_11
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f272]) ).
cnf(s12,plain,
( spl0_2
| ~ spl0_3
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f279]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_7
| spl0_14
| spl0_24 ),
inference(sat_conversion,[],[f284]) ).
cnf(s15,plain,
( spl0_1
| ~ spl0_3
| spl0_5
| spl0_27 ),
inference(sat_conversion,[],[f288]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_17
| spl0_23
| spl0_31 ),
inference(sat_conversion,[],[f304]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_14
| spl0_35
| spl0_36 ),
inference(sat_conversion,[],[f323]) ).
cnf(s26,plain,
( spl0_1
| ~ spl0_3
| spl0_15
| spl0_39 ),
inference(sat_conversion,[],[f335]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_5
| spl0_10
| spl0_39 ),
inference(sat_conversion,[],[f336]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_8
| spl0_13
| spl0_42 ),
inference(sat_conversion,[],[f347]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_10
| spl0_19
| spl0_47 ),
inference(sat_conversion,[],[f367]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_6
| spl0_20
| spl0_24 ),
inference(sat_conversion,[],[f371]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_26
| spl0_35
| spl0_38 ),
inference(sat_conversion,[],[f380]) ).
cnf(s46,plain,
( ~ spl0_3
| spl0_23
| spl0_47 ),
inference(sat_conversion,[],[f397]) ).
cnf(s51,plain,
( spl0_2
| ~ spl0_3
| spl0_24
| spl0_38 ),
inference(sat_conversion,[],[f408]) ).
cnf(s52,plain,
( spl0_2
| ~ spl0_3
| spl0_30
| spl0_52 ),
inference(sat_conversion,[],[f409]) ).
cnf(s53,plain,
( spl0_1
| ~ spl0_3
| spl0_27
| spl0_53 ),
inference(sat_conversion,[],[f410]) ).
cnf(s55,plain,
( spl0_1
| ~ spl0_3
| spl0_54 ),
inference(sat_conversion,[],[f415]) ).
cnf(s58,plain,
( ~ spl0_3
| spl0_12
| spl0_30
| spl0_60 ),
inference(sat_conversion,[],[f430]) ).
cnf(s59,plain,
( ~ spl0_3
| spl0_15
| spl0_50
| spl0_61 ),
inference(sat_conversion,[],[f434]) ).
cnf(s65,plain,
( ~ spl0_61
| ~ spl0_63 ),
inference(sat_conversion,[],[f448]) ).
cnf(s66,plain,
( ~ spl0_50
| ~ spl0_64 ),
inference(sat_conversion,[],[f453]) ).
cnf(s69,plain,
( ~ spl0_42
| ~ spl0_67 ),
inference(sat_conversion,[],[f467]) ).
cnf(s70,plain,
( ~ spl0_31
| ~ spl0_68 ),
inference(sat_conversion,[],[f472]) ).
cnf(s71,plain,
( ~ spl0_31
| ~ spl0_69 ),
inference(sat_conversion,[],[f476]) ).
cnf(s72,plain,
( ~ spl0_31
| ~ spl0_70 ),
inference(sat_conversion,[],[f480]) ).
cnf(s73,plain,
( ~ spl0_24
| ~ spl0_71 ),
inference(sat_conversion,[],[f485]) ).
cnf(s74,plain,
( ~ spl0_47
| ~ spl0_72 ),
inference(sat_conversion,[],[f490]) ).
cnf(s75,plain,
( ~ spl0_47
| ~ spl0_73 ),
inference(sat_conversion,[],[f494]) ).
cnf(s76,plain,
( ~ spl0_30
| ~ spl0_74 ),
inference(sat_conversion,[],[f499]) ).
cnf(s80,plain,
( ~ spl0_39
| ~ spl0_78 ),
inference(sat_conversion,[],[f518]) ).
cnf(s81,plain,
( ~ spl0_39
| ~ spl0_79 ),
inference(sat_conversion,[],[f522]) ).
cnf(s83,plain,
( ~ spl0_38
| ~ spl0_81 ),
inference(sat_conversion,[],[f532]) ).
cnf(s84,plain,
( ~ spl0_38
| ~ spl0_82 ),
inference(sat_conversion,[],[f536]) ).
cnf(s87,plain,
( ~ spl0_27
| ~ spl0_85 ),
inference(sat_conversion,[],[f550]) ).
cnf(s88,plain,
( ~ spl0_27
| ~ spl0_86 ),
inference(sat_conversion,[],[f554]) ).
cnf(s91,plain,
( ~ spl0_22
| ~ spl0_89 ),
inference(sat_conversion,[],[f568]) ).
cnf(s93,plain,
( ~ spl0_36
| ~ spl0_91 ),
inference(sat_conversion,[],[f578]) ).
cnf(s94,plain,
( ~ spl0_36
| ~ spl0_92 ),
inference(sat_conversion,[],[f582]) ).
cnf(s95,plain,
( ~ spl0_36
| ~ spl0_93 ),
inference(sat_conversion,[],[f586]) ).
cnf(s99,plain,
( ~ spl0_57
| ~ spl0_97 ),
inference(sat_conversion,[],[f604]) ).
cnf(s100,plain,
( ~ spl0_57
| ~ spl0_98 ),
inference(sat_conversion,[],[f608]) ).
cnf(s103,plain,
( ~ spl0_54
| ~ spl0_101 ),
inference(sat_conversion,[],[f622]) ).
cnf(s104,plain,
( ~ spl0_53
| ~ spl0_102 ),
inference(sat_conversion,[],[f627]) ).
cnf(s107,plain,
( ~ spl0_52
| ~ spl0_105 ),
inference(sat_conversion,[],[f641]) ).
cnf(s108,plain,
( ~ spl0_52
| ~ spl0_106 ),
inference(sat_conversion,[],[f645]) ).
cnf(s111,plain,
( ~ spl0_61
| spl0_109 ),
inference(sat_conversion,[],[f657]) ).
cnf(s112,plain,
( ~ spl0_61
| spl0_110 ),
inference(sat_conversion,[],[f661]) ).
cnf(s113,plain,
( ~ spl0_50
| spl0_111 ),
inference(sat_conversion,[],[f665]) ).
cnf(s114,plain,
( ~ spl0_50
| spl0_112 ),
inference(sat_conversion,[],[f669]) ).
cnf(s116,plain,
( ~ spl0_42
| spl0_114 ),
inference(sat_conversion,[],[f677]) ).
cnf(s117,plain,
( ~ spl0_42
| spl0_115 ),
inference(sat_conversion,[],[f681]) ).
cnf(s118,plain,
( ~ spl0_24
| spl0_116 ),
inference(sat_conversion,[],[f685]) ).
cnf(s119,plain,
( ~ spl0_24
| spl0_117 ),
inference(sat_conversion,[],[f689]) ).
cnf(s120,plain,
( ~ spl0_47
| spl0_118 ),
inference(sat_conversion,[],[f693]) ).
cnf(s121,plain,
( ~ spl0_30
| spl0_119 ),
inference(sat_conversion,[],[f697]) ).
cnf(s122,plain,
( ~ spl0_30
| spl0_120 ),
inference(sat_conversion,[],[f701]) ).
cnf(s126,plain,
( ~ spl0_39
| spl0_124 ),
inference(sat_conversion,[],[f717]) ).
cnf(s129,plain,
( ~ spl0_38
| spl0_127 ),
inference(sat_conversion,[],[f729]) ).
cnf(s131,plain,
( ~ spl0_27
| spl0_129 ),
inference(sat_conversion,[],[f737]) ).
cnf(s133,plain,
( ~ spl0_22
| spl0_131 ),
inference(sat_conversion,[],[f745]) ).
cnf(s134,plain,
( ~ spl0_22
| spl0_132 ),
inference(sat_conversion,[],[f749]) ).
cnf(s137,plain,
( ~ spl0_57
| spl0_135 ),
inference(sat_conversion,[],[f761]) ).
cnf(s139,plain,
( ~ spl0_54
| spl0_137 ),
inference(sat_conversion,[],[f769]) ).
cnf(s140,plain,
( ~ spl0_54
| spl0_138 ),
inference(sat_conversion,[],[f773]) ).
cnf(s141,plain,
( ~ spl0_53
| spl0_139 ),
inference(sat_conversion,[],[f777]) ).
cnf(s142,plain,
( ~ spl0_53
| spl0_140 ),
inference(sat_conversion,[],[f781]) ).
cnf(s144,plain,
( ~ spl0_52
| spl0_142 ),
inference(sat_conversion,[],[f789]) ).
cnf(s148,plain,
( ~ spl0_60
| spl0_146 ),
inference(sat_conversion,[],[f807]) ).
cnf(s149,plain,
( ~ spl0_60
| spl0_147 ),
inference(sat_conversion,[],[f811]) ).
cnf(s150,plain,
( ~ spl0_60
| spl0_148 ),
inference(sat_conversion,[],[f815]) ).
cnf(s152,plain,
( ~ spl0_58
| spl0_150 ),
inference(sat_conversion,[],[f824]) ).
cnf(s153,plain,
( ~ spl0_58
| spl0_151 ),
inference(sat_conversion,[],[f828]) ).
cnf(s155,plain,
( spl0_42
| spl0_47
| spl0_57 ),
inference(sat_conversion,[],[f830]) ).
cnf(s160,plain,
( spl0_48
| spl0_52
| spl0_58 ),
inference(sat_conversion,[],[f835]) ).
cnf(s162,plain,
( spl0_38
| spl0_54
| spl0_58 ),
inference(sat_conversion,[],[f837]) ).
cnf(s166,plain,
( spl0_3
| ~ spl0_48 ),
inference(sat_conversion,[],[f842]) ).
cnf(s189,plain,
( spl0_3
| ~ spl0_52 ),
inference(sat_conversion,[],[f865]) ).
cnf(s192,plain,
( spl0_3
| ~ spl0_58 ),
inference(sat_conversion,[],[f868]) ).
cnf(s193,plain,
( ~ spl0_2
| ~ spl0_137
| ~ spl0_138
| spl0_152 ),
inference(sat_conversion,[],[f875]) ).
cnf(s195,plain,
( ~ spl0_2
| ~ spl0_150
| ~ spl0_151
| spl0_154 ),
inference(sat_conversion,[],[f886]) ).
cnf(s198,plain,
( ~ spl0_11
| spl0_72
| ~ spl0_118
| ~ spl0_155 ),
inference(sat_conversion,[],[f907]) ).
cnf(s199,plain,
( ~ spl0_11
| spl0_101
| ~ spl0_138
| ~ spl0_152 ),
inference(sat_conversion,[],[f910]) ).
cnf(s200,plain,
( ~ spl0_7
| ~ spl0_11
| spl0_14 ),
inference(sat_conversion,[],[f911]) ).
cnf(s211,plain,
( ~ spl0_7
| spl0_13
| ~ spl0_15 ),
inference(sat_conversion,[],[f974]) ).
cnf(s217,plain,
( spl0_13
| ~ spl0_15
| ~ spl0_17 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s220,plain,
( ~ spl0_6
| ~ spl0_109
| ~ spl0_110
| spl0_160 ),
inference(sat_conversion,[],[f1025]) ).
cnf(s228,plain,
( ~ spl0_10
| spl0_97
| spl0_98
| ~ spl0_162 ),
inference(sat_conversion,[],[f1057]) ).
cnf(s232,plain,
( ~ spl0_10
| spl0_67
| ~ spl0_115
| spl0_158 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s242,plain,
( ~ spl0_8
| spl0_71
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s262,plain,
( ~ spl0_6
| spl0_89
| ~ spl0_131
| ~ spl0_132 ),
inference(sat_conversion,[],[f1178]) ).
cnf(s271,plain,
( ~ spl0_23
| ~ spl0_114
| ~ spl0_115
| ~ spl0_158 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s281,plain,
( ~ spl0_8
| spl0_81
| ~ spl0_127
| ~ spl0_166 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s284,plain,
( ~ spl0_1
| spl0_63
| ~ spl0_109
| ~ spl0_160 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s287,plain,
( ~ spl0_1
| spl0_82
| ~ spl0_127
| ~ spl0_166 ),
inference(sat_conversion,[],[f1241]) ).
cnf(s288,plain,
( ~ spl0_7
| spl0_63
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f1252]) ).
cnf(s289,plain,
( ~ spl0_7
| spl0_78
| ~ spl0_124
| ~ spl0_161 ),
inference(sat_conversion,[],[f1253]) ).
cnf(s290,plain,
( ~ spl0_7
| ~ spl0_131
| ~ spl0_132
| spl0_164 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s293,plain,
( ~ spl0_9
| spl0_67
| ~ spl0_114
| ~ spl0_115 ),
inference(sat_conversion,[],[f1269]) ).
cnf(s294,plain,
( ~ spl0_9
| spl0_97
| ~ spl0_135
| ~ spl0_162 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s296,plain,
( ~ spl0_13
| spl0_85
| spl0_86
| ~ spl0_129 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s298,plain,
( ~ spl0_13
| spl0_98
| ~ spl0_135
| spl0_162 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s303,plain,
( ~ spl0_1
| spl0_14
| ~ spl0_19 ),
inference(sat_conversion,[],[f1305]) ).
cnf(s304,plain,
( ~ spl0_17
| spl0_63
| ~ spl0_109
| spl0_160 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s305,plain,
( ~ spl0_17
| spl0_78
| spl0_79
| ~ spl0_124 ),
inference(sat_conversion,[],[f1319]) ).
cnf(s332,plain,
( ~ spl0_14
| spl0_64
| ~ spl0_111
| ~ spl0_112 ),
inference(sat_conversion,[],[f1370]) ).
cnf(s333,plain,
( ~ spl0_19
| spl0_72
| spl0_73
| ~ spl0_118 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s336,plain,
( ~ spl0_14
| spl0_73
| ~ spl0_118
| ~ spl0_155 ),
inference(sat_conversion,[],[f1395]) ).
cnf(s337,plain,
( ~ spl0_21
| spl0_78
| spl0_79
| spl0_161 ),
inference(sat_conversion,[],[f1410]) ).
cnf(s341,plain,
( ~ spl0_23
| ~ spl0_146
| ~ spl0_147
| ~ spl0_148 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s343,plain,
( ~ spl0_8
| ~ spl0_119
| ~ spl0_120
| spl0_170 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s344,plain,
( ~ spl0_1
| spl0_74
| ~ spl0_119
| ~ spl0_120 ),
inference(sat_conversion,[],[f1438]) ).
cnf(s354,plain,
( ~ spl0_12
| spl0_78
| ~ spl0_124
| spl0_161 ),
inference(sat_conversion,[],[f1447]) ).
cnf(s357,plain,
( ~ spl0_18
| spl0_79
| ~ spl0_124
| spl0_161 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s362,plain,
( ~ spl0_23
| ~ spl0_150
| ~ spl0_151
| ~ spl0_154 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s363,plain,
( ~ spl0_5
| spl0_89
| ~ spl0_131
| ~ spl0_164 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s365,plain,
( ~ spl0_5
| spl0_102
| ~ spl0_139
| ~ spl0_140 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s366,plain,
( ~ spl0_5
| spl0_106
| ~ spl0_142
| ~ spl0_169 ),
inference(sat_conversion,[],[f1484]) ).
cnf(s380,plain,
( ~ spl0_12
| spl0_81
| spl0_82
| ~ spl0_127 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s381,plain,
( ~ spl0_12
| spl0_105
| ~ spl0_142
| spl0_169 ),
inference(sat_conversion,[],[f1531]) ).
cnf(s397,plain,
( ~ spl0_21
| spl0_92
| spl0_93
| spl0_157 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s403,plain,
( ~ spl0_23
| ~ spl0_137
| ~ spl0_138
| ~ spl0_152 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s405,plain,
( ~ spl0_4
| ~ spl0_131
| ~ spl0_132
| ~ spl0_164 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s408,plain,
( ~ spl0_13
| spl0_63
| ~ spl0_110
| spl0_160 ),
inference(sat_conversion,[],[f1585]) ).
cnf(s409,plain,
( ~ spl0_13
| spl0_73
| ~ spl0_118
| spl0_155 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s434,plain,
( ~ spl0_13
| spl0_92
| spl0_93
| ~ spl0_157 ),
inference(sat_conversion,[],[f1608]) ).
cnf(s442,plain,
( ~ spl0_15
| spl0_72
| ~ spl0_118
| spl0_155 ),
inference(sat_conversion,[],[f1638]) ).
cnf(s447,plain,
( ~ spl0_18
| spl0_81
| ~ spl0_127
| spl0_166 ),
inference(sat_conversion,[],[f1668]) ).
cnf(s450,plain,
( ~ spl0_18
| spl0_105
| spl0_106
| ~ spl0_142 ),
inference(sat_conversion,[],[f1672]) ).
cnf(s456,plain,
( ~ spl0_17
| spl0_82
| ~ spl0_127
| spl0_166 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s457,plain,
( ~ spl0_17
| spl0_89
| ~ spl0_131
| spl0_164 ),
inference(sat_conversion,[],[f1691]) ).
cnf(s458,plain,
( ~ spl0_17
| spl0_106
| ~ spl0_142
| spl0_169 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s459,plain,
( ~ spl0_25
| ~ spl0_119
| ~ spl0_120
| ~ spl0_170 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s463,plain,
( ~ spl0_26
| spl0_68
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s464,plain,
( ~ spl0_26
| spl0_91
| spl0_92
| spl0_157 ),
inference(sat_conversion,[],[f1728]) ).
cnf(s466,plain,
( ~ spl0_17
| spl0_21
| ~ spl0_26 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s475,plain,
( ~ spl0_20
| spl0_68
| spl0_69
| spl0_163 ),
inference(sat_conversion,[],[f1753]) ).
cnf(s493,plain,
( ~ spl0_35
| spl0_68
| spl0_70
| ~ spl0_163 ),
inference(sat_conversion,[],[f1830]) ).
cnf(s495,plain,
( ~ spl0_35
| spl0_72
| spl0_73
| ~ spl0_155 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s499,plain,
spl0_3,
inference(rat,[],[s160,s166,s189,s192]) ).
cnf(s500,plain,
( spl0_8
| spl0_7
| spl0_13 ),
inference(rat,[],[s293,s69,s116,s117,s3,s29,s499]) ).
cnf(s501,plain,
( ~ spl0_42
| ~ spl0_9 ),
inference(rat,[],[s293,s69,s116,s117]) ).
cnf(s502,plain,
( ~ spl0_38
| ~ spl0_18
| ~ spl0_8 ),
inference(rat,[],[s447,s281,s83,s129]) ).
cnf(s503,plain,
( ~ spl0_24
| ~ spl0_8 ),
inference(rat,[],[s242,s73,s118,s119]) ).
cnf(s506,plain,
( ~ spl0_30
| ~ spl0_25
| ~ spl0_8 ),
inference(rat,[],[s343,s459,s121,s122]) ).
cnf(s507,plain,
( ~ spl0_8
| spl0_2 ),
inference(rat,[],[s333,s74,s75,s120,s46,s341,s148,s149,s150,s58,s506,s8,s456,s281,s380,s502,s83,s84,s129,s12,s51,s503,s499]) ).
cnf(s508,plain,
( spl0_13
| spl0_8
| spl0_1 ),
inference(rat,[],[s10,s337,s357,s289,s80,s81,s126,s26,s211,s500,s499]) ).
cnf(s509,plain,
( spl0_27
| spl0_1 ),
inference(rat,[],[s365,s104,s141,s142,s15,s53,s499]) ).
cnf(s510,plain,
( ~ spl0_164
| ~ spl0_22 ),
inference(rat,[],[s2,s363,s405,s262,s91,s133,s134,s499]) ).
cnf(s511,plain,
spl0_1,
inference(rat,[],[s41,s493,s463,s475,s502,s70,s71,s72,s8,s19,s457,s510,s38,s262,s333,s91,s133,s134,s74,s75,s120,s11,s46,s199,s403,s193,s507,s503,s508,s296,s87,s88,s131,s509,s103,s139,s140,s55,s499]) ).
cnf(s512,plain,
( ~ spl0_60
| ~ spl0_23 ),
inference(rat,[],[s341,s148,s149,s150]) ).
cnf(s513,plain,
~ spl0_30,
inference(rat,[],[s344,s76,s121,s122,s511]) ).
cnf(s514,plain,
( ~ spl0_38
| spl0_18 ),
inference(rat,[],[s333,s74,s75,s120,s46,s512,s8,s58,s456,s380,s287,s83,s84,s129,s499,s513,s511]) ).
cnf(s515,plain,
( ~ spl0_47
| ~ spl0_19 ),
inference(rat,[],[s333,s74,s75,s120]) ).
cnf(s516,plain,
( ~ spl0_54
| ~ spl0_23
| ~ spl0_2 ),
inference(rat,[],[s403,s193,s139,s140]) ).
cnf(s517,plain,
( ~ spl0_23
| spl0_38
| ~ spl0_2 ),
inference(rat,[],[s195,s362,s152,s153,s162,s516]) ).
cnf(s520,plain,
( ~ spl0_61
| ~ spl0_6 ),
inference(rat,[],[s284,s220,s65,s111,s112,s511]) ).
cnf(s521,plain,
( ~ spl0_50
| ~ spl0_14 ),
inference(rat,[],[s332,s66,s113,s114]) ).
cnf(s522,plain,
( spl0_63
| ~ spl0_109
| ~ spl0_17 ),
inference(rat,[],[s284,s304,s511]) ).
cnf(s523,plain,
( ~ spl0_61
| ~ spl0_17 ),
inference(rat,[],[s522,s65,s111]) ).
cnf(s524,plain,
( ~ spl0_22
| ~ spl0_17 ),
inference(rat,[],[s457,s510,s91,s133]) ).
cnf(s525,plain,
( spl0_18
| ~ spl0_8 ),
inference(rat,[],[s200,s14,s521,s59,s442,s198,s11,s524,s523,s8,s515,s74,s120,s46,s517,s514,s503,s507,s499]) ).
cnf(s526,plain,
( ~ spl0_17
| ~ spl0_8 ),
inference(rat,[],[s200,s14,s521,s59,s442,s198,s11,s524,s523,s503,s120,s74,s46,s517,s502,s525,s507,s499]) ).
cnf(s527,plain,
~ spl0_8,
inference(rat,[],[s262,s91,s133,s134,s11,s200,s14,s521,s59,s520,s38,s475,s442,s493,s495,s41,s463,s70,s71,s72,s19,s526,s74,s75,s120,s46,s517,s502,s525,s507,s503,s499]) ).
cnf(s528,plain,
( spl0_23
| ~ spl0_17 ),
inference(rat,[],[s200,s521,s500,s59,s409,s442,s198,s74,s75,s120,s11,s46,s523,s524,s527,s499]) ).
cnf(s530,plain,
( ~ spl0_14
| spl0_73
| ~ spl0_118
| spl0_72
| spl0_61 ),
inference(rat,[],[s442,s59,s336,s521,s499]) ).
cnf(s531,plain,
( spl0_73
| ~ spl0_118
| spl0_72
| ~ spl0_17
| spl0_38 ),
inference(rat,[],[s397,s434,s94,s95,s466,s23,s41,s495,s409,s6,s530,s523,s517,s528,s499]) ).
cnf(s533,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_47 ),
inference(rat,[],[s298,s294,s99,s100,s137,s155,s501]) ).
cnf(s539,plain,
( ~ spl0_57
| ~ spl0_13
| ~ spl0_10 ),
inference(rat,[],[s228,s298,s99,s100,s137]) ).
cnf(s540,plain,
( ~ spl0_42
| ~ spl0_10
| ~ spl0_23 ),
inference(rat,[],[s271,s232,s69,s116,s117]) ).
cnf(s541,plain,
( spl0_47
| spl0_19
| ~ spl0_23 ),
inference(rat,[],[s539,s155,s29,s540,s34,s499,s527]) ).
cnf(s542,plain,
( ~ spl0_47
| ~ spl0_17
| spl0_38 ),
inference(rat,[],[s531,s74,s75,s120]) ).
cnf(s544,plain,
( ~ spl0_10
| ~ spl0_13
| spl0_47
| ~ spl0_23 ),
inference(rat,[],[s155,s539,s540]) ).
cnf(s545,plain,
( ~ spl0_17
| spl0_38 ),
inference(rat,[],[s305,s80,s81,s126,s27,s544,s217,s59,s521,s303,s541,s542,s366,s458,s108,s144,s52,s517,s528,s523,s499,s511,s513]) ).
cnf(s546,plain,
( spl0_63
| ~ spl0_110
| ~ spl0_109 ),
inference(rat,[],[s408,s500,s284,s288,s511,s527]) ).
cnf(s547,plain,
~ spl0_61,
inference(rat,[],[s546,s65,s111,s112]) ).
cnf(s548,plain,
( spl0_13
| ~ spl0_15 ),
inference(rat,[],[s211,s500,s527]) ).
cnf(s549,plain,
spl0_18,
inference(rat,[],[s354,s289,s80,s126,s27,s3,s544,s533,s548,s59,s366,s381,s107,s108,s144,s52,s58,s517,s512,s46,s521,s515,s303,s8,s545,s514,s499,s527,s547,s513,s511]) ).
cnf(s551,plain,
( ~ spl0_22
| ~ spl0_7 ),
inference(rat,[],[s290,s510,s133,s134]) ).
cnf(s552,plain,
( spl0_13
| spl0_14 ),
inference(rat,[],[s380,s83,s84,s129,s58,s517,s512,s11,s551,s200,s6,s500,s499,s513,s527]) ).
cnf(s553,plain,
~ spl0_38,
inference(rat,[],[s447,s287,s83,s84,s129,s549,s511]) ).
cnf(s554,plain,
spl0_13,
inference(rat,[],[s521,s59,s552,s548,s499,s547]) ).
cnf(s555,plain,
( spl0_35
| spl0_14 ),
inference(rat,[],[s434,s464,s93,s94,s95,s41,s23,s553,s499,s554]) ).
cnf(s556,plain,
~ spl0_47,
inference(rat,[],[s555,s495,s530,s409,s74,s75,s120,s547,s554]) ).
cnf(s557,plain,
spl0_23,
inference(rat,[],[s46,s499,s556]) ).
cnf(s563,plain,
~ spl0_2,
inference(rat,[],[s517,s553,s557]) ).
cnf(s567,plain,
spl0_52,
inference(rat,[],[s52,s513,s499,s563]) ).
cnf(s571,plain,
spl0_142,
inference(rat,[],[s144,s567]) ).
cnf(s572,plain,
~ spl0_106,
inference(rat,[],[s108,s567]) ).
cnf(s573,plain,
~ spl0_105,
inference(rat,[],[s107,s567]) ).
cnf(s578,plain,
$false,
inference(rat,[],[s450,s571,s549,s572,s573]) ).
fof(f1837,plain,
$false,
inference(avatar_sat_refutation,[],[s578]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN475-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.08/0.18 % Computer : n015.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 16:14:17 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 2.21/0.72 % (2751948)Input is clausal, will run a generic CNF schedule.
% 2.21/0.72 % (2751959)dis-21_1_sil=8000:lcm=predicate:random_seed=2960144261: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)
% 2.21/0.72 % (2751959)First to succeed.
% 2.21/0.72 % (2751959)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2751948"
% 2.21/0.72 % (2751956)lrs+10_1_sil=8000:sp=occurrence:random_seed=2513881629:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.21/0.72 % (2751957)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=757338996:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.21/0.72 % (2751955)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2795985447:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.21/0.72 % (2751954)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=428504873:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.21/0.72 % (2751958)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2559308380:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.21/0.72 % (2751953)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=1072523766:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.21/0.72 % (2751957)Also succeeded, but the first one will report.
% 2.21/0.72 % (2751958)Also succeeded, but the first one will report.
% 2.21/0.72 % (2751956)Also succeeded, but the first one will report.
% 2.21/0.72 % (2751959)Refutation found. Thanks to Tanya!
% 2.21/0.72 % SZS status Unsatisfiable for theBenchmark
% 2.21/0.72 % SZS output start Proof for theBenchmark
% See solution above
% 2.57/0.91 % (2751959)------------------------------
% 2.57/0.91 % (2751959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.57/0.91 % (2751959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.91 % (2751959)CaDiCaL version: 2.1.3
% 2.57/0.91 % (2751959)Termination reason: Refutation
% 2.57/0.91 % (2751959)Time elapsed: 0.015 s
% 2.57/0.91 % (2751959)Peak memory usage: 90 MB
% 2.57/0.91 % (2751959)Instructions burned: 39 (million)
% 2.57/0.91 % (2751959)------------------------------
% 2.57/0.91 % (2751959)------------------------------
% 2.57/0.91 % (2751948)Success in time 0.305 s
% 2.57/0.91 % Vampire exiting
%------------------------------------------------------------------------------