%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN447-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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:51:44 PM UTC 2026
% Result : Unsatisfiable 0.83s 0.96s
% Output : Refutation 2.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 175
% Syntax : Number of formulae : 629 ( 26 unt; 101 def)
% Number of atoms : 1909 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2412 (1132 ~;1179 |; 0 &)
% ( 101 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 130 ( 129 usr; 126 prp; 0-1 aty)
% Number of functors : 20 ( 20 usr; 20 con; 0-0 aty)
% Number of variables : 87 ( 0 sgn 87 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp63
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( ~ hskp62
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f8,negated_conjecture,
( ~ hskp56
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f65,negated_conjecture,
( hskp0
| hskp29
| hskp30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f67,negated_conjecture,
( hskp39
| hskp17
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f69,negated_conjecture,
( hskp62
| hskp56
| hskp63 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f81,negated_conjecture,
( ~ hskp57
| c2_1(a1085) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp57
| c0_1(a1085) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp57
| c3_1(a1085) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f90,negated_conjecture,
( ~ hskp53
| c1_1(a1073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ hskp53
| c2_1(a1073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp53
| c0_1(a1073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f104,negated_conjecture,
( ~ hskp47
| c2_1(a1056) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ hskp47
| c1_1(a1056) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ hskp47
| c3_1(a1056) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f113,negated_conjecture,
( ~ hskp43
| c0_1(a1049) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f115,negated_conjecture,
( ~ hskp43
| c1_1(a1049) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ hskp42
| c1_1(a1046) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ hskp42
| c0_1(a1046) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f121,negated_conjecture,
( ~ hskp39
| c0_1(a1042) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ hskp39
| c2_1(a1042) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f126,negated_conjecture,
( ~ hskp37
| c0_1(a1037) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ hskp37
| c3_1(a1037) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f130,negated_conjecture,
( ~ hskp35
| c0_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f132,negated_conjecture,
( ~ hskp35
| c3_1(a1033) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f134,negated_conjecture,
( ~ hskp33
| c3_1(a1031) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
( ~ hskp33
| c2_1(a1031) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f140,negated_conjecture,
( ~ hskp30
| c3_1(a1022) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
( ~ hskp30
| c1_1(a1022) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
( ~ hskp29
| c2_1(a1021) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f152,negated_conjecture,
( ~ hskp19
| c1_1(a1079) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( ~ hskp18
| c2_1(a1078) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
( ~ hskp18
| c0_1(a1078) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
( ~ hskp17
| c3_1(a1077) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f158,negated_conjecture,
( ~ hskp15
| c3_1(a1059) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
( ~ hskp15
| c2_1(a1059) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
( ~ hskp13
| c0_1(a1048) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
( ~ hskp13
| c3_1(a1048) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f164,negated_conjecture,
( ~ hskp10
| c1_1(a1039) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
fof(f166,negated_conjecture,
( ~ hskp8
| c0_1(a1036) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f175,negated_conjecture,
( ~ hskp0
| c0_1(a1020) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f193,negated_conjecture,
( ~ c2_1(a1046)
| ~ hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause193) ).
fof(f197,negated_conjecture,
( ~ c1_1(a1042)
| ~ hskp39 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause197) ).
fof(f202,negated_conjecture,
( ~ c1_1(a1031)
| ~ hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause202) ).
fof(f206,negated_conjecture,
( ~ c1_1(a1021)
| ~ hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ c3_1(a1021)
| ~ hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause207) ).
fof(f223,negated_conjecture,
( ~ c0_1(a1080)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause223) ).
fof(f224,negated_conjecture,
( ~ c2_1(a1080)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause224) ).
fof(f226,negated_conjecture,
( ~ c0_1(a1079)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause226) ).
fof(f227,negated_conjecture,
( ~ c2_1(a1079)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause227) ).
fof(f228,negated_conjecture,
( ~ c1_1(a1078)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause228) ).
fof(f229,negated_conjecture,
( ~ c0_1(a1077)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause229) ).
fof(f230,negated_conjecture,
( ~ c2_1(a1077)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause230) ).
fof(f232,negated_conjecture,
( ~ c1_1(a1059)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause232) ).
fof(f241,negated_conjecture,
( ~ c2_1(a1039)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause241) ).
fof(f242,negated_conjecture,
( ~ c0_1(a1039)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause242) ).
fof(f245,negated_conjecture,
( ~ c3_1(a1036)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause245) ).
fof(f246,negated_conjecture,
( ~ c1_1(a1036)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause246) ).
fof(f260,negated_conjecture,
( ~ c1_1(a1020)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause260) ).
fof(f262,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause262) ).
fof(f266,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X0)
| hskp15
| hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause266) ).
fof(f269,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp19
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause269) ).
fof(f274,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp8
| hskp37 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause274) ).
fof(f276,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp13
| hskp43 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause276) ).
fof(f295,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c0_1(X1)
| hskp42 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause295) ).
fof(f298,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp35 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause298) ).
fof(f300,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| hskp33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause300) ).
fof(f303,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X1)
| hskp47 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause303) ).
fof(f304,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X1)
| hskp57 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause304) ).
fof(f309,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X0)
| hskp53 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause309) ).
fof(f311,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c0_1(X1)
| ~ c1_1(X0)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause311) ).
fof(f312,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c1_1(X2)
| c3_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause312) ).
fof(f313,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c0_1(X0)
| ~ c2_1(X1)
| c3_1(X2)
| c1_1(X2)
| c2_1(X2)
| c3_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause313) ).
fof(f316,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c3_1(X1)
| c1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause316) ).
fof(f318,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f319,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2)
| ~ c1_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f322,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f324,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f327,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f328,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f329,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f316,f327,f324,f321,f318]) ).
fof(f334,definition,
( spl0_6
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f335,plain,
( ! [X1] :
( c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f337,definition,
( spl0_7
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f338,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f341,definition,
( spl0_8
<=> ! [X2] :
( c0_1(X2)
| c1_1(X2)
| c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f342,plain,
( ! [X2] :
( c0_1(X2)
| c1_1(X2)
| c3_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f344,definition,
( spl0_9
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f345,plain,
( ! [X1] :
( c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f347,definition,
( spl0_10
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f348,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f351,definition,
( spl0_11
<=> ! [X2] :
( c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f352,plain,
( ! [X2] :
( c2_1(X2)
| c3_1(X2)
| c1_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f354,definition,
( spl0_12
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f355,plain,
( ! [X1] :
( c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f356,plain,
( spl0_11
| spl0_12
| spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f313,f324,f321,f354,f351]) ).
fof(f357,plain,
( spl0_8
| spl0_12
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f312,f337,f324,f354,f341]) ).
fof(f359,definition,
( spl0_13
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f360,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f362,definition,
( spl0_14
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f363,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f362]) ).
fof(f364,plain,
( ~ spl0_3
| spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f311,f362,f359,f324]) ).
fof(f369,definition,
( spl0_16
<=> ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f370,plain,
( ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,definition,
( spl0_17
<=> hskp53 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f376,definition,
( spl0_18
<=> ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f377,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f378,plain,
( spl0_17
| spl0_13
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f309,f376,f324,f359,f373]) ).
fof(f387,definition,
( spl0_21
<=> ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f388,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f402,definition,
( spl0_25
<=> hskp57 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f404,plain,
( spl0_25
| spl0_21
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f304,f376,f324,f387,f402]) ).
fof(f406,definition,
( spl0_26
<=> hskp47 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f409,definition,
( spl0_27
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f410,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,definition,
( spl0_28
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f413,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f414,plain,
( spl0_26
| spl0_27
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f303,f412,f324,f409,f406]) ).
fof(f430,definition,
( spl0_33
<=> hskp33 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f432,plain,
( spl0_33
| spl0_9
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f300,f318,f324,f344,f430]) ).
fof(f438,definition,
( spl0_35
<=> hskp35 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f440,plain,
( spl0_35
| spl0_6
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f298,f347,f324,f334,f438]) ).
fof(f445,definition,
( spl0_37
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f446,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f448,definition,
( spl0_38
<=> ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f449,plain,
( ! [X0] :
( c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f459,definition,
( spl0_41
<=> hskp42 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f461,plain,
( spl0_41
| spl0_12
| ~ spl0_3
| spl0_37 ),
inference(avatar_split_clause,[],[f295,f445,f324,f354,f459]) ).
fof(f470,definition,
( spl0_44
<=> ! [X1] :
( c3_1(X1)
| c0_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f471,plain,
( ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f514,definition,
( spl0_55
<=> hskp39 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f521,definition,
( spl0_57
<=> hskp56 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f543,definition,
( spl0_63
<=> hskp43 ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f546,definition,
( spl0_64
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f550,definition,
( spl0_65
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f552,plain,
( spl0_63
| spl0_65
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f276,f412,f324,f550,f543]) ).
fof(f561,definition,
( spl0_68
<=> hskp37 ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f564,definition,
( spl0_69
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f566,plain,
( spl0_68
| spl0_69
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f274,f369,f324,f564,f561]) ).
fof(f593,definition,
( spl0_77
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f596,definition,
( spl0_78
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f598,plain,
( spl0_77
| spl0_78
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f269,f321,f324,f596,f593]) ).
fof(f611,definition,
( spl0_82
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f613,plain,
( spl0_33
| spl0_82
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f266,f448,f324,f611,f430]) ).
fof(f626,plain,
( spl0_64
| spl0_44
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f262,f324,f470,f546]) ).
fof(f628,definition,
( spl0_86
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f635,definition,
( spl0_88
<=> c1_1(a1020) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f636,plain,
( ~ c1_1(a1020)
| spl0_88 ),
inference(avatar_component_clause,[],[f635]) ).
fof(f637,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f260,f635,f628]) ).
fof(f699,definition,
( spl0_102
<=> c1_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f700,plain,
( ~ c1_1(a1036)
| spl0_102 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f701,plain,
( ~ spl0_69
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f246,f699,f564]) ).
fof(f703,definition,
( spl0_103
<=> c3_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f704,plain,
( ~ c3_1(a1036)
| spl0_103 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f705,plain,
( ~ spl0_69
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f245,f703,f564]) ).
fof(f717,definition,
( spl0_106
<=> c0_1(a1039) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f718,plain,
( ~ c0_1(a1039)
| spl0_106 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f719,plain,
( ~ spl0_64
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f242,f717,f546]) ).
fof(f721,definition,
( spl0_107
<=> c2_1(a1039) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f722,plain,
( ~ c2_1(a1039)
| spl0_107 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f723,plain,
( ~ spl0_64
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f241,f721,f546]) ).
fof(f762,definition,
( spl0_116
<=> c1_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f763,plain,
( ~ c1_1(a1059)
| spl0_116 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f764,plain,
( ~ spl0_82
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f232,f762,f611]) ).
fof(f771,definition,
( spl0_118
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f774,definition,
( spl0_119
<=> c2_1(a1077) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f776,plain,
( ~ spl0_118
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f230,f774,f771]) ).
fof(f778,definition,
( spl0_120
<=> c0_1(a1077) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f779,plain,
( ~ c0_1(a1077)
| spl0_120 ),
inference(avatar_component_clause,[],[f778]) ).
fof(f780,plain,
( ~ spl0_118
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f229,f778,f771]) ).
fof(f782,definition,
( spl0_121
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f785,definition,
( spl0_122
<=> c1_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f786,plain,
( ~ c1_1(a1078)
| spl0_122 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f787,plain,
( ~ spl0_121
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f228,f785,f782]) ).
fof(f790,definition,
( spl0_123
<=> c2_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f791,plain,
( ~ c2_1(a1079)
| spl0_123 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f792,plain,
( ~ spl0_78
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f227,f790,f596]) ).
fof(f794,definition,
( spl0_124
<=> c0_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f795,plain,
( ~ c0_1(a1079)
| spl0_124 ),
inference(avatar_component_clause,[],[f794]) ).
fof(f796,plain,
( ~ spl0_78
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f226,f794,f596]) ).
fof(f803,definition,
( spl0_126
<=> c2_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f805,plain,
( ~ spl0_77
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f224,f803,f593]) ).
fof(f807,definition,
( spl0_127
<=> c0_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f808,plain,
( ~ c0_1(a1080)
| spl0_127 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f809,plain,
( ~ spl0_77
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f223,f807,f593]) ).
fof(f883,definition,
( spl0_145
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f886,definition,
( spl0_146
<=> c3_1(a1021) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f887,plain,
( ~ c3_1(a1021)
| spl0_146 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f888,plain,
( ~ spl0_145
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f207,f886,f883]) ).
fof(f890,definition,
( spl0_147
<=> c1_1(a1021) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f891,plain,
( ~ c1_1(a1021)
| spl0_147 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f892,plain,
( ~ spl0_145
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f206,f890,f883]) ).
fof(f894,definition,
( spl0_148
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f912,definition,
( spl0_152
<=> c1_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f914,plain,
( ~ spl0_33
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f202,f912,f430]) ).
fof(f936,definition,
( spl0_157
<=> c1_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f937,plain,
( ~ c1_1(a1042)
| spl0_157 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f938,plain,
( ~ spl0_55
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f197,f936,f514]) ).
fof(f955,definition,
( spl0_161
<=> c2_1(a1046) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f956,plain,
( ~ c2_1(a1046)
| spl0_161 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f957,plain,
( ~ spl0_41
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f193,f955,f459]) ).
fof(f1036,definition,
( spl0_179
<=> hskp63 ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f1043,definition,
( spl0_181
<=> c0_1(a1020) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1044,plain,
( c0_1(a1020)
| ~ spl0_181 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1045,plain,
( spl0_181
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f175,f628,f1043]) ).
fof(f1079,definition,
( spl0_190
<=> c0_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f1080,plain,
( c0_1(a1036)
| ~ spl0_190 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1081,plain,
( spl0_190
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f166,f564,f1079]) ).
fof(f1087,definition,
( spl0_192
<=> c1_1(a1039) ),
introduced(definition,[new_symbols(definition,[spl0_192])],[avatar_definition]) ).
fof(f1088,plain,
( c1_1(a1039)
| ~ spl0_192 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1089,plain,
( spl0_192
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f164,f546,f1087]) ).
fof(f1099,definition,
( spl0_195
<=> c3_1(a1048) ),
introduced(definition,[new_symbols(definition,[spl0_195])],[avatar_definition]) ).
fof(f1100,plain,
( c3_1(a1048)
| ~ spl0_195 ),
inference(avatar_component_clause,[],[f1099]) ).
fof(f1101,plain,
( spl0_195
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f161,f550,f1099]) ).
fof(f1103,definition,
( spl0_196
<=> c0_1(a1048) ),
introduced(definition,[new_symbols(definition,[spl0_196])],[avatar_definition]) ).
fof(f1104,plain,
( c0_1(a1048)
| ~ spl0_196 ),
inference(avatar_component_clause,[],[f1103]) ).
fof(f1105,plain,
( spl0_196
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f160,f550,f1103]) ).
fof(f1107,definition,
( spl0_197
<=> c2_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_197])],[avatar_definition]) ).
fof(f1108,plain,
( c2_1(a1059)
| ~ spl0_197 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1109,plain,
( spl0_197
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f159,f611,f1107]) ).
fof(f1111,definition,
( spl0_198
<=> c3_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_198])],[avatar_definition]) ).
fof(f1112,plain,
( c3_1(a1059)
| ~ spl0_198 ),
inference(avatar_component_clause,[],[f1111]) ).
fof(f1113,plain,
( spl0_198
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f158,f611,f1111]) ).
fof(f1123,definition,
( spl0_201
<=> c3_1(a1077) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f1125,plain,
( spl0_201
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f155,f771,f1123]) ).
fof(f1127,definition,
( spl0_202
<=> c0_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f1128,plain,
( c0_1(a1078)
| ~ spl0_202 ),
inference(avatar_component_clause,[],[f1127]) ).
fof(f1129,plain,
( spl0_202
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f154,f782,f1127]) ).
fof(f1131,definition,
( spl0_203
<=> c2_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f1132,plain,
( c2_1(a1078)
| ~ spl0_203 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1133,plain,
( spl0_203
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f153,f782,f1131]) ).
fof(f1135,definition,
( spl0_204
<=> c1_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f1137,plain,
( spl0_204
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f152,f596,f1135]) ).
fof(f1175,definition,
( spl0_214
<=> c2_1(a1021) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f1176,plain,
( c2_1(a1021)
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f1175]) ).
fof(f1177,plain,
( spl0_214
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f142,f883,f1175]) ).
fof(f1179,definition,
( spl0_215
<=> c1_1(a1022) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1180,plain,
( c1_1(a1022)
| ~ spl0_215 ),
inference(avatar_component_clause,[],[f1179]) ).
fof(f1181,plain,
( spl0_215
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f141,f894,f1179]) ).
fof(f1183,definition,
( spl0_216
<=> c3_1(a1022) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1184,plain,
( c3_1(a1022)
| ~ spl0_216 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1185,plain,
( spl0_216
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f140,f894,f1183]) ).
fof(f1203,definition,
( spl0_221
<=> c2_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f1204,plain,
( c2_1(a1031)
| ~ spl0_221 ),
inference(avatar_component_clause,[],[f1203]) ).
fof(f1205,plain,
( spl0_221
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f135,f430,f1203]) ).
fof(f1207,definition,
( spl0_222
<=> c3_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f1208,plain,
( c3_1(a1031)
| ~ spl0_222 ),
inference(avatar_component_clause,[],[f1207]) ).
fof(f1209,plain,
( spl0_222
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f134,f430,f1207]) ).
fof(f1215,definition,
( spl0_224
<=> c3_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f1216,plain,
( c3_1(a1033)
| ~ spl0_224 ),
inference(avatar_component_clause,[],[f1215]) ).
fof(f1218,plain,
( spl0_224
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f132,f438,f1215]) ).
fof(f1224,definition,
( spl0_226
<=> c0_1(a1033) ),
introduced(definition,[new_symbols(definition,[spl0_226])],[avatar_definition]) ).
fof(f1225,plain,
( c0_1(a1033)
| ~ spl0_226 ),
inference(avatar_component_clause,[],[f1224]) ).
fof(f1226,plain,
( spl0_226
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f130,f438,f1224]) ).
fof(f1236,definition,
( spl0_229
<=> c3_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f1238,plain,
( spl0_229
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f127,f561,f1236]) ).
fof(f1240,definition,
( spl0_230
<=> c0_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1241,plain,
( c0_1(a1037)
| ~ spl0_230 ),
inference(avatar_component_clause,[],[f1240]) ).
fof(f1242,plain,
( spl0_230
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f126,f561,f1240]) ).
fof(f1257,definition,
( spl0_234
<=> c2_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_234])],[avatar_definition]) ).
fof(f1258,plain,
( c2_1(a1042)
| ~ spl0_234 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1259,plain,
( spl0_234
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f122,f514,f1257]) ).
fof(f1261,definition,
( spl0_235
<=> c0_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_235])],[avatar_definition]) ).
fof(f1262,plain,
( c0_1(a1042)
| ~ spl0_235 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1263,plain,
( spl0_235
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f121,f514,f1261]) ).
fof(f1277,definition,
( spl0_239
<=> c0_1(a1046) ),
introduced(definition,[new_symbols(definition,[spl0_239])],[avatar_definition]) ).
fof(f1278,plain,
( c0_1(a1046)
| ~ spl0_239 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1279,plain,
( spl0_239
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f117,f459,f1277]) ).
fof(f1281,definition,
( spl0_240
<=> c1_1(a1046) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1283,plain,
( spl0_240
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f116,f459,f1281]) ).
fof(f1285,definition,
( spl0_241
<=> c1_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1286,plain,
( c1_1(a1049)
| ~ spl0_241 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1288,plain,
( spl0_241
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f115,f543,f1285]) ).
fof(f1294,definition,
( spl0_243
<=> c0_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f1295,plain,
( c0_1(a1049)
| ~ spl0_243 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1296,plain,
( spl0_243
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f113,f543,f1294]) ).
fof(f1323,definition,
( spl0_250
<=> c3_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_250])],[avatar_definition]) ).
fof(f1324,plain,
( c3_1(a1056)
| ~ spl0_250 ),
inference(avatar_component_clause,[],[f1323]) ).
fof(f1326,plain,
( spl0_250
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f106,f406,f1323]) ).
fof(f1328,definition,
( spl0_251
<=> c1_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f1329,plain,
( c1_1(a1056)
| ~ spl0_251 ),
inference(avatar_component_clause,[],[f1328]) ).
fof(f1330,plain,
( spl0_251
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f105,f406,f1328]) ).
fof(f1332,definition,
( spl0_252
<=> c2_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f1333,plain,
( c2_1(a1056)
| ~ spl0_252 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1334,plain,
( spl0_252
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f104,f406,f1332]) ).
fof(f1382,definition,
( spl0_264
<=> c0_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_264])],[avatar_definition]) ).
fof(f1383,plain,
( c0_1(a1073)
| ~ spl0_264 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1385,plain,
( spl0_264
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f92,f373,f1382]) ).
fof(f1387,definition,
( spl0_265
<=> c2_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_265])],[avatar_definition]) ).
fof(f1388,plain,
( c2_1(a1073)
| ~ spl0_265 ),
inference(avatar_component_clause,[],[f1387]) ).
fof(f1389,plain,
( spl0_265
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f91,f373,f1387]) ).
fof(f1391,definition,
( spl0_266
<=> c1_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_266])],[avatar_definition]) ).
fof(f1393,plain,
( spl0_266
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f90,f373,f1391]) ).
fof(f1420,definition,
( spl0_273
<=> c3_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_273])],[avatar_definition]) ).
fof(f1423,plain,
( spl0_273
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f83,f402,f1420]) ).
fof(f1425,definition,
( spl0_274
<=> c0_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_274])],[avatar_definition]) ).
fof(f1426,plain,
( c0_1(a1085)
| ~ spl0_274 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1427,plain,
( spl0_274
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f82,f402,f1425]) ).
fof(f1429,definition,
( spl0_275
<=> c2_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_275])],[avatar_definition]) ).
fof(f1430,plain,
( c2_1(a1085)
| ~ spl0_275 ),
inference(avatar_component_clause,[],[f1429]) ).
fof(f1431,plain,
( spl0_275
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f81,f402,f1429]) ).
fof(f1460,definition,
( spl0_283
<=> hskp62 ),
introduced(definition,[new_symbols(definition,[spl0_283])],[avatar_definition]) ).
fof(f1481,plain,
( spl0_179
| spl0_57
| spl0_283 ),
inference(avatar_split_clause,[],[f69,f1460,f521,f1036]) ).
fof(f1487,plain,
( spl0_121
| spl0_118
| spl0_55 ),
inference(avatar_split_clause,[],[f67,f514,f771,f782]) ).
fof(f1493,plain,
( spl0_148
| spl0_145
| spl0_86 ),
inference(avatar_split_clause,[],[f65,f628,f883,f894]) ).
fof(f1551,plain,
( spl0_3
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f8,f521,f324]) ).
fof(f1557,plain,
( spl0_3
| ~ spl0_283 ),
inference(avatar_split_clause,[],[f2,f1460,f324]) ).
fof(f1558,plain,
( spl0_3
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f1,f1036,f324]) ).
fof(f1559,plain,
( c1_1(a1020)
| c3_1(a1020)
| ~ spl0_2
| ~ spl0_181 ),
inference(resolution,[],[f322,f1044]) ).
fof(f1562,plain,
( c3_1(a1020)
| ~ spl0_2
| spl0_88
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f1559,f636]) ).
fof(f1591,plain,
( ! [X2] :
( c3_1(X2)
| c1_1(X2) )
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f352,f338]) ).
fof(f1614,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_13
| ~ spl0_16 ),
inference(resolution,[],[f370,f360]) ).
fof(f1621,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_13
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f1614]) ).
fof(f1624,plain,
( spl0_1
| ~ spl0_13
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1621,f369,f359,f318]) ).
fof(f1633,plain,
( c3_1(a1036)
| ~ c1_1(a1036)
| ~ spl0_4
| ~ spl0_190 ),
inference(resolution,[],[f1080,f328]) ).
fof(f1634,plain,
( c3_1(a1036)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_11
| ~ spl0_190 ),
inference(forward_subsumption_resolution,[],[f1633,f1591]) ).
fof(f1639,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_11
| spl0_103
| ~ spl0_190 ),
inference(forward_subsumption_resolution,[],[f1634,f704]) ).
fof(f1640,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_11
| spl0_103
| ~ spl0_190 ),
inference(avatar_contradiction_clause,[],[f1639]) ).
fof(f1646,plain,
( ~ c3_1(a1056)
| ~ c1_1(a1056)
| ~ spl0_1
| ~ spl0_252 ),
inference(resolution,[],[f319,f1333]) ).
fof(f1651,plain,
( ~ c1_1(a1056)
| ~ spl0_1
| ~ spl0_250
| ~ spl0_252 ),
inference(forward_subsumption_resolution,[],[f1646,f1324]) ).
fof(f1654,plain,
( $false
| ~ spl0_1
| ~ spl0_250
| ~ spl0_251
| ~ spl0_252 ),
inference(forward_subsumption_resolution,[],[f1651,f1329]) ).
fof(f1655,plain,
( ~ spl0_1
| ~ spl0_250
| ~ spl0_251
| ~ spl0_252 ),
inference(avatar_contradiction_clause,[],[f1654]) ).
fof(f1702,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_14
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f410,f363]) ).
fof(f1710,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f388,f360]) ).
fof(f1717,plain,
( ~ c3_1(a1020)
| ~ spl0_13
| ~ spl0_21
| ~ spl0_181 ),
inference(resolution,[],[f1710,f1044]) ).
fof(f1764,plain,
( ! [X1] :
( c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_10
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f446,f348]) ).
fof(f1788,plain,
( c2_1(a1077)
| ~ c3_1(a1077)
| ~ spl0_38
| spl0_120 ),
inference(resolution,[],[f449,f779]) ).
fof(f1808,plain,
( ~ c2_1(a1085)
| ~ c3_1(a1085)
| ~ spl0_13
| ~ spl0_274 ),
inference(resolution,[],[f1426,f360]) ).
fof(f1829,plain,
( ! [X0] :
( c0_1(X0)
| c2_1(X0) )
| ~ spl0_38
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f449,f471]) ).
fof(f1843,plain,
( c2_1(a1039)
| ~ c1_1(a1039)
| ~ spl0_9
| spl0_106 ),
inference(resolution,[],[f718,f345]) ).
fof(f1851,plain,
( c2_1(a1079)
| ~ c1_1(a1079)
| ~ spl0_9
| spl0_124 ),
inference(resolution,[],[f795,f345]) ).
fof(f1854,plain,
( ~ c2_1(a1078)
| ~ spl0_14
| ~ spl0_27
| ~ spl0_202 ),
inference(resolution,[],[f1128,f1702]) ).
fof(f1860,definition,
( spl0_294
<=> c3_1(a1078) ),
introduced(definition,[new_symbols(definition,[spl0_294])],[avatar_definition]) ).
fof(f1864,plain,
( ~ spl0_203
| ~ spl0_14
| ~ spl0_27
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f1854,f1127,f409,f362,f1131]) ).
fof(f1867,plain,
( ~ c2_1(a1042)
| ~ spl0_14
| ~ spl0_27
| ~ spl0_235 ),
inference(resolution,[],[f1262,f1702]) ).
fof(f1869,plain,
( ~ c2_1(a1042)
| ~ c3_1(a1042)
| ~ spl0_13
| ~ spl0_235 ),
inference(resolution,[],[f1262,f360]) ).
fof(f1872,plain,
( ~ c3_1(a1042)
| ~ spl0_13
| ~ spl0_234
| ~ spl0_235 ),
inference(forward_subsumption_resolution,[],[f1869,f1258]) ).
fof(f1873,plain,
( $false
| ~ spl0_14
| ~ spl0_27
| ~ spl0_234
| ~ spl0_235 ),
inference(forward_subsumption_resolution,[],[f1867,f1258]) ).
fof(f1874,plain,
( ~ spl0_14
| ~ spl0_27
| ~ spl0_234
| ~ spl0_235 ),
inference(avatar_contradiction_clause,[],[f1873]) ).
fof(f1875,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_13
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f413,f360]) ).
fof(f1882,plain,
( ! [X2] :
( ~ c3_1(X2)
| ~ c1_1(X2) )
| ~ spl0_1
| ~ spl0_10
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f319,f1764]) ).
fof(f1909,plain,
( ~ spl0_201
| spl0_119
| ~ spl0_38
| spl0_120 ),
inference(avatar_split_clause,[],[f1788,f778,f448,f774,f1123]) ).
fof(f1948,plain,
( ~ c3_1(a1049)
| ~ spl0_13
| ~ spl0_21
| ~ spl0_243 ),
inference(resolution,[],[f1710,f1295]) ).
fof(f1950,plain,
( ~ c3_1(a1037)
| ~ spl0_13
| ~ spl0_21
| ~ spl0_230 ),
inference(resolution,[],[f1710,f1241]) ).
fof(f1954,plain,
( ~ spl0_229
| ~ spl0_13
| ~ spl0_21
| ~ spl0_230 ),
inference(avatar_split_clause,[],[f1950,f1240,f387,f359,f1236]) ).
fof(f1991,plain,
( c2_1(a1080)
| ~ spl0_38
| ~ spl0_44
| spl0_127 ),
inference(resolution,[],[f1829,f808]) ).
fof(f2006,plain,
( c1_1(a1020)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| ~ spl0_21
| ~ spl0_181 ),
inference(resolution,[],[f1717,f1591]) ).
fof(f2007,plain,
( $false
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| ~ spl0_21
| spl0_88
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2006,f636]) ).
fof(f2008,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| ~ spl0_21
| spl0_88
| ~ spl0_181 ),
inference(avatar_contradiction_clause,[],[f2007]) ).
fof(f2014,plain,
( c1_1(a1021)
| c3_1(a1021)
| ~ spl0_7
| ~ spl0_214 ),
inference(resolution,[],[f1176,f338]) ).
fof(f2017,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_8
| ~ spl0_13
| ~ spl0_28 ),
inference(resolution,[],[f1875,f342]) ).
fof(f2059,plain,
( ~ c1_1(a1039)
| ~ spl0_9
| spl0_106
| spl0_107 ),
inference(forward_subsumption_resolution,[],[f1843,f722]) ).
fof(f2060,plain,
( ~ c1_1(a1079)
| ~ spl0_9
| spl0_123
| spl0_124 ),
inference(forward_subsumption_resolution,[],[f1851,f791]) ).
fof(f2065,plain,
( $false
| ~ spl0_9
| spl0_106
| spl0_107
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f2059,f1088]) ).
fof(f2066,plain,
( ~ spl0_9
| spl0_106
| spl0_107
| ~ spl0_192 ),
inference(avatar_contradiction_clause,[],[f2065]) ).
fof(f2069,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_2
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f322,f1710]) ).
fof(f2076,plain,
( spl0_126
| ~ spl0_38
| ~ spl0_44
| spl0_127 ),
inference(avatar_split_clause,[],[f1991,f807,f470,f448,f803]) ).
fof(f2083,plain,
( ~ c1_1(a1046)
| c3_1(a1046)
| ~ spl0_10
| spl0_161 ),
inference(resolution,[],[f956,f348]) ).
fof(f2086,plain,
( ~ c3_1(a1046)
| ~ spl0_13
| ~ spl0_21
| ~ spl0_239 ),
inference(resolution,[],[f1278,f1710]) ).
fof(f2103,plain,
( c1_1(a1042)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| ~ spl0_234
| ~ spl0_235 ),
inference(resolution,[],[f1872,f1591]) ).
fof(f2104,plain,
( $false
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| spl0_157
| ~ spl0_234
| ~ spl0_235 ),
inference(forward_subsumption_resolution,[],[f2103,f937]) ).
fof(f2105,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| spl0_157
| ~ spl0_234
| ~ spl0_235 ),
inference(avatar_contradiction_clause,[],[f2104]) ).
fof(f2187,plain,
( c1_1(a1042)
| ~ spl0_2
| ~ spl0_13
| ~ spl0_21
| ~ spl0_235 ),
inference(resolution,[],[f2069,f1262]) ).
fof(f2303,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f377,f319]) ).
fof(f2306,definition,
( spl0_302
<=> c3_1(a1042) ),
introduced(definition,[new_symbols(definition,[spl0_302])],[avatar_definition]) ).
fof(f2310,definition,
( spl0_303
<=> c3_1(a1020) ),
introduced(definition,[new_symbols(definition,[spl0_303])],[avatar_definition]) ).
fof(f2348,plain,
( ~ c3_1(a1085)
| ~ spl0_13
| ~ spl0_274
| ~ spl0_275 ),
inference(forward_subsumption_resolution,[],[f1808,f1430]) ).
fof(f2352,definition,
( spl0_304
<=> c3_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_304])],[avatar_definition]) ).
fof(f2353,plain,
( ~ c3_1(a1049)
| spl0_304 ),
inference(avatar_component_clause,[],[f2352]) ).
fof(f2469,plain,
( ~ c2_1(a1073)
| ~ c1_1(a1073)
| ~ spl0_14
| ~ spl0_264 ),
inference(resolution,[],[f363,f1383]) ).
fof(f2487,plain,
( ~ c1_1(a1073)
| ~ spl0_14
| ~ spl0_264
| ~ spl0_265 ),
inference(forward_subsumption_resolution,[],[f2469,f1388]) ).
fof(f2494,plain,
( c3_1(a1042)
| ~ spl0_302 ),
inference(avatar_component_clause,[],[f2306]) ).
fof(f2504,plain,
( ~ spl0_266
| ~ spl0_14
| ~ spl0_264
| ~ spl0_265 ),
inference(avatar_split_clause,[],[f2487,f1387,f1382,f362,f1391]) ).
fof(f2523,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1) )
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f322,f342]) ).
fof(f2611,plain,
( c1_1(a1021)
| ~ spl0_2
| ~ spl0_8
| spl0_146 ),
inference(resolution,[],[f2523,f887]) ).
fof(f2620,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| spl0_146
| spl0_147 ),
inference(forward_subsumption_resolution,[],[f2611,f891]) ).
fof(f2621,plain,
( ~ spl0_2
| ~ spl0_8
| spl0_146
| spl0_147 ),
inference(avatar_contradiction_clause,[],[f2620]) ).
fof(f3035,plain,
( ~ spl0_304
| ~ spl0_13
| ~ spl0_21
| ~ spl0_243 ),
inference(avatar_split_clause,[],[f1948,f1294,f387,f359,f2352]) ).
fof(f3036,plain,
( ~ spl0_273
| ~ spl0_13
| ~ spl0_274
| ~ spl0_275 ),
inference(avatar_split_clause,[],[f2348,f1429,f1425,f359,f1420]) ).
fof(f3053,plain,
( ~ c2_1(a1078)
| ~ spl0_13
| ~ spl0_28
| ~ spl0_202 ),
inference(resolution,[],[f1875,f1128]) ).
fof(f3062,plain,
( $false
| ~ spl0_13
| ~ spl0_28
| ~ spl0_202
| ~ spl0_203 ),
inference(forward_subsumption_resolution,[],[f3053,f1132]) ).
fof(f3063,plain,
( ~ spl0_13
| ~ spl0_28
| ~ spl0_202
| ~ spl0_203 ),
inference(avatar_contradiction_clause,[],[f3062]) ).
fof(f3207,plain,
( ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_8
| ~ spl0_27 ),
inference(resolution,[],[f410,f342]) ).
fof(f3215,plain,
( c1_1(a1042)
| ~ c2_1(a1042)
| ~ spl0_27
| ~ spl0_235 ),
inference(resolution,[],[f410,f1262]) ).
fof(f3218,plain,
( c1_1(a1078)
| ~ c2_1(a1078)
| ~ spl0_27
| ~ spl0_202 ),
inference(resolution,[],[f410,f1128]) ).
fof(f3225,plain,
( ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_8
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f3207]) ).
fof(f3230,plain,
( ~ c2_1(a1078)
| ~ spl0_27
| spl0_122
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f3218,f786]) ).
fof(f3232,plain,
( ~ c2_1(a1042)
| ~ spl0_27
| spl0_157
| ~ spl0_235 ),
inference(forward_subsumption_resolution,[],[f3215,f937]) ).
fof(f3238,plain,
( $false
| ~ spl0_27
| spl0_122
| ~ spl0_202
| ~ spl0_203 ),
inference(forward_subsumption_resolution,[],[f3230,f1132]) ).
fof(f3239,plain,
( ~ spl0_27
| spl0_122
| ~ spl0_202
| ~ spl0_203 ),
inference(avatar_contradiction_clause,[],[f3238]) ).
fof(f3240,plain,
( $false
| ~ spl0_27
| spl0_157
| ~ spl0_234
| ~ spl0_235 ),
inference(forward_subsumption_resolution,[],[f3232,f1258]) ).
fof(f3241,plain,
( ~ spl0_27
| spl0_157
| ~ spl0_234
| ~ spl0_235 ),
inference(avatar_contradiction_clause,[],[f3240]) ).
fof(f3256,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_18
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f413,f2303]) ).
fof(f3345,plain,
( ~ c2_1(a1042)
| ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_235 ),
inference(resolution,[],[f3256,f1262]) ).
fof(f3349,plain,
( ~ c2_1(a1078)
| ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_202 ),
inference(resolution,[],[f3256,f1128]) ).
fof(f3359,plain,
( $false
| ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_202
| ~ spl0_203 ),
inference(forward_subsumption_resolution,[],[f3349,f1132]) ).
fof(f3360,plain,
( ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_202
| ~ spl0_203 ),
inference(avatar_contradiction_clause,[],[f3359]) ).
fof(f3362,plain,
( $false
| ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_234
| ~ spl0_235 ),
inference(forward_subsumption_resolution,[],[f3345,f1258]) ).
fof(f3363,plain,
( ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_234
| ~ spl0_235 ),
inference(avatar_contradiction_clause,[],[f3362]) ).
fof(f3396,plain,
( ~ c3_1(a1033)
| ~ spl0_13
| ~ spl0_21
| ~ spl0_226 ),
inference(resolution,[],[f1710,f1225]) ).
fof(f3399,plain,
( ~ c3_1(a1048)
| ~ spl0_13
| ~ spl0_21
| ~ spl0_196 ),
inference(resolution,[],[f1710,f1104]) ).
fof(f3405,plain,
( $false
| ~ spl0_13
| ~ spl0_21
| ~ spl0_224
| ~ spl0_226 ),
inference(forward_subsumption_resolution,[],[f3396,f1216]) ).
fof(f3406,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_224
| ~ spl0_226 ),
inference(avatar_contradiction_clause,[],[f3405]) ).
fof(f3413,plain,
( c3_1(a1021)
| ~ spl0_7
| spl0_147
| ~ spl0_214 ),
inference(forward_subsumption_resolution,[],[f2014,f891]) ).
fof(f3427,plain,
( $false
| ~ spl0_7
| spl0_146
| spl0_147
| ~ spl0_214 ),
inference(forward_subsumption_resolution,[],[f3413,f887]) ).
fof(f3428,plain,
( ~ spl0_7
| spl0_146
| spl0_147
| ~ spl0_214 ),
inference(avatar_contradiction_clause,[],[f3427]) ).
fof(f3557,plain,
( ~ c1_1(a1046)
| ~ spl0_10
| ~ spl0_13
| ~ spl0_21
| spl0_161
| ~ spl0_239 ),
inference(forward_subsumption_resolution,[],[f2083,f2086]) ).
fof(f3559,plain,
( ~ spl0_240
| ~ spl0_10
| ~ spl0_13
| ~ spl0_21
| spl0_161
| ~ spl0_239 ),
inference(avatar_split_clause,[],[f3557,f1277,f955,f387,f359,f347,f1281]) ).
fof(f3608,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f3225,f409,f341,f337]) ).
fof(f3698,plain,
( ~ spl0_204
| ~ spl0_9
| spl0_123
| spl0_124 ),
inference(avatar_split_clause,[],[f2060,f794,f790,f344,f1135]) ).
fof(f3703,plain,
( ~ spl0_303
| ~ spl0_13
| ~ spl0_21
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f1717,f1043,f387,f359,f2310]) ).
fof(f3715,plain,
( ~ c1_1(a1022)
| ~ spl0_1
| ~ spl0_10
| ~ spl0_37
| ~ spl0_216 ),
inference(resolution,[],[f1882,f1184]) ).
fof(f3723,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| ~ spl0_37
| ~ spl0_215
| ~ spl0_216 ),
inference(forward_subsumption_resolution,[],[f3715,f1180]) ).
fof(f3724,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_37
| ~ spl0_215
| ~ spl0_216 ),
inference(avatar_contradiction_clause,[],[f3723]) ).
fof(f3839,plain,
( c3_1(a1049)
| ~ c1_1(a1049)
| ~ spl0_4
| ~ spl0_243 ),
inference(resolution,[],[f328,f1295]) ).
fof(f3851,plain,
( ~ c1_1(a1049)
| ~ spl0_4
| ~ spl0_243
| spl0_304 ),
inference(forward_subsumption_resolution,[],[f3839,f2353]) ).
fof(f3859,plain,
( $false
| ~ spl0_4
| ~ spl0_241
| ~ spl0_243
| spl0_304 ),
inference(forward_subsumption_resolution,[],[f3851,f1286]) ).
fof(f3860,plain,
( ~ spl0_4
| ~ spl0_241
| ~ spl0_243
| spl0_304 ),
inference(avatar_contradiction_clause,[],[f3859]) ).
fof(f3979,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_12
| ~ spl0_13 ),
inference(resolution,[],[f360,f355]) ).
fof(f3994,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_12
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f3979]) ).
fof(f4018,plain,
( spl0_303
| ~ spl0_2
| spl0_88
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f1562,f1043,f635,f321,f2310]) ).
fof(f4067,plain,
( spl0_18
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f3994,f359,f354,f376]) ).
fof(f4117,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_13
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f2017,f412,f359,f341,f337]) ).
fof(f4207,plain,
( $false
| ~ spl0_13
| ~ spl0_21
| ~ spl0_195
| ~ spl0_196 ),
inference(forward_subsumption_resolution,[],[f3399,f1100]) ).
fof(f4208,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_195
| ~ spl0_196 ),
inference(avatar_contradiction_clause,[],[f4207]) ).
fof(f4222,plain,
( spl0_157
| ~ spl0_2
| ~ spl0_13
| ~ spl0_21
| ~ spl0_235 ),
inference(avatar_split_clause,[],[f2187,f1261,f387,f359,f321,f936]) ).
fof(f4311,plain,
( c1_1(a1042)
| c3_1(a1042)
| ~ spl0_2
| ~ spl0_235 ),
inference(resolution,[],[f322,f1262]) ).
fof(f4314,plain,
( c1_1(a1078)
| c3_1(a1078)
| ~ spl0_2
| ~ spl0_202 ),
inference(resolution,[],[f322,f1128]) ).
fof(f4316,plain,
( c1_1(a1036)
| c3_1(a1036)
| ~ spl0_2
| ~ spl0_190 ),
inference(resolution,[],[f322,f1080]) ).
fof(f4319,plain,
( c3_1(a1036)
| ~ spl0_2
| spl0_102
| ~ spl0_190 ),
inference(forward_subsumption_resolution,[],[f4316,f700]) ).
fof(f4329,plain,
( $false
| ~ spl0_2
| spl0_102
| spl0_103
| ~ spl0_190 ),
inference(forward_subsumption_resolution,[],[f4319,f704]) ).
fof(f4330,plain,
( ~ spl0_2
| spl0_102
| spl0_103
| ~ spl0_190 ),
inference(avatar_contradiction_clause,[],[f4329]) ).
fof(f4390,plain,
( spl0_302
| spl0_157
| ~ spl0_2
| ~ spl0_235 ),
inference(avatar_split_clause,[],[f4311,f1261,f321,f936,f2306]) ).
fof(f4576,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f335,f360]) ).
fof(f4601,plain,
( ~ c3_1(a1031)
| ~ spl0_6
| ~ spl0_13
| ~ spl0_221 ),
inference(resolution,[],[f4576,f1204]) ).
fof(f4606,plain,
( ~ c3_1(a1059)
| ~ spl0_6
| ~ spl0_13
| ~ spl0_197 ),
inference(resolution,[],[f4576,f1108]) ).
fof(f4612,plain,
( $false
| ~ spl0_6
| ~ spl0_13
| ~ spl0_197
| ~ spl0_198 ),
inference(forward_subsumption_resolution,[],[f4606,f1112]) ).
fof(f4613,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_197
| ~ spl0_198 ),
inference(avatar_contradiction_clause,[],[f4612]) ).
fof(f4617,plain,
( $false
| ~ spl0_6
| ~ spl0_13
| ~ spl0_221
| ~ spl0_222 ),
inference(forward_subsumption_resolution,[],[f4601,f1208]) ).
fof(f4618,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_221
| ~ spl0_222 ),
inference(avatar_contradiction_clause,[],[f4617]) ).
fof(f4794,plain,
( c1_1(a1031)
| ~ c3_1(a1031)
| ~ spl0_18
| ~ spl0_221 ),
inference(resolution,[],[f377,f1204]) ).
fof(f4799,plain,
( c1_1(a1059)
| ~ c3_1(a1059)
| ~ spl0_18
| ~ spl0_197 ),
inference(resolution,[],[f377,f1108]) ).
fof(f4807,plain,
( ~ c3_1(a1059)
| ~ spl0_18
| spl0_116
| ~ spl0_197 ),
inference(forward_subsumption_resolution,[],[f4799,f763]) ).
fof(f4817,plain,
( $false
| ~ spl0_18
| spl0_116
| ~ spl0_197
| ~ spl0_198 ),
inference(forward_subsumption_resolution,[],[f4807,f1112]) ).
fof(f4818,plain,
( ~ spl0_18
| spl0_116
| ~ spl0_197
| ~ spl0_198 ),
inference(avatar_contradiction_clause,[],[f4817]) ).
fof(f4829,plain,
( spl0_294
| spl0_122
| ~ spl0_2
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f4314,f1127,f321,f785,f1860]) ).
fof(f4867,plain,
( c1_1(a1031)
| ~ spl0_18
| ~ spl0_221
| ~ spl0_222 ),
inference(forward_subsumption_resolution,[],[f4794,f1208]) ).
fof(f4874,plain,
( spl0_152
| ~ spl0_18
| ~ spl0_221
| ~ spl0_222 ),
inference(avatar_split_clause,[],[f4867,f1207,f1203,f376,f912]) ).
fof(f4876,plain,
( c1_1(a1042)
| ~ c3_1(a1042)
| ~ spl0_18
| ~ spl0_234 ),
inference(resolution,[],[f1258,f377]) ).
fof(f4877,plain,
( ~ c3_1(a1042)
| ~ spl0_18
| spl0_157
| ~ spl0_234 ),
inference(forward_subsumption_resolution,[],[f4876,f937]) ).
fof(f4878,plain,
( $false
| ~ spl0_18
| spl0_157
| ~ spl0_234
| ~ spl0_302 ),
inference(forward_subsumption_resolution,[],[f4877,f2494]) ).
fof(f4879,plain,
( ~ spl0_18
| spl0_157
| ~ spl0_234
| ~ spl0_302 ),
inference(avatar_contradiction_clause,[],[f4878]) ).
fof(f4884,plain,
( c1_1(a1078)
| ~ c3_1(a1078)
| ~ spl0_18
| ~ spl0_203 ),
inference(resolution,[],[f1132,f377]) ).
fof(f4885,plain,
( ~ c3_1(a1078)
| ~ spl0_18
| spl0_122
| ~ spl0_203 ),
inference(forward_subsumption_resolution,[],[f4884,f786]) ).
fof(f4886,plain,
( ~ spl0_294
| ~ spl0_18
| spl0_122
| ~ spl0_203 ),
inference(avatar_split_clause,[],[f4885,f1131,f785,f376,f1860]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f329]) ).
cnf(s4,plain,
( spl0_2
| ~ spl0_3
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f356]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_7
| spl0_8
| spl0_12 ),
inference(sat_conversion,[],[f357]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f364]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_13
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f378]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_18
| spl0_21
| spl0_25 ),
inference(sat_conversion,[],[f404]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f414]) ).
cnf(s17,plain,
( spl0_1
| ~ spl0_3
| spl0_9
| spl0_33 ),
inference(sat_conversion,[],[f432]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_6
| spl0_10
| spl0_35 ),
inference(sat_conversion,[],[f440]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_12
| spl0_37
| spl0_41 ),
inference(sat_conversion,[],[f461]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_28
| spl0_63
| spl0_65 ),
inference(sat_conversion,[],[f552]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_16
| spl0_68
| spl0_69 ),
inference(sat_conversion,[],[f566]) ).
cnf(s48,plain,
( spl0_2
| ~ spl0_3
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f598]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_33
| spl0_38
| spl0_82 ),
inference(sat_conversion,[],[f613]) ).
cnf(s55,plain,
( ~ spl0_3
| spl0_44
| spl0_64 ),
inference(sat_conversion,[],[f626]) ).
cnf(s57,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(sat_conversion,[],[f637]) ).
cnf(s71,plain,
( ~ spl0_69
| ~ spl0_102 ),
inference(sat_conversion,[],[f701]) ).
cnf(s72,plain,
( ~ spl0_69
| ~ spl0_103 ),
inference(sat_conversion,[],[f705]) ).
cnf(s75,plain,
( ~ spl0_64
| ~ spl0_106 ),
inference(sat_conversion,[],[f719]) ).
cnf(s76,plain,
( ~ spl0_64
| ~ spl0_107 ),
inference(sat_conversion,[],[f723]) ).
cnf(s85,plain,
( ~ spl0_82
| ~ spl0_116 ),
inference(sat_conversion,[],[f764]) ).
cnf(s87,plain,
( ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f776]) ).
cnf(s88,plain,
( ~ spl0_118
| ~ spl0_120 ),
inference(sat_conversion,[],[f780]) ).
cnf(s89,plain,
( ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f787]) ).
cnf(s90,plain,
( ~ spl0_78
| ~ spl0_123 ),
inference(sat_conversion,[],[f792]) ).
cnf(s91,plain,
( ~ spl0_78
| ~ spl0_124 ),
inference(sat_conversion,[],[f796]) ).
cnf(s93,plain,
( ~ spl0_77
| ~ spl0_126 ),
inference(sat_conversion,[],[f805]) ).
cnf(s94,plain,
( ~ spl0_77
| ~ spl0_127 ),
inference(sat_conversion,[],[f809]) ).
cnf(s110,plain,
( ~ spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f888]) ).
cnf(s111,plain,
( ~ spl0_145
| ~ spl0_147 ),
inference(sat_conversion,[],[f892]) ).
cnf(s115,plain,
( ~ spl0_33
| ~ spl0_152 ),
inference(sat_conversion,[],[f914]) ).
cnf(s120,plain,
( ~ spl0_55
| ~ spl0_157 ),
inference(sat_conversion,[],[f938]) ).
cnf(s124,plain,
( ~ spl0_41
| ~ spl0_161 ),
inference(sat_conversion,[],[f957]) ).
cnf(s142,plain,
( ~ spl0_86
| spl0_181 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s151,plain,
( ~ spl0_69
| spl0_190 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s153,plain,
( ~ spl0_64
| spl0_192 ),
inference(sat_conversion,[],[f1089]) ).
cnf(s156,plain,
( ~ spl0_65
| spl0_195 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s157,plain,
( ~ spl0_65
| spl0_196 ),
inference(sat_conversion,[],[f1105]) ).
cnf(s158,plain,
( ~ spl0_82
| spl0_197 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s159,plain,
( ~ spl0_82
| spl0_198 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s162,plain,
( ~ spl0_118
| spl0_201 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s163,plain,
( ~ spl0_121
| spl0_202 ),
inference(sat_conversion,[],[f1129]) ).
cnf(s164,plain,
( ~ spl0_121
| spl0_203 ),
inference(sat_conversion,[],[f1133]) ).
cnf(s165,plain,
( ~ spl0_78
| spl0_204 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s175,plain,
( ~ spl0_145
| spl0_214 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s176,plain,
( ~ spl0_148
| spl0_215 ),
inference(sat_conversion,[],[f1181]) ).
cnf(s177,plain,
( ~ spl0_148
| spl0_216 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s182,plain,
( ~ spl0_33
| spl0_221 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s183,plain,
( ~ spl0_33
| spl0_222 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s185,plain,
( ~ spl0_35
| spl0_224 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s187,plain,
( ~ spl0_35
| spl0_226 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s190,plain,
( ~ spl0_68
| spl0_229 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s191,plain,
( ~ spl0_68
| spl0_230 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s195,plain,
( ~ spl0_55
| spl0_234 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s196,plain,
( ~ spl0_55
| spl0_235 ),
inference(sat_conversion,[],[f1263]) ).
cnf(s200,plain,
( ~ spl0_41
| spl0_239 ),
inference(sat_conversion,[],[f1279]) ).
cnf(s201,plain,
( ~ spl0_41
| spl0_240 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s202,plain,
( ~ spl0_63
| spl0_241 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s204,plain,
( ~ spl0_63
| spl0_243 ),
inference(sat_conversion,[],[f1296]) ).
cnf(s211,plain,
( ~ spl0_26
| spl0_250 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s212,plain,
( ~ spl0_26
| spl0_251 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s213,plain,
( ~ spl0_26
| spl0_252 ),
inference(sat_conversion,[],[f1334]) ).
cnf(s225,plain,
( ~ spl0_17
| spl0_264 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s226,plain,
( ~ spl0_17
| spl0_265 ),
inference(sat_conversion,[],[f1389]) ).
cnf(s227,plain,
( ~ spl0_17
| spl0_266 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s234,plain,
( ~ spl0_25
| spl0_273 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s235,plain,
( ~ spl0_25
| spl0_274 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s236,plain,
( ~ spl0_25
| spl0_275 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s248,plain,
( spl0_57
| spl0_179
| spl0_283 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s250,plain,
( spl0_55
| spl0_118
| spl0_121 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s252,plain,
( spl0_86
| spl0_145
| spl0_148 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s309,plain,
( spl0_3
| ~ spl0_57 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s315,plain,
( spl0_3
| ~ spl0_283 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s316,plain,
( spl0_3
| ~ spl0_179 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s322,plain,
( spl0_1
| ~ spl0_13
| ~ spl0_16 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s327,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_11
| spl0_103
| ~ spl0_190 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s329,plain,
( ~ spl0_1
| ~ spl0_250
| ~ spl0_251
| ~ spl0_252 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s354,plain,
( ~ spl0_14
| ~ spl0_27
| ~ spl0_202
| ~ spl0_203 ),
inference(sat_conversion,[],[f1864]) ).
cnf(s355,plain,
( ~ spl0_14
| ~ spl0_27
| ~ spl0_234
| ~ spl0_235 ),
inference(sat_conversion,[],[f1874]) ).
cnf(s360,plain,
( ~ spl0_38
| spl0_119
| spl0_120
| ~ spl0_201 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s366,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_229
| ~ spl0_230 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s377,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| ~ spl0_21
| spl0_88
| ~ spl0_181 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s394,plain,
( ~ spl0_9
| spl0_106
| spl0_107
| ~ spl0_192 ),
inference(sat_conversion,[],[f2066]) ).
cnf(s399,plain,
( ~ spl0_38
| ~ spl0_44
| spl0_126
| spl0_127 ),
inference(sat_conversion,[],[f2076]) ).
cnf(s405,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_13
| spl0_157
| ~ spl0_234
| ~ spl0_235 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s495,plain,
( ~ spl0_14
| ~ spl0_264
| ~ spl0_265
| ~ spl0_266 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s521,plain,
( ~ spl0_2
| ~ spl0_8
| spl0_146
| spl0_147 ),
inference(sat_conversion,[],[f2621]) ).
cnf(s628,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_243
| ~ spl0_304 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s629,plain,
( ~ spl0_13
| ~ spl0_273
| ~ spl0_274
| ~ spl0_275 ),
inference(sat_conversion,[],[f3036]) ).
cnf(s639,plain,
( ~ spl0_13
| ~ spl0_28
| ~ spl0_202
| ~ spl0_203 ),
inference(sat_conversion,[],[f3063]) ).
cnf(s693,plain,
( ~ spl0_27
| spl0_122
| ~ spl0_202
| ~ spl0_203 ),
inference(sat_conversion,[],[f3239]) ).
cnf(s694,plain,
( ~ spl0_27
| spl0_157
| ~ spl0_234
| ~ spl0_235 ),
inference(sat_conversion,[],[f3241]) ).
cnf(s767,plain,
( ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_202
| ~ spl0_203 ),
inference(sat_conversion,[],[f3360]) ).
cnf(s769,plain,
( ~ spl0_1
| ~ spl0_18
| ~ spl0_28
| ~ spl0_234
| ~ spl0_235 ),
inference(sat_conversion,[],[f3363]) ).
cnf(s797,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_224
| ~ spl0_226 ),
inference(sat_conversion,[],[f3406]) ).
cnf(s803,plain,
( ~ spl0_7
| spl0_146
| spl0_147
| ~ spl0_214 ),
inference(sat_conversion,[],[f3428]) ).
cnf(s840,plain,
( ~ spl0_10
| ~ spl0_13
| ~ spl0_21
| spl0_161
| ~ spl0_239
| ~ spl0_240 ),
inference(sat_conversion,[],[f3559]) ).
cnf(s857,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_27 ),
inference(sat_conversion,[],[f3608]) ).
cnf(s914,plain,
( ~ spl0_9
| spl0_123
| spl0_124
| ~ spl0_204 ),
inference(sat_conversion,[],[f3698]) ).
cnf(s919,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_181
| ~ spl0_303 ),
inference(sat_conversion,[],[f3703]) ).
cnf(s924,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_37
| ~ spl0_215
| ~ spl0_216 ),
inference(sat_conversion,[],[f3724]) ).
cnf(s982,plain,
( ~ spl0_4
| ~ spl0_241
| ~ spl0_243
| spl0_304 ),
inference(sat_conversion,[],[f3860]) ).
cnf(s1009,plain,
( ~ spl0_2
| spl0_88
| ~ spl0_181
| spl0_303 ),
inference(sat_conversion,[],[f4018]) ).
cnf(s1045,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18 ),
inference(sat_conversion,[],[f4067]) ).
cnf(s1080,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_13
| ~ spl0_28 ),
inference(sat_conversion,[],[f4117]) ).
cnf(s1128,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_195
| ~ spl0_196 ),
inference(sat_conversion,[],[f4208]) ).
cnf(s1137,plain,
( ~ spl0_2
| ~ spl0_13
| ~ spl0_21
| spl0_157
| ~ spl0_235 ),
inference(sat_conversion,[],[f4222]) ).
cnf(s1198,plain,
( ~ spl0_2
| spl0_102
| spl0_103
| ~ spl0_190 ),
inference(sat_conversion,[],[f4330]) ).
cnf(s1234,plain,
( ~ spl0_2
| spl0_157
| ~ spl0_235
| spl0_302 ),
inference(sat_conversion,[],[f4390]) ).
cnf(s1305,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_197
| ~ spl0_198 ),
inference(sat_conversion,[],[f4613]) ).
cnf(s1308,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_221
| ~ spl0_222 ),
inference(sat_conversion,[],[f4618]) ).
cnf(s1388,plain,
( ~ spl0_18
| spl0_116
| ~ spl0_197
| ~ spl0_198 ),
inference(sat_conversion,[],[f4818]) ).
cnf(s1397,plain,
( ~ spl0_2
| spl0_122
| ~ spl0_202
| spl0_294 ),
inference(sat_conversion,[],[f4829]) ).
cnf(s1451,plain,
( ~ spl0_18
| spl0_152
| ~ spl0_221
| ~ spl0_222 ),
inference(sat_conversion,[],[f4874]) ).
cnf(s1452,plain,
( ~ spl0_18
| spl0_157
| ~ spl0_234
| ~ spl0_302 ),
inference(sat_conversion,[],[f4879]) ).
cnf(s1460,plain,
( ~ spl0_18
| spl0_122
| ~ spl0_203
| ~ spl0_294 ),
inference(sat_conversion,[],[f4886]) ).
cnf(s1461,plain,
spl0_3,
inference(rat,[],[s248,s309,s315,s316]) ).
cnf(s1462,plain,
( spl0_13
| spl0_18 ),
inference(rat,[],[s495,s225,s226,s227,s6,s8,s1461]) ).
cnf(s1463,plain,
( ~ spl0_12
| spl0_18 ),
inference(rat,[],[s1462,s1045]) ).
cnf(s1467,plain,
( ~ spl0_25
| ~ spl0_13 ),
inference(rat,[],[s629,s234,s235,s236]) ).
cnf(s1473,plain,
( ~ spl0_65
| spl0_18 ),
inference(rat,[],[s1128,s156,s157,s13,s1467,s1462,s1461]) ).
cnf(s1476,plain,
( ~ spl0_69
| ~ spl0_11
| ~ spl0_7
| ~ spl0_4 ),
inference(rat,[],[s327,s72,s151]) ).
cnf(s1477,plain,
( spl0_18
| ~ spl0_7
| spl0_2
| spl0_1 ),
inference(rat,[],[s366,s190,s191,s43,s1476,s13,s1467,s4,s322,s1463,s1462,s1,s1461]) ).
cnf(s1479,plain,
( ~ spl0_13
| spl0_69
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s366,s190,s191,s43,s322,s1461]) ).
cnf(s1480,plain,
( ~ spl0_33
| ~ spl0_18 ),
inference(rat,[],[s1451,s115,s182,s183]) ).
cnf(s1484,plain,
( ~ spl0_82
| ~ spl0_18 ),
inference(rat,[],[s1388,s85,s158,s159]) ).
cnf(s1486,plain,
( ~ spl0_78
| ~ spl0_9 ),
inference(rat,[],[s914,s90,s91,s165]) ).
cnf(s1487,plain,
( ~ spl0_9
| ~ spl0_38
| spl0_2 ),
inference(rat,[],[s394,s75,s76,s153,s55,s399,s93,s94,s48,s1486,s1461]) ).
cnf(s1488,plain,
( ~ spl0_18
| spl0_2
| spl0_1 ),
inference(rat,[],[s17,s1487,s51,s1484,s1480,s1461]) ).
cnf(s1489,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s982,s628,s202,s204,s41,s1080,s13,s5,s1467,s1477,s1473,s1463,s1462,s1488,s1,s1461]) ).
cnf(s1490,plain,
( ~ spl0_69
| ~ spl0_2 ),
inference(rat,[],[s1198,s71,s72,s151]) ).
cnf(s1495,plain,
( ~ spl0_118
| ~ spl0_38 ),
inference(rat,[],[s360,s87,s88,s162]) ).
cnf(s1497,plain,
( ~ spl0_121
| ~ spl0_18
| ~ spl0_2 ),
inference(rat,[],[s1397,s1460,s89,s163,s164]) ).
cnf(s1498,plain,
( ~ spl0_18
| ~ spl0_2 ),
inference(rat,[],[s1234,s1452,s120,s195,s196,s250,s1497,s1495,s51,s1484,s1480,s1461]) ).
cnf(s1499,plain,
spl0_1,
inference(rat,[],[s13,s1479,s1467,s1462,s1498,s1490,s1489,s1461]) ).
cnf(s1500,plain,
~ spl0_26,
inference(rat,[],[s329,s211,s212,s213,s1499]) ).
cnf(s1501,plain,
( ~ spl0_121
| ~ spl0_14
| ~ spl0_18 ),
inference(rat,[],[s14,s354,s767,s163,s164,s1461,s1500,s1499]) ).
cnf(s1502,plain,
( ~ spl0_14
| ~ spl0_18 ),
inference(rat,[],[s14,s355,s769,s195,s196,s250,s1501,s1495,s51,s1484,s1480,s1461,s1500,s1499]) ).
cnf(s1503,plain,
( ~ spl0_121
| ~ spl0_13 ),
inference(rat,[],[s14,s693,s639,s89,s163,s164,s1461,s1500]) ).
cnf(s1504,plain,
~ spl0_18,
inference(rat,[],[s14,s694,s769,s120,s195,s196,s250,s1503,s6,s1502,s1495,s51,s1484,s1480,s1461,s1500,s1499]) ).
cnf(s1505,plain,
spl0_13,
inference(rat,[],[s1462,s1504]) ).
cnf(s1506,plain,
~ spl0_12,
inference(rat,[],[s1463,s1504]) ).
cnf(s1508,plain,
~ spl0_25,
inference(rat,[],[s1467,s1505]) ).
cnf(s1509,plain,
~ spl0_121,
inference(rat,[],[s1503,s1505]) ).
cnf(s1510,plain,
spl0_21,
inference(rat,[],[s13,s1504,s1461,s1508]) ).
cnf(s1511,plain,
~ spl0_35,
inference(rat,[],[s797,s185,s187,s1505,s1510]) ).
cnf(s1512,plain,
( ~ spl0_41
| ~ spl0_10 ),
inference(rat,[],[s840,s124,s200,s201,s1505,s1510]) ).
cnf(s1523,plain,
( ~ spl0_148
| ~ spl0_10 ),
inference(rat,[],[s924,s176,s177,s22,s1512,s1499,s1506,s1461]) ).
cnf(s1524,plain,
( ~ spl0_145
| ~ spl0_7 ),
inference(rat,[],[s803,s110,s111,s175]) ).
cnf(s1525,plain,
( ~ spl0_181
| spl0_88
| ~ spl0_2 ),
inference(rat,[],[s919,s1009,s1510,s1505]) ).
cnf(s1526,plain,
( ~ spl0_86
| ~ spl0_2 ),
inference(rat,[],[s1525,s57,s142]) ).
cnf(s1527,plain,
( ~ spl0_33
| ~ spl0_6 ),
inference(rat,[],[s1308,s182,s183,s1505]) ).
cnf(s1528,plain,
( ~ spl0_82
| ~ spl0_6 ),
inference(rat,[],[s1305,s158,s159,s1505]) ).
cnf(s1529,plain,
( ~ spl0_55
| ~ spl0_2 ),
inference(rat,[],[s1137,s120,s196,s1510,s1505]) ).
cnf(s1530,plain,
( ~ spl0_145
| ~ spl0_2 ),
inference(rat,[],[s5,s521,s1524,s110,s111,s1461,s1506]) ).
cnf(s1531,plain,
~ spl0_2,
inference(rat,[],[s51,s1528,s1527,s19,s1523,s252,s1530,s1495,s250,s1529,s1526,s1461,s1511,s1509]) ).
cnf(s1532,plain,
spl0_11,
inference(rat,[],[s4,s1506,s1461,s1531]) ).
cnf(s1533,plain,
( ~ spl0_7
| spl0_148 ),
inference(rat,[],[s377,s57,s142,s252,s1524,s1532,s1505,s1510]) ).
cnf(s1534,plain,
( ~ spl0_8
| spl0_7 ),
inference(rat,[],[s14,s857,s1080,s1505,s1500,s1461]) ).
cnf(s1535,plain,
spl0_7,
inference(rat,[],[s1534,s5,s1461,s1506]) ).
cnf(s1537,plain,
spl0_148,
inference(rat,[],[s1533,s1535]) ).
cnf(s1541,plain,
~ spl0_10,
inference(rat,[],[s1523,s1537]) ).
cnf(s1543,plain,
spl0_6,
inference(rat,[],[s19,s1511,s1461,s1541]) ).
cnf(s1547,plain,
~ spl0_33,
inference(rat,[],[s1527,s1543]) ).
cnf(s1548,plain,
~ spl0_82,
inference(rat,[],[s1528,s1543]) ).
cnf(s1550,plain,
spl0_38,
inference(rat,[],[s51,s1547,s1461,s1548]) ).
cnf(s1552,plain,
~ spl0_118,
inference(rat,[],[s1495,s1550]) ).
cnf(s1554,plain,
spl0_55,
inference(rat,[],[s250,s1509,s1552]) ).
cnf(s1556,plain,
spl0_235,
inference(rat,[],[s196,s1554]) ).
cnf(s1557,plain,
spl0_234,
inference(rat,[],[s195,s1554]) ).
cnf(s1558,plain,
~ spl0_157,
inference(rat,[],[s120,s1554]) ).
cnf(s1561,plain,
$false,
inference(rat,[],[s405,s1556,s1505,s1532,s1535,s1557,s1558]) ).
fof(f4887,plain,
$false,
inference(avatar_sat_refutation,[],[s1561]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN447-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.18 % Computer : n004.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Mon Sep 28 16:04:26 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running first-order theorem proving
% 0.10/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
% 0.83/0.96 % (494907)Input is clausal, will run a generic CNF schedule.
% 0.83/0.96 % (494916)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3434932932:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.83/0.96 % (494916)First to succeed.
% 0.83/0.96 % (494917)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4288148319:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.83/0.96 % (494916)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-494907"
% 0.83/0.96 % (494913)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1627401821:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.83/0.96 % (494912)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=473969308:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.83/0.96 % (494914)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2975938776:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.83/0.96 % (494915)lrs+10_1_sil=8000:sp=occurrence:random_seed=846647276:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.83/0.96 % (494918)dis-21_1_sil=8000:lcm=predicate:random_seed=3068224739:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 0.83/0.96 % (494918)Also succeeded, but the first one will report.
% 0.83/0.96 % (494915)Instruction limit reached!
% 0.83/0.96 % (494915)------------------------------
% 0.83/0.96 % (494915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.83/0.96 % (494915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.83/0.96 % (494915)CaDiCaL version: 2.1.3
% 0.83/0.96 % (494915)Termination reason: Instruction limit
% 0.83/0.96 % (494915)Termination phase: Saturation
% 0.83/0.96 % (494915)Time elapsed: 0.070 s
% 0.83/0.96 % (494915)Peak memory usage: 90 MB
% 0.83/0.96 % (494915)Instructions burned: 107 (million)
% 0.83/0.96 % (494917)Also succeeded, but the first one will report.
% 0.83/0.96 % (494916)Refutation found. Thanks to Tanya!
% 0.83/0.96 % SZS status Unsatisfiable for theBenchmark
% 0.83/0.96 % SZS output start Proof for theBenchmark
% See solution above
% 2.78/1.15 % (494916)------------------------------
% 2.78/1.15 % (494916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.78/1.15 % (494916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.78/1.15 % (494916)CaDiCaL version: 2.1.3
% 2.78/1.15 % (494916)Termination reason: Refutation
% 2.78/1.15 % (494916)Time elapsed: 0.040 s
% 2.78/1.15 % (494916)Peak memory usage: 91 MB
% 2.78/1.15 % (494916)Instructions burned: 108 (million)
% 2.78/1.15 % (494916)------------------------------
% 2.78/1.15 % (494916)------------------------------
% 2.78/1.15 % (494907)Success in time 0.304 s
% 2.78/1.15 % Vampire exiting
%------------------------------------------------------------------------------