%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN445-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 : n018.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:43 PM UTC 2026
% Result : Unsatisfiable 3.21s 1.09s
% Output : Refutation 3.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 190
% Syntax : Number of formulae : 602 ( 15 unt; 107 def)
% Number of atoms : 1803 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 2090 ( 889 ~;1094 |; 0 &)
% ( 107 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 133 ( 132 usr; 129 prp; 0-1 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 90 ( 0 sgn 90 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp26
| hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( ~ hskp29
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
fof(f4,negated_conjecture,
( ~ hskp27
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
fof(f21,negated_conjecture,
( ~ hskp10
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
fof(f32,negated_conjecture,
( hskp29
| hskp27
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
fof(f33,negated_conjecture,
( hskp7
| hskp1
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
fof(f36,negated_conjecture,
( hskp26
| hskp11
| hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( hskp20
| hskp12
| hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f47,negated_conjecture,
( ~ hskp26
| c0_1(a349) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f51,negated_conjecture,
( ~ hskp21
| c3_1(a336) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp20
| c1_1(a333) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f56,negated_conjecture,
( ~ hskp17
| c0_1(a323) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp17
| c2_1(a323) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp16
| c2_1(a321) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp16
| c3_1(a321) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp15
| c1_1(a320) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp14
| c1_1(a315) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp14
| c2_1(a315) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f65,negated_conjecture,
( ~ hskp12
| c3_1(a310) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( ~ hskp11
| c1_1(a309) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( ~ hskp11
| c3_1(a309) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp10
| c1_1(a308) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp10
| c3_1(a308) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f72,negated_conjecture,
( ~ hskp7
| c0_1(a303) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp7
| c1_1(a303) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f76,negated_conjecture,
( ~ hskp3
| c0_1(a299) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp3
| c3_1(a299) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp2
| c1_1(a297) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp1
| c0_1(a295) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp1
| c2_1(a295) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ c2_1(a349)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ c3_1(a349)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ c0_1(a346)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ c1_1(a346)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ c3_1(a346)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f89,negated_conjecture,
( ~ c1_1(a338)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c2_1(a338)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c3_1(a338)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ c0_1(a336)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c1_1(a336)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c2_1(a333)
| ~ hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c3_1(a333)
| ~ hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f99,negated_conjecture,
( ~ c3_1(a323)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c1_1(a321)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c0_1(a320)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ c2_1(a320)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c0_1(a315)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f105,negated_conjecture,
( ~ c0_1(a310)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c2_1(a310)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c2_1(a309)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c0_1(a308)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f113,negated_conjecture,
( ~ c2_1(a303)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f118,negated_conjecture,
( ~ c0_1(a300)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c1_1(a300)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c2_1(a300)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c2_1(a299)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c0_1(a297)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c3_1(a297)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c1_1(a295)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ c0_1(a294)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c2_1(a294)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c3_1(a294)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp2
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f134,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp10
| hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause134) ).
fof(f137,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp14
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f140,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp11
| hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f144,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp15
| hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause144) ).
fof(f148,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp17
| hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f154,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause163) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c1_1(X1)
| hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause167) ).
fof(f169,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f172,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_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] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_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
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f176,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| c2_1(X1)
| c0_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f180,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| c2_1(X1)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f182,definition,
( spl0_1
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f183,plain,
( ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| c2_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,definition,
( spl0_2
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f186,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f188,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f191,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f192,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f180,f191,f188,f185,f182]) ).
fof(f195,definition,
( spl0_5
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f196,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f199,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f202,definition,
( spl0_7
<=> ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f203,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| ~ c1_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f212,definition,
( spl0_10
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f213,plain,
( ! [X2] :
( c0_1(X2)
| c1_1(X2)
| ~ c2_1(X2) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f215,definition,
( spl0_11
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f216,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f219,definition,
( spl0_12
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f220,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f222,definition,
( spl0_13
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f223,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f224,plain,
( spl0_12
| spl0_7
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f176,f222,f188,f202,f219]) ).
fof(f226,definition,
( spl0_14
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f227,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c1_1(X2) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,definition,
( spl0_15
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f230,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl0_16
<=> ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f234,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f235,plain,
( spl0_14
| spl0_12
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f174,f233,f188,f219,f226]) ).
fof(f237,definition,
( spl0_17
<=> ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f238,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1)
| c2_1(X1) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f239,plain,
( spl0_5
| spl0_17
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f173,f185,f188,f237,f195]) ).
fof(f241,definition,
( spl0_18
<=> ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f242,plain,
( ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f243,plain,
( spl0_5
| spl0_12
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f172,f241,f188,f219,f195]) ).
fof(f245,definition,
( spl0_19
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f252,definition,
( spl0_21
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f255,definition,
( spl0_22
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f256,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f257,plain,
( spl0_21
| spl0_15
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f170,f255,f188,f229,f252]) ).
fof(f258,plain,
( spl0_2
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f169,f255,f188,f185]) ).
fof(f260,definition,
( spl0_23
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f264,definition,
( spl0_24
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f265,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( spl0_19
| spl0_6
| ~ spl0_3
| spl0_24 ),
inference(avatar_split_clause,[],[f167,f264,f188,f198,f245]) ).
fof(f275,definition,
( spl0_27
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f278,definition,
( spl0_28
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f279,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f281,definition,
( spl0_29
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f282,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f285,definition,
( spl0_30
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f292,definition,
( spl0_32
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f294,plain,
( spl0_32
| spl0_16
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f163,f182,f188,f233,f292]) ).
fof(f296,definition,
( spl0_33
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f299,definition,
( spl0_34
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f300,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f314,definition,
( spl0_38
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f315,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f327,definition,
( spl0_41
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f330,definition,
( spl0_42
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f331,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) )
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f332,plain,
( spl0_41
| spl0_42
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f155,f185,f188,f330,f327]) ).
fof(f334,definition,
( spl0_43
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f336,plain,
( spl0_43
| spl0_10
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f154,f222,f188,f212,f334]) ).
fof(f347,plain,
( spl0_41
| spl0_5
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f149,f281,f188,f195,f327]) ).
fof(f349,definition,
( spl0_46
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f351,plain,
( spl0_46
| spl0_23
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f148,f191,f188,f260,f349]) ).
fof(f356,definition,
( spl0_48
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f368,definition,
( spl0_51
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f371,definition,
( spl0_52
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f373,plain,
( spl0_51
| spl0_52
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f144,f215,f188,f371,f368]) ).
fof(f380,definition,
( spl0_54
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f384,definition,
( spl0_55
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f386,plain,
( spl0_55
| spl0_21
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f140,f198,f188,f252,f384]) ).
fof(f395,plain,
( spl0_41
| spl0_30
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f137,f233,f188,f285,f327]) ).
fof(f397,definition,
( spl0_58
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f402,definition,
( spl0_59
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f404,plain,
( spl0_21
| spl0_59
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f134,f314,f188,f402,f252]) ).
fof(f408,definition,
( spl0_60
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f410,plain,
( spl0_41
| spl0_60
| ~ spl0_3
| spl0_42 ),
inference(avatar_split_clause,[],[f131,f330,f188,f408,f327]) ).
fof(f412,definition,
( spl0_61
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f414,plain,
( spl0_61
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f130,f182,f188,f412]) ).
fof(f415,plain,
( spl0_46
| ~ spl0_3
| spl0_34 ),
inference(avatar_split_clause,[],[f129,f299,f188,f349]) ).
fof(f416,plain,
( spl0_58
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f128,f278,f188,f397]) ).
fof(f419,definition,
( spl0_62
<=> c3_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f420,plain,
( ~ c3_1(a294)
| spl0_62 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f421,plain,
( ~ spl0_41
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f127,f419,f327]) ).
fof(f423,definition,
( spl0_63
<=> c2_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f425,plain,
( ~ spl0_41
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f126,f423,f327]) ).
fof(f427,definition,
( spl0_64
<=> c0_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f428,plain,
( ~ c0_1(a294)
| spl0_64 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f429,plain,
( ~ spl0_41
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f125,f427,f327]) ).
fof(f432,definition,
( spl0_65
<=> c1_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f434,plain,
( ~ spl0_43
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f124,f432,f334]) ).
fof(f437,definition,
( spl0_66
<=> c3_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f438,plain,
( ~ c3_1(a297)
| spl0_66 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f439,plain,
( ~ spl0_60
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f123,f437,f408]) ).
fof(f441,definition,
( spl0_67
<=> c0_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f442,plain,
( ~ c0_1(a297)
| spl0_67 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f443,plain,
( ~ spl0_60
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f122,f441,f408]) ).
fof(f446,definition,
( spl0_68
<=> c2_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f448,plain,
( ~ spl0_32
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f121,f446,f292]) ).
fof(f451,definition,
( spl0_69
<=> c2_1(a300) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f453,plain,
( ~ spl0_19
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f120,f451,f245]) ).
fof(f455,definition,
( spl0_70
<=> c1_1(a300) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f457,plain,
( ~ spl0_19
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f119,f455,f245]) ).
fof(f459,definition,
( spl0_71
<=> c0_1(a300) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f460,plain,
( ~ c0_1(a300)
| spl0_71 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( ~ spl0_19
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f118,f459,f245]) ).
fof(f482,definition,
( spl0_76
<=> c2_1(a303) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f484,plain,
( ~ spl0_27
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f113,f482,f275]) ).
fof(f505,definition,
( spl0_81
<=> c0_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f507,plain,
( ~ spl0_59
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f108,f505,f402]) ).
fof(f510,definition,
( spl0_82
<=> c2_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f512,plain,
( ~ spl0_21
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f107,f510,f252]) ).
fof(f515,definition,
( spl0_83
<=> c2_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f517,plain,
( ~ spl0_33
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f106,f515,f296]) ).
fof(f519,definition,
( spl0_84
<=> c0_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f520,plain,
( ~ c0_1(a310)
| spl0_84 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f521,plain,
( ~ spl0_33
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f105,f519,f296]) ).
fof(f529,definition,
( spl0_86
<=> c0_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f530,plain,
( ~ c0_1(a315)
| spl0_86 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f531,plain,
( ~ spl0_30
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f103,f529,f285]) ).
fof(f534,definition,
( spl0_87
<=> c2_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f536,plain,
( ~ spl0_52
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f102,f534,f371]) ).
fof(f538,definition,
( spl0_88
<=> c0_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f539,plain,
( ~ c0_1(a320)
| spl0_88 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( ~ spl0_52
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f101,f538,f371]) ).
fof(f543,definition,
( spl0_89
<=> c1_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f545,plain,
( ~ spl0_58
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f100,f543,f397]) ).
fof(f548,definition,
( spl0_90
<=> c3_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f549,plain,
( ~ c3_1(a323)
| spl0_90 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f550,plain,
( ~ spl0_23
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f99,f548,f260]) ).
fof(f567,definition,
( spl0_94
<=> c3_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f568,plain,
( ~ c3_1(a333)
| spl0_94 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f569,plain,
( ~ spl0_55
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f95,f567,f384]) ).
fof(f571,definition,
( spl0_95
<=> c2_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f573,plain,
( ~ spl0_55
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f94,f571,f384]) ).
fof(f576,definition,
( spl0_96
<=> c1_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f578,plain,
( ~ spl0_46
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f93,f576,f349]) ).
fof(f580,definition,
( spl0_97
<=> c0_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f581,plain,
( ~ c0_1(a336)
| spl0_97 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f582,plain,
( ~ spl0_46
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f92,f580,f349]) ).
fof(f585,definition,
( spl0_98
<=> c3_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f586,plain,
( ~ c3_1(a338)
| spl0_98 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f587,plain,
( ~ spl0_61
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f91,f585,f412]) ).
fof(f589,definition,
( spl0_99
<=> c2_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f591,plain,
( ~ spl0_61
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f90,f589,f412]) ).
fof(f593,definition,
( spl0_100
<=> c1_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f595,plain,
( ~ spl0_61
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f89,f593,f412]) ).
fof(f612,definition,
( spl0_104
<=> c3_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f613,plain,
( ~ c3_1(a346)
| spl0_104 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f614,plain,
( ~ spl0_51
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f85,f612,f368]) ).
fof(f616,definition,
( spl0_105
<=> c1_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f618,plain,
( ~ spl0_51
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f84,f616,f368]) ).
fof(f620,definition,
( spl0_106
<=> c0_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f621,plain,
( ~ c0_1(a346)
| spl0_106 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f622,plain,
( ~ spl0_51
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f83,f620,f368]) ).
fof(f625,definition,
( spl0_107
<=> c3_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f626,plain,
( ~ c3_1(a349)
| spl0_107 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f627,plain,
( ~ spl0_48
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f82,f625,f356]) ).
fof(f629,definition,
( spl0_108
<=> c2_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f631,plain,
( ~ spl0_48
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f81,f629,f356]) ).
fof(f633,definition,
( spl0_109
<=> c2_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f635,plain,
( spl0_109
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f80,f334,f633]) ).
fof(f637,definition,
( spl0_110
<=> c0_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f638,plain,
( c0_1(a295)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f639,plain,
( spl0_110
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f79,f334,f637]) ).
fof(f641,definition,
( spl0_111
<=> c1_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f643,plain,
( spl0_111
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f78,f408,f641]) ).
fof(f645,definition,
( spl0_112
<=> c3_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f646,plain,
( c3_1(a299)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f647,plain,
( spl0_112
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f77,f292,f645]) ).
fof(f649,definition,
( spl0_113
<=> c0_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f651,plain,
( spl0_113
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f76,f292,f649]) ).
fof(f661,definition,
( spl0_116
<=> c1_1(a303) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f663,plain,
( spl0_116
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f73,f275,f661]) ).
fof(f665,definition,
( spl0_117
<=> c0_1(a303) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f666,plain,
( c0_1(a303)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f667,plain,
( spl0_117
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f72,f275,f665]) ).
fof(f677,definition,
( spl0_120
<=> c3_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f678,plain,
( c3_1(a308)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f679,plain,
( spl0_120
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f69,f402,f677]) ).
fof(f681,definition,
( spl0_121
<=> c1_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f683,plain,
( spl0_121
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f68,f402,f681]) ).
fof(f685,definition,
( spl0_122
<=> c3_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f686,plain,
( c3_1(a309)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f685]) ).
fof(f687,plain,
( spl0_122
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f67,f252,f685]) ).
fof(f689,definition,
( spl0_123
<=> c1_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f691,plain,
( spl0_123
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f66,f252,f689]) ).
fof(f693,definition,
( spl0_124
<=> c3_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f694,plain,
( c3_1(a310)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f695,plain,
( spl0_124
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f65,f296,f693]) ).
fof(f705,definition,
( spl0_127
<=> c2_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f707,plain,
( spl0_127
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f62,f285,f705]) ).
fof(f709,definition,
( spl0_128
<=> c1_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f711,plain,
( spl0_128
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f61,f285,f709]) ).
fof(f713,definition,
( spl0_129
<=> c1_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f715,plain,
( spl0_129
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f60,f371,f713]) ).
fof(f717,definition,
( spl0_130
<=> c3_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f718,plain,
( c3_1(a321)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f719,plain,
( spl0_130
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f59,f397,f717]) ).
fof(f721,definition,
( spl0_131
<=> c2_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f723,plain,
( spl0_131
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f58,f397,f721]) ).
fof(f725,definition,
( spl0_132
<=> c2_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f727,plain,
( spl0_132
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f57,f260,f725]) ).
fof(f729,definition,
( spl0_133
<=> c0_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f731,plain,
( spl0_133
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f56,f260,f729]) ).
fof(f745,definition,
( spl0_137
<=> c1_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f747,plain,
( spl0_137
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f52,f384,f745]) ).
fof(f749,definition,
( spl0_138
<=> c3_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f750,plain,
( c3_1(a336)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f751,plain,
( spl0_138
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f51,f349,f749]) ).
fof(f765,definition,
( spl0_142
<=> c0_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f767,plain,
( spl0_142
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f47,f356,f765]) ).
fof(f798,definition,
( spl0_150
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f809,plain,
( spl0_51
| spl0_33
| spl0_55 ),
inference(avatar_split_clause,[],[f37,f384,f296,f368]) ).
fof(f810,plain,
( spl0_33
| spl0_21
| spl0_48 ),
inference(avatar_split_clause,[],[f36,f356,f252,f296]) ).
fof(f813,plain,
( spl0_59
| spl0_43
| spl0_27 ),
inference(avatar_split_clause,[],[f33,f275,f334,f402]) ).
fof(f815,plain,
( spl0_59
| spl0_54
| spl0_150 ),
inference(avatar_split_clause,[],[f32,f798,f380,f402]) ).
fof(f827,plain,
( spl0_3
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f21,f402,f188]) ).
fof(f844,plain,
( spl0_3
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f4,f380,f188]) ).
fof(f846,plain,
( spl0_3
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f2,f798,f188]) ).
fof(f847,plain,
( spl0_58
| spl0_48 ),
inference(avatar_split_clause,[],[f1,f356,f397]) ).
fof(f848,plain,
( c2_1(a308)
| ~ c1_1(a308)
| ~ spl0_2
| ~ spl0_120 ),
inference(resolution,[],[f186,f678]) ).
fof(f856,definition,
( spl0_153
<=> c2_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f858,plain,
( ~ spl0_121
| spl0_153
| ~ spl0_2
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f848,f677,f185,f856,f681]) ).
fof(f867,plain,
( c2_1(a310)
| c1_1(a310)
| ~ spl0_5
| spl0_84 ),
inference(resolution,[],[f196,f520]) ).
fof(f869,plain,
( c2_1(a346)
| c1_1(a346)
| ~ spl0_5
| spl0_106 ),
inference(resolution,[],[f196,f621]) ).
fof(f870,plain,
( c2_1(a294)
| c1_1(a294)
| ~ spl0_5
| spl0_64 ),
inference(resolution,[],[f196,f428]) ).
fof(f872,definition,
( spl0_155
<=> c1_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f875,plain,
( spl0_155
| spl0_63
| ~ spl0_5
| spl0_64 ),
inference(avatar_split_clause,[],[f870,f427,f195,f423,f872]) ).
fof(f878,definition,
( spl0_156
<=> c2_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f880,plain,
( spl0_105
| spl0_156
| ~ spl0_5
| spl0_106 ),
inference(avatar_split_clause,[],[f869,f620,f195,f878,f616]) ).
fof(f882,definition,
( spl0_157
<=> c1_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f888,plain,
( c2_1(a310)
| ~ c1_1(a310)
| ~ spl0_7
| spl0_84 ),
inference(resolution,[],[f203,f520]) ).
fof(f892,plain,
( c2_1(a294)
| ~ c1_1(a294)
| ~ spl0_7
| spl0_64 ),
inference(resolution,[],[f203,f428]) ).
fof(f894,plain,
( ~ spl0_155
| spl0_63
| ~ spl0_7
| spl0_64 ),
inference(avatar_split_clause,[],[f892,f427,f202,f423,f872]) ).
fof(f898,plain,
( ~ spl0_157
| spl0_83
| ~ spl0_7
| spl0_84 ),
inference(avatar_split_clause,[],[f888,f519,f202,f515,f882]) ).
fof(f908,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_4 ),
inference(resolution,[],[f183,f192]) ).
fof(f909,plain,
( ~ c1_1(a333)
| c2_1(a333)
| ~ spl0_1
| spl0_94 ),
inference(resolution,[],[f183,f568]) ).
fof(f914,plain,
( ~ c1_1(a294)
| c2_1(a294)
| ~ spl0_1
| spl0_62 ),
inference(resolution,[],[f183,f420]) ).
fof(f915,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f908]) ).
fof(f916,plain,
( spl0_63
| ~ spl0_155
| ~ spl0_1
| spl0_62 ),
inference(avatar_split_clause,[],[f914,f419,f182,f872,f423]) ).
fof(f920,plain,
( spl0_29
| ~ spl0_1
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f915,f191,f182,f281]) ).
fof(f938,plain,
( c0_1(a294)
| c2_1(a294)
| ~ spl0_12
| spl0_62 ),
inference(resolution,[],[f220,f420]) ).
fof(f940,plain,
( spl0_63
| spl0_64
| ~ spl0_12
| spl0_62 ),
inference(avatar_split_clause,[],[f938,f419,f219,f427,f423]) ).
fof(f943,definition,
( spl0_159
<=> c0_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f949,definition,
( spl0_160
<=> c0_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f950,plain,
( c0_1(a333)
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f953,plain,
( c1_1(a321)
| ~ c2_1(a321)
| ~ spl0_13
| ~ spl0_130 ),
inference(resolution,[],[f223,f718]) ).
fof(f962,plain,
( ~ spl0_131
| spl0_89
| ~ spl0_13
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f953,f717,f222,f543,f721]) ).
fof(f965,definition,
( spl0_161
<=> c1_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f995,definition,
( spl0_163
<=> c0_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1005,plain,
( c1_1(a338)
| c2_1(a338)
| ~ spl0_17
| spl0_98 ),
inference(resolution,[],[f238,f586]) ).
fof(f1006,plain,
( c1_1(a294)
| c2_1(a294)
| ~ spl0_17
| spl0_62 ),
inference(resolution,[],[f238,f420]) ).
fof(f1007,plain,
( spl0_63
| spl0_155
| ~ spl0_17
| spl0_62 ),
inference(avatar_split_clause,[],[f1006,f419,f237,f872,f423]) ).
fof(f1021,plain,
( c2_1(a309)
| ~ c1_1(a309)
| ~ spl0_2
| ~ spl0_122 ),
inference(resolution,[],[f186,f686]) ).
fof(f1027,plain,
( ~ spl0_123
| spl0_82
| ~ spl0_2
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1021,f685,f185,f510,f689]) ).
fof(f1034,plain,
( c0_1(a338)
| c1_1(a338)
| ~ spl0_14
| spl0_98 ),
inference(resolution,[],[f227,f586]) ).
fof(f1035,plain,
( c0_1(a294)
| c1_1(a294)
| ~ spl0_14
| spl0_62 ),
inference(resolution,[],[f227,f420]) ).
fof(f1036,plain,
( spl0_155
| spl0_64
| ~ spl0_14
| spl0_62 ),
inference(avatar_split_clause,[],[f1035,f419,f226,f427,f872]) ).
fof(f1037,plain,
( spl0_100
| spl0_159
| ~ spl0_14
| spl0_98 ),
inference(avatar_split_clause,[],[f1034,f585,f226,f943,f593]) ).
fof(f1048,plain,
( c2_1(a320)
| ~ c1_1(a320)
| ~ spl0_7
| spl0_88 ),
inference(resolution,[],[f539,f203]) ).
fof(f1051,plain,
( ~ spl0_129
| spl0_87
| ~ spl0_7
| spl0_88 ),
inference(avatar_split_clause,[],[f1048,f538,f202,f534,f713]) ).
fof(f1069,plain,
( ~ c1_1(a315)
| ~ c2_1(a315)
| ~ spl0_18
| spl0_86 ),
inference(resolution,[],[f242,f530]) ).
fof(f1078,plain,
( ~ spl0_127
| ~ spl0_128
| ~ spl0_18
| spl0_86 ),
inference(avatar_split_clause,[],[f1069,f529,f241,f709,f705]) ).
fof(f1084,plain,
( c0_1(a321)
| ~ c2_1(a321)
| ~ spl0_16
| ~ spl0_130 ),
inference(resolution,[],[f234,f718]) ).
fof(f1086,plain,
( c0_1(a308)
| ~ c2_1(a308)
| ~ spl0_16
| ~ spl0_120 ),
inference(resolution,[],[f234,f678]) ).
fof(f1090,plain,
( ~ spl0_153
| spl0_81
| ~ spl0_16
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1086,f677,f233,f505,f856]) ).
fof(f1091,plain,
( ~ spl0_131
| spl0_163
| ~ spl0_16
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1084,f717,f233,f995,f721]) ).
fof(f1126,plain,
( c1_1(a299)
| ~ c0_1(a299)
| ~ spl0_24
| ~ spl0_112 ),
inference(resolution,[],[f265,f646]) ).
fof(f1128,plain,
( ~ spl0_113
| spl0_161
| ~ spl0_24
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1126,f645,f264,f965,f649]) ).
fof(f1166,plain,
( c2_1(a299)
| c1_1(a299)
| ~ spl0_28
| ~ spl0_112 ),
inference(resolution,[],[f279,f646]) ).
fof(f1167,plain,
( spl0_161
| spl0_68
| ~ spl0_28
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1166,f645,f278,f446,f965]) ).
fof(f1202,plain,
( c2_1(a303)
| ~ c1_1(a303)
| ~ spl0_29
| ~ spl0_117 ),
inference(resolution,[],[f282,f666]) ).
fof(f1212,plain,
( ~ spl0_116
| spl0_76
| ~ spl0_29
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1202,f665,f281,f482,f661]) ).
fof(f1215,plain,
( spl0_157
| spl0_83
| ~ spl0_5
| spl0_84 ),
inference(avatar_split_clause,[],[f867,f519,f195,f515,f882]) ).
fof(f1266,plain,
( c1_1(a336)
| ~ c2_1(a336)
| ~ spl0_13
| ~ spl0_138 ),
inference(resolution,[],[f750,f223]) ).
fof(f1271,plain,
( c2_1(a336)
| c1_1(a336)
| ~ spl0_28
| ~ spl0_138 ),
inference(resolution,[],[f750,f279]) ).
fof(f1274,definition,
( spl0_169
<=> c2_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1276,plain,
( spl0_96
| spl0_169
| ~ spl0_28
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1271,f749,f278,f1274,f576]) ).
fof(f1280,plain,
( ~ spl0_169
| spl0_96
| ~ spl0_13
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1266,f749,f222,f576,f1274]) ).
fof(f1310,plain,
( c2_1(a336)
| c1_1(a336)
| ~ spl0_5
| spl0_97 ),
inference(resolution,[],[f196,f581]) ).
fof(f1314,plain,
( c2_1(a300)
| c1_1(a300)
| ~ spl0_5
| spl0_71 ),
inference(resolution,[],[f196,f460]) ).
fof(f1317,plain,
( spl0_70
| spl0_69
| ~ spl0_5
| spl0_71 ),
inference(avatar_split_clause,[],[f1314,f459,f195,f451,f455]) ).
fof(f1318,plain,
( spl0_96
| spl0_169
| ~ spl0_5
| spl0_97 ),
inference(avatar_split_clause,[],[f1310,f580,f195,f1274,f576]) ).
fof(f1355,plain,
( ~ c0_1(a323)
| ~ c2_1(a323)
| ~ spl0_15
| spl0_90 ),
inference(resolution,[],[f230,f549]) ).
fof(f1365,plain,
( ~ spl0_132
| ~ spl0_133
| ~ spl0_15
| spl0_90 ),
inference(avatar_split_clause,[],[f1355,f548,f229,f729,f725]) ).
fof(f1448,plain,
( ~ c0_1(a349)
| c2_1(a349)
| ~ spl0_34
| spl0_107 ),
inference(resolution,[],[f300,f626]) ).
fof(f1455,plain,
( ~ c0_1(a338)
| c2_1(a338)
| ~ spl0_34
| spl0_98 ),
inference(resolution,[],[f300,f586]) ).
fof(f1462,plain,
( spl0_99
| ~ spl0_159
| ~ spl0_34
| spl0_98 ),
inference(avatar_split_clause,[],[f1455,f585,f299,f943,f589]) ).
fof(f1464,plain,
( spl0_108
| ~ spl0_142
| ~ spl0_34
| spl0_107 ),
inference(avatar_split_clause,[],[f1448,f625,f299,f765,f629]) ).
fof(f1536,plain,
( c2_1(a310)
| c0_1(a310)
| ~ spl0_38
| ~ spl0_124 ),
inference(resolution,[],[f315,f694]) ).
fof(f1538,plain,
( spl0_84
| spl0_83
| ~ spl0_38
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1536,f693,f314,f515,f519]) ).
fof(f1544,plain,
( c0_1(a336)
| ~ c2_1(a336)
| ~ spl0_16
| ~ spl0_138 ),
inference(resolution,[],[f750,f234]) ).
fof(f1546,plain,
( c2_1(a336)
| c0_1(a336)
| ~ spl0_38
| ~ spl0_138 ),
inference(resolution,[],[f750,f315]) ).
fof(f1547,plain,
( spl0_97
| spl0_169
| ~ spl0_38
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1546,f749,f314,f1274,f580]) ).
fof(f1548,plain,
( ~ spl0_169
| spl0_97
| ~ spl0_16
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1544,f749,f233,f580,f1274]) ).
fof(f1558,plain,
( spl0_99
| spl0_100
| ~ spl0_17
| spl0_98 ),
inference(avatar_split_clause,[],[f1005,f585,f237,f593,f589]) ).
fof(f1584,plain,
( c1_1(a295)
| ~ c2_1(a295)
| ~ spl0_6
| ~ spl0_110 ),
inference(resolution,[],[f199,f638]) ).
fof(f1597,plain,
( c1_1(a336)
| ~ c2_1(a336)
| ~ spl0_10
| spl0_97 ),
inference(resolution,[],[f213,f581]) ).
fof(f1604,plain,
( c1_1(a346)
| ~ c2_1(a346)
| ~ spl0_10
| spl0_106 ),
inference(resolution,[],[f213,f621]) ).
fof(f1623,plain,
( c0_1(a338)
| c2_1(a338)
| ~ spl0_12
| spl0_98 ),
inference(resolution,[],[f220,f586]) ).
fof(f1624,plain,
( spl0_99
| spl0_159
| ~ spl0_12
| spl0_98 ),
inference(avatar_split_clause,[],[f1623,f585,f219,f943,f589]) ).
fof(f1654,plain,
( ~ c0_1(a321)
| ~ c2_1(a321)
| ~ spl0_22
| ~ spl0_130 ),
inference(resolution,[],[f256,f718]) ).
fof(f1660,plain,
( ~ spl0_131
| ~ spl0_163
| ~ spl0_22
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1654,f717,f255,f995,f721]) ).
fof(f1675,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c1_1(X0)
| c2_1(X0) )
| ~ spl0_17
| ~ spl0_42 ),
inference(resolution,[],[f331,f238]) ).
fof(f1676,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_12
| ~ spl0_42 ),
inference(resolution,[],[f331,f220]) ).
fof(f1682,plain,
( c1_1(a336)
| c0_1(a336)
| ~ spl0_42
| ~ spl0_138 ),
inference(resolution,[],[f331,f750]) ).
fof(f1683,plain,
( c1_1(a321)
| c0_1(a321)
| ~ spl0_42
| ~ spl0_130 ),
inference(resolution,[],[f331,f718]) ).
fof(f1687,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_12
| ~ spl0_42 ),
inference(duplicate_literal_removal,[],[f1676]) ).
fof(f1688,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_17
| ~ spl0_42 ),
inference(duplicate_literal_removal,[],[f1675]) ).
fof(f1690,plain,
( spl0_163
| spl0_89
| ~ spl0_42
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1683,f717,f330,f543,f995]) ).
fof(f1691,plain,
( spl0_97
| spl0_96
| ~ spl0_42
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1682,f749,f330,f576,f580]) ).
fof(f1694,plain,
( spl0_5
| ~ spl0_12
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1687,f330,f219,f195]) ).
fof(f1695,plain,
( spl0_5
| ~ spl0_17
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1688,f330,f237,f195]) ).
fof(f1700,plain,
( ~ c1_1(a297)
| ~ c2_1(a297)
| ~ spl0_11
| spl0_66 ),
inference(resolution,[],[f438,f216]) ).
fof(f1706,definition,
( spl0_173
<=> c2_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1710,plain,
( ~ spl0_173
| ~ spl0_111
| ~ spl0_11
| spl0_66 ),
inference(avatar_split_clause,[],[f1700,f437,f215,f641,f1706]) ).
fof(f1719,plain,
( c2_1(a297)
| ~ c1_1(a297)
| ~ spl0_7
| spl0_67 ),
inference(resolution,[],[f442,f203]) ).
fof(f1720,plain,
( ~ spl0_111
| spl0_173
| ~ spl0_7
| spl0_67 ),
inference(avatar_split_clause,[],[f1719,f441,f202,f1706,f641]) ).
fof(f1725,plain,
( c0_1(a333)
| c2_1(a333)
| ~ spl0_12
| spl0_94 ),
inference(resolution,[],[f568,f220]) ).
fof(f1726,plain,
( spl0_95
| spl0_160
| ~ spl0_12
| spl0_94 ),
inference(avatar_split_clause,[],[f1725,f567,f219,f949,f571]) ).
fof(f1728,plain,
( c0_1(a346)
| c2_1(a346)
| ~ spl0_12
| spl0_104 ),
inference(resolution,[],[f613,f220]) ).
fof(f1729,plain,
( spl0_156
| spl0_106
| ~ spl0_12
| spl0_104 ),
inference(avatar_split_clause,[],[f1728,f612,f219,f620,f878]) ).
fof(f1738,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_2
| ~ spl0_12 ),
inference(resolution,[],[f186,f220]) ).
fof(f1746,plain,
( c2_1(a299)
| ~ c1_1(a299)
| ~ spl0_2
| ~ spl0_112 ),
inference(resolution,[],[f186,f646]) ).
fof(f1747,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_2
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f1738]) ).
fof(f1748,plain,
( ~ spl0_161
| spl0_68
| ~ spl0_2
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1746,f645,f185,f446,f965]) ).
fof(f1759,plain,
( ~ c0_1(a299)
| ~ c1_1(a299)
| ~ spl0_4
| ~ spl0_112 ),
inference(resolution,[],[f192,f646]) ).
fof(f1761,plain,
( ~ spl0_161
| ~ spl0_113
| ~ spl0_4
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1759,f645,f191,f649,f965]) ).
fof(f1764,plain,
( c2_1(a333)
| ~ c1_1(a333)
| ~ spl0_29
| ~ spl0_160 ),
inference(resolution,[],[f950,f282]) ).
fof(f1765,plain,
( ~ spl0_137
| spl0_95
| ~ spl0_29
| ~ spl0_160 ),
inference(avatar_split_clause,[],[f1764,f949,f281,f571,f745]) ).
fof(f1766,plain,
( spl0_95
| ~ spl0_137
| ~ spl0_1
| spl0_94 ),
inference(avatar_split_clause,[],[f909,f567,f182,f745,f571]) ).
fof(f1773,plain,
( ~ spl0_109
| spl0_65
| ~ spl0_6
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f1584,f637,f198,f432,f633]) ).
fof(f1775,plain,
( ~ spl0_169
| spl0_96
| ~ spl0_10
| spl0_97 ),
inference(avatar_split_clause,[],[f1597,f580,f212,f576,f1274]) ).
fof(f1777,plain,
( ~ spl0_156
| spl0_105
| ~ spl0_10
| spl0_106 ),
inference(avatar_split_clause,[],[f1604,f620,f212,f616,f878]) ).
fof(f1788,plain,
( spl0_7
| ~ spl0_2
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1747,f219,f185,f202]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f193]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_7
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f224]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_12
| spl0_14
| spl0_16 ),
inference(sat_conversion,[],[f235]) ).
cnf(s8,plain,
( spl0_2
| ~ spl0_3
| spl0_5
| spl0_17 ),
inference(sat_conversion,[],[f239]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_5
| spl0_12
| spl0_18 ),
inference(sat_conversion,[],[f243]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_15
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f257]) ).
cnf(s12,plain,
( spl0_2
| ~ spl0_3
| spl0_22 ),
inference(sat_conversion,[],[f258]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_6
| spl0_19
| spl0_24 ),
inference(sat_conversion,[],[f266]) ).
cnf(s18,plain,
( spl0_1
| ~ spl0_3
| spl0_16
| spl0_32 ),
inference(sat_conversion,[],[f294]) ).
cnf(s26,plain,
( spl0_2
| ~ spl0_3
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f332]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_10
| spl0_13
| spl0_43 ),
inference(sat_conversion,[],[f336]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_5
| spl0_29
| spl0_41 ),
inference(sat_conversion,[],[f347]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_4
| spl0_23
| spl0_46 ),
inference(sat_conversion,[],[f351]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_11
| spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f373]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_6
| spl0_21
| spl0_55 ),
inference(sat_conversion,[],[f386]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_16
| spl0_30
| spl0_41 ),
inference(sat_conversion,[],[f395]) ).
cnf(s47,plain,
( ~ spl0_3
| spl0_21
| spl0_38
| spl0_59 ),
inference(sat_conversion,[],[f404]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_41
| spl0_42
| spl0_60 ),
inference(sat_conversion,[],[f410]) ).
cnf(s51,plain,
( spl0_1
| ~ spl0_3
| spl0_61 ),
inference(sat_conversion,[],[f414]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_34
| spl0_46 ),
inference(sat_conversion,[],[f415]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_28
| spl0_58 ),
inference(sat_conversion,[],[f416]) ).
cnf(s54,plain,
( ~ spl0_41
| ~ spl0_62 ),
inference(sat_conversion,[],[f421]) ).
cnf(s55,plain,
( ~ spl0_41
| ~ spl0_63 ),
inference(sat_conversion,[],[f425]) ).
cnf(s56,plain,
( ~ spl0_41
| ~ spl0_64 ),
inference(sat_conversion,[],[f429]) ).
cnf(s57,plain,
( ~ spl0_43
| ~ spl0_65 ),
inference(sat_conversion,[],[f434]) ).
cnf(s58,plain,
( ~ spl0_60
| ~ spl0_66 ),
inference(sat_conversion,[],[f439]) ).
cnf(s59,plain,
( ~ spl0_60
| ~ spl0_67 ),
inference(sat_conversion,[],[f443]) ).
cnf(s60,plain,
( ~ spl0_32
| ~ spl0_68 ),
inference(sat_conversion,[],[f448]) ).
cnf(s61,plain,
( ~ spl0_19
| ~ spl0_69 ),
inference(sat_conversion,[],[f453]) ).
cnf(s62,plain,
( ~ spl0_19
| ~ spl0_70 ),
inference(sat_conversion,[],[f457]) ).
cnf(s63,plain,
( ~ spl0_19
| ~ spl0_71 ),
inference(sat_conversion,[],[f461]) ).
cnf(s68,plain,
( ~ spl0_27
| ~ spl0_76 ),
inference(sat_conversion,[],[f484]) ).
cnf(s73,plain,
( ~ spl0_59
| ~ spl0_81 ),
inference(sat_conversion,[],[f507]) ).
cnf(s74,plain,
( ~ spl0_21
| ~ spl0_82 ),
inference(sat_conversion,[],[f512]) ).
cnf(s75,plain,
( ~ spl0_33
| ~ spl0_83 ),
inference(sat_conversion,[],[f517]) ).
cnf(s76,plain,
( ~ spl0_33
| ~ spl0_84 ),
inference(sat_conversion,[],[f521]) ).
cnf(s78,plain,
( ~ spl0_30
| ~ spl0_86 ),
inference(sat_conversion,[],[f531]) ).
cnf(s79,plain,
( ~ spl0_52
| ~ spl0_87 ),
inference(sat_conversion,[],[f536]) ).
cnf(s80,plain,
( ~ spl0_52
| ~ spl0_88 ),
inference(sat_conversion,[],[f540]) ).
cnf(s81,plain,
( ~ spl0_58
| ~ spl0_89 ),
inference(sat_conversion,[],[f545]) ).
cnf(s82,plain,
( ~ spl0_23
| ~ spl0_90 ),
inference(sat_conversion,[],[f550]) ).
cnf(s86,plain,
( ~ spl0_55
| ~ spl0_94 ),
inference(sat_conversion,[],[f569]) ).
cnf(s87,plain,
( ~ spl0_55
| ~ spl0_95 ),
inference(sat_conversion,[],[f573]) ).
cnf(s88,plain,
( ~ spl0_46
| ~ spl0_96 ),
inference(sat_conversion,[],[f578]) ).
cnf(s89,plain,
( ~ spl0_46
| ~ spl0_97 ),
inference(sat_conversion,[],[f582]) ).
cnf(s90,plain,
( ~ spl0_61
| ~ spl0_98 ),
inference(sat_conversion,[],[f587]) ).
cnf(s91,plain,
( ~ spl0_61
| ~ spl0_99 ),
inference(sat_conversion,[],[f591]) ).
cnf(s92,plain,
( ~ spl0_61
| ~ spl0_100 ),
inference(sat_conversion,[],[f595]) ).
cnf(s96,plain,
( ~ spl0_51
| ~ spl0_104 ),
inference(sat_conversion,[],[f614]) ).
cnf(s97,plain,
( ~ spl0_51
| ~ spl0_105 ),
inference(sat_conversion,[],[f618]) ).
cnf(s98,plain,
( ~ spl0_51
| ~ spl0_106 ),
inference(sat_conversion,[],[f622]) ).
cnf(s99,plain,
( ~ spl0_48
| ~ spl0_107 ),
inference(sat_conversion,[],[f627]) ).
cnf(s100,plain,
( ~ spl0_48
| ~ spl0_108 ),
inference(sat_conversion,[],[f631]) ).
cnf(s101,plain,
( ~ spl0_43
| spl0_109 ),
inference(sat_conversion,[],[f635]) ).
cnf(s102,plain,
( ~ spl0_43
| spl0_110 ),
inference(sat_conversion,[],[f639]) ).
cnf(s103,plain,
( ~ spl0_60
| spl0_111 ),
inference(sat_conversion,[],[f643]) ).
cnf(s104,plain,
( ~ spl0_32
| spl0_112 ),
inference(sat_conversion,[],[f647]) ).
cnf(s105,plain,
( ~ spl0_32
| spl0_113 ),
inference(sat_conversion,[],[f651]) ).
cnf(s108,plain,
( ~ spl0_27
| spl0_116 ),
inference(sat_conversion,[],[f663]) ).
cnf(s109,plain,
( ~ spl0_27
| spl0_117 ),
inference(sat_conversion,[],[f667]) ).
cnf(s112,plain,
( ~ spl0_59
| spl0_120 ),
inference(sat_conversion,[],[f679]) ).
cnf(s113,plain,
( ~ spl0_59
| spl0_121 ),
inference(sat_conversion,[],[f683]) ).
cnf(s114,plain,
( ~ spl0_21
| spl0_122 ),
inference(sat_conversion,[],[f687]) ).
cnf(s115,plain,
( ~ spl0_21
| spl0_123 ),
inference(sat_conversion,[],[f691]) ).
cnf(s116,plain,
( ~ spl0_33
| spl0_124 ),
inference(sat_conversion,[],[f695]) ).
cnf(s119,plain,
( ~ spl0_30
| spl0_127 ),
inference(sat_conversion,[],[f707]) ).
cnf(s120,plain,
( ~ spl0_30
| spl0_128 ),
inference(sat_conversion,[],[f711]) ).
cnf(s121,plain,
( ~ spl0_52
| spl0_129 ),
inference(sat_conversion,[],[f715]) ).
cnf(s122,plain,
( ~ spl0_58
| spl0_130 ),
inference(sat_conversion,[],[f719]) ).
cnf(s123,plain,
( ~ spl0_58
| spl0_131 ),
inference(sat_conversion,[],[f723]) ).
cnf(s124,plain,
( ~ spl0_23
| spl0_132 ),
inference(sat_conversion,[],[f727]) ).
cnf(s125,plain,
( ~ spl0_23
| spl0_133 ),
inference(sat_conversion,[],[f731]) ).
cnf(s129,plain,
( ~ spl0_55
| spl0_137 ),
inference(sat_conversion,[],[f747]) ).
cnf(s130,plain,
( ~ spl0_46
| spl0_138 ),
inference(sat_conversion,[],[f751]) ).
cnf(s134,plain,
( ~ spl0_48
| spl0_142 ),
inference(sat_conversion,[],[f767]) ).
cnf(s144,plain,
( spl0_33
| spl0_51
| spl0_55 ),
inference(sat_conversion,[],[f809]) ).
cnf(s145,plain,
( spl0_21
| spl0_33
| spl0_48 ),
inference(sat_conversion,[],[f810]) ).
cnf(s148,plain,
( spl0_27
| spl0_43
| spl0_59 ),
inference(sat_conversion,[],[f813]) ).
cnf(s149,plain,
( spl0_54
| spl0_59
| spl0_150 ),
inference(sat_conversion,[],[f815]) ).
cnf(s160,plain,
( spl0_3
| ~ spl0_59 ),
inference(sat_conversion,[],[f827]) ).
cnf(s177,plain,
( spl0_3
| ~ spl0_54 ),
inference(sat_conversion,[],[f844]) ).
cnf(s179,plain,
( spl0_3
| ~ spl0_150 ),
inference(sat_conversion,[],[f846]) ).
cnf(s180,plain,
( spl0_48
| spl0_58 ),
inference(sat_conversion,[],[f847]) ).
cnf(s182,plain,
( ~ spl0_2
| ~ spl0_120
| ~ spl0_121
| spl0_153 ),
inference(sat_conversion,[],[f858]) ).
cnf(s184,plain,
( ~ spl0_5
| spl0_63
| spl0_64
| spl0_155 ),
inference(sat_conversion,[],[f875]) ).
cnf(s185,plain,
( ~ spl0_5
| spl0_105
| spl0_106
| spl0_156 ),
inference(sat_conversion,[],[f880]) ).
cnf(s187,plain,
( ~ spl0_7
| spl0_63
| spl0_64
| ~ spl0_155 ),
inference(sat_conversion,[],[f894]) ).
cnf(s190,plain,
( ~ spl0_7
| spl0_83
| spl0_84
| ~ spl0_157 ),
inference(sat_conversion,[],[f898]) ).
cnf(s193,plain,
( ~ spl0_1
| spl0_62
| spl0_63
| ~ spl0_155 ),
inference(sat_conversion,[],[f916]) ).
cnf(s195,plain,
( ~ spl0_1
| ~ spl0_4
| spl0_29 ),
inference(sat_conversion,[],[f920]) ).
cnf(s198,plain,
( ~ spl0_12
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f940]) ).
cnf(s203,plain,
( ~ spl0_13
| spl0_89
| ~ spl0_130
| ~ spl0_131 ),
inference(sat_conversion,[],[f962]) ).
cnf(s210,plain,
( ~ spl0_17
| spl0_62
| spl0_63
| spl0_155 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s218,plain,
( ~ spl0_2
| spl0_82
| ~ spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s219,plain,
( ~ spl0_14
| spl0_62
| spl0_64
| spl0_155 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s220,plain,
( ~ spl0_14
| spl0_98
| spl0_100
| spl0_159 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s225,plain,
( ~ spl0_7
| spl0_87
| spl0_88
| ~ spl0_129 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s232,plain,
( ~ spl0_18
| spl0_86
| ~ spl0_127
| ~ spl0_128 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s236,plain,
( ~ spl0_16
| spl0_81
| ~ spl0_120
| ~ spl0_153 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s237,plain,
( ~ spl0_16
| ~ spl0_130
| ~ spl0_131
| spl0_163 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s246,plain,
( ~ spl0_24
| ~ spl0_112
| ~ spl0_113
| spl0_161 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s253,plain,
( ~ spl0_28
| spl0_68
| ~ spl0_112
| spl0_161 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s264,plain,
( ~ spl0_29
| spl0_76
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s266,plain,
( ~ spl0_5
| spl0_83
| spl0_84
| spl0_157 ),
inference(sat_conversion,[],[f1215]) ).
cnf(s285,plain,
( ~ spl0_28
| spl0_96
| ~ spl0_138
| spl0_169 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s287,plain,
( ~ spl0_13
| spl0_96
| ~ spl0_138
| ~ spl0_169 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s297,plain,
( ~ spl0_5
| spl0_69
| spl0_70
| spl0_71 ),
inference(sat_conversion,[],[f1317]) ).
cnf(s298,plain,
( ~ spl0_5
| spl0_96
| spl0_97
| spl0_169 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s309,plain,
( ~ spl0_15
| spl0_90
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f1365]) ).
cnf(s331,plain,
( ~ spl0_34
| spl0_98
| spl0_99
| ~ spl0_159 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s333,plain,
( ~ spl0_34
| spl0_107
| spl0_108
| ~ spl0_142 ),
inference(sat_conversion,[],[f1464]) ).
cnf(s355,plain,
( ~ spl0_38
| spl0_83
| spl0_84
| ~ spl0_124 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s359,plain,
( ~ spl0_38
| spl0_97
| ~ spl0_138
| spl0_169 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s360,plain,
( ~ spl0_16
| spl0_97
| ~ spl0_138
| ~ spl0_169 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s371,plain,
( ~ spl0_17
| spl0_98
| spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s395,plain,
( ~ spl0_12
| spl0_98
| spl0_99
| spl0_159 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s410,plain,
( ~ spl0_22
| ~ spl0_130
| ~ spl0_131
| ~ spl0_163 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s420,plain,
( ~ spl0_42
| spl0_89
| ~ spl0_130
| spl0_163 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s421,plain,
( ~ spl0_42
| spl0_96
| spl0_97
| ~ spl0_138 ),
inference(sat_conversion,[],[f1691]) ).
cnf(s423,plain,
( spl0_5
| ~ spl0_12
| ~ spl0_42 ),
inference(sat_conversion,[],[f1694]) ).
cnf(s424,plain,
( spl0_5
| ~ spl0_17
| ~ spl0_42 ),
inference(sat_conversion,[],[f1695]) ).
cnf(s428,plain,
( ~ spl0_11
| spl0_66
| ~ spl0_111
| ~ spl0_173 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s439,plain,
( ~ spl0_7
| spl0_67
| ~ spl0_111
| spl0_173 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s441,plain,
( ~ spl0_12
| spl0_94
| spl0_95
| spl0_160 ),
inference(sat_conversion,[],[f1726]) ).
cnf(s442,plain,
( ~ spl0_12
| spl0_104
| spl0_106
| spl0_156 ),
inference(sat_conversion,[],[f1729]) ).
cnf(s444,plain,
( ~ spl0_2
| spl0_68
| ~ spl0_112
| ~ spl0_161 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s445,plain,
( ~ spl0_4
| ~ spl0_112
| ~ spl0_113
| ~ spl0_161 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s448,plain,
( ~ spl0_29
| spl0_95
| ~ spl0_137
| ~ spl0_160 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s449,plain,
( ~ spl0_1
| spl0_94
| spl0_95
| ~ spl0_137 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s456,plain,
( ~ spl0_6
| spl0_65
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s458,plain,
( ~ spl0_10
| spl0_96
| spl0_97
| ~ spl0_169 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s460,plain,
( ~ spl0_10
| spl0_105
| spl0_106
| ~ spl0_156 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s474,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_12 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s475,plain,
spl0_3,
inference(rat,[],[s149,s160,s177,s179]) ).
cnf(s476,plain,
( ~ spl0_19
| ~ spl0_5 ),
inference(rat,[],[s297,s61,s62,s63]) ).
cnf(s477,plain,
( ~ spl0_33
| ~ spl0_7
| ~ spl0_5 ),
inference(rat,[],[s266,s190,s75,s76]) ).
cnf(s479,plain,
( ~ spl0_48
| ~ spl0_34 ),
inference(rat,[],[s333,s99,s100,s134]) ).
cnf(s480,plain,
( ~ spl0_58
| ~ spl0_16
| ~ spl0_22 ),
inference(rat,[],[s410,s237,s122,s123]) ).
cnf(s481,plain,
( ~ spl0_16
| ~ spl0_5
| ~ spl0_22 ),
inference(rat,[],[s298,s360,s88,s89,s130,s52,s479,s180,s480,s475]) ).
cnf(s482,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s5,s187,s198,s184,s54,s55,s56,s26,s203,s420,s410,s81,s122,s123,s53,s253,s445,s60,s104,s105,s18,s481,s8,s1,s12,s371,s90,s91,s92,s51,s475]) ).
cnf(s483,plain,
( ~ spl0_46
| ~ spl0_16
| ~ spl0_5 ),
inference(rat,[],[s298,s360,s88,s89,s130]) ).
cnf(s484,plain,
( ~ spl0_21
| ~ spl0_2 ),
inference(rat,[],[s218,s74,s114,s115]) ).
cnf(s485,plain,
( ~ spl0_46
| ~ spl0_5
| spl0_1 ),
inference(rat,[],[s14,s456,s246,s57,s101,s102,s444,s27,s60,s104,s105,s458,s18,s287,s298,s483,s88,s89,s130,s482,s476,s475]) ).
cnf(s486,plain,
( ~ spl0_5
| spl0_1 ),
inference(rat,[],[s5,s203,s477,s81,s122,s123,s145,s180,s395,s479,s331,s52,s485,s91,s90,s51,s484,s482,s475]) ).
cnf(s487,plain,
( ~ spl0_34
| spl0_1 ),
inference(rat,[],[s236,s182,s73,s112,s113,s47,s355,s75,s76,s116,s7,s145,s220,s395,s479,s331,s92,s91,s90,s51,s484,s482,s475]) ).
cnf(s488,plain,
( ~ spl0_16
| spl0_1 ),
inference(rat,[],[s236,s182,s73,s112,s113,s47,s359,s360,s484,s482,s130,s89,s52,s487,s475]) ).
cnf(s489,plain,
( ~ spl0_30
| ~ spl0_18 ),
inference(rat,[],[s232,s78,s119,s120]) ).
cnf(s490,plain,
( spl0_12
| ~ spl0_7
| spl0_1 ),
inference(rat,[],[s219,s187,s54,s55,s56,s44,s489,s7,s9,s486,s488,s475]) ).
cnf(s491,plain,
( ~ spl0_41
| ~ spl0_12 ),
inference(rat,[],[s198,s54,s55,s56]) ).
cnf(s492,plain,
( ~ spl0_55
| ~ spl0_29
| ~ spl0_12 ),
inference(rat,[],[s441,s448,s86,s87,s129]) ).
cnf(s493,plain,
( ~ spl0_43
| ~ spl0_6 ),
inference(rat,[],[s456,s57,s101,s102]) ).
cnf(s494,plain,
( ~ spl0_23
| ~ spl0_15 ),
inference(rat,[],[s309,s82,s124,s125]) ).
cnf(s495,plain,
( ~ spl0_27
| ~ spl0_29 ),
inference(rat,[],[s264,s68,s108,s109]) ).
cnf(s496,plain,
( ~ spl0_52
| ~ spl0_7 ),
inference(rat,[],[s225,s79,s80,s121]) ).
cnf(s497,plain,
( ~ spl0_7
| spl0_1 ),
inference(rat,[],[s442,s460,s96,s97,s98,s37,s496,s27,s493,s41,s492,s428,s439,s58,s59,s103,s32,s50,s491,s490,s484,s486,s421,s88,s89,s130,s52,s487,s203,s81,s122,s123,s53,s253,s444,s60,s482,s104,s18,s488,s475]) ).
cnf(s498,plain,
spl0_1,
inference(rat,[],[s5,s474,s497,s203,s81,s122,s123,s53,s253,s444,s60,s104,s18,s488,s482,s475]) ).
cnf(s499,plain,
( ~ spl0_58
| ~ spl0_13 ),
inference(rat,[],[s203,s81,s122,s123]) ).
cnf(s500,plain,
~ spl0_13,
inference(rat,[],[s285,s287,s88,s130,s52,s479,s53,s180,s499,s475]) ).
cnf(s501,plain,
( ~ spl0_12
| spl0_5 ),
inference(rat,[],[s460,s442,s27,s96,s97,s98,s493,s37,s41,s496,s428,s439,s492,s474,s484,s58,s59,s103,s32,s26,s50,s491,s423,s500,s475]) ).
cnf(s502,plain,
( spl0_41
| spl0_43
| ~ spl0_2
| spl0_5 ),
inference(rat,[],[s236,s182,s73,s112,s113,s148,s495,s44,s32,s489,s9,s501,s475]) ).
cnf(s503,plain,
( ~ spl0_59
| ~ spl0_16
| ~ spl0_2 ),
inference(rat,[],[s236,s182,s73,s112,s113]) ).
cnf(s504,plain,
( ~ spl0_46
| ~ spl0_38
| ~ spl0_16 ),
inference(rat,[],[s359,s360,s89,s130]) ).
cnf(s505,plain,
( spl0_43
| ~ spl0_2
| spl0_5 ),
inference(rat,[],[s480,s11,s180,s494,s479,s33,s52,s504,s195,s495,s148,s47,s503,s7,s219,s187,s54,s55,s56,s502,s5,s501,s484,s475,s498,s500]) ).
cnf(s506,plain,
~ spl0_55,
inference(rat,[],[s449,s86,s87,s129,s498]) ).
cnf(s507,plain,
( ~ spl0_2
| spl0_5 ),
inference(rat,[],[s493,s41,s505,s484,s475,s506]) ).
cnf(s508,plain,
spl0_5,
inference(rat,[],[s210,s187,s54,s55,s56,s26,s424,s8,s507,s5,s501,s475,s500]) ).
cnf(s510,plain,
( ~ spl0_51
| ~ spl0_10 ),
inference(rat,[],[s460,s185,s97,s98,s508]) ).
cnf(s511,plain,
( spl0_7
| ~ spl0_2 ),
inference(rat,[],[s5,s474,s500,s475]) ).
cnf(s512,plain,
~ spl0_2,
inference(rat,[],[s511,s477,s144,s510,s27,s493,s41,s484,s508,s506,s475,s500]) ).
cnf(s513,plain,
spl0_22,
inference(rat,[],[s12,s475,s512]) ).
cnf(s515,plain,
( ~ spl0_46
| ~ spl0_42 ),
inference(rat,[],[s421,s88,s89,s130]) ).
cnf(s516,plain,
~ spl0_42,
inference(rat,[],[s420,s410,s81,s122,s123,s180,s479,s52,s515,s513,s475]) ).
cnf(s517,plain,
spl0_41,
inference(rat,[],[s26,s512,s475,s516]) ).
cnf(s518,plain,
~ spl0_64,
inference(rat,[],[s56,s517]) ).
cnf(s519,plain,
~ spl0_63,
inference(rat,[],[s55,s517]) ).
cnf(s520,plain,
~ spl0_62,
inference(rat,[],[s54,s517]) ).
cnf(s522,plain,
spl0_155,
inference(rat,[],[s184,s518,s508,s519]) ).
cnf(s523,plain,
$false,
inference(rat,[],[s193,s522,s498,s519,s520]) ).
fof(f1789,plain,
$false,
inference(avatar_sat_refutation,[],[s523]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN445-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n018.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Mon Sep 28 16:06:14 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.21/1.09 % (3512260)Input is clausal, will run a generic CNF schedule.
% 3.21/1.09 % (3512266)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1281994668:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.21/1.09 % (3512270)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3571545487:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.21/1.09 % (3512268)lrs+10_1_sil=8000:sp=occurrence:random_seed=561965666:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.21/1.09 % (3512269)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3854913029:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.21/1.09 % (3512267)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3020440365:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.21/1.09 % (3512265)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=282951735:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.21/1.09 % (3512271)dis-21_1_sil=8000:lcm=predicate:random_seed=1130890431:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.21/1.09 % (3512271)First to succeed.
% 3.21/1.09 % (3512271)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3512260"
% 3.21/1.09 % (3512268)Also succeeded, but the first one will report.
% 3.21/1.09 % (3512269)Also succeeded, but the first one will report.
% 3.21/1.09 % (3512270)Also succeeded, but the first one will report.
% 3.21/1.09 % (3512271)Refutation found. Thanks to Tanya!
% 3.21/1.09 % SZS status Unsatisfiable for theBenchmark
% 3.21/1.09 % SZS output start Proof for theBenchmark
% See solution above
% 3.55/1.19 % (3512271)------------------------------
% 3.55/1.19 % (3512271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.55/1.19 % (3512271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.55/1.19 % (3512271)CaDiCaL version: 2.1.3
% 3.55/1.19 % (3512271)Termination reason: Refutation
% 3.55/1.19 % (3512271)Time elapsed: 0.025 s
% 3.55/1.19 % (3512271)Peak memory usage: 90 MB
% 3.55/1.19 % (3512271)Instructions burned: 36 (million)
% 3.55/1.19 % (3512271)------------------------------
% 3.55/1.19 % (3512271)------------------------------
% 3.55/1.19 % (3512260)Success in time 0.427 s
% 3.55/1.19 % Vampire exiting
%------------------------------------------------------------------------------