%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN448-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 2.99s 1.11s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 211
% Syntax : Number of formulae : 652 ( 19 unt; 117 def)
% Number of atoms : 1948 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 2262 ( 966 ~;1179 |; 0 &)
% ( 117 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 145 ( 144 usr; 141 prp; 0-1 aty)
% Number of functors : 22 ( 22 usr; 22 con; 0-0 aty)
% Number of variables : 95 ( 0 sgn 95 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,negated_conjecture,
( ~ hskp27
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
fof(f8,negated_conjecture,
( ~ hskp22
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f13,negated_conjecture,
( ~ hskp17
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
fof(f31,negated_conjecture,
( hskp27
| hskp22
| hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
fof(f32,negated_conjecture,
( hskp8
| hskp15
| hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
fof(f33,negated_conjecture,
( hskp25
| hskp5
| hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
fof(f34,negated_conjecture,
( hskp9
| hskp23
| hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f37,negated_conjecture,
( hskp20
| hskp6
| hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f41,negated_conjecture,
( ~ hskp27
| c0_1(a473) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
( ~ hskp27
| c1_1(a473) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp27
| c3_1(a473) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp26
| c1_1(a470) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
fof(f46,negated_conjecture,
( ~ hskp26
| c3_1(a470) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp25
| c0_1(a461) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f49,negated_conjecture,
( ~ hskp25
| c3_1(a461) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
fof(f52,negated_conjecture,
( ~ hskp22
| c0_1(a524) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp22
| c1_1(a524) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
fof(f56,negated_conjecture,
( ~ hskp20
| c2_1(a503) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp20
| c3_1(a503) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp19
| c2_1(a502) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp19
| c3_1(a502) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
fof(f62,negated_conjecture,
( ~ hskp16
| c1_1(a493) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp15
| c1_1(a492) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp15
| c3_1(a492) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f67,negated_conjecture,
( ~ hskp11
| c2_1(a478) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
fof(f70,negated_conjecture,
( ~ hskp9
| c0_1(a476) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp9
| c2_1(a476) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp8
| c0_1(a475) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp8
| c1_1(a475) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f75,negated_conjecture,
( ~ hskp6
| c2_1(a471) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp5
| c0_1(a468) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp5
| c3_1(a468) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f79,negated_conjecture,
( ~ hskp3
| c1_1(a466) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp3
| c3_1(a466) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp1
| c2_1(a463) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp0
| c0_1(a460) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f85,negated_conjecture,
( ~ c1_1(a533)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ c3_1(a533)
| ~ hskp23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ c2_1(a524)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f89,negated_conjecture,
( ~ c1_1(a503)
| ~ hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c0_1(a502)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f92,negated_conjecture,
( ~ c0_1(a494)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c1_1(a494)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c3_1(a494)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c0_1(a493)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c2_1(a493)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c2_1(a492)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c1_1(a488)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c2_1(a488)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c3_1(a488)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f102,negated_conjecture,
( ~ c0_1(a480)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c1_1(a480)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c2_1(a480)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c0_1(a478)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c3_1(a478)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f108,negated_conjecture,
( ~ c1_1(a476)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c3_1(a475)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c1_1(a474)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c2_1(a474)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c1_1(a471)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c3_1(a471)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f117,negated_conjecture,
( ~ c0_1(a466)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c0_1(a465)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c2_1(a465)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c3_1(a465)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c0_1(a463)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c1_1(a463)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c2_1(a460)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c3_1(a460)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| hskp0
| hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp3
| hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp6
| hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp0
| hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp16
| hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f133,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp19
| hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp12
| hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp11
| hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause135) ).
fof(f137,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp3
| hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f139,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp15
| hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause139) ).
fof(f143,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause144) ).
fof(f146,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause146) ).
fof(f151,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause151) ).
fof(f154,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X1)
| c1_1(X1)
| hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
fof(f166,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause166) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c1_1(X1)
| hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f172,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| c0_1(X0)
| c0_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X2)
| c2_1(X2)
| c3_1(X2)
| c0_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f178,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f179,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f181,definition,
( spl0_2
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f182,plain,
( ! [X1] :
( c3_1(X1)
| ~ c2_1(X1)
| c1_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f184,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f187,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f188,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f189,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f176,f187,f184,f181,f178]) ).
fof(f191,definition,
( spl0_5
<=> ! [X2] :
( c1_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f192,plain,
( ! [X2] :
( c3_1(X2)
| c1_1(X2)
| c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f194,definition,
( spl0_6
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f195,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f196,plain,
( spl0_5
| spl0_1
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f175,f194,f184,f178,f191]) ).
fof(f198,definition,
( spl0_7
<=> ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f199,plain,
( ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f201,definition,
( spl0_8
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f202,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f203,plain,
( spl0_7
| spl0_8
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f174,f178,f184,f201,f198]) ).
fof(f205,definition,
( spl0_9
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f206,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,definition,
( spl0_10
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f209,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f211,definition,
( spl0_11
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f212,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f213,plain,
( spl0_9
| spl0_10
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f173,f211,f184,f208,f205]) ).
fof(f215,definition,
( spl0_12
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f216,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f217,plain,
( spl0_9
| spl0_8
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f172,f215,f184,f201,f205]) ).
fof(f226,definition,
( spl0_15
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f229,definition,
( spl0_16
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f230,plain,
( ! [X1] :
( c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f232,definition,
( spl0_17
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f233,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f234,plain,
( spl0_15
| spl0_16
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f170,f232,f184,f229,f226]) ).
fof(f243,definition,
( spl0_20
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f245,plain,
( spl0_20
| spl0_8
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f168,f232,f184,f201,f243]) ).
fof(f247,definition,
( spl0_21
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f251,definition,
( spl0_22
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f253,plain,
( spl0_22
| spl0_12
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f166,f194,f184,f215,f251]) ).
fof(f255,definition,
( spl0_23
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f259,definition,
( spl0_24
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f262,definition,
( spl0_25
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f263,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f266,definition,
( spl0_26
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f270,definition,
( spl0_27
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f277,definition,
( spl0_29
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f278,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f281,definition,
( spl0_30
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f284,definition,
( spl0_31
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f285,plain,
( ! [X1] :
( c1_1(X1)
| ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f286,plain,
( spl0_30
| spl0_31
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f160,f232,f184,f284,f281]) ).
fof(f291,definition,
( spl0_33
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f292,plain,
( ! [X1] :
( c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f304,definition,
( spl0_37
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f305,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f309,definition,
( spl0_38
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f310,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( spl0_24
| spl0_29
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f155,f178,f184,f277,f259]) ).
fof(f313,plain,
( spl0_26
| spl0_7
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f154,f208,f184,f198,f266]) ).
fof(f322,definition,
( spl0_41
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f326,definition,
( spl0_42
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f328,plain,
( spl0_42
| spl0_37
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f151,f215,f184,f304,f326]) ).
fof(f339,definition,
( spl0_45
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f343,definition,
( spl0_46
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f344,plain,
( ! [X1] :
( c3_1(X1)
| c0_1(X1)
| c2_1(X1) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f345,plain,
( spl0_21
| spl0_46
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f146,f215,f184,f343,f247]) ).
fof(f347,definition,
( spl0_47
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f351,definition,
( spl0_48
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f353,plain,
( spl0_48
| spl0_9
| ~ spl0_3
| spl0_31 ),
inference(avatar_split_clause,[],[f144,f284,f184,f205,f351]) ).
fof(f355,definition,
( spl0_49
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f357,plain,
( spl0_49
| spl0_46
| spl0_5
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f143,f184,f191,f343,f355]) ).
fof(f361,definition,
( spl0_50
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f364,plain,
( spl0_45
| spl0_50
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f139,f187,f184,f361,f339]) ).
fof(f366,definition,
( spl0_51
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f372,plain,
( spl0_42
| spl0_22
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f137,f262,f184,f251,f326]) ).
fof(f374,plain,
( spl0_21
| spl0_27
| ~ spl0_3
| spl0_33 ),
inference(avatar_split_clause,[],[f135,f291,f184,f270,f247]) ).
fof(f375,plain,
( spl0_20
| spl0_42
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f134,f181,f184,f326,f243]) ).
fof(f377,definition,
( spl0_53
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f379,plain,
( spl0_51
| spl0_53
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f133,f181,f184,f377,f366]) ).
fof(f382,definition,
( spl0_54
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f389,plain,
( spl0_15
| spl0_54
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f129,f309,f184,f382,f226]) ).
fof(f391,definition,
( spl0_56
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f392,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f393,plain,
( spl0_42
| spl0_48
| ~ spl0_3
| spl0_56 ),
inference(avatar_split_clause,[],[f128,f391,f184,f351,f326]) ).
fof(f395,definition,
( spl0_57
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f397,plain,
( spl0_45
| spl0_57
| ~ spl0_3
| spl0_31 ),
inference(avatar_split_clause,[],[f127,f284,f184,f395,f339]) ).
fof(f398,plain,
( spl0_50
| spl0_22
| spl0_5
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f126,f184,f191,f251,f361]) ).
fof(f399,plain,
( spl0_23
| spl0_48
| spl0_9
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f125,f184,f205,f351,f255]) ).
fof(f402,definition,
( spl0_58
<=> c3_1(a460) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f403,plain,
( ~ c3_1(a460)
| spl0_58 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( ~ spl0_48
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f124,f402,f351]) ).
fof(f406,definition,
( spl0_59
<=> c2_1(a460) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f408,plain,
( ~ spl0_48
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f123,f406,f351]) ).
fof(f411,definition,
( spl0_60
<=> c1_1(a463) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f412,plain,
( ~ c1_1(a463)
| spl0_60 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f413,plain,
( ~ spl0_23
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f122,f411,f255]) ).
fof(f415,definition,
( spl0_61
<=> c0_1(a463) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f417,plain,
( ~ spl0_23
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f121,f415,f255]) ).
fof(f420,definition,
( spl0_62
<=> c3_1(a465) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f421,plain,
( ~ c3_1(a465)
| spl0_62 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f422,plain,
( ~ spl0_45
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f120,f420,f339]) ).
fof(f424,definition,
( spl0_63
<=> c2_1(a465) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f426,plain,
( ~ spl0_45
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f119,f424,f339]) ).
fof(f428,definition,
( spl0_64
<=> c0_1(a465) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f430,plain,
( ~ spl0_45
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f118,f428,f339]) ).
fof(f433,definition,
( spl0_65
<=> c0_1(a466) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f435,plain,
( ~ spl0_22
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f117,f433,f251]) ).
fof(f452,definition,
( spl0_69
<=> c3_1(a471) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f453,plain,
( ~ c3_1(a471)
| spl0_69 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f454,plain,
( ~ spl0_57
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f113,f452,f395]) ).
fof(f456,definition,
( spl0_70
<=> c1_1(a471) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f458,plain,
( ~ spl0_57
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f112,f456,f395]) ).
fof(f461,definition,
( spl0_71
<=> c2_1(a474) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f463,plain,
( ~ spl0_21
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f111,f461,f247]) ).
fof(f465,definition,
( spl0_72
<=> c1_1(a474) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f466,plain,
( ~ c1_1(a474)
| spl0_72 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( ~ spl0_21
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f110,f465,f247]) ).
fof(f470,definition,
( spl0_73
<=> c3_1(a475) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f471,plain,
( ~ c3_1(a475)
| spl0_73 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( ~ spl0_26
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f109,f470,f266]) ).
fof(f475,definition,
( spl0_74
<=> c1_1(a476) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f476,plain,
( ~ c1_1(a476)
| spl0_74 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f477,plain,
( ~ spl0_24
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f108,f475,f259]) ).
fof(f485,definition,
( spl0_76
<=> c3_1(a478) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f486,plain,
( ~ c3_1(a478)
| spl0_76 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f487,plain,
( ~ spl0_27
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f106,f485,f270]) ).
fof(f489,definition,
( spl0_77
<=> c0_1(a478) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f491,plain,
( ~ spl0_27
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f105,f489,f270]) ).
fof(f494,definition,
( spl0_78
<=> c2_1(a480) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f496,plain,
( ~ spl0_42
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f104,f494,f326]) ).
fof(f498,definition,
( spl0_79
<=> c1_1(a480) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f499,plain,
( ~ c1_1(a480)
| spl0_79 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f500,plain,
( ~ spl0_42
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f103,f498,f326]) ).
fof(f502,definition,
( spl0_80
<=> c0_1(a480) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f504,plain,
( ~ spl0_42
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f102,f502,f326]) ).
fof(f512,definition,
( spl0_82
<=> c3_1(a488) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f513,plain,
( ~ c3_1(a488)
| spl0_82 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( ~ spl0_20
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f100,f512,f243]) ).
fof(f516,definition,
( spl0_83
<=> c2_1(a488) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f518,plain,
( ~ spl0_20
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f99,f516,f243]) ).
fof(f520,definition,
( spl0_84
<=> c1_1(a488) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f521,plain,
( ~ c1_1(a488)
| spl0_84 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f522,plain,
( ~ spl0_20
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f98,f520,f243]) ).
fof(f525,definition,
( spl0_85
<=> c2_1(a492) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f527,plain,
( ~ spl0_50
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f97,f525,f361]) ).
fof(f530,definition,
( spl0_86
<=> c2_1(a493) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f532,plain,
( ~ spl0_54
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f96,f530,f382]) ).
fof(f534,definition,
( spl0_87
<=> c0_1(a493) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f536,plain,
( ~ spl0_54
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f95,f534,f382]) ).
fof(f539,definition,
( spl0_88
<=> c3_1(a494) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f540,plain,
( ~ c3_1(a494)
| spl0_88 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f541,plain,
( ~ spl0_15
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f94,f539,f226]) ).
fof(f543,definition,
( spl0_89
<=> c1_1(a494) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f544,plain,
( ~ c1_1(a494)
| spl0_89 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f545,plain,
( ~ spl0_15
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f93,f543,f226]) ).
fof(f547,definition,
( spl0_90
<=> c0_1(a494) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f549,plain,
( ~ spl0_15
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f92,f547,f226]) ).
fof(f557,definition,
( spl0_92
<=> c0_1(a502) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f559,plain,
( ~ spl0_53
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f90,f557,f377]) ).
fof(f562,definition,
( spl0_93
<=> c1_1(a503) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f563,plain,
( ~ c1_1(a503)
| spl0_93 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f564,plain,
( ~ spl0_51
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f89,f562,f366]) ).
fof(f571,definition,
( spl0_95
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f574,definition,
( spl0_96
<=> c2_1(a524) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f576,plain,
( ~ spl0_95
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f87,f574,f571]) ).
fof(f578,definition,
( spl0_97
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f581,definition,
( spl0_98
<=> c3_1(a533) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f582,plain,
( ~ c3_1(a533)
| spl0_98 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( ~ spl0_97
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f86,f581,f578]) ).
fof(f585,definition,
( spl0_99
<=> c1_1(a533) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f587,plain,
( ~ spl0_97
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f85,f585,f578]) ).
fof(f600,definition,
( spl0_103
<=> c0_1(a460) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f602,plain,
( spl0_103
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f82,f351,f600]) ).
fof(f604,definition,
( spl0_104
<=> c2_1(a463) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f606,plain,
( spl0_104
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f81,f255,f604]) ).
fof(f608,definition,
( spl0_105
<=> c3_1(a466) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f609,plain,
( c3_1(a466)
| ~ spl0_105 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f610,plain,
( spl0_105
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f80,f251,f608]) ).
fof(f612,definition,
( spl0_106
<=> c1_1(a466) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f614,plain,
( spl0_106
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f79,f251,f612]) ).
fof(f620,definition,
( spl0_108
<=> c3_1(a468) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f621,plain,
( c3_1(a468)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f622,plain,
( spl0_108
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f77,f322,f620]) ).
fof(f624,definition,
( spl0_109
<=> c0_1(a468) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f626,plain,
( spl0_109
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f76,f322,f624]) ).
fof(f628,definition,
( spl0_110
<=> c2_1(a471) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f630,plain,
( spl0_110
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f75,f395,f628]) ).
fof(f636,definition,
( spl0_112
<=> c1_1(a475) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f637,plain,
( c1_1(a475)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f638,plain,
( spl0_112
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f73,f266,f636]) ).
fof(f640,definition,
( spl0_113
<=> c0_1(a475) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f642,plain,
( spl0_113
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f72,f266,f640]) ).
fof(f644,definition,
( spl0_114
<=> c2_1(a476) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f646,plain,
( spl0_114
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f71,f259,f644]) ).
fof(f648,definition,
( spl0_115
<=> c0_1(a476) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f650,plain,
( spl0_115
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f70,f259,f648]) ).
fof(f660,definition,
( spl0_118
<=> c2_1(a478) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f662,plain,
( spl0_118
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f67,f270,f660]) ).
fof(f672,definition,
( spl0_121
<=> c3_1(a492) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f673,plain,
( c3_1(a492)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f674,plain,
( spl0_121
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f64,f361,f672]) ).
fof(f676,definition,
( spl0_122
<=> c1_1(a492) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f677,plain,
( c1_1(a492)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f678,plain,
( spl0_122
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f63,f361,f676]) ).
fof(f680,definition,
( spl0_123
<=> c1_1(a493) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f681,plain,
( c1_1(a493)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f682,plain,
( spl0_123
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f62,f382,f680]) ).
fof(f692,definition,
( spl0_126
<=> c3_1(a502) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f693,plain,
( c3_1(a502)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f694,plain,
( spl0_126
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f59,f377,f692]) ).
fof(f696,definition,
( spl0_127
<=> c2_1(a502) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f698,plain,
( spl0_127
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f58,f377,f696]) ).
fof(f700,definition,
( spl0_128
<=> c3_1(a503) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f701,plain,
( c3_1(a503)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f700]) ).
fof(f702,plain,
( spl0_128
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f57,f366,f700]) ).
fof(f704,definition,
( spl0_129
<=> c2_1(a503) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f706,plain,
( spl0_129
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f56,f366,f704]) ).
fof(f716,definition,
( spl0_132
<=> c1_1(a524) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f717,plain,
( c1_1(a524)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f716]) ).
fof(f718,plain,
( spl0_132
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f53,f571,f716]) ).
fof(f720,definition,
( spl0_133
<=> c0_1(a524) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f722,plain,
( spl0_133
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f52,f571,f720]) ).
fof(f732,definition,
( spl0_136
<=> c3_1(a461) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f733,plain,
( c3_1(a461)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f732]) ).
fof(f735,plain,
( spl0_136
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f49,f347,f732]) ).
fof(f741,definition,
( spl0_138
<=> c0_1(a461) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f743,plain,
( spl0_138
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f47,f347,f741]) ).
fof(f745,definition,
( spl0_139
<=> c3_1(a470) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f746,plain,
( c3_1(a470)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f748,plain,
( spl0_139
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f46,f281,f745]) ).
fof(f754,definition,
( spl0_141
<=> c1_1(a470) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f756,plain,
( spl0_141
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f44,f281,f754]) ).
fof(f758,definition,
( spl0_142
<=> c3_1(a473) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f759,plain,
( c3_1(a473)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f761,plain,
( spl0_142
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f43,f355,f758]) ).
fof(f763,definition,
( spl0_143
<=> c1_1(a473) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f765,plain,
( spl0_143
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f42,f355,f763]) ).
fof(f767,definition,
( spl0_144
<=> c0_1(a473) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f769,plain,
( spl0_144
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f41,f355,f767]) ).
fof(f783,plain,
( spl0_42
| spl0_57
| spl0_51 ),
inference(avatar_split_clause,[],[f37,f366,f395,f326]) ).
fof(f788,plain,
( spl0_51
| spl0_97
| spl0_24 ),
inference(avatar_split_clause,[],[f34,f259,f578,f366]) ).
fof(f789,plain,
( spl0_20
| spl0_41
| spl0_47 ),
inference(avatar_split_clause,[],[f33,f347,f322,f243]) ).
fof(f790,plain,
( spl0_54
| spl0_50
| spl0_26 ),
inference(avatar_split_clause,[],[f32,f266,f361,f382]) ).
fof(f792,plain,
( spl0_15
| spl0_95
| spl0_49 ),
inference(avatar_split_clause,[],[f31,f355,f571,f226]) ).
fof(f811,plain,
( spl0_3
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f13,f226,f184]) ).
fof(f816,plain,
( spl0_3
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f8,f571,f184]) ).
fof(f821,plain,
( spl0_3
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f3,f355,f184]) ).
fof(f824,plain,
( ~ c2_1(a471)
| c1_1(a471)
| ~ spl0_2
| spl0_69 ),
inference(resolution,[],[f182,f453]) ).
fof(f825,plain,
( ~ c2_1(a494)
| c1_1(a494)
| ~ spl0_2
| spl0_88 ),
inference(resolution,[],[f182,f540]) ).
fof(f828,definition,
( spl0_148
<=> c2_1(a494) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f830,plain,
( spl0_89
| ~ spl0_148
| ~ spl0_2
| spl0_88 ),
inference(avatar_split_clause,[],[f825,f539,f181,f828,f543]) ).
fof(f833,plain,
( spl0_70
| ~ spl0_110
| ~ spl0_2
| spl0_69 ),
inference(avatar_split_clause,[],[f824,f452,f181,f628,f456]) ).
fof(f840,definition,
( spl0_149
<=> c0_1(a492) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f854,definition,
( spl0_150
<=> c1_1(a468) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f858,plain,
( c2_1(a492)
| c0_1(a492)
| ~ spl0_7
| ~ spl0_122 ),
inference(resolution,[],[f199,f677]) ).
fof(f863,plain,
( c0_1(a492)
| ~ c1_1(a492)
| ~ spl0_8
| ~ spl0_121 ),
inference(resolution,[],[f202,f673]) ).
fof(f866,plain,
( ~ spl0_122
| spl0_149
| ~ spl0_8
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f863,f672,f201,f840,f676]) ).
fof(f869,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_1
| ~ spl0_2 ),
inference(resolution,[],[f179,f182]) ).
fof(f870,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_1
| ~ spl0_2 ),
inference(duplicate_literal_removal,[],[f869]) ).
fof(f871,plain,
( spl0_31
| ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f870,f181,f178,f284]) ).
fof(f876,plain,
( c2_1(a494)
| c0_1(a494)
| ~ spl0_9
| spl0_89 ),
inference(resolution,[],[f206,f544]) ).
fof(f877,plain,
( c2_1(a480)
| c0_1(a480)
| ~ spl0_9
| spl0_79 ),
inference(resolution,[],[f206,f499]) ).
fof(f881,plain,
( spl0_80
| spl0_78
| ~ spl0_9
| spl0_79 ),
inference(avatar_split_clause,[],[f877,f498,f205,f494,f502]) ).
fof(f964,plain,
( spl0_90
| spl0_148
| ~ spl0_9
| spl0_89 ),
inference(avatar_split_clause,[],[f876,f543,f205,f828,f547]) ).
fof(f969,plain,
( c1_1(a503)
| ~ c2_1(a503)
| ~ spl0_10
| ~ spl0_128 ),
inference(resolution,[],[f701,f209]) ).
fof(f974,definition,
( spl0_155
<=> c0_1(a503) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f977,plain,
( c2_1(a524)
| ~ c0_1(a524)
| ~ spl0_4
| ~ spl0_132 ),
inference(resolution,[],[f717,f188]) ).
fof(f980,plain,
( ~ spl0_133
| spl0_96
| ~ spl0_4
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f977,f716,f187,f574,f720]) ).
fof(f1016,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_2
| ~ spl0_17 ),
inference(resolution,[],[f233,f182]) ).
fof(f1018,plain,
( ~ c0_1(a503)
| ~ c2_1(a503)
| ~ spl0_17
| ~ spl0_128 ),
inference(resolution,[],[f233,f701]) ).
fof(f1023,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_2
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1016]) ).
fof(f1043,definition,
( spl0_158
<=> c0_1(a488) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f1049,plain,
( c2_1(a488)
| c0_1(a488)
| ~ spl0_9
| spl0_84 ),
inference(resolution,[],[f521,f206]) ).
fof(f1063,plain,
( c2_1(a474)
| c0_1(a474)
| ~ spl0_9
| spl0_72 ),
inference(resolution,[],[f466,f206]) ).
fof(f1066,definition,
( spl0_159
<=> c0_1(a474) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1069,plain,
( spl0_159
| spl0_71
| ~ spl0_9
| spl0_72 ),
inference(avatar_split_clause,[],[f1063,f465,f205,f461,f1066]) ).
fof(f1074,plain,
( ~ c0_1(a475)
| ~ c2_1(a475)
| ~ spl0_11
| spl0_73 ),
inference(resolution,[],[f471,f212]) ).
fof(f1077,definition,
( spl0_160
<=> c2_1(a475) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1095,plain,
( c0_1(a466)
| ~ c1_1(a466)
| ~ spl0_8
| ~ spl0_105 ),
inference(resolution,[],[f202,f609]) ).
fof(f1098,plain,
( ~ spl0_106
| spl0_65
| ~ spl0_8
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f1095,f608,f201,f433,f612]) ).
fof(f1124,plain,
( ~ c0_1(a488)
| c2_1(a488)
| ~ spl0_12
| spl0_82 ),
inference(resolution,[],[f216,f513]) ).
fof(f1125,plain,
( spl0_83
| ~ spl0_158
| ~ spl0_12
| spl0_82 ),
inference(avatar_split_clause,[],[f1124,f512,f215,f1043,f516]) ).
fof(f1128,plain,
( ~ c0_1(a503)
| ~ c2_1(a503)
| ~ spl0_16
| spl0_93 ),
inference(resolution,[],[f230,f563]) ).
fof(f1129,plain,
( ~ c0_1(a476)
| ~ c2_1(a476)
| ~ spl0_16
| spl0_74 ),
inference(resolution,[],[f230,f476]) ).
fof(f1143,plain,
( ~ spl0_114
| ~ spl0_115
| ~ spl0_16
| spl0_74 ),
inference(avatar_split_clause,[],[f1129,f475,f229,f648,f644]) ).
fof(f1145,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_12
| ~ spl0_25 ),
inference(resolution,[],[f263,f216]) ).
fof(f1150,plain,
( c1_1(a503)
| ~ c0_1(a503)
| ~ spl0_25
| ~ spl0_128 ),
inference(resolution,[],[f263,f701]) ).
fof(f1152,plain,
( c1_1(a468)
| ~ c0_1(a468)
| ~ spl0_25
| ~ spl0_108 ),
inference(resolution,[],[f263,f621]) ).
fof(f1158,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_12
| ~ spl0_25 ),
inference(duplicate_literal_removal,[],[f1145]) ).
fof(f1162,plain,
( ~ spl0_109
| spl0_150
| ~ spl0_25
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1152,f620,f262,f854,f624]) ).
fof(f1166,plain,
( ~ spl0_155
| spl0_93
| ~ spl0_25
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1150,f700,f262,f562,f974]) ).
fof(f1168,plain,
( spl0_38
| ~ spl0_12
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1158,f262,f215,f309]) ).
fof(f1171,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c1_1(X0)
| c2_1(X0) )
| ~ spl0_5
| ~ spl0_29 ),
inference(resolution,[],[f278,f192]) ).
fof(f1180,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c1_1(X0) )
| ~ spl0_5
| ~ spl0_29 ),
inference(duplicate_literal_removal,[],[f1171]) ).
fof(f1187,plain,
( ~ c2_1(a503)
| c0_1(a503)
| ~ spl0_31
| spl0_93 ),
inference(resolution,[],[f285,f563]) ).
fof(f1190,plain,
( ~ c2_1(a463)
| c0_1(a463)
| ~ spl0_31
| spl0_60 ),
inference(resolution,[],[f285,f412]) ).
fof(f1191,plain,
( ~ c2_1(a494)
| c0_1(a494)
| ~ spl0_31
| spl0_89 ),
inference(resolution,[],[f285,f544]) ).
fof(f1203,definition,
( spl0_161
<=> c1_1(a465) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1213,plain,
( c0_1(a470)
| ~ c1_1(a470)
| ~ spl0_8
| ~ spl0_139 ),
inference(resolution,[],[f746,f202]) ).
fof(f1216,definition,
( spl0_162
<=> c0_1(a470) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1230,plain,
( ~ c1_1(a465)
| c2_1(a465)
| ~ spl0_33
| spl0_62 ),
inference(resolution,[],[f292,f421]) ).
fof(f1234,plain,
( spl0_63
| ~ spl0_161
| ~ spl0_33
| spl0_62 ),
inference(avatar_split_clause,[],[f1230,f420,f291,f1203,f424]) ).
fof(f1278,plain,
( c1_1(a461)
| ~ c0_1(a461)
| ~ spl0_25
| ~ spl0_136 ),
inference(resolution,[],[f733,f263]) ).
fof(f1281,definition,
( spl0_164
<=> c1_1(a461) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1286,plain,
( ~ spl0_138
| spl0_164
| ~ spl0_25
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1278,f732,f262,f1281,f741]) ).
fof(f1329,plain,
( ~ c0_1(a488)
| c1_1(a488)
| ~ spl0_37
| spl0_82 ),
inference(resolution,[],[f305,f513]) ).
fof(f1339,plain,
( c2_1(a474)
| ~ c0_1(a474)
| ~ spl0_38
| spl0_72 ),
inference(resolution,[],[f310,f466]) ).
fof(f1371,plain,
( c0_1(a488)
| c2_1(a488)
| ~ spl0_46
| spl0_82 ),
inference(resolution,[],[f344,f513]) ).
fof(f1372,plain,
( c0_1(a465)
| c2_1(a465)
| ~ spl0_46
| spl0_62 ),
inference(resolution,[],[f344,f421]) ).
fof(f1377,plain,
( spl0_63
| spl0_64
| ~ spl0_46
| spl0_62 ),
inference(avatar_split_clause,[],[f1372,f420,f343,f428,f424]) ).
fof(f1378,plain,
( spl0_83
| spl0_158
| ~ spl0_46
| spl0_82 ),
inference(avatar_split_clause,[],[f1371,f512,f343,f1043,f516]) ).
fof(f1408,plain,
( ~ c2_1(a478)
| c0_1(a478)
| ~ spl0_56
| spl0_76 ),
inference(resolution,[],[f392,f486]) ).
fof(f1416,plain,
( spl0_77
| ~ spl0_118
| ~ spl0_56
| spl0_76 ),
inference(avatar_split_clause,[],[f1408,f485,f391,f660,f489]) ).
fof(f1419,plain,
( ~ c0_1(a460)
| c2_1(a460)
| ~ spl0_12
| spl0_58 ),
inference(resolution,[],[f403,f216]) ).
fof(f1431,plain,
( spl0_59
| ~ spl0_103
| ~ spl0_12
| spl0_58 ),
inference(avatar_split_clause,[],[f1419,f402,f215,f600,f406]) ).
fof(f1437,plain,
( ~ spl0_159
| spl0_71
| ~ spl0_38
| spl0_72 ),
inference(avatar_split_clause,[],[f1339,f465,f309,f461,f1066]) ).
fof(f1438,plain,
( spl0_149
| spl0_85
| ~ spl0_7
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f858,f676,f198,f525,f840]) ).
fof(f1439,plain,
( spl0_16
| ~ spl0_2
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1023,f232,f181,f229]) ).
fof(f1445,plain,
( spl0_155
| ~ spl0_129
| ~ spl0_31
| spl0_93 ),
inference(avatar_split_clause,[],[f1187,f562,f284,f704,f974]) ).
fof(f1451,plain,
( spl0_158
| spl0_83
| ~ spl0_9
| spl0_84 ),
inference(avatar_split_clause,[],[f1049,f520,f205,f516,f1043]) ).
fof(f1452,plain,
( spl0_84
| ~ spl0_158
| ~ spl0_37
| spl0_82 ),
inference(avatar_split_clause,[],[f1329,f512,f304,f1043,f520]) ).
fof(f1453,plain,
( ~ spl0_129
| ~ spl0_155
| ~ spl0_17
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1018,f700,f232,f974,f704]) ).
fof(f1461,plain,
( ~ spl0_129
| ~ spl0_155
| ~ spl0_16
| spl0_93 ),
inference(avatar_split_clause,[],[f1128,f562,f229,f974,f704]) ).
fof(f1490,plain,
( c1_1(a488)
| c2_1(a488)
| ~ spl0_5
| spl0_82 ),
inference(resolution,[],[f192,f513]) ).
fof(f1491,plain,
( c1_1(a465)
| c2_1(a465)
| ~ spl0_5
| spl0_62 ),
inference(resolution,[],[f192,f421]) ).
fof(f1492,plain,
( spl0_63
| spl0_161
| ~ spl0_5
| spl0_62 ),
inference(avatar_split_clause,[],[f1491,f420,f191,f1203,f424]) ).
fof(f1493,plain,
( spl0_83
| spl0_84
| ~ spl0_5
| spl0_82 ),
inference(avatar_split_clause,[],[f1490,f512,f191,f520,f516]) ).
fof(f1501,plain,
( c2_1(a493)
| c0_1(a493)
| ~ spl0_7
| ~ spl0_123 ),
inference(resolution,[],[f199,f681]) ).
fof(f1509,plain,
( spl0_87
| spl0_86
| ~ spl0_7
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1501,f680,f198,f530,f534]) ).
fof(f1515,plain,
( ~ spl0_141
| spl0_162
| ~ spl0_8
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1213,f745,f201,f1216,f754]) ).
fof(f1522,plain,
( ~ spl0_129
| spl0_93
| ~ spl0_10
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f969,f700,f208,f562,f704]) ).
fof(f1524,plain,
( spl0_9
| ~ spl0_5
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f1180,f277,f191,f205]) ).
fof(f1526,plain,
( spl0_90
| ~ spl0_148
| ~ spl0_31
| spl0_89 ),
inference(avatar_split_clause,[],[f1191,f543,f284,f828,f547]) ).
fof(f1527,plain,
( spl0_61
| ~ spl0_104
| ~ spl0_31
| spl0_60 ),
inference(avatar_split_clause,[],[f1190,f411,f284,f604,f415]) ).
fof(f1528,plain,
( c1_1(a533)
| c2_1(a533)
| ~ spl0_5
| spl0_98 ),
inference(resolution,[],[f582,f192]) ).
fof(f1529,plain,
( ~ c2_1(a533)
| c1_1(a533)
| ~ spl0_2
| spl0_98 ),
inference(resolution,[],[f582,f182]) ).
fof(f1535,definition,
( spl0_166
<=> c2_1(a533) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1537,plain,
( spl0_99
| ~ spl0_166
| ~ spl0_2
| spl0_98 ),
inference(avatar_split_clause,[],[f1529,f581,f181,f1535,f585]) ).
fof(f1539,plain,
( spl0_166
| spl0_99
| ~ spl0_5
| spl0_98 ),
inference(avatar_split_clause,[],[f1528,f581,f191,f585,f1535]) ).
fof(f1545,plain,
( c0_1(a502)
| ~ c2_1(a502)
| ~ spl0_1
| ~ spl0_126 ),
inference(resolution,[],[f179,f693]) ).
fof(f1553,plain,
( ~ spl0_127
| spl0_92
| ~ spl0_1
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1545,f692,f178,f557,f696]) ).
fof(f1556,plain,
( ~ spl0_160
| ~ spl0_113
| ~ spl0_11
| spl0_73 ),
inference(avatar_split_clause,[],[f1074,f470,f211,f640,f1077]) ).
fof(f1571,plain,
( c1_1(a494)
| c2_1(a494)
| ~ spl0_5
| spl0_88 ),
inference(resolution,[],[f540,f192]) ).
fof(f1572,plain,
( spl0_148
| spl0_89
| ~ spl0_5
| spl0_88 ),
inference(avatar_split_clause,[],[f1571,f539,f191,f543,f828]) ).
fof(f1573,plain,
( c0_1(a503)
| ~ c2_1(a503)
| ~ spl0_1
| ~ spl0_128 ),
inference(resolution,[],[f701,f179]) ).
fof(f1574,plain,
( ~ spl0_129
| spl0_155
| ~ spl0_1
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1573,f700,f178,f974,f704]) ).
fof(f1576,plain,
( ~ c0_1(a473)
| ~ c1_1(a473)
| ~ spl0_6
| ~ spl0_142 ),
inference(resolution,[],[f195,f759]) ).
fof(f1577,plain,
( ~ c0_1(a470)
| ~ c1_1(a470)
| ~ spl0_6
| ~ spl0_139 ),
inference(resolution,[],[f195,f746]) ).
fof(f1578,plain,
( ~ c0_1(a461)
| ~ c1_1(a461)
| ~ spl0_6
| ~ spl0_136 ),
inference(resolution,[],[f195,f733]) ).
fof(f1582,plain,
( ~ c0_1(a492)
| ~ c1_1(a492)
| ~ spl0_6
| ~ spl0_121 ),
inference(resolution,[],[f195,f673]) ).
fof(f1584,plain,
( ~ c0_1(a468)
| ~ c1_1(a468)
| ~ spl0_6
| ~ spl0_108 ),
inference(resolution,[],[f195,f621]) ).
fof(f1586,plain,
( ~ spl0_150
| ~ spl0_109
| ~ spl0_6
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1584,f620,f194,f624,f854]) ).
fof(f1587,plain,
( ~ spl0_122
| ~ spl0_149
| ~ spl0_6
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f1582,f672,f194,f840,f676]) ).
fof(f1589,definition,
( spl0_168
<=> c1_1(a502) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1592,plain,
( ~ spl0_164
| ~ spl0_138
| ~ spl0_6
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1578,f732,f194,f741,f1281]) ).
fof(f1593,plain,
( ~ spl0_141
| ~ spl0_162
| ~ spl0_6
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1577,f745,f194,f1216,f754]) ).
fof(f1594,plain,
( ~ spl0_143
| ~ spl0_144
| ~ spl0_6
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1576,f758,f194,f767,f763]) ).
fof(f1606,plain,
( c2_1(a475)
| ~ c0_1(a475)
| ~ spl0_4
| ~ spl0_112 ),
inference(resolution,[],[f188,f637]) ).
fof(f1609,plain,
( ~ spl0_113
| spl0_160
| ~ spl0_4
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1606,f636,f187,f1077,f640]) ).
fof(f1614,plain,
( c0_1(a502)
| ~ c1_1(a502)
| ~ spl0_8
| ~ spl0_126 ),
inference(resolution,[],[f202,f693]) ).
fof(f1619,plain,
( ~ spl0_168
| spl0_92
| ~ spl0_8
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1614,f692,f201,f557,f1589]) ).
fof(f1624,plain,
( c1_1(a502)
| ~ c2_1(a502)
| ~ spl0_10
| ~ spl0_126 ),
inference(resolution,[],[f209,f693]) ).
fof(f1632,plain,
( ~ spl0_127
| spl0_168
| ~ spl0_10
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1624,f692,f208,f1589,f696]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f189]) ).
cnf(s2,plain,
( spl0_1
| ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f196]) ).
cnf(s3,plain,
( spl0_1
| ~ spl0_3
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f203]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_9
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f213]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_8
| spl0_9
| spl0_12 ),
inference(sat_conversion,[],[f217]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f234]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_8
| spl0_17
| spl0_20 ),
inference(sat_conversion,[],[f245]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_6
| spl0_12
| spl0_22 ),
inference(sat_conversion,[],[f253]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_17
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f286]) ).
cnf(s22,plain,
( spl0_1
| ~ spl0_3
| spl0_24
| spl0_29 ),
inference(sat_conversion,[],[f312]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_7
| spl0_10
| spl0_26 ),
inference(sat_conversion,[],[f313]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_12
| spl0_37
| spl0_42 ),
inference(sat_conversion,[],[f328]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_12
| spl0_21
| spl0_46 ),
inference(sat_conversion,[],[f345]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_9
| spl0_31
| spl0_48 ),
inference(sat_conversion,[],[f353]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_5
| spl0_46
| spl0_49 ),
inference(sat_conversion,[],[f357]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_4
| spl0_45
| spl0_50 ),
inference(sat_conversion,[],[f364]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_22
| spl0_25
| spl0_42 ),
inference(sat_conversion,[],[f372]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_21
| spl0_27
| spl0_33 ),
inference(sat_conversion,[],[f374]) ).
cnf(s43,plain,
( spl0_2
| ~ spl0_3
| spl0_20
| spl0_42 ),
inference(sat_conversion,[],[f375]) ).
cnf(s44,plain,
( spl0_2
| ~ spl0_3
| spl0_51
| spl0_53 ),
inference(sat_conversion,[],[f379]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_15
| spl0_38
| spl0_54 ),
inference(sat_conversion,[],[f389]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_42
| spl0_48
| spl0_56 ),
inference(sat_conversion,[],[f393]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_31
| spl0_45
| spl0_57 ),
inference(sat_conversion,[],[f397]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_5
| spl0_22
| spl0_50 ),
inference(sat_conversion,[],[f398]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_9
| spl0_23
| spl0_48 ),
inference(sat_conversion,[],[f399]) ).
cnf(s53,plain,
( ~ spl0_48
| ~ spl0_58 ),
inference(sat_conversion,[],[f404]) ).
cnf(s54,plain,
( ~ spl0_48
| ~ spl0_59 ),
inference(sat_conversion,[],[f408]) ).
cnf(s55,plain,
( ~ spl0_23
| ~ spl0_60 ),
inference(sat_conversion,[],[f413]) ).
cnf(s56,plain,
( ~ spl0_23
| ~ spl0_61 ),
inference(sat_conversion,[],[f417]) ).
cnf(s57,plain,
( ~ spl0_45
| ~ spl0_62 ),
inference(sat_conversion,[],[f422]) ).
cnf(s58,plain,
( ~ spl0_45
| ~ spl0_63 ),
inference(sat_conversion,[],[f426]) ).
cnf(s59,plain,
( ~ spl0_45
| ~ spl0_64 ),
inference(sat_conversion,[],[f430]) ).
cnf(s60,plain,
( ~ spl0_22
| ~ spl0_65 ),
inference(sat_conversion,[],[f435]) ).
cnf(s64,plain,
( ~ spl0_57
| ~ spl0_69 ),
inference(sat_conversion,[],[f454]) ).
cnf(s65,plain,
( ~ spl0_57
| ~ spl0_70 ),
inference(sat_conversion,[],[f458]) ).
cnf(s66,plain,
( ~ spl0_21
| ~ spl0_71 ),
inference(sat_conversion,[],[f463]) ).
cnf(s67,plain,
( ~ spl0_21
| ~ spl0_72 ),
inference(sat_conversion,[],[f467]) ).
cnf(s68,plain,
( ~ spl0_26
| ~ spl0_73 ),
inference(sat_conversion,[],[f472]) ).
cnf(s69,plain,
( ~ spl0_24
| ~ spl0_74 ),
inference(sat_conversion,[],[f477]) ).
cnf(s71,plain,
( ~ spl0_27
| ~ spl0_76 ),
inference(sat_conversion,[],[f487]) ).
cnf(s72,plain,
( ~ spl0_27
| ~ spl0_77 ),
inference(sat_conversion,[],[f491]) ).
cnf(s73,plain,
( ~ spl0_42
| ~ spl0_78 ),
inference(sat_conversion,[],[f496]) ).
cnf(s74,plain,
( ~ spl0_42
| ~ spl0_79 ),
inference(sat_conversion,[],[f500]) ).
cnf(s75,plain,
( ~ spl0_42
| ~ spl0_80 ),
inference(sat_conversion,[],[f504]) ).
cnf(s77,plain,
( ~ spl0_20
| ~ spl0_82 ),
inference(sat_conversion,[],[f514]) ).
cnf(s78,plain,
( ~ spl0_20
| ~ spl0_83 ),
inference(sat_conversion,[],[f518]) ).
cnf(s79,plain,
( ~ spl0_20
| ~ spl0_84 ),
inference(sat_conversion,[],[f522]) ).
cnf(s80,plain,
( ~ spl0_50
| ~ spl0_85 ),
inference(sat_conversion,[],[f527]) ).
cnf(s81,plain,
( ~ spl0_54
| ~ spl0_86 ),
inference(sat_conversion,[],[f532]) ).
cnf(s82,plain,
( ~ spl0_54
| ~ spl0_87 ),
inference(sat_conversion,[],[f536]) ).
cnf(s83,plain,
( ~ spl0_15
| ~ spl0_88 ),
inference(sat_conversion,[],[f541]) ).
cnf(s84,plain,
( ~ spl0_15
| ~ spl0_89 ),
inference(sat_conversion,[],[f545]) ).
cnf(s85,plain,
( ~ spl0_15
| ~ spl0_90 ),
inference(sat_conversion,[],[f549]) ).
cnf(s87,plain,
( ~ spl0_53
| ~ spl0_92 ),
inference(sat_conversion,[],[f559]) ).
cnf(s88,plain,
( ~ spl0_51
| ~ spl0_93 ),
inference(sat_conversion,[],[f564]) ).
cnf(s90,plain,
( ~ spl0_95
| ~ spl0_96 ),
inference(sat_conversion,[],[f576]) ).
cnf(s91,plain,
( ~ spl0_97
| ~ spl0_98 ),
inference(sat_conversion,[],[f583]) ).
cnf(s92,plain,
( ~ spl0_97
| ~ spl0_99 ),
inference(sat_conversion,[],[f587]) ).
cnf(s95,plain,
( ~ spl0_48
| spl0_103 ),
inference(sat_conversion,[],[f602]) ).
cnf(s96,plain,
( ~ spl0_23
| spl0_104 ),
inference(sat_conversion,[],[f606]) ).
cnf(s97,plain,
( ~ spl0_22
| spl0_105 ),
inference(sat_conversion,[],[f610]) ).
cnf(s98,plain,
( ~ spl0_22
| spl0_106 ),
inference(sat_conversion,[],[f614]) ).
cnf(s100,plain,
( ~ spl0_41
| spl0_108 ),
inference(sat_conversion,[],[f622]) ).
cnf(s101,plain,
( ~ spl0_41
| spl0_109 ),
inference(sat_conversion,[],[f626]) ).
cnf(s102,plain,
( ~ spl0_57
| spl0_110 ),
inference(sat_conversion,[],[f630]) ).
cnf(s104,plain,
( ~ spl0_26
| spl0_112 ),
inference(sat_conversion,[],[f638]) ).
cnf(s105,plain,
( ~ spl0_26
| spl0_113 ),
inference(sat_conversion,[],[f642]) ).
cnf(s106,plain,
( ~ spl0_24
| spl0_114 ),
inference(sat_conversion,[],[f646]) ).
cnf(s107,plain,
( ~ spl0_24
| spl0_115 ),
inference(sat_conversion,[],[f650]) ).
cnf(s110,plain,
( ~ spl0_27
| spl0_118 ),
inference(sat_conversion,[],[f662]) ).
cnf(s113,plain,
( ~ spl0_50
| spl0_121 ),
inference(sat_conversion,[],[f674]) ).
cnf(s114,plain,
( ~ spl0_50
| spl0_122 ),
inference(sat_conversion,[],[f678]) ).
cnf(s115,plain,
( ~ spl0_54
| spl0_123 ),
inference(sat_conversion,[],[f682]) ).
cnf(s118,plain,
( ~ spl0_53
| spl0_126 ),
inference(sat_conversion,[],[f694]) ).
cnf(s119,plain,
( ~ spl0_53
| spl0_127 ),
inference(sat_conversion,[],[f698]) ).
cnf(s120,plain,
( ~ spl0_51
| spl0_128 ),
inference(sat_conversion,[],[f702]) ).
cnf(s121,plain,
( ~ spl0_51
| spl0_129 ),
inference(sat_conversion,[],[f706]) ).
cnf(s124,plain,
( ~ spl0_95
| spl0_132 ),
inference(sat_conversion,[],[f718]) ).
cnf(s125,plain,
( ~ spl0_95
| spl0_133 ),
inference(sat_conversion,[],[f722]) ).
cnf(s128,plain,
( ~ spl0_47
| spl0_136 ),
inference(sat_conversion,[],[f735]) ).
cnf(s130,plain,
( ~ spl0_47
| spl0_138 ),
inference(sat_conversion,[],[f743]) ).
cnf(s131,plain,
( ~ spl0_30
| spl0_139 ),
inference(sat_conversion,[],[f748]) ).
cnf(s133,plain,
( ~ spl0_30
| spl0_141 ),
inference(sat_conversion,[],[f756]) ).
cnf(s134,plain,
( ~ spl0_49
| spl0_142 ),
inference(sat_conversion,[],[f761]) ).
cnf(s135,plain,
( ~ spl0_49
| spl0_143 ),
inference(sat_conversion,[],[f765]) ).
cnf(s136,plain,
( ~ spl0_49
| spl0_144 ),
inference(sat_conversion,[],[f769]) ).
cnf(s140,plain,
( spl0_42
| spl0_51
| spl0_57 ),
inference(sat_conversion,[],[f783]) ).
cnf(s143,plain,
( spl0_24
| spl0_51
| spl0_97 ),
inference(sat_conversion,[],[f788]) ).
cnf(s144,plain,
( spl0_20
| spl0_41
| spl0_47 ),
inference(sat_conversion,[],[f789]) ).
cnf(s145,plain,
( spl0_26
| spl0_50
| spl0_54 ),
inference(sat_conversion,[],[f790]) ).
cnf(s146,plain,
( spl0_15
| spl0_49
| spl0_95 ),
inference(sat_conversion,[],[f792]) ).
cnf(s164,plain,
( spl0_3
| ~ spl0_15 ),
inference(sat_conversion,[],[f811]) ).
cnf(s169,plain,
( spl0_3
| ~ spl0_95 ),
inference(sat_conversion,[],[f816]) ).
cnf(s174,plain,
( spl0_3
| ~ spl0_49 ),
inference(sat_conversion,[],[f821]) ).
cnf(s177,plain,
( ~ spl0_2
| spl0_88
| spl0_89
| ~ spl0_148 ),
inference(sat_conversion,[],[f830]) ).
cnf(s178,plain,
( ~ spl0_2
| spl0_69
| spl0_70
| ~ spl0_110 ),
inference(sat_conversion,[],[f833]) ).
cnf(s185,plain,
( ~ spl0_8
| ~ spl0_121
| ~ spl0_122
| spl0_149 ),
inference(sat_conversion,[],[f866]) ).
cnf(s186,plain,
( ~ spl0_1
| ~ spl0_2
| spl0_31 ),
inference(sat_conversion,[],[f871]) ).
cnf(s187,plain,
( ~ spl0_9
| spl0_78
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f881]) ).
cnf(s201,plain,
( ~ spl0_9
| spl0_89
| spl0_90
| spl0_148 ),
inference(sat_conversion,[],[f964]) ).
cnf(s205,plain,
( ~ spl0_4
| spl0_96
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f980]) ).
cnf(s221,plain,
( ~ spl0_9
| spl0_71
| spl0_72
| spl0_159 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s231,plain,
( ~ spl0_8
| spl0_65
| ~ spl0_105
| ~ spl0_106 ),
inference(sat_conversion,[],[f1098]) ).
cnf(s240,plain,
( ~ spl0_12
| spl0_82
| spl0_83
| ~ spl0_158 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s245,plain,
( ~ spl0_16
| spl0_74
| ~ spl0_114
| ~ spl0_115 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s248,plain,
( ~ spl0_25
| ~ spl0_108
| ~ spl0_109
| spl0_150 ),
inference(sat_conversion,[],[f1162]) ).
cnf(s250,plain,
( ~ spl0_25
| spl0_93
| ~ spl0_128
| ~ spl0_155 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s252,plain,
( ~ spl0_12
| ~ spl0_25
| spl0_38 ),
inference(sat_conversion,[],[f1168]) ).
cnf(s266,plain,
( ~ spl0_33
| spl0_62
| spl0_63
| ~ spl0_161 ),
inference(sat_conversion,[],[f1234]) ).
cnf(s284,plain,
( ~ spl0_25
| ~ spl0_136
| ~ spl0_138
| spl0_164 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s297,plain,
( ~ spl0_46
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f1377]) ).
cnf(s298,plain,
( ~ spl0_46
| spl0_82
| spl0_83
| spl0_158 ),
inference(sat_conversion,[],[f1378]) ).
cnf(s304,plain,
( ~ spl0_56
| spl0_76
| spl0_77
| ~ spl0_118 ),
inference(sat_conversion,[],[f1416]) ).
cnf(s309,plain,
( ~ spl0_12
| spl0_58
| spl0_59
| ~ spl0_103 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s315,plain,
( ~ spl0_38
| spl0_71
| spl0_72
| ~ spl0_159 ),
inference(sat_conversion,[],[f1437]) ).
cnf(s316,plain,
( ~ spl0_7
| spl0_85
| ~ spl0_122
| spl0_149 ),
inference(sat_conversion,[],[f1438]) ).
cnf(s317,plain,
( ~ spl0_2
| spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f1439]) ).
cnf(s325,plain,
( ~ spl0_31
| spl0_93
| ~ spl0_129
| spl0_155 ),
inference(sat_conversion,[],[f1445]) ).
cnf(s331,plain,
( ~ spl0_9
| spl0_83
| spl0_84
| spl0_158 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s332,plain,
( ~ spl0_37
| spl0_82
| spl0_84
| ~ spl0_158 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s333,plain,
( ~ spl0_17
| ~ spl0_128
| ~ spl0_129
| ~ spl0_155 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s342,plain,
( ~ spl0_16
| spl0_93
| ~ spl0_129
| ~ spl0_155 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s363,plain,
( ~ spl0_5
| spl0_62
| spl0_63
| spl0_161 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s364,plain,
( ~ spl0_5
| spl0_82
| spl0_83
| spl0_84 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s367,plain,
( ~ spl0_7
| spl0_86
| spl0_87
| ~ spl0_123 ),
inference(sat_conversion,[],[f1509]) ).
cnf(s372,plain,
( ~ spl0_8
| ~ spl0_139
| ~ spl0_141
| spl0_162 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s379,plain,
( ~ spl0_10
| spl0_93
| ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f1522]) ).
cnf(s381,plain,
( ~ spl0_5
| spl0_9
| ~ spl0_29 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s385,plain,
( ~ spl0_31
| spl0_89
| spl0_90
| ~ spl0_148 ),
inference(sat_conversion,[],[f1526]) ).
cnf(s386,plain,
( ~ spl0_31
| spl0_60
| spl0_61
| ~ spl0_104 ),
inference(sat_conversion,[],[f1527]) ).
cnf(s388,plain,
( ~ spl0_2
| spl0_98
| spl0_99
| ~ spl0_166 ),
inference(sat_conversion,[],[f1537]) ).
cnf(s389,plain,
( ~ spl0_5
| spl0_98
| spl0_99
| spl0_166 ),
inference(sat_conversion,[],[f1539]) ).
cnf(s391,plain,
( ~ spl0_1
| spl0_92
| ~ spl0_126
| ~ spl0_127 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s395,plain,
( ~ spl0_11
| spl0_73
| ~ spl0_113
| ~ spl0_160 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s405,plain,
( ~ spl0_5
| spl0_88
| spl0_89
| spl0_148 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s406,plain,
( ~ spl0_1
| ~ spl0_128
| ~ spl0_129
| spl0_155 ),
inference(sat_conversion,[],[f1574]) ).
cnf(s407,plain,
( ~ spl0_6
| ~ spl0_108
| ~ spl0_109
| ~ spl0_150 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s408,plain,
( ~ spl0_6
| ~ spl0_121
| ~ spl0_122
| ~ spl0_149 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s410,plain,
( ~ spl0_6
| ~ spl0_136
| ~ spl0_138
| ~ spl0_164 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s411,plain,
( ~ spl0_6
| ~ spl0_139
| ~ spl0_141
| ~ spl0_162 ),
inference(sat_conversion,[],[f1593]) ).
cnf(s412,plain,
( ~ spl0_6
| ~ spl0_142
| ~ spl0_143
| ~ spl0_144 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s419,plain,
( ~ spl0_4
| ~ spl0_112
| ~ spl0_113
| spl0_160 ),
inference(sat_conversion,[],[f1609]) ).
cnf(s420,plain,
( ~ spl0_8
| spl0_92
| ~ spl0_126
| ~ spl0_168 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s422,plain,
( ~ spl0_10
| ~ spl0_126
| ~ spl0_127
| spl0_168 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s426,plain,
spl0_3,
inference(rat,[],[s146,s164,s169,s174]) ).
cnf(s427,plain,
( ~ spl0_49
| ~ spl0_6 ),
inference(rat,[],[s412,s134,s135,s136]) ).
cnf(s429,plain,
( ~ spl0_95
| ~ spl0_4 ),
inference(rat,[],[s205,s90,s124,s125]) ).
cnf(s431,plain,
( ~ spl0_50
| ~ spl0_8
| ~ spl0_6 ),
inference(rat,[],[s185,s408,s113,s114]) ).
cnf(s432,plain,
( ~ spl0_8
| ~ spl0_6
| spl0_5 ),
inference(rat,[],[s231,s60,s97,s98,s51,s431,s426]) ).
cnf(s433,plain,
( ~ spl0_50
| ~ spl0_7
| ~ spl0_6 ),
inference(rat,[],[s316,s408,s80,s113,s114]) ).
cnf(s434,plain,
( ~ spl0_20
| ~ spl0_12
| ~ spl0_46 ),
inference(rat,[],[s240,s298,s77,s78]) ).
cnf(s436,plain,
( ~ spl0_48
| ~ spl0_12 ),
inference(rat,[],[s309,s53,s54,s95]) ).
cnf(s437,plain,
( spl0_48
| spl0_9 ),
inference(rat,[],[s386,s55,s56,s96,s33,s52,s426]) ).
cnf(s438,plain,
( spl0_9
| spl0_8 ),
inference(rat,[],[s437,s436,s5,s426]) ).
cnf(s439,plain,
( ~ spl0_42
| ~ spl0_9 ),
inference(rat,[],[s187,s73,s74,s75]) ).
cnf(s440,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s332,s26,s331,s434,s77,s78,s79,s43,s439,s438,s432,s34,s427,s2,s426]) ).
cnf(s441,plain,
( ~ spl0_20
| ~ spl0_5 ),
inference(rat,[],[s364,s77,s78,s79]) ).
cnf(s443,plain,
( ~ spl0_22
| ~ spl0_8 ),
inference(rat,[],[s231,s60,s97,s98]) ).
cnf(s444,plain,
( ~ spl0_54
| ~ spl0_7 ),
inference(rat,[],[s367,s81,s82,s115]) ).
cnf(s446,plain,
( ~ spl0_30
| ~ spl0_6
| ~ spl0_8 ),
inference(rat,[],[s372,s411,s131,s133]) ).
cnf(s450,plain,
( ~ spl0_53
| ~ spl0_10
| ~ spl0_8 ),
inference(rat,[],[s420,s422,s87,s118,s119]) ).
cnf(s451,plain,
( ~ spl0_10
| ~ spl0_8
| spl0_2 ),
inference(rat,[],[s379,s88,s120,s121,s44,s450,s426]) ).
cnf(s452,plain,
( ~ spl0_26
| ~ spl0_11
| ~ spl0_4 ),
inference(rat,[],[s395,s419,s68,s104,s105]) ).
cnf(s453,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s145,s433,s11,s444,s23,s452,s4,s451,s443,s436,s437,s438,s439,s43,s441,s440,s1,s426]) ).
cnf(s454,plain,
( spl0_9
| spl0_1 ),
inference(rat,[],[s405,s385,s83,s84,s85,s17,s7,s317,s245,s69,s106,s107,s22,s381,s446,s432,s11,s436,s443,s437,s438,s453,s426]) ).
cnf(s455,plain,
( ~ spl0_41
| ~ spl0_25
| ~ spl0_6 ),
inference(rat,[],[s248,s407,s100,s101]) ).
cnf(s456,plain,
( ~ spl0_8
| ~ spl0_6
| spl0_42 ),
inference(rat,[],[s284,s410,s128,s130,s144,s455,s441,s40,s432,s443,s426]) ).
cnf(s459,plain,
( ~ spl0_15
| spl0_1 ),
inference(rat,[],[s177,s201,s83,s84,s85,s453,s454]) ).
cnf(s461,plain,
( ~ spl0_21
| ~ spl0_38
| ~ spl0_9 ),
inference(rat,[],[s221,s315,s66,s67]) ).
cnf(s462,plain,
( ~ spl0_6
| spl0_1 ),
inference(rat,[],[s304,s49,s71,s72,s110,s436,s42,s31,s461,s266,s363,s34,s297,s57,s58,s59,s38,s429,s48,s146,s444,s433,s3,s456,s427,s439,s454,s459,s426]) ).
cnf(s463,plain,
( ~ spl0_45
| ~ spl0_46 ),
inference(rat,[],[s297,s57,s58,s59]) ).
cnf(s468,plain,
( ~ spl0_57
| ~ spl0_2 ),
inference(rat,[],[s178,s64,s65,s102]) ).
cnf(s469,plain,
( spl0_22
| spl0_1 ),
inference(rat,[],[s304,s71,s72,s110,s42,s266,s363,s57,s58,s50,s325,s250,s461,s49,s252,s436,s40,s11,s2,s462,s121,s120,s88,s140,s468,s453,s439,s454,s426]) ).
cnf(s470,plain,
spl0_1,
inference(rat,[],[s304,s71,s72,s110,s49,s42,s436,s266,s31,s363,s463,s57,s58,s50,s461,s325,s48,s333,s444,s9,s3,s443,s469,s88,s120,s121,s140,s468,s441,s2,s462,s459,s439,s454,s453,s426]) ).
cnf(s472,plain,
~ spl0_53,
inference(rat,[],[s391,s87,s118,s119,s470]) ).
cnf(s473,plain,
( ~ spl0_51
| spl0_9 ),
inference(rat,[],[s405,s385,s83,s84,s85,s7,s17,s342,s333,s406,s88,s120,s121,s432,s446,s11,s436,s437,s443,s438,s426,s470]) ).
cnf(s475,plain,
( ~ spl0_24
| ~ spl0_16 ),
inference(rat,[],[s245,s69,s106,s107]) ).
cnf(s478,plain,
( ~ spl0_15
| spl0_9 ),
inference(rat,[],[s405,s385,s83,s84,s85,s432,s11,s436,s437,s443,s438,s186,s44,s473,s470,s472,s426]) ).
cnf(s479,plain,
( spl0_16
| spl0_9 ),
inference(rat,[],[s7,s317,s44,s473,s478,s426,s472]) ).
cnf(s480,plain,
spl0_9,
inference(rat,[],[s388,s389,s91,s92,s143,s475,s479,s44,s473,s432,s11,s436,s443,s437,s438,s426,s472]) ).
cnf(s481,plain,
~ spl0_42,
inference(rat,[],[s439,s480]) ).
cnf(s482,plain,
~ spl0_20,
inference(rat,[],[s26,s332,s240,s331,s77,s78,s79,s426,s481,s480]) ).
cnf(s483,plain,
spl0_2,
inference(rat,[],[s43,s481,s426,s482]) ).
cnf(s484,plain,
~ spl0_57,
inference(rat,[],[s468,s483]) ).
cnf(s486,plain,
spl0_51,
inference(rat,[],[s140,s481,s484]) ).
cnf(s487,plain,
spl0_129,
inference(rat,[],[s121,s486]) ).
cnf(s488,plain,
spl0_128,
inference(rat,[],[s120,s486]) ).
cnf(s489,plain,
~ spl0_93,
inference(rat,[],[s88,s486]) ).
cnf(s490,plain,
spl0_155,
inference(rat,[],[s406,s470,s487,s488]) ).
cnf(s492,plain,
~ spl0_17,
inference(rat,[],[s333,s487,s490,s488]) ).
cnf(s493,plain,
~ spl0_25,
inference(rat,[],[s250,s488,s489,s490]) ).
cnf(s495,plain,
spl0_8,
inference(rat,[],[s9,s482,s426,s492]) ).
cnf(s496,plain,
spl0_22,
inference(rat,[],[s40,s481,s426,s493]) ).
cnf(s499,plain,
$false,
inference(rat,[],[s443,s495,s496]) ).
fof(f1637,plain,
$false,
inference(avatar_sat_refutation,[],[s499]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN448-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n017.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 15:59:37 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.99/1.11 % (3671728)Input is clausal, will run a generic CNF schedule.
% 2.99/1.11 % (3671735)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=113191640:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.99/1.11 % (3671738)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=937001767:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.99/1.11 % (3671734)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3128126544:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.99/1.11 % (3671736)lrs+10_1_sil=8000:sp=occurrence:random_seed=485122131:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.99/1.11 % (3671733)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=2122201369:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.99/1.11 % (3671737)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2973557029:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.99/1.11 % (3671739)dis-21_1_sil=8000:lcm=predicate:random_seed=2298609404: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.99/1.11 % (3671739)First to succeed.
% 2.99/1.11 % (3671739)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3671728"
% 2.99/1.11 % (3671737)Also succeeded, but the first one will report.
% 2.99/1.11 % (3671736)Also succeeded, but the first one will report.
% 2.99/1.11 % (3671738)Also succeeded, but the first one will report.
% 2.99/1.11 % (3671739)Refutation found. Thanks to Tanya!
% 2.99/1.11 % SZS status Unsatisfiable for theBenchmark
% 2.99/1.11 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/1.20 % (3671739)------------------------------
% 0.21/1.20 % (3671739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/1.20 % (3671739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/1.20 % (3671739)CaDiCaL version: 2.1.3
% 0.21/1.20 % (3671739)Termination reason: Refutation
% 0.21/1.20 % (3671739)Time elapsed: 0.023 s
% 0.21/1.20 % (3671739)Peak memory usage: 90 MB
% 0.21/1.20 % (3671739)Instructions burned: 34 (million)
% 0.21/1.20 % (3671739)------------------------------
% 0.21/1.20 % (3671739)------------------------------
% 0.21/1.20 % (3671728)Success in time 0.44 s
% 0.21/1.20 % Vampire exiting
%------------------------------------------------------------------------------