%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN443-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 02:08:24 PM UTC 2026
% Result : Unsatisfiable 0.23s 0.28s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 206
% Syntax : Number of formulae : 730 ( 17 unt; 114 def)
% Number of atoms : 2271 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2634 (1093 ~;1427 |; 0 &)
% ( 114 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 141 ( 140 usr; 137 prp; 0-1 aty)
% Number of functors : 21 ( 21 usr; 21 con; 0-0 aty)
% Number of variables : 142 ( 0 sgn 142 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp11
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( ~ hskp30
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f14,negated_conjecture,
( ~ hskp18
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
fof(f30,negated_conjecture,
( ~ hskp2
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
fof(f33,negated_conjecture,
( hskp28
| hskp1
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f34,negated_conjecture,
( hskp28
| hskp7
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f37,negated_conjecture,
( hskp30
| hskp2
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( hskp30
| hskp27
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f40,negated_conjecture,
( hskp2
| hskp24
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f42,negated_conjecture,
( ~ hskp30
| c0_1(a33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp30
| c2_1(a33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp30
| c3_1(a33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp29
| c0_1(a25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp29
| c1_1(a25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp29
| c2_1(a25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp28
| c0_1(a15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp28
| c1_1(a15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp28
| c3_1(a15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp27
| c1_1(a10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp27
| c2_1(a10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp27
| c3_1(a10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f57,negated_conjecture,
( ~ hskp24
| c0_1(a58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp24
| c3_1(a58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp23
| c0_1(a52) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp22
| c2_1(a43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp21
| c2_1(a42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp21
| c3_1(a42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp20
| c1_1(a38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp20
| c3_1(a38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp18
| c3_1(a34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f67,negated_conjecture,
( ~ hskp16
| c2_1(a31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp15
| c0_1(a27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp15
| c1_1(a27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f71,negated_conjecture,
( ~ hskp11
| c0_1(a19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp11
| c1_1(a19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp9
| c1_1(a12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f76,negated_conjecture,
( ~ hskp7
| c1_1(a9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f78,negated_conjecture,
( ~ hskp5
| c0_1(a6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp5
| c2_1(a6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp4
| c2_1(a5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp4
| c3_1(a5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f83,negated_conjecture,
( ~ hskp2
| c0_1(a3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ hskp2
| c2_1(a3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ hskp1
| c0_1(a2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ hskp1
| c3_1(a2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ hskp0
| c1_1(a1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp0
| c2_1(a1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f92,negated_conjecture,
( ~ c1_1(a58)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c1_1(a52)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c2_1(a52)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c1_1(a43)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c3_1(a43)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c0_1(a42)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c0_1(a38)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f102,negated_conjecture,
( ~ c1_1(a34)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c2_1(a34)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f107,negated_conjecture,
( ~ c1_1(a31)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c2_1(a27)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f112,negated_conjecture,
( ~ c0_1(a22)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c2_1(a22)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f117,negated_conjecture,
( ~ c3_1(a19)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f121,negated_conjecture,
( ~ c2_1(a12)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c3_1(a12)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f124,negated_conjecture,
( ~ c0_1(a9)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ c2_1(a9)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f128,negated_conjecture,
( ~ c3_1(a6)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( ~ c1_1(a5)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f132,negated_conjecture,
( ~ c1_1(a3)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( ~ c2_1(a2)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
( ~ c0_1(a1)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f138,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp5
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f142,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp28
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f146,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp29
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f148,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp0
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp2
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp15
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp2
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp1
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f178,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f180,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X2)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X2)
| ~ c2_1(X2)
| c2_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f185,plain,
( hskp30
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f2]) ).
fof(f197,plain,
( ~ hskp18
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f213,plain,
( ~ hskp2
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f216,plain,
( ~ hskp28
| ~ hskp1
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f217,plain,
( ~ hskp28
| ~ hskp7
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f220,plain,
( ~ hskp30
| hskp2
| hskp18 ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f221,plain,
( ~ hskp30
| hskp27
| ~ hskp7 ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f223,plain,
( hskp2
| ~ hskp24
| hskp23 ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f225,plain,
( hskp30
| c0_1(a33) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f226,plain,
( hskp30
| c2_1(a33) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f227,plain,
( hskp30
| ~ c3_1(a33) ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f228,plain,
( hskp29
| c0_1(a25) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f229,plain,
( hskp29
| c1_1(a25) ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f230,plain,
( hskp29
| c2_1(a25) ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f231,plain,
( hskp28
| c0_1(a15) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f232,plain,
( hskp28
| c1_1(a15) ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f233,plain,
( hskp28
| ~ c3_1(a15) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f234,plain,
( ~ hskp27
| ~ c3_1(a10) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f237,plain,
( hskp24
| c0_1(a58) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f238,plain,
( hskp24
| ~ c3_1(a58) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f239,plain,
( hskp21
| c2_1(a42) ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f240,plain,
( hskp21
| ~ c3_1(a42) ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f241,plain,
( ~ hskp20
| ~ c3_1(a38) ),
inference(consistent_polarity_flipping,[],[f64]) ).
fof(f242,plain,
( ~ hskp18
| ~ c3_1(a34) ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f244,plain,
( hskp15
| c0_1(a27) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f245,plain,
( hskp15
| c1_1(a27) ),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f247,plain,
( hskp9
| c1_1(a12) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f248,plain,
( hskp7
| c1_1(a9) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f249,plain,
( hskp5
| c0_1(a6) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f250,plain,
( hskp5
| c2_1(a6) ),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f251,plain,
( hskp4
| c2_1(a5) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f252,plain,
( hskp4
| ~ c3_1(a5) ),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f254,plain,
( hskp1
| c0_1(a2) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f255,plain,
( hskp1
| ~ c3_1(a2) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f258,plain,
( ~ c1_1(a58)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f92]) ).
fof(f259,plain,
( c3_1(a43)
| ~ hskp22 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f260,plain,
( ~ c0_1(a42)
| hskp21 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f262,plain,
( ~ c2_1(a27)
| hskp15 ),
inference(consistent_polarity_flipping,[],[f108]) ).
fof(f269,plain,
( c3_1(a19)
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f273,plain,
( ~ c2_1(a12)
| hskp9 ),
inference(consistent_polarity_flipping,[],[f121]) ).
fof(f274,plain,
( c3_1(a12)
| hskp9 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f276,plain,
( ~ c0_1(a9)
| hskp7 ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f277,plain,
( ~ c2_1(a9)
| hskp7 ),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f279,plain,
( c3_1(a6)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f280,plain,
( ~ c1_1(a5)
| hskp4 ),
inference(consistent_polarity_flipping,[],[f129]) ).
fof(f283,plain,
( ~ c2_1(a2)
| hskp1 ),
inference(consistent_polarity_flipping,[],[f133]) ).
fof(f287,plain,
! [X0] :
( ~ c2_1(X0)
| ndr1_0
| c0_1(X0)
| c1_1(X0)
| ~ hskp5
| hskp0 ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f291,plain,
! [X0] :
( ~ c1_1(X0)
| ndr1_0
| c0_1(X0)
| c2_1(X0)
| ~ hskp28
| hskp27 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f295,plain,
! [X0] :
( ~ c0_1(X0)
| ndr1_0
| c1_1(X0)
| c2_1(X0)
| ~ hskp29
| hskp20 ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f297,plain,
! [X0] :
( ~ c0_1(X0)
| ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp0
| ~ hskp21 ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f298,plain,
! [X0] :
( ~ c0_1(X0)
| ndr1_0
| c2_1(X0)
| ~ c3_1(X0)
| hskp2
| ~ hskp4 ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f299,plain,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ndr1_0
| c0_1(X0)
| ~ hskp15
| ~ hskp4 ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f301,plain,
! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| c1_1(X0)
| hskp2
| hskp23 ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f302,plain,
! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| c1_1(X0)
| ~ hskp1
| hskp0 ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f309,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ndr1_0
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ hskp1 ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f316,plain,
! [X0,X1] :
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| c3_1(X1)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp22 ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f317,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f319,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| ~ c3_1(X0)
| c1_1(X1)
| hskp13 ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f322,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c2_1(X1)
| c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ hskp5 ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f323,plain,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ hskp29 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f324,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1)
| ~ hskp29 ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f325,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| c1_1(X1)
| hskp16 ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f327,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| ~ c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f329,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X2)
| c1_1(X0)
| ~ c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f330,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| ~ c3_1(X1)
| c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f331,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c3_1(X2)
| ~ c3_1(X0)
| c1_1(X1)
| c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f332,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X2)
| ~ c2_1(X2)
| c2_1(X1)
| c1_1(X2) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f333,plain,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f184]) ).
fof(f335,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| ~ c2_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f336,plain,
( ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c0_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f338,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f339,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f341,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f345,definition,
( spl0_4
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f346,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f347,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f333,f345,f341,f338,f335]) ).
fof(f349,definition,
( spl0_5
<=> ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f350,plain,
( ! [X2] :
( c1_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f352,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f353,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f354,plain,
( spl0_5
| spl0_6
| spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f332,f338,f341,f352,f349]) ).
fof(f356,definition,
( spl0_7
<=> ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f357,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,definition,
( spl0_8
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f360,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f361,plain,
( spl0_7
| spl0_5
| spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f331,f359,f341,f349,f356]) ).
fof(f363,definition,
( spl0_9
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f364,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f366,definition,
( spl0_10
<=> ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f367,plain,
( ! [X1] :
( c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f369,definition,
( spl0_11
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f370,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f371,plain,
( spl0_9
| spl0_10
| spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f330,f369,f341,f366,f363]) ).
fof(f373,definition,
( spl0_12
<=> ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f374,plain,
( ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f376,definition,
( spl0_13
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f377,plain,
( ! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f378,plain,
( spl0_12
| spl0_9
| spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f329,f376,f341,f363,f373]) ).
fof(f380,definition,
( spl0_14
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f381,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f383,definition,
( spl0_15
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f384,plain,
( ! [X1] :
( c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f386,definition,
( spl0_16
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f387,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f390,definition,
( spl0_17
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f391,plain,
( ! [X1] :
( c1_1(X1)
| ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f392,plain,
( spl0_14
| spl0_17
| spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f327,f376,f341,f390,f380]) ).
fof(f398,definition,
( spl0_19
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f399,plain,
( ! [X1] :
( c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f402,definition,
( spl0_20
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f406,definition,
( spl0_21
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f407,plain,
( ! [X1] :
( c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f409,definition,
( spl0_22
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f410,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f411,plain,
( spl0_20
| spl0_21
| spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f325,f409,f341,f406,f402]) ).
fof(f413,definition,
( spl0_23
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f417,definition,
( spl0_24
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f418,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( ~ spl0_23
| spl0_13
| spl0_3
| spl0_24 ),
inference(avatar_split_clause,[],[f324,f417,f341,f376,f413]) ).
fof(f421,definition,
( spl0_25
<=> ! [X1] :
( c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f422,plain,
( ! [X1] :
( c1_1(X1)
| c2_1(X1)
| c3_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f423,plain,
( ~ spl0_23
| spl0_25
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f323,f345,f341,f421,f413]) ).
fof(f425,definition,
( spl0_26
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f428,plain,
( ~ spl0_26
| spl0_7
| spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f322,f349,f341,f356,f425]) ).
fof(f438,definition,
( spl0_29
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f446,definition,
( spl0_31
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f449,plain,
( spl0_31
| spl0_5
| spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f319,f386,f341,f349,f446]) ).
fof(f452,definition,
( spl0_32
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f455,plain,
( spl0_32
| spl0_25
| spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f317,f409,f341,f421,f452]) ).
fof(f457,definition,
( spl0_33
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f460,plain,
( spl0_33
| spl0_25
| spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f316,f398,f341,f421,f457]) ).
fof(f475,definition,
( spl0_37
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f489,definition,
( spl0_40
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f492,plain,
( ~ spl0_40
| spl0_14
| spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f309,f349,f341,f380,f489]) ).
fof(f502,definition,
( spl0_43
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f515,definition,
( spl0_46
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f527,definition,
( spl0_49
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f535,plain,
( spl0_32
| ~ spl0_40
| spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f302,f398,f341,f489,f452]) ).
fof(f537,definition,
( spl0_51
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f540,plain,
( spl0_51
| spl0_43
| spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f301,f398,f341,f502,f537]) ).
fof(f543,definition,
( spl0_52
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f547,definition,
( spl0_53
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f550,plain,
( ~ spl0_52
| ~ spl0_53
| spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f299,f363,f341,f547,f543]) ).
fof(f551,plain,
( ~ spl0_52
| spl0_43
| spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f298,f386,f341,f502,f543]) ).
fof(f553,definition,
( spl0_54
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f556,plain,
( ~ spl0_54
| spl0_32
| spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f297,f383,f341,f452,f553]) ).
fof(f559,definition,
( spl0_55
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f562,plain,
( spl0_55
| ~ spl0_23
| spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f295,f383,f341,f413,f559]) ).
fof(f570,definition,
( spl0_57
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f575,definition,
( spl0_58
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f578,plain,
( spl0_46
| ~ spl0_58
| spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f291,f373,f341,f575,f515]) ).
fof(f589,definition,
( spl0_61
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f593,plain,
( spl0_32
| ~ spl0_26
| spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f287,f390,f341,f425,f452]) ).
fof(f596,definition,
( spl0_62
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f602,definition,
( spl0_63
<=> c0_1(a1) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f605,plain,
( ~ spl0_32
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f134,f602,f452]) ).
fof(f607,definition,
( spl0_64
<=> c2_1(a2) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f610,plain,
( spl0_40
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f283,f607,f489]) ).
fof(f612,definition,
( spl0_65
<=> c1_1(a3) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f614,plain,
( ~ c1_1(a3)
| spl0_65 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f615,plain,
( ~ spl0_43
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f132,f612,f502]) ).
fof(f627,definition,
( spl0_68
<=> c1_1(a5) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f629,plain,
( ~ c1_1(a5)
| spl0_68 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f630,plain,
( spl0_52
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f280,f627,f543]) ).
fof(f632,definition,
( spl0_69
<=> c3_1(a6) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f634,plain,
( c3_1(a6)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( spl0_26
| spl0_69 ),
inference(avatar_split_clause,[],[f279,f632,f425]) ).
fof(f647,definition,
( spl0_72
<=> c2_1(a9) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f650,plain,
( spl0_61
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f277,f647,f589]) ).
fof(f652,definition,
( spl0_73
<=> c0_1(a9) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f655,plain,
( spl0_61
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f276,f652,f589]) ).
fof(f662,definition,
( spl0_75
<=> c3_1(a12) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f664,plain,
( c3_1(a12)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f665,plain,
( spl0_37
| spl0_75 ),
inference(avatar_split_clause,[],[f274,f662,f475]) ).
fof(f667,definition,
( spl0_76
<=> c2_1(a12) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f670,plain,
( spl0_37
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f273,f667,f475]) ).
fof(f687,definition,
( spl0_80
<=> c3_1(a19) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f690,plain,
( ~ spl0_57
| spl0_80 ),
inference(avatar_split_clause,[],[f269,f687,f570]) ).
fof(f707,definition,
( spl0_84
<=> c2_1(a22) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f709,plain,
( ~ c2_1(a22)
| spl0_84 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f710,plain,
( ~ spl0_31
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f113,f707,f446]) ).
fof(f712,definition,
( spl0_85
<=> c0_1(a22) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f715,plain,
( ~ spl0_31
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f112,f712,f446]) ).
fof(f732,definition,
( spl0_89
<=> c2_1(a27) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f735,plain,
( spl0_53
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f262,f732,f547]) ).
fof(f737,definition,
( spl0_90
<=> c1_1(a31) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f739,plain,
( ~ c1_1(a31)
| spl0_90 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f740,plain,
( ~ spl0_20
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f107,f737,f402]) ).
fof(f757,definition,
( spl0_94
<=> c2_1(a34) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f760,plain,
( ~ spl0_49
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f103,f757,f527]) ).
fof(f762,definition,
( spl0_95
<=> c1_1(a34) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f764,plain,
( ~ c1_1(a34)
| spl0_95 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f765,plain,
( ~ spl0_49
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f102,f762,f527]) ).
fof(f782,definition,
( spl0_99
<=> c0_1(a38) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f785,plain,
( ~ spl0_55
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f98,f782,f559]) ).
fof(f787,definition,
( spl0_100
<=> c0_1(a42) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f790,plain,
( spl0_54
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f260,f787,f553]) ).
fof(f792,definition,
( spl0_101
<=> c3_1(a43) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f795,plain,
( ~ spl0_33
| spl0_101 ),
inference(avatar_split_clause,[],[f259,f792,f457]) ).
fof(f797,definition,
( spl0_102
<=> c1_1(a43) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f799,plain,
( ~ c1_1(a43)
| spl0_102 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f800,plain,
( ~ spl0_33
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f95,f797,f457]) ).
fof(f802,definition,
( spl0_103
<=> c2_1(a52) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f805,plain,
( ~ spl0_51
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f94,f802,f537]) ).
fof(f807,definition,
( spl0_104
<=> c1_1(a52) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f809,plain,
( ~ c1_1(a52)
| spl0_104 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f810,plain,
( ~ spl0_51
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f93,f807,f537]) ).
fof(f812,definition,
( spl0_105
<=> c1_1(a58) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f814,plain,
( ~ c1_1(a58)
| spl0_105 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f815,plain,
( spl0_29
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f258,f812,f438]) ).
fof(f836,definition,
( spl0_110
<=> c2_1(a1) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f839,plain,
( spl0_110
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f88,f452,f836]) ).
fof(f841,definition,
( spl0_111
<=> c1_1(a1) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f843,plain,
( c1_1(a1)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f841]) ).
fof(f844,plain,
( spl0_111
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f87,f452,f841]) ).
fof(f846,definition,
( spl0_112
<=> c3_1(a2) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f848,plain,
( ~ c3_1(a2)
| spl0_112 ),
inference(avatar_component_clause,[],[f846]) ).
fof(f849,plain,
( ~ spl0_112
| spl0_40 ),
inference(avatar_split_clause,[],[f255,f489,f846]) ).
fof(f851,definition,
( spl0_113
<=> c0_1(a2) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f854,plain,
( spl0_113
| spl0_40 ),
inference(avatar_split_clause,[],[f254,f489,f851]) ).
fof(f856,definition,
( spl0_114
<=> c2_1(a3) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f859,plain,
( spl0_114
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f84,f502,f856]) ).
fof(f861,definition,
( spl0_115
<=> c0_1(a3) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f864,plain,
( spl0_115
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f83,f502,f861]) ).
fof(f871,definition,
( spl0_117
<=> c3_1(a5) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f873,plain,
( ~ c3_1(a5)
| spl0_117 ),
inference(avatar_component_clause,[],[f871]) ).
fof(f874,plain,
( ~ spl0_117
| spl0_52 ),
inference(avatar_split_clause,[],[f252,f543,f871]) ).
fof(f876,definition,
( spl0_118
<=> c2_1(a5) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f879,plain,
( spl0_118
| spl0_52 ),
inference(avatar_split_clause,[],[f251,f543,f876]) ).
fof(f881,definition,
( spl0_119
<=> c2_1(a6) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f884,plain,
( spl0_119
| spl0_26 ),
inference(avatar_split_clause,[],[f250,f425,f881]) ).
fof(f886,definition,
( spl0_120
<=> c0_1(a6) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f889,plain,
( spl0_120
| spl0_26 ),
inference(avatar_split_clause,[],[f249,f425,f886]) ).
fof(f896,definition,
( spl0_122
<=> c1_1(a9) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f898,plain,
( c1_1(a9)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f899,plain,
( spl0_122
| spl0_61 ),
inference(avatar_split_clause,[],[f248,f589,f896]) ).
fof(f911,definition,
( spl0_125
<=> c1_1(a12) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f913,plain,
( c1_1(a12)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f911]) ).
fof(f914,plain,
( spl0_125
| spl0_37 ),
inference(avatar_split_clause,[],[f247,f475,f911]) ).
fof(f916,definition,
( spl0_126
<=> c1_1(a19) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f918,plain,
( c1_1(a19)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f919,plain,
( spl0_126
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f72,f570,f916]) ).
fof(f921,definition,
( spl0_127
<=> c0_1(a19) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f924,plain,
( spl0_127
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f71,f570,f921]) ).
fof(f931,definition,
( spl0_129
<=> c1_1(a27) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f933,plain,
( c1_1(a27)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f931]) ).
fof(f934,plain,
( spl0_129
| spl0_53 ),
inference(avatar_split_clause,[],[f245,f547,f931]) ).
fof(f936,definition,
( spl0_130
<=> c0_1(a27) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f939,plain,
( spl0_130
| spl0_53 ),
inference(avatar_split_clause,[],[f244,f547,f936]) ).
fof(f941,definition,
( spl0_131
<=> c2_1(a31) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f944,plain,
( spl0_131
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f67,f402,f941]) ).
fof(f951,definition,
( spl0_133
<=> c3_1(a34) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f953,plain,
( ~ c3_1(a34)
| spl0_133 ),
inference(avatar_component_clause,[],[f951]) ).
fof(f954,plain,
( ~ spl0_133
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f242,f527,f951]) ).
fof(f956,definition,
( spl0_134
<=> c3_1(a38) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f959,plain,
( ~ spl0_134
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f241,f559,f956]) ).
fof(f961,definition,
( spl0_135
<=> c1_1(a38) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f963,plain,
( c1_1(a38)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f964,plain,
( spl0_135
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f63,f559,f961]) ).
fof(f966,definition,
( spl0_136
<=> c3_1(a42) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f968,plain,
( ~ c3_1(a42)
| spl0_136 ),
inference(avatar_component_clause,[],[f966]) ).
fof(f969,plain,
( ~ spl0_136
| spl0_54 ),
inference(avatar_split_clause,[],[f240,f553,f966]) ).
fof(f971,definition,
( spl0_137
<=> c2_1(a42) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f974,plain,
( spl0_137
| spl0_54 ),
inference(avatar_split_clause,[],[f239,f553,f971]) ).
fof(f976,definition,
( spl0_138
<=> c2_1(a43) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f979,plain,
( spl0_138
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f60,f457,f976]) ).
fof(f981,definition,
( spl0_139
<=> c0_1(a52) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f984,plain,
( spl0_139
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f59,f537,f981]) ).
fof(f986,definition,
( spl0_140
<=> c3_1(a58) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f988,plain,
( ~ c3_1(a58)
| spl0_140 ),
inference(avatar_component_clause,[],[f986]) ).
fof(f989,plain,
( ~ spl0_140
| spl0_29 ),
inference(avatar_split_clause,[],[f238,f438,f986]) ).
fof(f991,definition,
( spl0_141
<=> c0_1(a58) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f994,plain,
( spl0_141
| spl0_29 ),
inference(avatar_split_clause,[],[f237,f438,f991]) ).
fof(f1011,definition,
( spl0_145
<=> c3_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1013,plain,
( ~ c3_1(a10)
| spl0_145 ),
inference(avatar_component_clause,[],[f1011]) ).
fof(f1014,plain,
( ~ spl0_145
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f234,f515,f1011]) ).
fof(f1016,definition,
( spl0_146
<=> c2_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1019,plain,
( spl0_146
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f52,f515,f1016]) ).
fof(f1021,definition,
( spl0_147
<=> c1_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1023,plain,
( c1_1(a10)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f1021]) ).
fof(f1024,plain,
( spl0_147
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f51,f515,f1021]) ).
fof(f1026,definition,
( spl0_148
<=> c3_1(a15) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1028,plain,
( ~ c3_1(a15)
| spl0_148 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1029,plain,
( ~ spl0_148
| spl0_58 ),
inference(avatar_split_clause,[],[f233,f575,f1026]) ).
fof(f1031,definition,
( spl0_149
<=> c1_1(a15) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1033,plain,
( c1_1(a15)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1034,plain,
( spl0_149
| spl0_58 ),
inference(avatar_split_clause,[],[f232,f575,f1031]) ).
fof(f1036,definition,
( spl0_150
<=> c0_1(a15) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1039,plain,
( spl0_150
| spl0_58 ),
inference(avatar_split_clause,[],[f231,f575,f1036]) ).
fof(f1041,definition,
( spl0_151
<=> c2_1(a25) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f1044,plain,
( spl0_151
| spl0_23 ),
inference(avatar_split_clause,[],[f230,f413,f1041]) ).
fof(f1046,definition,
( spl0_152
<=> c1_1(a25) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1048,plain,
( c1_1(a25)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1049,plain,
( spl0_152
| spl0_23 ),
inference(avatar_split_clause,[],[f229,f413,f1046]) ).
fof(f1051,definition,
( spl0_153
<=> c0_1(a25) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1054,plain,
( spl0_153
| spl0_23 ),
inference(avatar_split_clause,[],[f228,f413,f1051]) ).
fof(f1056,definition,
( spl0_154
<=> c3_1(a33) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f1058,plain,
( ~ c3_1(a33)
| spl0_154 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1059,plain,
( ~ spl0_154
| spl0_62 ),
inference(avatar_split_clause,[],[f227,f596,f1056]) ).
fof(f1061,definition,
( spl0_155
<=> c2_1(a33) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1064,plain,
( spl0_155
| spl0_62 ),
inference(avatar_split_clause,[],[f226,f596,f1061]) ).
fof(f1066,definition,
( spl0_156
<=> c0_1(a33) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f1069,plain,
( spl0_156
| spl0_62 ),
inference(avatar_split_clause,[],[f225,f596,f1066]) ).
fof(f1071,plain,
( spl0_51
| ~ spl0_29
| spl0_43 ),
inference(avatar_split_clause,[],[f223,f502,f438,f537]) ).
fof(f1073,plain,
( ~ spl0_61
| spl0_46
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f221,f596,f515,f589]) ).
fof(f1074,plain,
( spl0_49
| spl0_43
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f220,f596,f502,f527]) ).
fof(f1077,plain,
( ~ spl0_37
| ~ spl0_61
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f217,f575,f589,f475]) ).
fof(f1078,plain,
( ~ spl0_37
| ~ spl0_40
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f216,f575,f489,f475]) ).
fof(f1081,plain,
( ~ spl0_3
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f213,f502,f341]) ).
fof(f1097,plain,
( ~ spl0_3
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f197,f527,f341]) ).
fof(f1109,plain,
( ~ spl0_3
| spl0_62 ),
inference(avatar_split_clause,[],[f185,f596,f341]) ).
fof(f1110,plain,
( spl0_33
| spl0_57 ),
inference(avatar_split_clause,[],[f1,f570,f457]) ).
fof(f1117,plain,
( c0_1(a10)
| ~ c2_1(a10)
| ~ spl0_7
| spl0_145 ),
inference(resolution,[],[f357,f1013]) ).
fof(f1122,plain,
( c0_1(a42)
| ~ c2_1(a42)
| ~ spl0_7
| spl0_136 ),
inference(resolution,[],[f357,f968]) ).
fof(f1153,definition,
( spl0_160
<=> c2_1(a38) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1158,definition,
( spl0_161
<=> c2_1(a58) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1163,definition,
( spl0_162
<=> c2_1(a15) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1186,plain,
( ~ c3_1(a43)
| ~ c2_1(a43)
| ~ spl0_10
| spl0_102 ),
inference(resolution,[],[f367,f799]) ).
fof(f1189,plain,
( ~ c3_1(a31)
| ~ c2_1(a31)
| ~ spl0_10
| spl0_90 ),
inference(resolution,[],[f367,f739]) ).
fof(f1212,plain,
( c2_1(a15)
| ~ c0_1(a15)
| ~ spl0_11
| spl0_148 ),
inference(resolution,[],[f370,f1028]) ).
fof(f1216,plain,
( c2_1(a58)
| ~ c0_1(a58)
| ~ spl0_11
| spl0_140 ),
inference(resolution,[],[f370,f988]) ).
fof(f1220,plain,
( c2_1(a34)
| ~ c0_1(a34)
| ~ spl0_11
| spl0_133 ),
inference(resolution,[],[f370,f953]) ).
fof(f1230,plain,
( c2_1(a2)
| ~ c0_1(a2)
| ~ spl0_11
| spl0_112 ),
inference(resolution,[],[f370,f848]) ).
fof(f1242,definition,
( spl0_166
<=> c0_1(a5) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1252,definition,
( spl0_168
<=> c0_1(a12) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1257,definition,
( spl0_169
<=> c0_1(a34) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1272,definition,
( spl0_172
<=> c0_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f1277,plain,
( c2_1(a9)
| c0_1(a9)
| ~ spl0_12
| ~ spl0_122 ),
inference(resolution,[],[f374,f898]) ).
fof(f1280,plain,
( spl0_73
| spl0_72
| ~ spl0_12
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1277,f896,f373,f647,f652]) ).
fof(f1281,plain,
( ~ spl0_146
| spl0_172
| ~ spl0_7
| spl0_145 ),
inference(avatar_split_clause,[],[f1117,f1011,f356,f1272,f1016]) ).
fof(f1285,plain,
( c2_1(a12)
| c0_1(a12)
| ~ spl0_12
| ~ spl0_125 ),
inference(resolution,[],[f913,f374]) ).
fof(f1289,plain,
( spl0_168
| spl0_76
| ~ spl0_12
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f1285,f911,f373,f667,f1252]) ).
fof(f1291,plain,
( c0_1(a10)
| ~ c2_1(a10)
| ~ spl0_9
| ~ spl0_147 ),
inference(resolution,[],[f1023,f364]) ).
fof(f1293,plain,
( c3_1(a10)
| ~ c0_1(a10)
| ~ spl0_2
| ~ spl0_147 ),
inference(resolution,[],[f1023,f339]) ).
fof(f1294,plain,
( ~ spl0_172
| spl0_145
| ~ spl0_2
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1293,f1021,f338,f1011,f1272]) ).
fof(f1297,plain,
( ~ c0_1(a6)
| ~ c2_1(a6)
| ~ spl0_8
| ~ spl0_69 ),
inference(resolution,[],[f634,f360]) ).
fof(f1298,plain,
( ~ spl0_119
| ~ spl0_120
| ~ spl0_8
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1297,f632,f359,f886,f881]) ).
fof(f1300,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_5 ),
inference(resolution,[],[f350,f339]) ).
fof(f1304,plain,
( ~ c0_1(a58)
| ~ c2_1(a58)
| ~ spl0_5
| spl0_105 ),
inference(resolution,[],[f350,f814]) ).
fof(f1321,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_2
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f1300]) ).
fof(f1323,plain,
( spl0_24
| ~ spl0_2
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1321,f349,f338,f417]) ).
fof(f1329,plain,
( c3_1(a27)
| ~ c0_1(a27)
| ~ spl0_2
| ~ spl0_129 ),
inference(resolution,[],[f933,f339]) ).
fof(f1331,definition,
( spl0_173
<=> c3_1(a27) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1333,plain,
( c3_1(a27)
| ~ spl0_173 ),
inference(avatar_component_clause,[],[f1331]) ).
fof(f1334,plain,
( ~ spl0_130
| spl0_173
| ~ spl0_2
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1329,f931,f338,f1331,f936]) ).
fof(f1342,plain,
( ~ c3_1(a52)
| ~ c0_1(a52)
| ~ spl0_13
| spl0_104 ),
inference(resolution,[],[f377,f809]) ).
fof(f1359,definition,
( spl0_174
<=> c3_1(a52) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f1361,plain,
( ~ c3_1(a52)
| spl0_174 ),
inference(avatar_component_clause,[],[f1359]) ).
fof(f1363,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_12
| ~ spl0_14 ),
inference(resolution,[],[f381,f374]) ).
fof(f1371,plain,
( c2_1(a34)
| c0_1(a34)
| ~ spl0_14
| spl0_95 ),
inference(resolution,[],[f381,f764]) ).
fof(f1383,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0) )
| ~ spl0_12
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f1363]) ).
fof(f1393,plain,
( spl0_169
| spl0_94
| ~ spl0_14
| spl0_95 ),
inference(avatar_split_clause,[],[f1371,f762,f380,f757,f1257]) ).
fof(f1400,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_15 ),
inference(resolution,[],[f384,f339]) ).
fof(f1403,plain,
( c2_1(a58)
| ~ c0_1(a58)
| ~ spl0_15
| spl0_105 ),
inference(resolution,[],[f384,f814]) ).
fof(f1404,plain,
( c2_1(a52)
| ~ c0_1(a52)
| ~ spl0_15
| spl0_104 ),
inference(resolution,[],[f384,f809]) ).
fof(f1419,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_2
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f1400]) ).
fof(f1422,plain,
( spl0_11
| ~ spl0_2
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1419,f383,f338,f369]) ).
fof(f1425,plain,
( c2_1(a38)
| c0_1(a38)
| ~ spl0_12
| ~ spl0_135 ),
inference(resolution,[],[f963,f374]) ).
fof(f1427,plain,
( spl0_99
| spl0_160
| ~ spl0_12
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1425,f961,f373,f1153,f782]) ).
fof(f1428,plain,
( ~ spl0_141
| spl0_161
| ~ spl0_11
| spl0_140 ),
inference(avatar_split_clause,[],[f1216,f986,f369,f1158,f991]) ).
fof(f1433,plain,
( ~ spl0_161
| ~ spl0_141
| ~ spl0_5
| spl0_105 ),
inference(avatar_split_clause,[],[f1304,f812,f349,f991,f1158]) ).
fof(f1450,plain,
( ~ c0_1(a27)
| c2_1(a27)
| ~ spl0_16
| ~ spl0_173 ),
inference(resolution,[],[f387,f1333]) ).
fof(f1452,plain,
( ~ c0_1(a12)
| c2_1(a12)
| ~ spl0_16
| ~ spl0_75 ),
inference(resolution,[],[f387,f664]) ).
fof(f1465,definition,
( spl0_176
<=> c3_1(a31) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f1468,plain,
( ~ spl0_131
| ~ spl0_176
| ~ spl0_10
| spl0_90 ),
inference(avatar_split_clause,[],[f1189,f737,f366,f1465,f941]) ).
fof(f1486,plain,
( c3_1(a15)
| ~ c0_1(a15)
| ~ spl0_2
| ~ spl0_149 ),
inference(resolution,[],[f1033,f339]) ).
fof(f1506,plain,
( c0_1(a22)
| ~ spl0_12
| ~ spl0_14
| spl0_84 ),
inference(resolution,[],[f1383,f709]) ).
fof(f1509,plain,
( spl0_85
| ~ spl0_12
| ~ spl0_14
| spl0_84 ),
inference(avatar_split_clause,[],[f1506,f707,f380,f373,f712]) ).
fof(f1546,plain,
( ~ c2_1(a5)
| c0_1(a5)
| ~ spl0_17
| spl0_68 ),
inference(resolution,[],[f391,f629]) ).
fof(f1554,plain,
( spl0_166
| ~ spl0_118
| ~ spl0_17
| spl0_68 ),
inference(avatar_split_clause,[],[f1546,f627,f390,f876,f1242]) ).
fof(f1559,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_19 ),
inference(resolution,[],[f399,f339]) ).
fof(f1564,plain,
( ~ c2_1(a31)
| c3_1(a31)
| ~ spl0_19
| spl0_90 ),
inference(resolution,[],[f399,f739]) ).
fof(f1567,plain,
( ~ c2_1(a5)
| c3_1(a5)
| ~ spl0_19
| spl0_68 ),
inference(resolution,[],[f399,f629]) ).
fof(f1572,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_19 ),
inference(duplicate_literal_removal,[],[f1559]) ).
fof(f1575,plain,
( spl0_117
| ~ spl0_118
| ~ spl0_19
| spl0_68 ),
inference(avatar_split_clause,[],[f1567,f627,f398,f876,f871]) ).
fof(f1581,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_5
| ~ spl0_22 ),
inference(resolution,[],[f410,f350]) ).
fof(f1589,plain,
( ~ c3_1(a19)
| ~ c0_1(a19)
| ~ spl0_22
| ~ spl0_126 ),
inference(resolution,[],[f410,f918]) ).
fof(f1595,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_5
| ~ spl0_22 ),
inference(duplicate_literal_removal,[],[f1581]) ).
fof(f1604,plain,
( spl0_8
| ~ spl0_5
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1595,f409,f349,f359]) ).
fof(f1605,plain,
( ~ c0_1(a33)
| ~ c2_1(a33)
| ~ spl0_24
| spl0_154 ),
inference(resolution,[],[f418,f1058]) ).
fof(f1606,plain,
( ~ c0_1(a15)
| ~ c2_1(a15)
| ~ spl0_24
| spl0_148 ),
inference(resolution,[],[f418,f1028]) ).
fof(f1608,plain,
( ~ c0_1(a58)
| ~ c2_1(a58)
| ~ spl0_24
| spl0_140 ),
inference(resolution,[],[f418,f988]) ).
fof(f1618,plain,
( ~ c0_1(a5)
| ~ c2_1(a5)
| ~ spl0_24
| spl0_117 ),
inference(resolution,[],[f418,f873]) ).
fof(f1625,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_25 ),
inference(resolution,[],[f422,f339]) ).
fof(f1626,plain,
( c2_1(a58)
| c3_1(a58)
| ~ spl0_25
| spl0_105 ),
inference(resolution,[],[f422,f814]) ).
fof(f1627,plain,
( c2_1(a52)
| c3_1(a52)
| ~ spl0_25
| spl0_104 ),
inference(resolution,[],[f422,f809]) ).
fof(f1629,plain,
( c2_1(a34)
| c3_1(a34)
| ~ spl0_25
| spl0_95 ),
inference(resolution,[],[f422,f764]) ).
fof(f1638,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_25 ),
inference(duplicate_literal_removal,[],[f1625]) ).
fof(f1646,plain,
( spl0_11
| ~ spl0_2
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1638,f421,f338,f369]) ).
fof(f1647,plain,
( ~ spl0_138
| ~ spl0_101
| ~ spl0_10
| spl0_102 ),
inference(avatar_split_clause,[],[f1186,f797,f366,f792,f976]) ).
fof(f1651,plain,
( ~ spl0_137
| spl0_100
| ~ spl0_7
| spl0_136 ),
inference(avatar_split_clause,[],[f1122,f966,f356,f787,f971]) ).
fof(f1655,plain,
( spl0_89
| ~ spl0_130
| ~ spl0_16
| ~ spl0_173 ),
inference(avatar_split_clause,[],[f1450,f1331,f386,f936,f732]) ).
fof(f1659,plain,
( spl0_24
| ~ spl0_2
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1572,f398,f338,f417]) ).
fof(f1661,plain,
( spl0_176
| ~ spl0_131
| ~ spl0_19
| spl0_90 ),
inference(avatar_split_clause,[],[f1564,f737,f398,f941,f1465]) ).
fof(f1676,plain,
( ~ c2_1(a25)
| ~ c0_1(a25)
| ~ spl0_1
| ~ spl0_152 ),
inference(resolution,[],[f336,f1048]) ).
fof(f1677,plain,
( ~ c2_1(a15)
| ~ c0_1(a15)
| ~ spl0_1
| ~ spl0_149 ),
inference(resolution,[],[f336,f1033]) ).
fof(f1678,plain,
( ~ c2_1(a10)
| ~ c0_1(a10)
| ~ spl0_1
| ~ spl0_147 ),
inference(resolution,[],[f336,f1023]) ).
fof(f1692,plain,
( ~ spl0_150
| ~ spl0_162
| ~ spl0_1
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1677,f1031,f335,f1163,f1036]) ).
fof(f1696,plain,
( c3_1(a15)
| ~ c2_1(a15)
| ~ spl0_4
| ~ spl0_149 ),
inference(resolution,[],[f346,f1033]) ).
fof(f1697,plain,
( c3_1(a10)
| ~ c2_1(a10)
| ~ spl0_4
| ~ spl0_147 ),
inference(resolution,[],[f346,f1023]) ).
fof(f1698,plain,
( c3_1(a38)
| ~ c2_1(a38)
| ~ spl0_4
| ~ spl0_135 ),
inference(resolution,[],[f346,f963]) ).
fof(f1717,plain,
( c2_1(a15)
| ~ c0_1(a15)
| ~ spl0_6
| ~ spl0_149 ),
inference(resolution,[],[f353,f1033]) ).
fof(f1722,plain,
( c2_1(a12)
| ~ c0_1(a12)
| ~ spl0_6
| ~ spl0_125 ),
inference(resolution,[],[f353,f913]) ).
fof(f1739,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4
| ~ spl0_5 ),
inference(resolution,[],[f350,f346]) ).
fof(f1748,plain,
( ~ c0_1(a3)
| ~ c2_1(a3)
| ~ spl0_5
| spl0_65 ),
inference(resolution,[],[f350,f614]) ).
fof(f1751,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_4
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f1739]) ).
fof(f1752,plain,
( spl0_24
| ~ spl0_4
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1751,f349,f345,f417]) ).
fof(f1755,plain,
( ~ spl0_168
| spl0_76
| ~ spl0_6
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f1722,f911,f352,f667,f1252]) ).
fof(f1761,plain,
( ~ spl0_141
| spl0_161
| ~ spl0_15
| spl0_105 ),
inference(avatar_split_clause,[],[f1403,f812,f383,f1158,f991]) ).
fof(f1765,plain,
( spl0_140
| spl0_161
| ~ spl0_25
| spl0_105 ),
inference(avatar_split_clause,[],[f1626,f812,f421,f1158,f986]) ).
fof(f1773,plain,
( ~ spl0_150
| spl0_148
| ~ spl0_2
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1486,f1031,f338,f1026,f1036]) ).
fof(f1778,plain,
( ~ spl0_114
| ~ spl0_115
| ~ spl0_5
| spl0_65 ),
inference(avatar_split_clause,[],[f1748,f612,f349,f861,f856]) ).
fof(f1780,plain,
( ~ spl0_169
| spl0_94
| ~ spl0_11
| spl0_133 ),
inference(avatar_split_clause,[],[f1220,f951,f369,f757,f1257]) ).
fof(f1783,plain,
( ~ spl0_113
| spl0_64
| ~ spl0_11
| spl0_112 ),
inference(avatar_split_clause,[],[f1230,f846,f369,f607,f851]) ).
fof(f1784,plain,
( spl0_76
| ~ spl0_168
| ~ spl0_16
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f1452,f662,f386,f1252,f667]) ).
fof(f1785,plain,
( ~ spl0_155
| ~ spl0_156
| ~ spl0_24
| spl0_154 ),
inference(avatar_split_clause,[],[f1605,f1056,f417,f1066,f1061]) ).
fof(f1789,plain,
( ~ spl0_118
| ~ spl0_166
| ~ spl0_24
| spl0_117 ),
inference(avatar_split_clause,[],[f1618,f871,f417,f1242,f876]) ).
fof(f1793,plain,
( ~ spl0_150
| spl0_162
| ~ spl0_6
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1717,f1031,f352,f1163,f1036]) ).
fof(f1841,plain,
( c2_1(a52)
| ~ c0_1(a52)
| ~ spl0_11
| spl0_174 ),
inference(resolution,[],[f370,f1361]) ).
fof(f1849,plain,
( ~ spl0_139
| spl0_103
| ~ spl0_11
| spl0_174 ),
inference(avatar_split_clause,[],[f1841,f1359,f369,f802,f981]) ).
fof(f1851,plain,
( ~ spl0_162
| spl0_148
| ~ spl0_4
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1696,f1031,f345,f1026,f1163]) ).
fof(f1852,plain,
( ~ spl0_146
| spl0_145
| ~ spl0_4
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1697,f1021,f345,f1011,f1016]) ).
fof(f1853,plain,
( ~ spl0_160
| spl0_134
| ~ spl0_4
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1698,f961,f345,f956,f1153]) ).
fof(f1857,plain,
( ~ spl0_146
| spl0_172
| ~ spl0_9
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1291,f1021,f363,f1272,f1016]) ).
fof(f1861,plain,
( ~ spl0_150
| spl0_162
| ~ spl0_11
| spl0_148 ),
inference(avatar_split_clause,[],[f1212,f1026,f369,f1163,f1036]) ).
fof(f1862,plain,
( ~ spl0_162
| ~ spl0_150
| ~ spl0_24
| spl0_148 ),
inference(avatar_split_clause,[],[f1606,f1026,f417,f1036,f1163]) ).
fof(f1901,plain,
( c0_1(a1)
| ~ c2_1(a1)
| ~ spl0_9
| ~ spl0_111 ),
inference(resolution,[],[f364,f843]) ).
fof(f1910,plain,
( ~ spl0_139
| ~ spl0_174
| ~ spl0_13
| spl0_104 ),
inference(avatar_split_clause,[],[f1342,f807,f376,f1359,f981]) ).
fof(f1950,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4
| ~ spl0_17 ),
inference(resolution,[],[f391,f346]) ).
fof(f1957,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_4
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1950]) ).
fof(f1958,plain,
( spl0_7
| ~ spl0_4
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1957,f390,f345,f356]) ).
fof(f1986,plain,
( ~ c0_1(a52)
| c3_1(a52)
| ~ spl0_21
| spl0_104 ),
inference(resolution,[],[f407,f809]) ).
fof(f1993,plain,
( spl0_174
| ~ spl0_139
| ~ spl0_21
| spl0_104 ),
inference(avatar_split_clause,[],[f1986,f807,f406,f981,f1359]) ).
fof(f1998,plain,
( ~ spl0_161
| ~ spl0_141
| ~ spl0_24
| spl0_140 ),
inference(avatar_split_clause,[],[f1608,f986,f417,f991,f1158]) ).
fof(f2000,plain,
( ~ c0_1(a58)
| c3_1(a58)
| ~ spl0_21
| spl0_105 ),
inference(resolution,[],[f814,f407]) ).
fof(f2006,plain,
( spl0_140
| ~ spl0_141
| ~ spl0_21
| spl0_105 ),
inference(avatar_split_clause,[],[f2000,f812,f406,f991,f986]) ).
fof(f2007,plain,
( ~ spl0_153
| ~ spl0_151
| ~ spl0_1
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f1676,f1046,f335,f1041,f1051]) ).
fof(f2008,plain,
( ~ spl0_172
| ~ spl0_146
| ~ spl0_1
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1678,f1021,f335,f1016,f1272]) ).
fof(f2014,plain,
( ~ spl0_110
| spl0_63
| ~ spl0_9
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f1901,f841,f363,f602,f836]) ).
fof(f2018,plain,
( ~ spl0_139
| spl0_103
| ~ spl0_15
| spl0_104 ),
inference(avatar_split_clause,[],[f1404,f807,f383,f802,f981]) ).
fof(f2023,plain,
( ~ spl0_127
| ~ spl0_80
| ~ spl0_22
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1589,f916,f409,f687,f921]) ).
fof(f2025,plain,
( spl0_174
| spl0_103
| ~ spl0_25
| spl0_104 ),
inference(avatar_split_clause,[],[f1627,f807,f421,f802,f1359]) ).
fof(f2026,plain,
( spl0_133
| spl0_94
| ~ spl0_25
| spl0_95 ),
inference(avatar_split_clause,[],[f1629,f762,f421,f757,f951]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f347]) ).
cnf(s2,plain,
( spl0_2
| spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f354]) ).
cnf(s3,plain,
( spl0_3
| spl0_5
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f361]) ).
cnf(s4,plain,
( spl0_3
| spl0_9
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f371]) ).
cnf(s5,plain,
( spl0_3
| spl0_9
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f378]) ).
cnf(s7,plain,
( spl0_3
| spl0_13
| spl0_14
| spl0_17 ),
inference(sat_conversion,[],[f392]) ).
cnf(s9,plain,
( spl0_3
| spl0_20
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f411]) ).
cnf(s10,plain,
( spl0_3
| spl0_13
| ~ spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f419]) ).
cnf(s11,plain,
( spl0_3
| spl0_4
| ~ spl0_23
| spl0_25 ),
inference(sat_conversion,[],[f423]) ).
cnf(s12,plain,
( spl0_3
| spl0_5
| spl0_7
| ~ spl0_26 ),
inference(sat_conversion,[],[f428]) ).
cnf(s15,plain,
( spl0_3
| spl0_5
| spl0_16
| spl0_31 ),
inference(sat_conversion,[],[f449]) ).
cnf(s17,plain,
( spl0_3
| spl0_22
| spl0_25
| spl0_32 ),
inference(sat_conversion,[],[f455]) ).
cnf(s18,plain,
( spl0_3
| spl0_19
| spl0_25
| spl0_33 ),
inference(sat_conversion,[],[f460]) ).
cnf(s25,plain,
( spl0_3
| spl0_5
| spl0_14
| ~ spl0_40 ),
inference(sat_conversion,[],[f492]) ).
cnf(s32,plain,
( spl0_3
| spl0_19
| spl0_32
| ~ spl0_40 ),
inference(sat_conversion,[],[f535]) ).
cnf(s33,plain,
( spl0_3
| spl0_19
| spl0_43
| spl0_51 ),
inference(sat_conversion,[],[f540]) ).
cnf(s35,plain,
( spl0_3
| spl0_9
| ~ spl0_52
| ~ spl0_53 ),
inference(sat_conversion,[],[f550]) ).
cnf(s36,plain,
( spl0_3
| spl0_16
| spl0_43
| ~ spl0_52 ),
inference(sat_conversion,[],[f551]) ).
cnf(s37,plain,
( spl0_3
| spl0_15
| spl0_32
| ~ spl0_54 ),
inference(sat_conversion,[],[f556]) ).
cnf(s39,plain,
( spl0_3
| spl0_15
| ~ spl0_23
| spl0_55 ),
inference(sat_conversion,[],[f562]) ).
cnf(s43,plain,
( spl0_3
| spl0_12
| spl0_46
| ~ spl0_58 ),
inference(sat_conversion,[],[f578]) ).
cnf(s47,plain,
( spl0_3
| spl0_17
| ~ spl0_26
| spl0_32 ),
inference(sat_conversion,[],[f593]) ).
cnf(s51,plain,
( ~ spl0_32
| ~ spl0_63 ),
inference(sat_conversion,[],[f605]) ).
cnf(s52,plain,
( spl0_40
| ~ spl0_64 ),
inference(sat_conversion,[],[f610]) ).
cnf(s53,plain,
( ~ spl0_43
| ~ spl0_65 ),
inference(sat_conversion,[],[f615]) ).
cnf(s56,plain,
( spl0_52
| ~ spl0_68 ),
inference(sat_conversion,[],[f630]) ).
cnf(s57,plain,
( spl0_26
| spl0_69 ),
inference(sat_conversion,[],[f635]) ).
cnf(s60,plain,
( spl0_61
| ~ spl0_72 ),
inference(sat_conversion,[],[f650]) ).
cnf(s61,plain,
( spl0_61
| ~ spl0_73 ),
inference(sat_conversion,[],[f655]) ).
cnf(s63,plain,
( spl0_37
| spl0_75 ),
inference(sat_conversion,[],[f665]) ).
cnf(s64,plain,
( spl0_37
| ~ spl0_76 ),
inference(sat_conversion,[],[f670]) ).
cnf(s68,plain,
( ~ spl0_57
| spl0_80 ),
inference(sat_conversion,[],[f690]) ).
cnf(s72,plain,
( ~ spl0_31
| ~ spl0_84 ),
inference(sat_conversion,[],[f710]) ).
cnf(s73,plain,
( ~ spl0_31
| ~ spl0_85 ),
inference(sat_conversion,[],[f715]) ).
cnf(s77,plain,
( spl0_53
| ~ spl0_89 ),
inference(sat_conversion,[],[f735]) ).
cnf(s78,plain,
( ~ spl0_20
| ~ spl0_90 ),
inference(sat_conversion,[],[f740]) ).
cnf(s82,plain,
( ~ spl0_49
| ~ spl0_94 ),
inference(sat_conversion,[],[f760]) ).
cnf(s83,plain,
( ~ spl0_49
| ~ spl0_95 ),
inference(sat_conversion,[],[f765]) ).
cnf(s87,plain,
( ~ spl0_55
| ~ spl0_99 ),
inference(sat_conversion,[],[f785]) ).
cnf(s88,plain,
( spl0_54
| ~ spl0_100 ),
inference(sat_conversion,[],[f790]) ).
cnf(s89,plain,
( ~ spl0_33
| spl0_101 ),
inference(sat_conversion,[],[f795]) ).
cnf(s90,plain,
( ~ spl0_33
| ~ spl0_102 ),
inference(sat_conversion,[],[f800]) ).
cnf(s91,plain,
( ~ spl0_51
| ~ spl0_103 ),
inference(sat_conversion,[],[f805]) ).
cnf(s92,plain,
( ~ spl0_51
| ~ spl0_104 ),
inference(sat_conversion,[],[f810]) ).
cnf(s93,plain,
( spl0_29
| ~ spl0_105 ),
inference(sat_conversion,[],[f815]) ).
cnf(s97,plain,
( ~ spl0_32
| spl0_110 ),
inference(sat_conversion,[],[f839]) ).
cnf(s98,plain,
( ~ spl0_32
| spl0_111 ),
inference(sat_conversion,[],[f844]) ).
cnf(s99,plain,
( spl0_40
| ~ spl0_112 ),
inference(sat_conversion,[],[f849]) ).
cnf(s100,plain,
( spl0_40
| spl0_113 ),
inference(sat_conversion,[],[f854]) ).
cnf(s101,plain,
( ~ spl0_43
| spl0_114 ),
inference(sat_conversion,[],[f859]) ).
cnf(s102,plain,
( ~ spl0_43
| spl0_115 ),
inference(sat_conversion,[],[f864]) ).
cnf(s104,plain,
( spl0_52
| ~ spl0_117 ),
inference(sat_conversion,[],[f874]) ).
cnf(s105,plain,
( spl0_52
| spl0_118 ),
inference(sat_conversion,[],[f879]) ).
cnf(s106,plain,
( spl0_26
| spl0_119 ),
inference(sat_conversion,[],[f884]) ).
cnf(s107,plain,
( spl0_26
| spl0_120 ),
inference(sat_conversion,[],[f889]) ).
cnf(s109,plain,
( spl0_61
| spl0_122 ),
inference(sat_conversion,[],[f899]) ).
cnf(s112,plain,
( spl0_37
| spl0_125 ),
inference(sat_conversion,[],[f914]) ).
cnf(s113,plain,
( ~ spl0_57
| spl0_126 ),
inference(sat_conversion,[],[f919]) ).
cnf(s114,plain,
( ~ spl0_57
| spl0_127 ),
inference(sat_conversion,[],[f924]) ).
cnf(s116,plain,
( spl0_53
| spl0_129 ),
inference(sat_conversion,[],[f934]) ).
cnf(s117,plain,
( spl0_53
| spl0_130 ),
inference(sat_conversion,[],[f939]) ).
cnf(s118,plain,
( ~ spl0_20
| spl0_131 ),
inference(sat_conversion,[],[f944]) ).
cnf(s120,plain,
( ~ spl0_49
| ~ spl0_133 ),
inference(sat_conversion,[],[f954]) ).
cnf(s121,plain,
( ~ spl0_55
| ~ spl0_134 ),
inference(sat_conversion,[],[f959]) ).
cnf(s122,plain,
( ~ spl0_55
| spl0_135 ),
inference(sat_conversion,[],[f964]) ).
cnf(s123,plain,
( spl0_54
| ~ spl0_136 ),
inference(sat_conversion,[],[f969]) ).
cnf(s124,plain,
( spl0_54
| spl0_137 ),
inference(sat_conversion,[],[f974]) ).
cnf(s125,plain,
( ~ spl0_33
| spl0_138 ),
inference(sat_conversion,[],[f979]) ).
cnf(s126,plain,
( ~ spl0_51
| spl0_139 ),
inference(sat_conversion,[],[f984]) ).
cnf(s127,plain,
( spl0_29
| ~ spl0_140 ),
inference(sat_conversion,[],[f989]) ).
cnf(s128,plain,
( spl0_29
| spl0_141 ),
inference(sat_conversion,[],[f994]) ).
cnf(s132,plain,
( ~ spl0_46
| ~ spl0_145 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s133,plain,
( ~ spl0_46
| spl0_146 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s134,plain,
( ~ spl0_46
| spl0_147 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s135,plain,
( spl0_58
| ~ spl0_148 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s136,plain,
( spl0_58
| spl0_149 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s137,plain,
( spl0_58
| spl0_150 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s138,plain,
( spl0_23
| spl0_151 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s139,plain,
( spl0_23
| spl0_152 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s140,plain,
( spl0_23
| spl0_153 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s141,plain,
( spl0_62
| ~ spl0_154 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s142,plain,
( spl0_62
| spl0_155 ),
inference(sat_conversion,[],[f1064]) ).
cnf(s143,plain,
( spl0_62
| spl0_156 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s145,plain,
( ~ spl0_29
| spl0_43
| spl0_51 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s147,plain,
( spl0_46
| ~ spl0_61
| ~ spl0_62 ),
inference(sat_conversion,[],[f1073]) ).
cnf(s148,plain,
( spl0_43
| spl0_49
| ~ spl0_62 ),
inference(sat_conversion,[],[f1074]) ).
cnf(s151,plain,
( ~ spl0_37
| ~ spl0_58
| ~ spl0_61 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s152,plain,
( ~ spl0_37
| ~ spl0_40
| ~ spl0_58 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s155,plain,
( ~ spl0_3
| ~ spl0_43 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s171,plain,
( ~ spl0_3
| ~ spl0_49 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s183,plain,
( ~ spl0_3
| spl0_62 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s184,plain,
( spl0_33
| spl0_57 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s203,plain,
( ~ spl0_12
| spl0_72
| spl0_73
| ~ spl0_122 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s204,plain,
( ~ spl0_7
| spl0_145
| ~ spl0_146
| spl0_172 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s205,plain,
( ~ spl0_12
| spl0_76
| ~ spl0_125
| spl0_168 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s206,plain,
( ~ spl0_2
| spl0_145
| ~ spl0_147
| ~ spl0_172 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s209,plain,
( ~ spl0_8
| ~ spl0_69
| ~ spl0_119
| ~ spl0_120 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s211,plain,
( ~ spl0_2
| ~ spl0_5
| spl0_24 ),
inference(sat_conversion,[],[f1323]) ).
cnf(s214,plain,
( ~ spl0_2
| ~ spl0_129
| ~ spl0_130
| spl0_173 ),
inference(sat_conversion,[],[f1334]) ).
cnf(s225,plain,
( ~ spl0_14
| spl0_94
| spl0_95
| spl0_169 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s232,plain,
( ~ spl0_2
| spl0_11
| ~ spl0_15 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s233,plain,
( ~ spl0_12
| spl0_99
| ~ spl0_135
| spl0_160 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s234,plain,
( ~ spl0_11
| spl0_140
| ~ spl0_141
| spl0_161 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s239,plain,
( ~ spl0_5
| spl0_105
| ~ spl0_141
| ~ spl0_161 ),
inference(sat_conversion,[],[f1433]) ).
cnf(s249,plain,
( ~ spl0_10
| spl0_90
| ~ spl0_131
| ~ spl0_176 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s253,plain,
( ~ spl0_12
| ~ spl0_14
| spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f1509]) ).
cnf(s266,plain,
( ~ spl0_17
| spl0_68
| ~ spl0_118
| spl0_166 ),
inference(sat_conversion,[],[f1554]) ).
cnf(s272,plain,
( ~ spl0_19
| spl0_68
| spl0_117
| ~ spl0_118 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s285,plain,
( ~ spl0_5
| spl0_8
| ~ spl0_22 ),
inference(sat_conversion,[],[f1604]) ).
cnf(s292,plain,
( ~ spl0_2
| spl0_11
| ~ spl0_25 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s293,plain,
( ~ spl0_10
| ~ spl0_101
| spl0_102
| ~ spl0_138 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s297,plain,
( ~ spl0_7
| spl0_100
| spl0_136
| ~ spl0_137 ),
inference(sat_conversion,[],[f1651]) ).
cnf(s301,plain,
( ~ spl0_16
| spl0_89
| ~ spl0_130
| ~ spl0_173 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s305,plain,
( ~ spl0_2
| ~ spl0_19
| spl0_24 ),
inference(sat_conversion,[],[f1659]) ).
cnf(s307,plain,
( ~ spl0_19
| spl0_90
| ~ spl0_131
| spl0_176 ),
inference(sat_conversion,[],[f1661]) ).
cnf(s320,plain,
( ~ spl0_1
| ~ spl0_149
| ~ spl0_150
| ~ spl0_162 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s332,plain,
( ~ spl0_4
| ~ spl0_5
| spl0_24 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s335,plain,
( ~ spl0_6
| spl0_76
| ~ spl0_125
| ~ spl0_168 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s341,plain,
( ~ spl0_15
| spl0_105
| ~ spl0_141
| spl0_161 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s345,plain,
( ~ spl0_25
| spl0_105
| spl0_140
| spl0_161 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s354,plain,
( ~ spl0_2
| spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s359,plain,
( ~ spl0_5
| spl0_65
| ~ spl0_114
| ~ spl0_115 ),
inference(sat_conversion,[],[f1778]) ).
cnf(s361,plain,
( ~ spl0_11
| spl0_94
| spl0_133
| ~ spl0_169 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s364,plain,
( ~ spl0_11
| spl0_64
| spl0_112
| ~ spl0_113 ),
inference(sat_conversion,[],[f1783]) ).
cnf(s365,plain,
( ~ spl0_16
| ~ spl0_75
| spl0_76
| ~ spl0_168 ),
inference(sat_conversion,[],[f1784]) ).
cnf(s366,plain,
( ~ spl0_24
| spl0_154
| ~ spl0_155
| ~ spl0_156 ),
inference(sat_conversion,[],[f1785]) ).
cnf(s370,plain,
( ~ spl0_24
| spl0_117
| ~ spl0_118
| ~ spl0_166 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s374,plain,
( ~ spl0_6
| ~ spl0_149
| ~ spl0_150
| spl0_162 ),
inference(sat_conversion,[],[f1793]) ).
cnf(s380,plain,
( ~ spl0_11
| spl0_103
| ~ spl0_139
| spl0_174 ),
inference(sat_conversion,[],[f1849]) ).
cnf(s382,plain,
( ~ spl0_4
| spl0_148
| ~ spl0_149
| ~ spl0_162 ),
inference(sat_conversion,[],[f1851]) ).
cnf(s383,plain,
( ~ spl0_4
| spl0_145
| ~ spl0_146
| ~ spl0_147 ),
inference(sat_conversion,[],[f1852]) ).
cnf(s384,plain,
( ~ spl0_4
| spl0_134
| ~ spl0_135
| ~ spl0_160 ),
inference(sat_conversion,[],[f1853]) ).
cnf(s388,plain,
( ~ spl0_9
| ~ spl0_146
| ~ spl0_147
| spl0_172 ),
inference(sat_conversion,[],[f1857]) ).
cnf(s392,plain,
( ~ spl0_11
| spl0_148
| ~ spl0_150
| spl0_162 ),
inference(sat_conversion,[],[f1861]) ).
cnf(s393,plain,
( ~ spl0_24
| spl0_148
| ~ spl0_150
| ~ spl0_162 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s404,plain,
( ~ spl0_13
| spl0_104
| ~ spl0_139
| ~ spl0_174 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s405,plain,
( ~ spl0_4
| spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f1958]) ).
cnf(s406,plain,
( ~ spl0_21
| spl0_104
| ~ spl0_139
| spl0_174 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s411,plain,
( ~ spl0_24
| spl0_140
| ~ spl0_141
| ~ spl0_161 ),
inference(sat_conversion,[],[f1998]) ).
cnf(s412,plain,
( ~ spl0_21
| spl0_105
| spl0_140
| ~ spl0_141 ),
inference(sat_conversion,[],[f2006]) ).
cnf(s413,plain,
( ~ spl0_1
| ~ spl0_151
| ~ spl0_152
| ~ spl0_153 ),
inference(sat_conversion,[],[f2007]) ).
cnf(s414,plain,
( ~ spl0_1
| ~ spl0_146
| ~ spl0_147
| ~ spl0_172 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s420,plain,
( ~ spl0_9
| spl0_63
| ~ spl0_110
| ~ spl0_111 ),
inference(sat_conversion,[],[f2014]) ).
cnf(s424,plain,
( ~ spl0_15
| spl0_103
| spl0_104
| ~ spl0_139 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s429,plain,
( ~ spl0_22
| ~ spl0_80
| ~ spl0_126
| ~ spl0_127 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s431,plain,
( ~ spl0_25
| spl0_103
| spl0_104
| spl0_174 ),
inference(sat_conversion,[],[f2025]) ).
cnf(s432,plain,
( ~ spl0_25
| spl0_94
| spl0_95
| spl0_133 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s434,plain,
( spl0_7
| spl0_5
| spl0_3 ),
inference(rat,[],[s209,s57,s106,s107,s3,s12]) ).
cnf(s435,plain,
( spl0_26
| ~ spl0_8 ),
inference(rat,[],[s209,s57,s106,s107]) ).
cnf(s436,plain,
( spl0_40
| ~ spl0_11 ),
inference(rat,[],[s364,s52,s99,s100]) ).
cnf(s438,plain,
( ~ spl0_51
| ~ spl0_13
| ~ spl0_11 ),
inference(rat,[],[s380,s404,s91,s92,s126]) ).
cnf(s440,plain,
( spl0_58
| ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s382,s374,s135,s136,s137]) ).
cnf(s441,plain,
( ~ spl0_46
| ~ spl0_4 ),
inference(rat,[],[s383,s132,s133,s134]) ).
cnf(s442,plain,
( spl0_37
| ~ spl0_12
| ~ spl0_6 ),
inference(rat,[],[s205,s335,s64,s112]) ).
cnf(s443,plain,
( ~ spl0_6
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s203,s60,s61,s109,s151,s442,s43,s440,s441]) ).
cnf(s444,plain,
( ~ spl0_43
| ~ spl0_5 ),
inference(rat,[],[s359,s53,s101,s102]) ).
cnf(s448,plain,
( ~ spl0_33
| ~ spl0_10 ),
inference(rat,[],[s293,s89,s90,s125]) ).
cnf(s449,plain,
( ~ spl0_10
| spl0_21
| ~ spl0_19
| spl0_3 ),
inference(rat,[],[s249,s307,s78,s118,s9,s429,s68,s113,s114,s184,s448]) ).
cnf(s450,plain,
( ~ spl0_32
| ~ spl0_9 ),
inference(rat,[],[s420,s51,s97,s98]) ).
cnf(s451,plain,
( spl0_51
| spl0_11
| ~ spl0_5
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s47,s405,s435,s297,s285,s88,s123,s124,s17,s37,s450,s4,s449,s341,s345,s412,s411,s93,s127,s128,s145,s33,s332,s444]) ).
cnf(s452,plain,
( spl0_9
| spl0_103
| spl0_104
| ~ spl0_139
| spl0_11
| spl0_12
| spl0_3 ),
inference(rat,[],[s449,s18,s406,s431,s448,s404,s4,s5]) ).
cnf(s454,plain,
( spl0_62
| ~ spl0_24 ),
inference(rat,[],[s366,s141,s142,s143]) ).
cnf(s455,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s47,s405,s435,s297,s285,s88,s123,s124,s17,s37,s450,s452,s424,s91,s92,s126,s451,s392,s382,s135,s136,s137,s43,s203,s432,s60,s61,s109,s82,s83,s120,s147,s148,s454,s444,s332,s2,s443,s441,s1]) ).
cnf(s456,plain,
~ spl0_3,
inference(rat,[],[s148,s155,s171,s183]) ).
cnf(s457,plain,
( spl0_58
| ~ spl0_2 ),
inference(rat,[],[s354,s135,s136,s137]) ).
cnf(s458,plain,
( spl0_46
| ~ spl0_62
| ~ spl0_58 ),
inference(rat,[],[s203,s60,s61,s109,s43,s147,s456]) ).
cnf(s459,plain,
( ~ spl0_51
| ~ spl0_139
| spl0_12
| spl0_11
| spl0_9 ),
inference(rat,[],[s452,s91,s92,s456]) ).
cnf(s462,plain,
( spl0_52
| ~ spl0_19 ),
inference(rat,[],[s272,s56,s104,s105]) ).
cnf(s463,plain,
( ~ spl0_52
| ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s301,s214,s77,s116,s117,s36,s35,s444,s388,s206,s132,s134,s133,s458,s454,s211,s457,s456]) ).
cnf(s464,plain,
( ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s7,s225,s438,s361,s4,s448,s18,s33,s266,s370,s462,s56,s104,s105,s463,s388,s206,s132,s133,s134,s458,s432,s82,s83,s120,s148,s454,s444,s211,s457,s456]) ).
cnf(s465,plain,
( spl0_54
| ~ spl0_7 ),
inference(rat,[],[s297,s88,s123,s124]) ).
cnf(s466,plain,
( ~ spl0_46
| ~ spl0_2 ),
inference(rat,[],[s206,s204,s132,s133,s134,s434,s464,s456]) ).
cnf(s467,plain,
( spl0_32
| ~ spl0_2 ),
inference(rat,[],[s436,s232,s32,s37,s465,s434,s464,s305,s454,s458,s466,s457,s456]) ).
cnf(s468,plain,
( spl0_11
| ~ spl0_2 ),
inference(rat,[],[s448,s18,s4,s292,s305,s454,s458,s466,s457,s450,s467,s456]) ).
cnf(s469,plain,
~ spl0_2,
inference(rat,[],[s253,s72,s73,s15,s365,s205,s63,s64,s112,s152,s25,s436,s468,s43,s466,s464,s457,s456]) ).
cnf(s470,plain,
spl0_1,
inference(rat,[],[s455,s456,s469]) ).
cnf(s471,plain,
( ~ spl0_49
| ~ spl0_25 ),
inference(rat,[],[s432,s82,s83,s120]) ).
cnf(s472,plain,
spl0_23,
inference(rat,[],[s413,s138,s139,s140,s470]) ).
cnf(s473,plain,
( ~ spl0_25
| ~ spl0_51
| spl0_43 ),
inference(rat,[],[s454,s10,s148,s404,s471,s431,s126,s92,s91,s472,s456]) ).
cnf(s474,plain,
( ~ spl0_51
| spl0_32
| ~ spl0_5 ),
inference(rat,[],[s47,s435,s405,s285,s11,s17,s473,s465,s37,s424,s91,s92,s126,s444,s456,s472]) ).
cnf(s475,plain,
( spl0_51
| ~ spl0_5 ),
inference(rat,[],[s451,s11,s234,s345,s239,s93,s127,s128,s145,s444,s456,s472]) ).
cnf(s476,plain,
~ spl0_5,
inference(rat,[],[s392,s393,s459,s135,s137,s233,s458,s384,s454,s87,s121,s122,s332,s441,s39,s450,s11,s424,s474,s473,s91,s92,s126,s475,s444,s472,s456]) ).
cnf(s477,plain,
spl0_6,
inference(rat,[],[s2,s456,s469,s476]) ).
cnf(s478,plain,
spl0_7,
inference(rat,[],[s434,s456,s476]) ).
cnf(s490,plain,
~ spl0_46,
inference(rat,[],[s204,s414,s132,s133,s134,s478,s470]) ).
cnf(s501,plain,
( ~ spl0_149
| ~ spl0_150 ),
inference(rat,[],[s374,s320,s470,s477]) ).
cnf(s502,plain,
spl0_58,
inference(rat,[],[s501,s136,s137]) ).
cnf(s504,plain,
spl0_12,
inference(rat,[],[s43,s490,s456,s502]) ).
cnf(s508,plain,
spl0_37,
inference(rat,[],[s442,s477,s504]) ).
cnf(s509,plain,
~ spl0_61,
inference(rat,[],[s151,s502,s508]) ).
cnf(s510,plain,
spl0_122,
inference(rat,[],[s109,s509]) ).
cnf(s511,plain,
~ spl0_73,
inference(rat,[],[s61,s509]) ).
cnf(s512,plain,
~ spl0_72,
inference(rat,[],[s60,s509]) ).
cnf(s513,plain,
$false,
inference(rat,[],[s203,s512,s504,s510,s511]) ).
fof(f2028,plain,
$false,
inference(avatar_sat_refutation,[],[s513]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN443-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 16:08:03 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.23/0.28 % (3735830)Will run a generic schedule for satisfiability detection.
% 0.23/0.28 % (3735840)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2683941573:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.23/0.28 % (3735836)% WARNING: option uhcvi not known.
% 0.23/0.28 % (3735836)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2987478194:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.23/0.28 % (3735835)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3226523942_2999 on theBenchmark for (2999ds/0Mi)
% 0.23/0.28 % (3735837)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3267969049:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.23/0.28 % (3735838)dis+10_1_sil=32000:sp=arity:random_seed=193442809:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.23/0.28 % (3735839)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4176942545:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.23/0.28 % (3735841)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2136160405:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.23/0.28 % Detected minimum model sizes of [1]
% 0.23/0.28 % Detected maximum model sizes of [31]
% 0.23/0.28 % TRYING [1]
% 0.23/0.28 % TRYING [2]
% 0.23/0.28 % TRYING [3]
% 0.23/0.28 % TRYING [4]
% 0.23/0.28 % (3735841) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3735830-3735841"...
% 0.23/0.28 % (3735840) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3735830-3735840"...
% 0.23/0.28 % (3735841)...printing done.
% 0.23/0.28 % (3735841)Refutation found. Thanks to Tanya!
% 0.23/0.28 % SZS status Unsatisfiable for theBenchmark
% 0.23/0.28 % SZS output start Proof for theBenchmark
% See solution above
% 0.23/0.29 % (3735841)------------------------------
% 0.23/0.29 % (3735841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.29 % (3735841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.29 % (3735841)CaDiCaL version: 2.1.3
% 0.23/0.29 % (3735841)Termination reason: Refutation
% 0.23/0.29 % (3735841)Time elapsed: 0.025 s
% 0.23/0.29 % (3735841)Peak memory usage: 13 MB
% 0.23/0.29 % (3735841)Instructions burned: 37 (million)
% 0.23/0.29 % (3735830)Success in time 0.064 s
% 0.23/0.29 % Vampire exiting
%------------------------------------------------------------------------------