%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN506-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 : 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 02:16:17 PM UTC 2026
% Result : Unsatisfiable 0.20s 0.29s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 209
% Syntax : Number of formulae : 728 ( 25 unt; 116 def)
% Number of atoms : 2305 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2783 (1206 ~;1461 |; 0 &)
% ( 116 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 142 ( 141 usr; 138 prp; 0-1 aty)
% Number of functors : 20 ( 20 usr; 20 con; 0-0 aty)
% Number of variables : 178 ( 0 sgn 178 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp25
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( hskp24
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f6,negated_conjecture,
( ~ hskp25
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
fof(f15,negated_conjecture,
( ~ hskp16
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
fof(f39,negated_conjecture,
( ~ hskp28
| c0_1(a343) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( ~ hskp28
| c1_1(a343) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f41,negated_conjecture,
( ~ hskp28
| c2_1(a343) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
( ~ hskp27
| c1_1(a341) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp27
| c2_1(a341) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp27
| c3_1(a341) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp26
| c0_1(a333) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp26
| c1_1(a333) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp26
| c3_1(a333) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp25
| c0_1(a419) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp24
| c1_1(a401) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f52,negated_conjecture,
( ~ hskp22
| c3_1(a367) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp21
| c3_1(a359) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f60,negated_conjecture,
( ~ hskp16
| c1_1(a349) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp16
| c3_1(a349) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp15
| c0_1(a348) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f65,negated_conjecture,
( ~ hskp13
| c0_1(a346) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( ~ hskp13
| c2_1(a346) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( ~ hskp12
| c0_1(a345) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp12
| c3_1(a345) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp10
| c0_1(a337) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f71,negated_conjecture,
( ~ hskp7
| c3_1(a330) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp6
| c2_1(a329) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp5
| c0_1(a327) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp5
| c1_1(a327) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp4
| c0_1(a326) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp4
| c2_1(a326) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp3
| c0_1(a325) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp3
| c1_1(a325) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f81,negated_conjecture,
( ~ c1_1(a419)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ c2_1(a419)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ c0_1(a401)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ c2_1(a401)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f86,negated_conjecture,
( ~ c1_1(a367)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ c2_1(a367)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ c0_1(a359)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ c2_1(a359)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f96,negated_conjecture,
( ~ c2_1(a349)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c1_1(a348)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c3_1(a348)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f100,negated_conjecture,
( ~ c3_1(a346)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c2_1(a345)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f105,negated_conjecture,
( ~ c2_1(a337)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c3_1(a337)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f109,negated_conjecture,
( ~ c0_1(a332)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c2_1(a332)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c3_1(a332)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c0_1(a330)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c1_1(a330)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ c1_1(a329)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c3_1(a329)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c3_1(a327)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c1_1(a326)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c2_1(a325)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c0_1(a324)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c1_1(a324)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c3_1(a324)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c1_1(a323)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c2_1(a323)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c3_1(a323)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f133,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp7
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp28
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f137,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp13
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp3
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp4
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp2
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f150,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp3
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
fof(f154,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f161,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f177,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
fof(f182,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X0)
| c2_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f185,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause185) ).
fof(f187,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X2)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f191,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause191) ).
fof(f193,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| c2_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X2)
| c3_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| c2_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| c2_1(X1)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause196) ).
fof(f197,plain,
( hskp25
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f1]) ).
fof(f198,plain,
( ~ hskp24
| hskp7 ),
inference(consistent_polarity_flipping,[],[f2]) ).
fof(f205,plain,
( hskp16
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f222,plain,
( hskp28
| c0_1(a343) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f223,plain,
( hskp28
| c1_1(a343) ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f224,plain,
( hskp28
| ~ c2_1(a343) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f225,plain,
( hskp27
| c1_1(a341) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f226,plain,
( hskp27
| ~ c2_1(a341) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f227,plain,
( hskp27
| c3_1(a341) ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f228,plain,
( hskp26
| c0_1(a333) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f229,plain,
( hskp26
| c1_1(a333) ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f230,plain,
( hskp26
| c3_1(a333) ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f231,plain,
( hskp24
| c1_1(a401) ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f232,plain,
( hskp21
| c3_1(a359) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f237,plain,
( hskp16
| c1_1(a349) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f238,plain,
( hskp16
| c3_1(a349) ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f240,plain,
( hskp13
| c0_1(a346) ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f241,plain,
( hskp13
| ~ c2_1(a346) ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f242,plain,
( hskp12
| c0_1(a345) ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f243,plain,
( hskp12
| c3_1(a345) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f245,plain,
( hskp6
| ~ c2_1(a329) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f246,plain,
( hskp5
| c0_1(a327) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f247,plain,
( hskp5
| c1_1(a327) ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f248,plain,
( hskp4
| c0_1(a326) ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f249,plain,
( hskp4
| ~ c2_1(a326) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f250,plain,
( hskp3
| c0_1(a325) ),
inference(consistent_polarity_flipping,[],[f77]) ).
fof(f251,plain,
( hskp3
| c1_1(a325) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f253,plain,
( c2_1(a419)
| ~ hskp25 ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f254,plain,
( ~ c0_1(a401)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f255,plain,
( c2_1(a401)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f84]) ).
fof(f256,plain,
( c2_1(a367)
| ~ hskp22 ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f257,plain,
( ~ c0_1(a359)
| hskp21 ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f258,plain,
( c2_1(a359)
| hskp21 ),
inference(consistent_polarity_flipping,[],[f89]) ).
fof(f261,plain,
( c2_1(a349)
| hskp16 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f262,plain,
( ~ c3_1(a346)
| hskp13 ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f263,plain,
( c2_1(a345)
| hskp12 ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f267,plain,
( c2_1(a337)
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f270,plain,
( c2_1(a332)
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f271,plain,
( ~ c1_1(a329)
| hskp6 ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f272,plain,
( ~ c3_1(a329)
| hskp6 ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f273,plain,
( ~ c3_1(a327)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f274,plain,
( ~ c1_1(a326)
| hskp4 ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f275,plain,
( c2_1(a325)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f276,plain,
( ~ c0_1(a324)
| hskp2 ),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f277,plain,
( ~ c1_1(a324)
| hskp2 ),
inference(consistent_polarity_flipping,[],[f120]) ).
fof(f278,plain,
( ~ c3_1(a324)
| hskp2 ),
inference(consistent_polarity_flipping,[],[f121]) ).
fof(f279,plain,
( c2_1(a323)
| ~ hskp1 ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f287,plain,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ c2_1(X0)
| hskp7
| hskp22 ),
inference(consistent_polarity_flipping,[],[f133]) ).
fof(f288,plain,
! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp15 ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f289,plain,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| c3_1(X0)
| ~ hskp28
| ~ hskp27 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f291,plain,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ hskp28 ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f296,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ hskp13
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f297,plain,
! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| ~ hskp3
| hskp10 ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f298,plain,
! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| ~ hskp4
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f145]) ).
fof(f299,plain,
! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| ~ hskp2
| hskp1 ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f303,plain,
! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ hskp3
| hskp10 ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f307,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ c2_1(X0)
| c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f308,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| ~ hskp26 ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f314,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| ~ hskp21 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f315,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp22 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f316,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| ~ hskp6 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f320,plain,
! [X0,X1] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c0_1(X1)
| ~ c2_1(X1)
| ~ hskp4 ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f321,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X0)
| c0_1(X1)
| ~ c2_1(X1)
| ~ hskp28 ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f322,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X0)
| c0_1(X1)
| c3_1(X1)
| ~ hskp26 ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f326,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c2_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| ~ hskp5 ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f330,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f177]) ).
fof(f335,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f336,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X0)
| ~ c2_1(X1)
| hskp8 ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f338,plain,
! [X0,X1] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| hskp22 ),
inference(consistent_polarity_flipping,[],[f185]) ).
fof(f340,plain,
! [X0,X1] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f341,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f344,plain,
! [X2,X0,X1] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X2)
| c1_1(X0)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2) ),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f346,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X1)
| c0_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f347,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| ~ c1_1(X2)
| c3_1(X1)
| c0_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f194]) ).
fof(f348,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| ~ c2_1(X1)
| c1_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f195]) ).
fof(f349,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f196]) ).
fof(f351,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f352,plain,
( ! [X2] :
( c3_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f354,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f355,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f357,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f361,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f362,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f349,f361,f357,f354,f351]) ).
fof(f365,definition,
( spl0_5
<=> ! [X2] :
( ~ c3_1(X2)
| ~ c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f366,plain,
( ! [X2] :
( ~ c3_1(X2)
| ~ c2_1(X2)
| c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f368,definition,
( spl0_6
<=> ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f369,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f371,definition,
( spl0_7
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f372,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f373,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f348,f371,f357,f368,f365]) ).
fof(f375,definition,
( spl0_8
<=> ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f376,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f378,definition,
( spl0_9
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f379,plain,
( ! [X1] :
( c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f380,plain,
( spl0_8
| spl0_9
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f347,f371,f357,f378,f375]) ).
fof(f381,plain,
( spl0_8
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f346,f361,f357,f354,f375]) ).
fof(f383,definition,
( spl0_10
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f384,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| ~ c1_1(X2) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f386,definition,
( spl0_11
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f387,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f390,definition,
( spl0_12
<=> ! [X2] :
( c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f391,plain,
( ! [X2] :
( c2_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f393,definition,
( spl0_13
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f394,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,definition,
( spl0_14
<=> ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f397,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c2_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f398,plain,
( spl0_12
| spl0_13
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f344,f396,f357,f393,f390]) ).
fof(f400,definition,
( spl0_15
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f401,plain,
( ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f403,definition,
( spl0_16
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f404,plain,
( ! [X1] :
( c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f410,definition,
( spl0_18
<=> ! [X2] :
( ~ c3_1(X2)
| ~ c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f411,plain,
( ! [X2] :
( ~ c3_1(X2)
| ~ c2_1(X2)
| c0_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f413,plain,
( spl0_8
| spl0_16
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f341,f351,f357,f403,f375]) ).
fof(f415,definition,
( spl0_19
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f419,definition,
( spl0_20
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f420,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,definition,
( spl0_21
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f423,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f424,plain,
( spl0_19
| spl0_20
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f340,f422,f357,f419,f415]) ).
fof(f430,definition,
( spl0_23
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f431,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f434,definition,
( spl0_24
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f437,plain,
( spl0_24
| spl0_14
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f338,f422,f357,f396,f434]) ).
fof(f439,definition,
( spl0_25
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f444,definition,
( spl0_26
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f448,definition,
( spl0_27
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f449,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f450,plain,
( spl0_26
| spl0_23
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f336,f448,f357,f430,f444]) ).
fof(f451,plain,
( spl0_19
| spl0_1
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f335,f371,f357,f351,f415]) ).
fof(f468,definition,
( spl0_31
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f475,definition,
( spl0_33
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f476,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f479,definition,
( spl0_34
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f482,plain,
( ~ spl0_34
| spl0_10
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f330,f403,f357,f383,f479]) ).
fof(f484,definition,
( spl0_35
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f488,definition,
( spl0_36
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f489,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f493,definition,
( spl0_37
<=> ! [X1] :
( c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f494,plain,
( ! [X1] :
( c3_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f497,definition,
( spl0_38
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f500,plain,
( ~ spl0_38
| spl0_37
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f326,f403,f357,f493,f497]) ).
fof(f502,definition,
( spl0_39
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f507,definition,
( spl0_40
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f519,definition,
( spl0_43
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f522,plain,
( ~ spl0_43
| spl0_15
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f322,f354,f357,f400,f519]) ).
fof(f524,definition,
( spl0_44
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f527,plain,
( ~ spl0_44
| spl0_18
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f321,f354,f357,f410,f524]) ).
fof(f528,plain,
( ~ spl0_31
| spl0_8
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f320,f378,f357,f375,f468]) ).
fof(f532,definition,
( spl0_45
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f533,plain,
( ! [X1] :
( c3_1(X1)
| c0_1(X1)
| c1_1(X1) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f535,plain,
( ~ spl0_25
| spl0_45
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f316,f371,f357,f532,f439]) ).
fof(f537,definition,
( spl0_46
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f538,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f539,plain,
( spl0_24
| spl0_46
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f315,f351,f357,f537,f434]) ).
fof(f541,definition,
( spl0_47
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f545,definition,
( spl0_48
<=> ! [X1] :
( c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f546,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f547,plain,
( ~ spl0_47
| spl0_48
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f314,f448,f357,f545,f541]) ).
fof(f551,definition,
( spl0_49
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f565,plain,
( ~ spl0_43
| spl0_36
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f308,f386,f357,f488,f519]) ).
fof(f566,plain,
( ~ spl0_34
| spl0_48
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f307,f365,f357,f545,f479]) ).
fof(f572,definition,
( spl0_53
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f582,definition,
( spl0_55
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f585,plain,
( spl0_19
| ~ spl0_55
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f303,f422,f357,f582,f415]) ).
fof(f587,definition,
( spl0_56
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f592,definition,
( spl0_57
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f597,plain,
( spl0_53
| ~ spl0_39
| ~ spl0_3
| spl0_33 ),
inference(avatar_split_clause,[],[f299,f475,f357,f502,f572]) ).
fof(f598,plain,
( ~ spl0_56
| ~ spl0_31
| ~ spl0_3
| spl0_33 ),
inference(avatar_split_clause,[],[f298,f475,f357,f468,f587]) ).
fof(f599,plain,
( spl0_19
| ~ spl0_55
| ~ spl0_3
| spl0_33 ),
inference(avatar_split_clause,[],[f297,f475,f357,f582,f415]) ).
fof(f601,definition,
( spl0_58
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f604,plain,
( ~ spl0_34
| ~ spl0_58
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f296,f430,f357,f601,f479]) ).
fof(f618,plain,
( ~ spl0_44
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f291,f368,f357,f524]) ).
fof(f620,plain,
( ~ spl0_49
| ~ spl0_44
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f289,f351,f357,f524,f551]) ).
fof(f621,plain,
( spl0_40
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f288,f396,f357,f507]) ).
fof(f622,plain,
( spl0_24
| spl0_35
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f287,f386,f357,f484,f434]) ).
fof(f639,definition,
( spl0_63
<=> c3_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f641,plain,
( ~ c3_1(a323)
| spl0_63 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f642,plain,
( ~ spl0_53
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f124,f639,f572]) ).
fof(f644,definition,
( spl0_64
<=> c2_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f647,plain,
( ~ spl0_53
| spl0_64 ),
inference(avatar_split_clause,[],[f279,f644,f572]) ).
fof(f649,definition,
( spl0_65
<=> c1_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f652,plain,
( ~ spl0_53
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f122,f649,f572]) ).
fof(f654,definition,
( spl0_66
<=> c3_1(a324) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f656,plain,
( ~ c3_1(a324)
| spl0_66 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f657,plain,
( spl0_39
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f278,f654,f502]) ).
fof(f659,definition,
( spl0_67
<=> c1_1(a324) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f662,plain,
( spl0_39
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f277,f659,f502]) ).
fof(f664,definition,
( spl0_68
<=> c0_1(a324) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f667,plain,
( spl0_39
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f276,f664,f502]) ).
fof(f669,definition,
( spl0_69
<=> c2_1(a325) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f671,plain,
( c2_1(a325)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
( spl0_55
| spl0_69 ),
inference(avatar_split_clause,[],[f275,f669,f582]) ).
fof(f674,definition,
( spl0_70
<=> c1_1(a326) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f677,plain,
( spl0_31
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f274,f674,f468]) ).
fof(f679,definition,
( spl0_71
<=> c3_1(a327) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f681,plain,
( ~ c3_1(a327)
| spl0_71 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f682,plain,
( spl0_38
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f273,f679,f497]) ).
fof(f684,definition,
( spl0_72
<=> c3_1(a329) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f686,plain,
( ~ c3_1(a329)
| spl0_72 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f687,plain,
( spl0_25
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f272,f684,f439]) ).
fof(f689,definition,
( spl0_73
<=> c1_1(a329) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f692,plain,
( spl0_25
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f271,f689,f439]) ).
fof(f694,definition,
( spl0_74
<=> c1_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f697,plain,
( ~ spl0_35
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f113,f694,f484]) ).
fof(f699,definition,
( spl0_75
<=> c0_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f702,plain,
( ~ spl0_35
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f112,f699,f484]) ).
fof(f704,definition,
( spl0_76
<=> c3_1(a332) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f706,plain,
( ~ c3_1(a332)
| spl0_76 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f707,plain,
( ~ spl0_26
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f111,f704,f444]) ).
fof(f709,definition,
( spl0_77
<=> c2_1(a332) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f711,plain,
( c2_1(a332)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f712,plain,
( ~ spl0_26
| spl0_77 ),
inference(avatar_split_clause,[],[f270,f709,f444]) ).
fof(f714,definition,
( spl0_78
<=> c0_1(a332) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f717,plain,
( ~ spl0_26
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f109,f714,f444]) ).
fof(f729,definition,
( spl0_81
<=> c3_1(a337) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f731,plain,
( ~ c3_1(a337)
| spl0_81 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f732,plain,
( ~ spl0_19
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f106,f729,f415]) ).
fof(f734,definition,
( spl0_82
<=> c2_1(a337) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f736,plain,
( c2_1(a337)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f737,plain,
( ~ spl0_19
| spl0_82 ),
inference(avatar_split_clause,[],[f267,f734,f415]) ).
fof(f754,definition,
( spl0_86
<=> c2_1(a345) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f756,plain,
( c2_1(a345)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f757,plain,
( spl0_34
| spl0_86 ),
inference(avatar_split_clause,[],[f263,f754,f479]) ).
fof(f759,definition,
( spl0_87
<=> c3_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f761,plain,
( ~ c3_1(a346)
| spl0_87 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f762,plain,
( spl0_58
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f262,f759,f601]) ).
fof(f769,definition,
( spl0_89
<=> c3_1(a348) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f771,plain,
( ~ c3_1(a348)
| spl0_89 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f772,plain,
( ~ spl0_40
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f98,f769,f507]) ).
fof(f774,definition,
( spl0_90
<=> c1_1(a348) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f777,plain,
( ~ spl0_40
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f97,f774,f507]) ).
fof(f779,definition,
( spl0_91
<=> c2_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f782,plain,
( spl0_56
| spl0_91 ),
inference(avatar_split_clause,[],[f261,f779,f587]) ).
fof(f814,definition,
( spl0_98
<=> c2_1(a359) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f816,plain,
( c2_1(a359)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f817,plain,
( spl0_47
| spl0_98 ),
inference(avatar_split_clause,[],[f258,f814,f541]) ).
fof(f819,definition,
( spl0_99
<=> c0_1(a359) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f822,plain,
( spl0_47
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f257,f819,f541]) ).
fof(f824,definition,
( spl0_100
<=> c2_1(a367) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f827,plain,
( ~ spl0_24
| spl0_100 ),
inference(avatar_split_clause,[],[f256,f824,f434]) ).
fof(f829,definition,
( spl0_101
<=> c1_1(a367) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f832,plain,
( ~ spl0_24
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f86,f829,f434]) ).
fof(f839,definition,
( spl0_103
<=> c2_1(a401) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f841,plain,
( c2_1(a401)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f842,plain,
( spl0_57
| spl0_103 ),
inference(avatar_split_clause,[],[f255,f839,f592]) ).
fof(f844,definition,
( spl0_104
<=> c0_1(a401) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f847,plain,
( spl0_57
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f254,f844,f592]) ).
fof(f849,definition,
( spl0_105
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f853,definition,
( spl0_106
<=> c2_1(a419) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f855,plain,
( c2_1(a419)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f856,plain,
( ~ spl0_105
| spl0_106 ),
inference(avatar_split_clause,[],[f253,f853,f849]) ).
fof(f858,definition,
( spl0_107
<=> c1_1(a419) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f861,plain,
( ~ spl0_105
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f81,f858,f849]) ).
fof(f873,definition,
( spl0_110
<=> c1_1(a325) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f876,plain,
( spl0_110
| spl0_55 ),
inference(avatar_split_clause,[],[f251,f582,f873]) ).
fof(f878,definition,
( spl0_111
<=> c0_1(a325) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f881,plain,
( spl0_111
| spl0_55 ),
inference(avatar_split_clause,[],[f250,f582,f878]) ).
fof(f883,definition,
( spl0_112
<=> c2_1(a326) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f885,plain,
( ~ c2_1(a326)
| spl0_112 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f886,plain,
( ~ spl0_112
| spl0_31 ),
inference(avatar_split_clause,[],[f249,f468,f883]) ).
fof(f888,definition,
( spl0_113
<=> c0_1(a326) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f891,plain,
( spl0_113
| spl0_31 ),
inference(avatar_split_clause,[],[f248,f468,f888]) ).
fof(f893,definition,
( spl0_114
<=> c1_1(a327) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f896,plain,
( spl0_114
| spl0_38 ),
inference(avatar_split_clause,[],[f247,f497,f893]) ).
fof(f898,definition,
( spl0_115
<=> c0_1(a327) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f901,plain,
( spl0_115
| spl0_38 ),
inference(avatar_split_clause,[],[f246,f497,f898]) ).
fof(f903,definition,
( spl0_116
<=> c2_1(a329) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f906,plain,
( ~ spl0_116
| spl0_25 ),
inference(avatar_split_clause,[],[f245,f439,f903]) ).
fof(f908,definition,
( spl0_117
<=> c3_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f910,plain,
( c3_1(a330)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f911,plain,
( spl0_117
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f71,f484,f908]) ).
fof(f918,definition,
( spl0_119
<=> c0_1(a337) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f921,plain,
( spl0_119
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f69,f415,f918]) ).
fof(f923,definition,
( spl0_120
<=> c3_1(a345) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f925,plain,
( c3_1(a345)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f923]) ).
fof(f926,plain,
( spl0_120
| spl0_34 ),
inference(avatar_split_clause,[],[f243,f479,f923]) ).
fof(f928,definition,
( spl0_121
<=> c0_1(a345) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f931,plain,
( spl0_121
| spl0_34 ),
inference(avatar_split_clause,[],[f242,f479,f928]) ).
fof(f933,definition,
( spl0_122
<=> c2_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f936,plain,
( ~ spl0_122
| spl0_58 ),
inference(avatar_split_clause,[],[f241,f601,f933]) ).
fof(f938,definition,
( spl0_123
<=> c0_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f941,plain,
( spl0_123
| spl0_58 ),
inference(avatar_split_clause,[],[f240,f601,f938]) ).
fof(f953,definition,
( spl0_126
<=> c0_1(a348) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f956,plain,
( spl0_126
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f62,f507,f953]) ).
fof(f958,definition,
( spl0_127
<=> c3_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f960,plain,
( c3_1(a349)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f961,plain,
( spl0_127
| spl0_56 ),
inference(avatar_split_clause,[],[f238,f587,f958]) ).
fof(f963,definition,
( spl0_128
<=> c1_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f966,plain,
( spl0_128
| spl0_56 ),
inference(avatar_split_clause,[],[f237,f587,f963]) ).
fof(f998,definition,
( spl0_135
<=> c3_1(a359) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f1000,plain,
( c3_1(a359)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f998]) ).
fof(f1001,plain,
( spl0_135
| spl0_47 ),
inference(avatar_split_clause,[],[f232,f541,f998]) ).
fof(f1003,definition,
( spl0_136
<=> c3_1(a367) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f1005,plain,
( c3_1(a367)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f1003]) ).
fof(f1006,plain,
( spl0_136
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f52,f434,f1003]) ).
fof(f1018,definition,
( spl0_139
<=> c1_1(a401) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1021,plain,
( spl0_139
| spl0_57 ),
inference(avatar_split_clause,[],[f231,f592,f1018]) ).
fof(f1023,definition,
( spl0_140
<=> c0_1(a419) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1026,plain,
( spl0_140
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f48,f849,f1023]) ).
fof(f1028,definition,
( spl0_141
<=> c3_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1030,plain,
( c3_1(a333)
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f1028]) ).
fof(f1031,plain,
( spl0_141
| spl0_43 ),
inference(avatar_split_clause,[],[f230,f519,f1028]) ).
fof(f1033,definition,
( spl0_142
<=> c1_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1036,plain,
( spl0_142
| spl0_43 ),
inference(avatar_split_clause,[],[f229,f519,f1033]) ).
fof(f1038,definition,
( spl0_143
<=> c0_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1041,plain,
( spl0_143
| spl0_43 ),
inference(avatar_split_clause,[],[f228,f519,f1038]) ).
fof(f1043,definition,
( spl0_144
<=> c3_1(a341) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1045,plain,
( c3_1(a341)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1046,plain,
( spl0_144
| spl0_49 ),
inference(avatar_split_clause,[],[f227,f551,f1043]) ).
fof(f1048,definition,
( spl0_145
<=> c2_1(a341) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1050,plain,
( ~ c2_1(a341)
| spl0_145 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1051,plain,
( ~ spl0_145
| spl0_49 ),
inference(avatar_split_clause,[],[f226,f551,f1048]) ).
fof(f1053,definition,
( spl0_146
<=> c1_1(a341) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1056,plain,
( spl0_146
| spl0_49 ),
inference(avatar_split_clause,[],[f225,f551,f1053]) ).
fof(f1058,definition,
( spl0_147
<=> c2_1(a343) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1060,plain,
( ~ c2_1(a343)
| spl0_147 ),
inference(avatar_component_clause,[],[f1058]) ).
fof(f1061,plain,
( ~ spl0_147
| spl0_44 ),
inference(avatar_split_clause,[],[f224,f524,f1058]) ).
fof(f1063,definition,
( spl0_148
<=> c1_1(a343) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1066,plain,
( spl0_148
| spl0_44 ),
inference(avatar_split_clause,[],[f223,f524,f1063]) ).
fof(f1068,definition,
( spl0_149
<=> c0_1(a343) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1071,plain,
( spl0_149
| spl0_44 ),
inference(avatar_split_clause,[],[f222,f524,f1068]) ).
fof(f1095,plain,
( spl0_3
| spl0_56 ),
inference(avatar_split_clause,[],[f205,f587,f357]) ).
fof(f1104,plain,
( spl0_3
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f6,f849,f357]) ).
fof(f1108,plain,
( spl0_35
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f198,f592,f484]) ).
fof(f1109,plain,
( ~ spl0_56
| spl0_105 ),
inference(avatar_split_clause,[],[f197,f849,f587]) ).
fof(f1131,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_2 ),
inference(resolution,[],[f355,f352]) ).
fof(f1132,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_2 ),
inference(duplicate_literal_removal,[],[f1131]) ).
fof(f1133,plain,
( ~ c0_1(a325)
| ~ spl0_1
| ~ spl0_2
| ~ spl0_69 ),
inference(resolution,[],[f1132,f671]) ).
fof(f1135,plain,
( ~ c0_1(a419)
| ~ spl0_1
| ~ spl0_2
| ~ spl0_106 ),
inference(resolution,[],[f1132,f855]) ).
fof(f1136,plain,
( ~ spl0_140
| ~ spl0_1
| ~ spl0_2
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f1135,f853,f354,f351,f1023]) ).
fof(f1137,plain,
( ~ spl0_111
| ~ spl0_1
| ~ spl0_2
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1133,f669,f354,f351,f878]) ).
fof(f1140,plain,
( ~ c0_1(a343)
| ~ c1_1(a343)
| ~ spl0_7
| spl0_147 ),
inference(resolution,[],[f372,f1060]) ).
fof(f1141,plain,
( ~ c0_1(a341)
| ~ c1_1(a341)
| ~ spl0_7
| spl0_145 ),
inference(resolution,[],[f372,f1050]) ).
fof(f1160,plain,
( ~ spl0_148
| ~ spl0_149
| ~ spl0_7
| spl0_147 ),
inference(avatar_split_clause,[],[f1140,f1058,f371,f1068,f1063]) ).
fof(f1161,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f352,f369]) ).
fof(f1184,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_6 ),
inference(duplicate_literal_removal,[],[f1161]) ).
fof(f1188,plain,
( ~ c1_1(a332)
| c0_1(a332)
| ~ spl0_8
| ~ spl0_77 ),
inference(resolution,[],[f376,f711]) ).
fof(f1191,definition,
( spl0_150
<=> c1_1(a332) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1194,plain,
( spl0_78
| ~ spl0_150
| ~ spl0_8
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f1188,f709,f375,f1191,f714]) ).
fof(f1196,plain,
( ~ c0_1(a419)
| c1_1(a419)
| ~ spl0_11
| ~ spl0_106 ),
inference(resolution,[],[f387,f855]) ).
fof(f1213,plain,
( c1_1(a330)
| c2_1(a330)
| ~ spl0_14
| ~ spl0_117 ),
inference(resolution,[],[f397,f910]) ).
fof(f1221,definition,
( spl0_152
<=> c2_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1222,plain,
( ~ c2_1(a330)
| spl0_152 ),
inference(avatar_component_clause,[],[f1221]) ).
fof(f1249,definition,
( spl0_153
<=> c1_1(a337) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1254,definition,
( spl0_154
<=> c1_1(a345) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f1259,definition,
( spl0_155
<=> c1_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1269,definition,
( spl0_157
<=> c1_1(a359) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1324,definition,
( spl0_164
<=> c0_1(a341) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1330,plain,
( ~ c2_1(a333)
| ~ c1_1(a333)
| ~ spl0_6
| ~ spl0_141 ),
inference(resolution,[],[f1030,f369]) ).
fof(f1331,plain,
( ~ c0_1(a333)
| c2_1(a333)
| ~ spl0_4
| ~ spl0_141 ),
inference(resolution,[],[f1030,f362]) ).
fof(f1333,definition,
( spl0_165
<=> c2_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1334,plain,
( ~ c2_1(a333)
| spl0_165 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1336,plain,
( spl0_165
| ~ spl0_143
| ~ spl0_4
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f1331,f1028,f361,f1038,f1333]) ).
fof(f1344,plain,
( ~ c0_1(a333)
| ~ c1_1(a333)
| ~ spl0_7
| spl0_165 ),
inference(resolution,[],[f1334,f372]) ).
fof(f1345,plain,
( ~ spl0_142
| ~ spl0_143
| ~ spl0_7
| spl0_165 ),
inference(avatar_split_clause,[],[f1344,f1333,f371,f1038,f1033]) ).
fof(f1362,plain,
( c0_1(a341)
| ~ c1_1(a341)
| ~ spl0_10
| ~ spl0_144 ),
inference(resolution,[],[f384,f1045]) ).
fof(f1388,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_15
| ~ spl0_18 ),
inference(resolution,[],[f411,f401]) ).
fof(f1390,plain,
( ~ c2_1(a367)
| c0_1(a367)
| ~ spl0_18
| ~ spl0_136 ),
inference(resolution,[],[f411,f1005]) ).
fof(f1391,plain,
( ~ c2_1(a330)
| c0_1(a330)
| ~ spl0_18
| ~ spl0_117 ),
inference(resolution,[],[f411,f910]) ).
fof(f1393,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_15
| ~ spl0_18 ),
inference(duplicate_literal_removal,[],[f1388]) ).
fof(f1396,definition,
( spl0_167
<=> c0_1(a367) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1399,plain,
( spl0_167
| ~ spl0_100
| ~ spl0_18
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1390,f1003,f410,f824,f1396]) ).
fof(f1404,plain,
( c1_1(a367)
| ~ c0_1(a367)
| ~ spl0_13
| ~ spl0_136 ),
inference(resolution,[],[f394,f1005]) ).
fof(f1415,plain,
( ~ spl0_146
| ~ spl0_164
| ~ spl0_7
| spl0_145 ),
inference(avatar_split_clause,[],[f1141,f1048,f371,f1324,f1053]) ).
fof(f1418,plain,
( ~ c2_1(a345)
| ~ c1_1(a345)
| ~ spl0_6
| ~ spl0_120 ),
inference(resolution,[],[f925,f369]) ).
fof(f1432,plain,
( ~ c2_1(a345)
| ~ c0_1(a345)
| ~ spl0_2
| ~ spl0_120 ),
inference(resolution,[],[f355,f925]) ).
fof(f1435,plain,
( ~ spl0_121
| ~ spl0_86
| ~ spl0_2
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1432,f923,f354,f754,f928]) ).
fof(f1450,plain,
( ~ c2_1(a349)
| ~ c1_1(a349)
| ~ spl0_6
| ~ spl0_127 ),
inference(resolution,[],[f960,f369]) ).
fof(f1459,plain,
( spl0_8
| ~ spl0_15
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f1393,f410,f400,f375]) ).
fof(f1477,plain,
( ~ c0_1(a337)
| ~ c2_1(a337)
| ~ spl0_1
| spl0_81 ),
inference(resolution,[],[f352,f731]) ).
fof(f1497,plain,
( ~ c1_1(a401)
| c0_1(a401)
| ~ spl0_8
| ~ spl0_103 ),
inference(resolution,[],[f376,f841]) ).
fof(f1505,plain,
( spl0_104
| ~ spl0_139
| ~ spl0_8
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f1497,f839,f375,f1018,f844]) ).
fof(f1506,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_4
| ~ spl0_9 ),
inference(resolution,[],[f379,f362]) ).
fof(f1517,plain,
( ~ c1_1(a346)
| c2_1(a346)
| ~ spl0_9
| spl0_87 ),
inference(resolution,[],[f379,f761]) ).
fof(f1524,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_9 ),
inference(duplicate_literal_removal,[],[f1506]) ).
fof(f1539,plain,
( c1_1(a330)
| c0_1(a330)
| ~ spl0_12
| spl0_152 ),
inference(resolution,[],[f391,f1222]) ).
fof(f1550,plain,
( spl0_75
| spl0_74
| ~ spl0_12
| spl0_152 ),
inference(avatar_split_clause,[],[f1539,f1221,f390,f694,f699]) ).
fof(f1559,plain,
( spl0_152
| spl0_74
| ~ spl0_14
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1213,f908,f396,f694,f1221]) ).
fof(f1565,plain,
( spl0_7
| ~ spl0_4
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1524,f378,f361,f371]) ).
fof(f1586,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_20 ),
inference(resolution,[],[f420,f352]) ).
fof(f1597,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f1586]) ).
fof(f1600,plain,
( ~ c1_1(a341)
| c2_1(a341)
| ~ spl0_21
| ~ spl0_144 ),
inference(resolution,[],[f423,f1045]) ).
fof(f1622,plain,
( ~ c0_1(a337)
| ~ c1_1(a337)
| ~ spl0_23
| ~ spl0_82 ),
inference(resolution,[],[f431,f736]) ).
fof(f1626,plain,
( ~ c0_1(a325)
| ~ c1_1(a325)
| ~ spl0_23
| ~ spl0_69 ),
inference(resolution,[],[f431,f671]) ).
fof(f1629,plain,
( ~ spl0_110
| ~ spl0_111
| ~ spl0_23
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1626,f669,f430,f878,f873]) ).
fof(f1633,plain,
( ~ spl0_82
| ~ spl0_119
| ~ spl0_1
| spl0_81 ),
inference(avatar_split_clause,[],[f1477,f729,f351,f918,f734]) ).
fof(f1647,plain,
( spl0_145
| ~ spl0_146
| ~ spl0_21
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1600,f1043,f422,f1053,f1048]) ).
fof(f1701,plain,
( c1_1(a326)
| ~ c0_1(a326)
| ~ spl0_16
| spl0_112 ),
inference(resolution,[],[f404,f885]) ).
fof(f1716,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_21
| ~ spl0_27 ),
inference(resolution,[],[f449,f423]) ).
fof(f1719,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_4
| ~ spl0_27 ),
inference(resolution,[],[f449,f362]) ).
fof(f1730,plain,
( ~ c0_1(a327)
| ~ c1_1(a327)
| ~ spl0_27
| spl0_71 ),
inference(resolution,[],[f449,f681]) ).
fof(f1736,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_4
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f1719]) ).
fof(f1738,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_21
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f1716]) ).
fof(f1740,plain,
( ~ spl0_114
| ~ spl0_115
| ~ spl0_27
| spl0_71 ),
inference(avatar_split_clause,[],[f1730,f679,f448,f898,f893]) ).
fof(f1747,plain,
( spl0_7
| ~ spl0_4
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1736,f448,f361,f371]) ).
fof(f1759,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_21
| ~ spl0_33 ),
inference(resolution,[],[f476,f423]) ).
fof(f1771,plain,
( ~ c0_1(a346)
| c2_1(a346)
| ~ spl0_33
| spl0_87 ),
inference(resolution,[],[f476,f761]) ).
fof(f1781,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_21
| ~ spl0_33 ),
inference(duplicate_literal_removal,[],[f1759]) ).
fof(f1791,plain,
( ~ spl0_146
| spl0_164
| ~ spl0_10
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1362,f1043,f383,f1324,f1053]) ).
fof(f1795,plain,
( ~ spl0_167
| spl0_101
| ~ spl0_13
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1404,f1003,f393,f829,f1396]) ).
fof(f1802,plain,
( spl0_23
| ~ spl0_1
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1597,f419,f351,f430]) ).
fof(f1865,plain,
( ~ c2_1(a367)
| c1_1(a367)
| ~ spl0_5
| ~ spl0_136 ),
inference(resolution,[],[f366,f1005]) ).
fof(f1874,plain,
( ~ c2_1(a330)
| c1_1(a330)
| ~ spl0_5
| ~ spl0_117 ),
inference(resolution,[],[f366,f910]) ).
fof(f1882,plain,
( spl0_101
| ~ spl0_100
| ~ spl0_5
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1865,f1003,f365,f824,f829]) ).
fof(f1887,plain,
( spl0_75
| ~ spl0_152
| ~ spl0_18
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1391,f908,f410,f1221,f699]) ).
fof(f1897,plain,
( spl0_7
| ~ spl0_21
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1738,f448,f422,f371]) ).
fof(f1899,plain,
( spl0_122
| ~ spl0_123
| ~ spl0_33
| spl0_87 ),
inference(avatar_split_clause,[],[f1771,f759,f475,f938,f933]) ).
fof(f1901,plain,
( spl0_7
| ~ spl0_21
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1781,f475,f422,f371]) ).
fof(f1904,plain,
( spl0_23
| ~ spl0_1
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1184,f368,f351,f430]) ).
fof(f1905,plain,
( ~ spl0_142
| ~ spl0_165
| ~ spl0_6
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f1330,f1028,f368,f1333,f1033]) ).
fof(f1906,plain,
( ~ spl0_154
| ~ spl0_86
| ~ spl0_6
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1418,f923,f368,f754,f1254]) ).
fof(f1907,plain,
( ~ spl0_128
| ~ spl0_91
| ~ spl0_6
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1450,f958,f368,f779,f963]) ).
fof(f1927,plain,
( spl0_74
| ~ spl0_152
| ~ spl0_5
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1874,f908,f365,f1221,f694]) ).
fof(f1928,plain,
( spl0_107
| ~ spl0_140
| ~ spl0_11
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f1196,f853,f386,f1023,f858]) ).
fof(f1943,plain,
( ~ c2_1(a359)
| c1_1(a359)
| ~ spl0_5
| ~ spl0_135 ),
inference(resolution,[],[f366,f1000]) ).
fof(f1967,plain,
( ~ c0_1(a345)
| c1_1(a345)
| ~ spl0_11
| ~ spl0_86 ),
inference(resolution,[],[f387,f756]) ).
fof(f2035,plain,
( ~ c1_1(a359)
| c0_1(a359)
| ~ spl0_8
| ~ spl0_98 ),
inference(resolution,[],[f816,f376]) ).
fof(f2050,plain,
( c1_1(a330)
| c0_1(a330)
| ~ spl0_36
| ~ spl0_117 ),
inference(resolution,[],[f489,f910]) ).
fof(f2052,plain,
( spl0_75
| spl0_74
| ~ spl0_36
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f2050,f908,f488,f694,f699]) ).
fof(f2065,plain,
( c2_1(a329)
| c1_1(a329)
| ~ spl0_37
| spl0_72 ),
inference(resolution,[],[f494,f686]) ).
fof(f2157,plain,
( c0_1(a324)
| c1_1(a324)
| ~ spl0_45
| spl0_66 ),
inference(resolution,[],[f533,f656]) ).
fof(f2176,plain,
( ~ c0_1(a348)
| c1_1(a348)
| ~ spl0_46
| spl0_89 ),
inference(resolution,[],[f538,f771]) ).
fof(f2177,plain,
( ~ c0_1(a346)
| c1_1(a346)
| ~ spl0_46
| spl0_87 ),
inference(resolution,[],[f538,f761]) ).
fof(f2178,plain,
( ~ c0_1(a337)
| c1_1(a337)
| ~ spl0_46
| spl0_81 ),
inference(resolution,[],[f538,f731]) ).
fof(f2200,plain,
( c1_1(a337)
| ~ c2_1(a337)
| ~ spl0_48
| spl0_81 ),
inference(resolution,[],[f546,f731]) ).
fof(f2204,plain,
( c1_1(a332)
| ~ c2_1(a332)
| ~ spl0_48
| spl0_76 ),
inference(resolution,[],[f546,f706]) ).
fof(f2206,plain,
( c1_1(a323)
| ~ c2_1(a323)
| ~ spl0_48
| spl0_63 ),
inference(resolution,[],[f546,f641]) ).
fof(f2210,plain,
( ~ spl0_64
| spl0_65
| ~ spl0_48
| spl0_63 ),
inference(avatar_split_clause,[],[f2206,f639,f545,f649,f644]) ).
fof(f2211,plain,
( ~ spl0_77
| spl0_150
| ~ spl0_48
| spl0_76 ),
inference(avatar_split_clause,[],[f2204,f704,f545,f1191,f709]) ).
fof(f2213,plain,
( ~ spl0_82
| spl0_153
| ~ spl0_48
| spl0_81 ),
inference(avatar_split_clause,[],[f2200,f729,f545,f1249,f734]) ).
fof(f2215,plain,
( spl0_99
| ~ spl0_157
| ~ spl0_8
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f2035,f814,f375,f1269,f819]) ).
fof(f2220,plain,
( spl0_122
| ~ spl0_155
| ~ spl0_9
| spl0_87 ),
inference(avatar_split_clause,[],[f1517,f759,f378,f1259,f933]) ).
fof(f2233,plain,
( ~ spl0_113
| spl0_70
| ~ spl0_16
| spl0_112 ),
inference(avatar_split_clause,[],[f1701,f883,f403,f674,f888]) ).
fof(f2238,plain,
( ~ spl0_153
| ~ spl0_119
| ~ spl0_23
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1622,f734,f430,f918,f1249]) ).
fof(f2244,plain,
( spl0_73
| spl0_116
| ~ spl0_37
| spl0_72 ),
inference(avatar_split_clause,[],[f2065,f684,f493,f903,f689]) ).
fof(f2253,plain,
( spl0_67
| spl0_68
| ~ spl0_45
| spl0_66 ),
inference(avatar_split_clause,[],[f2157,f654,f532,f664,f659]) ).
fof(f2256,plain,
( spl0_90
| ~ spl0_126
| ~ spl0_46
| spl0_89 ),
inference(avatar_split_clause,[],[f2176,f769,f537,f953,f774]) ).
fof(f2257,plain,
( spl0_155
| ~ spl0_123
| ~ spl0_46
| spl0_87 ),
inference(avatar_split_clause,[],[f2177,f759,f537,f938,f1259]) ).
fof(f2258,plain,
( spl0_153
| ~ spl0_119
| ~ spl0_46
| spl0_81 ),
inference(avatar_split_clause,[],[f2178,f729,f537,f918,f1249]) ).
fof(f2263,plain,
( spl0_157
| ~ spl0_98
| ~ spl0_5
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1943,f998,f365,f814,f1269]) ).
fof(f2265,plain,
( spl0_154
| ~ spl0_121
| ~ spl0_11
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f1967,f754,f386,f928,f1254]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f363]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f373]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f380]) ).
cnf(s4,plain,
( spl0_2
| ~ spl0_3
| spl0_4
| spl0_8 ),
inference(sat_conversion,[],[f381]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f398]) ).
cnf(s9,plain,
( spl0_1
| ~ spl0_3
| spl0_8
| spl0_16 ),
inference(sat_conversion,[],[f413]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_19
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f424]) ).
cnf(s12,plain,
( ~ spl0_3
| spl0_14
| spl0_21
| spl0_24 ),
inference(sat_conversion,[],[f437]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_23
| spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f450]) ).
cnf(s15,plain,
( spl0_1
| ~ spl0_3
| spl0_7
| spl0_19 ),
inference(sat_conversion,[],[f451]) ).
cnf(s20,plain,
( ~ spl0_3
| spl0_10
| spl0_16
| ~ spl0_34 ),
inference(sat_conversion,[],[f482]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_16
| spl0_37
| ~ spl0_38 ),
inference(sat_conversion,[],[f500]) ).
cnf(s28,plain,
( spl0_2
| ~ spl0_3
| spl0_15
| ~ spl0_43 ),
inference(sat_conversion,[],[f522]) ).
cnf(s29,plain,
( spl0_2
| ~ spl0_3
| spl0_18
| ~ spl0_44 ),
inference(sat_conversion,[],[f527]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_8
| spl0_9
| ~ spl0_31 ),
inference(sat_conversion,[],[f528]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_25
| spl0_45 ),
inference(sat_conversion,[],[f535]) ).
cnf(s35,plain,
( spl0_1
| ~ spl0_3
| spl0_24
| spl0_46 ),
inference(sat_conversion,[],[f539]) ).
cnf(s36,plain,
( ~ spl0_3
| spl0_27
| ~ spl0_47
| spl0_48 ),
inference(sat_conversion,[],[f547]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_11
| spl0_36
| ~ spl0_43 ),
inference(sat_conversion,[],[f565]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_34
| spl0_48 ),
inference(sat_conversion,[],[f566]) ).
cnf(s47,plain,
( ~ spl0_3
| spl0_19
| spl0_21
| ~ spl0_55 ),
inference(sat_conversion,[],[f585]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_33
| ~ spl0_39
| spl0_53 ),
inference(sat_conversion,[],[f597]) ).
cnf(s52,plain,
( ~ spl0_3
| ~ spl0_31
| spl0_33
| ~ spl0_56 ),
inference(sat_conversion,[],[f598]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_19
| spl0_33
| ~ spl0_55 ),
inference(sat_conversion,[],[f599]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_23
| ~ spl0_34
| ~ spl0_58 ),
inference(sat_conversion,[],[f604]) ).
cnf(s60,plain,
( ~ spl0_3
| spl0_6
| ~ spl0_44 ),
inference(sat_conversion,[],[f618]) ).
cnf(s62,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_44
| ~ spl0_49 ),
inference(sat_conversion,[],[f620]) ).
cnf(s63,plain,
( ~ spl0_3
| spl0_14
| spl0_40 ),
inference(sat_conversion,[],[f621]) ).
cnf(s64,plain,
( ~ spl0_3
| spl0_11
| spl0_24
| spl0_35 ),
inference(sat_conversion,[],[f622]) ).
cnf(s73,plain,
( ~ spl0_53
| ~ spl0_63 ),
inference(sat_conversion,[],[f642]) ).
cnf(s74,plain,
( ~ spl0_53
| spl0_64 ),
inference(sat_conversion,[],[f647]) ).
cnf(s75,plain,
( ~ spl0_53
| ~ spl0_65 ),
inference(sat_conversion,[],[f652]) ).
cnf(s76,plain,
( spl0_39
| ~ spl0_66 ),
inference(sat_conversion,[],[f657]) ).
cnf(s77,plain,
( spl0_39
| ~ spl0_67 ),
inference(sat_conversion,[],[f662]) ).
cnf(s78,plain,
( spl0_39
| ~ spl0_68 ),
inference(sat_conversion,[],[f667]) ).
cnf(s79,plain,
( spl0_55
| spl0_69 ),
inference(sat_conversion,[],[f672]) ).
cnf(s80,plain,
( spl0_31
| ~ spl0_70 ),
inference(sat_conversion,[],[f677]) ).
cnf(s81,plain,
( spl0_38
| ~ spl0_71 ),
inference(sat_conversion,[],[f682]) ).
cnf(s82,plain,
( spl0_25
| ~ spl0_72 ),
inference(sat_conversion,[],[f687]) ).
cnf(s83,plain,
( spl0_25
| ~ spl0_73 ),
inference(sat_conversion,[],[f692]) ).
cnf(s84,plain,
( ~ spl0_35
| ~ spl0_74 ),
inference(sat_conversion,[],[f697]) ).
cnf(s85,plain,
( ~ spl0_35
| ~ spl0_75 ),
inference(sat_conversion,[],[f702]) ).
cnf(s86,plain,
( ~ spl0_26
| ~ spl0_76 ),
inference(sat_conversion,[],[f707]) ).
cnf(s87,plain,
( ~ spl0_26
| spl0_77 ),
inference(sat_conversion,[],[f712]) ).
cnf(s88,plain,
( ~ spl0_26
| ~ spl0_78 ),
inference(sat_conversion,[],[f717]) ).
cnf(s91,plain,
( ~ spl0_19
| ~ spl0_81 ),
inference(sat_conversion,[],[f732]) ).
cnf(s92,plain,
( ~ spl0_19
| spl0_82 ),
inference(sat_conversion,[],[f737]) ).
cnf(s96,plain,
( spl0_34
| spl0_86 ),
inference(sat_conversion,[],[f757]) ).
cnf(s97,plain,
( spl0_58
| ~ spl0_87 ),
inference(sat_conversion,[],[f762]) ).
cnf(s99,plain,
( ~ spl0_40
| ~ spl0_89 ),
inference(sat_conversion,[],[f772]) ).
cnf(s100,plain,
( ~ spl0_40
| ~ spl0_90 ),
inference(sat_conversion,[],[f777]) ).
cnf(s101,plain,
( spl0_56
| spl0_91 ),
inference(sat_conversion,[],[f782]) ).
cnf(s108,plain,
( spl0_47
| spl0_98 ),
inference(sat_conversion,[],[f817]) ).
cnf(s109,plain,
( spl0_47
| ~ spl0_99 ),
inference(sat_conversion,[],[f822]) ).
cnf(s110,plain,
( ~ spl0_24
| spl0_100 ),
inference(sat_conversion,[],[f827]) ).
cnf(s111,plain,
( ~ spl0_24
| ~ spl0_101 ),
inference(sat_conversion,[],[f832]) ).
cnf(s113,plain,
( spl0_57
| spl0_103 ),
inference(sat_conversion,[],[f842]) ).
cnf(s114,plain,
( spl0_57
| ~ spl0_104 ),
inference(sat_conversion,[],[f847]) ).
cnf(s115,plain,
( ~ spl0_105
| spl0_106 ),
inference(sat_conversion,[],[f856]) ).
cnf(s116,plain,
( ~ spl0_105
| ~ spl0_107 ),
inference(sat_conversion,[],[f861]) ).
cnf(s119,plain,
( spl0_55
| spl0_110 ),
inference(sat_conversion,[],[f876]) ).
cnf(s120,plain,
( spl0_55
| spl0_111 ),
inference(sat_conversion,[],[f881]) ).
cnf(s121,plain,
( spl0_31
| ~ spl0_112 ),
inference(sat_conversion,[],[f886]) ).
cnf(s122,plain,
( spl0_31
| spl0_113 ),
inference(sat_conversion,[],[f891]) ).
cnf(s123,plain,
( spl0_38
| spl0_114 ),
inference(sat_conversion,[],[f896]) ).
cnf(s124,plain,
( spl0_38
| spl0_115 ),
inference(sat_conversion,[],[f901]) ).
cnf(s125,plain,
( spl0_25
| ~ spl0_116 ),
inference(sat_conversion,[],[f906]) ).
cnf(s126,plain,
( ~ spl0_35
| spl0_117 ),
inference(sat_conversion,[],[f911]) ).
cnf(s128,plain,
( ~ spl0_19
| spl0_119 ),
inference(sat_conversion,[],[f921]) ).
cnf(s129,plain,
( spl0_34
| spl0_120 ),
inference(sat_conversion,[],[f926]) ).
cnf(s130,plain,
( spl0_34
| spl0_121 ),
inference(sat_conversion,[],[f931]) ).
cnf(s131,plain,
( spl0_58
| ~ spl0_122 ),
inference(sat_conversion,[],[f936]) ).
cnf(s132,plain,
( spl0_58
| spl0_123 ),
inference(sat_conversion,[],[f941]) ).
cnf(s135,plain,
( ~ spl0_40
| spl0_126 ),
inference(sat_conversion,[],[f956]) ).
cnf(s136,plain,
( spl0_56
| spl0_127 ),
inference(sat_conversion,[],[f961]) ).
cnf(s137,plain,
( spl0_56
| spl0_128 ),
inference(sat_conversion,[],[f966]) ).
cnf(s144,plain,
( spl0_47
| spl0_135 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s145,plain,
( ~ spl0_24
| spl0_136 ),
inference(sat_conversion,[],[f1006]) ).
cnf(s148,plain,
( spl0_57
| spl0_139 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s149,plain,
( ~ spl0_105
| spl0_140 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s150,plain,
( spl0_43
| spl0_141 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s151,plain,
( spl0_43
| spl0_142 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s152,plain,
( spl0_43
| spl0_143 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s153,plain,
( spl0_49
| spl0_144 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s154,plain,
( spl0_49
| ~ spl0_145 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s155,plain,
( spl0_49
| spl0_146 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s156,plain,
( spl0_44
| ~ spl0_147 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s157,plain,
( spl0_44
| spl0_148 ),
inference(sat_conversion,[],[f1066]) ).
cnf(s158,plain,
( spl0_44
| spl0_149 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s182,plain,
( spl0_3
| spl0_56 ),
inference(sat_conversion,[],[f1095]) ).
cnf(s191,plain,
( spl0_3
| ~ spl0_105 ),
inference(sat_conversion,[],[f1104]) ).
cnf(s195,plain,
( spl0_35
| ~ spl0_57 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s196,plain,
( ~ spl0_56
| spl0_105 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s197,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_106
| ~ spl0_140 ),
inference(sat_conversion,[],[f1136]) ).
cnf(s198,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_69
| ~ spl0_111 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s199,plain,
( ~ spl0_7
| spl0_147
| ~ spl0_148
| ~ spl0_149 ),
inference(sat_conversion,[],[f1160]) ).
cnf(s200,plain,
( ~ spl0_8
| ~ spl0_77
| spl0_78
| ~ spl0_150 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s218,plain,
( ~ spl0_4
| ~ spl0_141
| ~ spl0_143
| spl0_165 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s222,plain,
( ~ spl0_7
| ~ spl0_142
| ~ spl0_143
| spl0_165 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s229,plain,
( ~ spl0_18
| ~ spl0_100
| ~ spl0_136
| spl0_167 ),
inference(sat_conversion,[],[f1399]) ).
cnf(s236,plain,
( ~ spl0_7
| spl0_145
| ~ spl0_146
| ~ spl0_164 ),
inference(sat_conversion,[],[f1415]) ).
cnf(s239,plain,
( ~ spl0_2
| ~ spl0_86
| ~ spl0_120
| ~ spl0_121 ),
inference(sat_conversion,[],[f1435]) ).
cnf(s254,plain,
( spl0_8
| ~ spl0_15
| ~ spl0_18 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s256,plain,
( ~ spl0_8
| ~ spl0_103
| spl0_104
| ~ spl0_139 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s261,plain,
( ~ spl0_12
| spl0_74
| spl0_75
| spl0_152 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s270,plain,
( ~ spl0_14
| spl0_74
| ~ spl0_117
| spl0_152 ),
inference(sat_conversion,[],[f1559]) ).
cnf(s276,plain,
( ~ spl0_4
| spl0_7
| ~ spl0_9 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s281,plain,
( ~ spl0_23
| ~ spl0_69
| ~ spl0_110
| ~ spl0_111 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s285,plain,
( ~ spl0_1
| spl0_81
| ~ spl0_82
| ~ spl0_119 ),
inference(sat_conversion,[],[f1633]) ).
cnf(s299,plain,
( ~ spl0_21
| ~ spl0_144
| spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s320,plain,
( ~ spl0_27
| spl0_71
| ~ spl0_114
| ~ spl0_115 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s327,plain,
( ~ spl0_4
| spl0_7
| ~ spl0_27 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s336,plain,
( ~ spl0_10
| ~ spl0_144
| ~ spl0_146
| spl0_164 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s340,plain,
( ~ spl0_13
| spl0_101
| ~ spl0_136
| ~ spl0_167 ),
inference(sat_conversion,[],[f1795]) ).
cnf(s347,plain,
( ~ spl0_1
| ~ spl0_20
| spl0_23 ),
inference(sat_conversion,[],[f1802]) ).
cnf(s363,plain,
( ~ spl0_5
| ~ spl0_100
| spl0_101
| ~ spl0_136 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s369,plain,
( ~ spl0_18
| spl0_75
| ~ spl0_117
| ~ spl0_152 ),
inference(sat_conversion,[],[f1887]) ).
cnf(s379,plain,
( spl0_7
| ~ spl0_21
| ~ spl0_27 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s381,plain,
( ~ spl0_33
| spl0_87
| spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f1899]) ).
cnf(s383,plain,
( spl0_7
| ~ spl0_21
| ~ spl0_33 ),
inference(sat_conversion,[],[f1901]) ).
cnf(s386,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_23 ),
inference(sat_conversion,[],[f1904]) ).
cnf(s388,plain,
( ~ spl0_6
| ~ spl0_141
| ~ spl0_142
| ~ spl0_165 ),
inference(sat_conversion,[],[f1905]) ).
cnf(s389,plain,
( ~ spl0_6
| ~ spl0_86
| ~ spl0_120
| ~ spl0_154 ),
inference(sat_conversion,[],[f1906]) ).
cnf(s390,plain,
( ~ spl0_6
| ~ spl0_91
| ~ spl0_127
| ~ spl0_128 ),
inference(sat_conversion,[],[f1907]) ).
cnf(s411,plain,
( ~ spl0_5
| spl0_74
| ~ spl0_117
| ~ spl0_152 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s412,plain,
( ~ spl0_11
| ~ spl0_106
| spl0_107
| ~ spl0_140 ),
inference(sat_conversion,[],[f1928]) ).
cnf(s423,plain,
( ~ spl0_36
| spl0_74
| spl0_75
| ~ spl0_117 ),
inference(sat_conversion,[],[f2052]) ).
cnf(s447,plain,
( ~ spl0_48
| spl0_63
| ~ spl0_64
| spl0_65 ),
inference(sat_conversion,[],[f2210]) ).
cnf(s448,plain,
( ~ spl0_48
| spl0_76
| ~ spl0_77
| spl0_150 ),
inference(sat_conversion,[],[f2211]) ).
cnf(s450,plain,
( ~ spl0_48
| spl0_81
| ~ spl0_82
| spl0_153 ),
inference(sat_conversion,[],[f2213]) ).
cnf(s452,plain,
( ~ spl0_8
| ~ spl0_98
| spl0_99
| ~ spl0_157 ),
inference(sat_conversion,[],[f2215]) ).
cnf(s457,plain,
( ~ spl0_9
| spl0_87
| spl0_122
| ~ spl0_155 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s470,plain,
( ~ spl0_16
| spl0_70
| spl0_112
| ~ spl0_113 ),
inference(sat_conversion,[],[f2233]) ).
cnf(s475,plain,
( ~ spl0_23
| ~ spl0_82
| ~ spl0_119
| ~ spl0_153 ),
inference(sat_conversion,[],[f2238]) ).
cnf(s481,plain,
( ~ spl0_37
| spl0_72
| spl0_73
| spl0_116 ),
inference(sat_conversion,[],[f2244]) ).
cnf(s490,plain,
( ~ spl0_45
| spl0_66
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s493,plain,
( ~ spl0_46
| spl0_89
| spl0_90
| ~ spl0_126 ),
inference(sat_conversion,[],[f2256]) ).
cnf(s494,plain,
( ~ spl0_46
| spl0_87
| ~ spl0_123
| spl0_155 ),
inference(sat_conversion,[],[f2257]) ).
cnf(s495,plain,
( ~ spl0_46
| spl0_81
| ~ spl0_119
| spl0_153 ),
inference(sat_conversion,[],[f2258]) ).
cnf(s500,plain,
( ~ spl0_5
| ~ spl0_98
| ~ spl0_135
| spl0_157 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s502,plain,
( ~ spl0_11
| ~ spl0_86
| ~ spl0_121
| spl0_154 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s508,plain,
spl0_3,
inference(rat,[],[s196,s182,s191]) ).
cnf(s509,plain,
( spl0_6
| spl0_5 ),
inference(rat,[],[s199,s156,s157,s158,s2,s60,s508]) ).
cnf(s510,plain,
( spl0_44
| ~ spl0_7 ),
inference(rat,[],[s199,s156,s157,s158]) ).
cnf(s511,plain,
( spl0_43
| ~ spl0_7
| ~ spl0_6 ),
inference(rat,[],[s388,s222,s150,s151,s152]) ).
cnf(s512,plain,
( ~ spl0_35
| spl0_21
| ~ spl0_18 ),
inference(rat,[],[s229,s340,s110,s111,s145,s6,s12,s261,s270,s369,s84,s85,s126,s508]) ).
cnf(s513,plain,
( ~ spl0_7
| ~ spl0_6
| spl0_2
| spl0_1 ),
inference(rat,[],[s256,s113,s114,s148,s195,s512,s254,s28,s511,s299,s153,s154,s155,s29,s62,s510,s508]) ).
cnf(s515,plain,
( spl0_57
| ~ spl0_8 ),
inference(rat,[],[s256,s113,s114,s148]) ).
cnf(s516,plain,
( spl0_43
| ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s388,s218,s150,s151,s152]) ).
cnf(s517,plain,
( spl0_34
| ~ spl0_11
| ~ spl0_6 ),
inference(rat,[],[s389,s502,s96,s129,s130]) ).
cnf(s518,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s448,s200,s86,s87,s88,s14,s475,s450,s43,s517,s42,s516,s423,s84,s85,s126,s195,s515,s91,s92,s128,s3,s15,s276,s327,s513,s509,s1,s508]) ).
cnf(s519,plain,
( ~ spl0_24
| ~ spl0_5 ),
inference(rat,[],[s363,s110,s111,s145]) ).
cnf(s520,plain,
( ~ spl0_40
| ~ spl0_46 ),
inference(rat,[],[s493,s99,s100,s135]) ).
cnf(s521,plain,
( ~ spl0_35
| ~ spl0_14
| ~ spl0_5 ),
inference(rat,[],[s270,s411,s84,s126]) ).
cnf(s522,plain,
( spl0_7
| spl0_8
| ~ spl0_4 ),
inference(rat,[],[s3,s276,s508]) ).
cnf(s523,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s60,s513,s510,s522,s515,s195,s521,s63,s520,s35,s519,s518,s1,s508]) ).
cnf(s526,plain,
( ~ spl0_26
| ~ spl0_48
| ~ spl0_8 ),
inference(rat,[],[s86,s448,s200,s87,s88]) ).
cnf(s528,plain,
( spl0_39
| ~ spl0_45 ),
inference(rat,[],[s490,s76,s77,s78]) ).
cnf(s529,plain,
( ~ spl0_53
| ~ spl0_48 ),
inference(rat,[],[s447,s73,s74,s75]) ).
cnf(s531,plain,
( spl0_34
| ~ spl0_2 ),
inference(rat,[],[s239,s96,s129,s130]) ).
cnf(s532,plain,
( spl0_56
| ~ spl0_6 ),
inference(rat,[],[s390,s101,s136,s137]) ).
cnf(s533,plain,
( spl0_7
| spl0_5
| spl0_1 ),
inference(rat,[],[s14,s320,s526,s81,s123,s124,s9,s24,s470,s80,s121,s122,s52,s481,s82,s83,s125,s34,s528,s51,s381,s97,s131,s132,s54,s475,s450,s91,s92,s128,s15,s529,s43,s531,s523,s532,s509,s508]) ).
cnf(s534,plain,
( spl0_31
| ~ spl0_16 ),
inference(rat,[],[s470,s80,s121,s122]) ).
cnf(s535,plain,
( spl0_58
| ~ spl0_33 ),
inference(rat,[],[s381,s97,s131,s132]) ).
cnf(s536,plain,
( spl0_55
| ~ spl0_23 ),
inference(rat,[],[s281,s79,s119,s120]) ).
cnf(s537,plain,
( spl0_5
| spl0_1 ),
inference(rat,[],[s450,s475,s91,s92,s128,s47,s536,s54,s535,s52,s534,s20,s336,s299,s236,s153,s154,s155,s62,s510,s533,s532,s43,s509,s531,s523,s508]) ).
cnf(s538,plain,
( ~ spl0_105
| ~ spl0_11 ),
inference(rat,[],[s412,s115,s116,s149]) ).
cnf(s539,plain,
spl0_1,
inference(rat,[],[s457,s494,s97,s131,s132,s54,s475,s495,s91,s92,s128,s15,s510,s60,s532,s196,s538,s30,s534,s9,s515,s64,s195,s521,s63,s520,s35,s519,s537,s531,s523,s508]) ).
cnf(s540,plain,
~ spl0_19,
inference(rat,[],[s285,s91,s92,s128,s539]) ).
cnf(s541,plain,
~ spl0_6,
inference(rat,[],[s423,s84,s85,s126,s195,s515,s254,s42,s28,s29,s511,s510,s383,s53,s47,s197,s538,s115,s149,s196,s536,s532,s386,s508,s540,s539]) ).
cnf(s542,plain,
~ spl0_44,
inference(rat,[],[s60,s508,s541]) ).
cnf(s543,plain,
spl0_5,
inference(rat,[],[s509,s541]) ).
cnf(s547,plain,
~ spl0_7,
inference(rat,[],[s510,s542]) ).
cnf(s555,plain,
( spl0_8
| spl0_2 ),
inference(rat,[],[s522,s4,s508,s547]) ).
cnf(s557,plain,
~ spl0_55,
inference(rat,[],[s383,s53,s47,s547,s540,s508]) ).
cnf(s558,plain,
spl0_111,
inference(rat,[],[s120,s557]) ).
cnf(s560,plain,
spl0_69,
inference(rat,[],[s79,s557]) ).
cnf(s561,plain,
~ spl0_23,
inference(rat,[],[s536,s557]) ).
cnf(s562,plain,
~ spl0_2,
inference(rat,[],[s198,s558,s539,s560]) ).
cnf(s564,plain,
~ spl0_20,
inference(rat,[],[s347,s539,s561]) ).
cnf(s565,plain,
spl0_8,
inference(rat,[],[s555,s562]) ).
cnf(s569,plain,
spl0_21,
inference(rat,[],[s10,s508,s540,s564]) ).
cnf(s574,plain,
~ spl0_27,
inference(rat,[],[s379,s547,s569]) ).
cnf(s577,plain,
spl0_26,
inference(rat,[],[s14,s508,s561,s574]) ).
cnf(s588,plain,
~ spl0_48,
inference(rat,[],[s526,s565,s577]) ).
cnf(s594,plain,
~ spl0_47,
inference(rat,[],[s36,s508,s574,s588]) ).
cnf(s604,plain,
spl0_135,
inference(rat,[],[s144,s594]) ).
cnf(s605,plain,
~ spl0_99,
inference(rat,[],[s109,s594]) ).
cnf(s606,plain,
spl0_98,
inference(rat,[],[s108,s594]) ).
cnf(s614,plain,
spl0_157,
inference(rat,[],[s500,s604,s543,s606]) ).
cnf(s616,plain,
$false,
inference(rat,[],[s452,s605,s565,s614,s606]) ).
fof(f2271,plain,
$false,
inference(avatar_sat_refutation,[],[s616]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN506-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.09/0.19 % Computer : n018.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:22:40 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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.20/0.29 % (3517499)Will run a generic schedule for satisfiability detection.
% 0.20/0.29 % (3517508)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3263654117_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.29 % Detected minimum model sizes of [1]
% 0.20/0.29 % Detected maximum model sizes of [29]
% 0.20/0.29 % TRYING [1]
% 0.20/0.29 % TRYING [2]
% 0.20/0.29 % (3517509)% WARNING: option uhcvi not known.
% 0.20/0.29 % TRYING [3]
% 0.20/0.29 % TRYING [4]
% 0.20/0.29 % (3517509)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3710916390:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.29 % (3517510)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1867979676:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.29 % (3517512)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1463368752:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.29 % (3517511)dis+10_1_sil=32000:sp=arity:random_seed=1725486121:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.29 % (3517514)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4256271126:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.29 % (3517513)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3736218810:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.29 % TRYING [5]
% 0.20/0.29 % (3517514) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3517499-3517514"...
% 0.20/0.29 % TRYING [6]
% 0.20/0.29 % (3517514)...printing done.
% 0.20/0.29 % (3517514)Refutation found. Thanks to Tanya!
% 0.20/0.29 % SZS status Unsatisfiable for theBenchmark
% 0.20/0.29 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.30 % (3517514)------------------------------
% 0.20/0.30 % (3517514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (3517514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (3517514)CaDiCaL version: 2.1.3
% 0.20/0.30 % (3517514)Termination reason: Refutation
% 0.20/0.30 % (3517514)Time elapsed: 0.028 s
% 0.20/0.30 % (3517514)Peak memory usage: 13 MB
% 0.20/0.30 % (3517514)Instructions burned: 42 (million)
% 0.20/0.30 % (3517499)Success in time 0.056 s
% 0.20/0.30 % Vampire exiting
%------------------------------------------------------------------------------