%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN454-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:55 PM UTC 2026
% Result : Unsatisfiable 0.20s 0.32s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 208
% Syntax : Number of formulae : 759 ( 23 unt; 114 def)
% Number of atoms : 2370 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2816 (1205 ~;1497 |; 0 &)
% ( 114 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 140 ( 139 usr; 136 prp; 0-1 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 151 ( 0 sgn 151 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp29
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f6,negated_conjecture,
( ~ hskp24
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
fof(f19,negated_conjecture,
( ~ hskp11
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
fof(f35,negated_conjecture,
( hskp20
| hskp29
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( hskp20
| hskp3
| hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( hskp14
| hskp16
| hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( hskp14
| hskp12
| hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
( hskp14
| hskp1
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( hskp29
| hskp24
| hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
fof(f43,negated_conjecture,
( ~ hskp29
| c1_1(a165) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp29
| c2_1(a165) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp29
| c3_1(a165) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
fof(f52,negated_conjecture,
( ~ hskp26
| c0_1(a94) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp26
| c1_1(a94) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp26
| c2_1(a94) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
fof(f60,negated_conjecture,
( ~ hskp21
| c3_1(a145) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp20
| c0_1(a133) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp20
| c3_1(a133) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp19
| c0_1(a127) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp19
| c2_1(a127) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f67,negated_conjecture,
( ~ hskp16
| c1_1(a118) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp15
| c1_1(a116) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp15
| c3_1(a116) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp14
| c0_1(a115) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp13
| c0_1(a112) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp13
| c3_1(a112) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp12
| c2_1(a110) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp12
| c3_1(a110) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp11
| c2_1(a109) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp10
| c1_1(a106) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp10
| c3_1(a106) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f80,negated_conjecture,
( ~ hskp7
| c0_1(a103) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp6
| c1_1(a102) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp6
| c2_1(a102) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp5
| c3_1(a101) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f85,negated_conjecture,
( ~ hskp3
| c2_1(a99) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f87,negated_conjecture,
( ~ hskp1
| c2_1(a97) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp1
| c3_1(a97) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f96,negated_conjecture,
( ~ c0_1(a145)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c2_1(a145)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c2_1(a133)
| ~ hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c3_1(a127)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f104,negated_conjecture,
( ~ c2_1(a118)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c3_1(a118)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c0_1(a116)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c2_1(a115)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c3_1(a115)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c1_1(a112)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c0_1(a110)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c0_1(a109)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c3_1(a109)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c2_1(a106)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f115,negated_conjecture,
( ~ c0_1(a104)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c2_1(a104)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c3_1(a104)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c1_1(a103)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c3_1(a103)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c3_1(a102)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c1_1(a101)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c2_1(a101)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f125,negated_conjecture,
( ~ c1_1(a99)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c3_1(a99)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f129,negated_conjecture,
( ~ c1_1(a97)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ c1_1(a96)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( ~ c2_1(a96)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ c3_1(a96)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f135,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp13
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause135) ).
fof(f138,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp20
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause139) ).
fof(f142,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp26
| hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp14
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp16
| hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause144) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp19
| hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause147) ).
fof(f154,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp12
| hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
fof(f158,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause158) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause164) ).
fof(f166,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause166) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X1)
| c2_1(X1)
| hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause168) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause170) ).
fof(f172,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X2)
| c2_1(X2)
| c3_1(X2)
| c0_1(X1)
| c3_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X2)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| c2_1(X0)
| c2_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c0_1(X0)
| c0_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X2)
| c2_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| c2_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c1_1(X2)
| c2_1(X1)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause180) ).
fof(f181,plain,
( hskp29
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f1]) ).
fof(f184,plain,
( hskp24
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f194,plain,
( hskp11
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f204,plain,
( ~ hskp20
| ~ hskp29
| hskp0 ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f205,plain,
( ~ hskp20
| ~ hskp3
| hskp8 ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f206,plain,
( ~ hskp14
| ~ hskp16
| hskp21 ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f207,plain,
( ~ hskp14
| ~ hskp12
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f208,plain,
( ~ hskp14
| hskp1
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f209,plain,
( ~ hskp29
| ~ hskp24
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f212,plain,
( hskp29
| c1_1(a165) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f213,plain,
( hskp29
| c2_1(a165) ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f214,plain,
( hskp29
| c3_1(a165) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f225,plain,
( hskp20
| c0_1(a133) ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f226,plain,
( hskp20
| c3_1(a133) ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f229,plain,
( hskp16
| c1_1(a118) ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f230,plain,
( hskp15
| c1_1(a116) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f231,plain,
( hskp15
| c3_1(a116) ),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f232,plain,
( hskp14
| c0_1(a115) ),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f233,plain,
( hskp12
| c2_1(a110) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f234,plain,
( hskp12
| c3_1(a110) ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f235,plain,
( hskp11
| c2_1(a109) ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f236,plain,
( hskp10
| c1_1(a106) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f237,plain,
( hskp10
| c3_1(a106) ),
inference(consistent_polarity_flipping,[],[f77]) ).
fof(f240,plain,
( hskp7
| c0_1(a103) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f241,plain,
( hskp5
| c3_1(a101) ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f242,plain,
( hskp3
| c2_1(a99) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f248,plain,
( ~ c2_1(a133)
| hskp20 ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f253,plain,
( ~ c2_1(a118)
| hskp16 ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f254,plain,
( ~ c3_1(a118)
| hskp16 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f255,plain,
( ~ c0_1(a116)
| hskp15 ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f256,plain,
( ~ c2_1(a115)
| hskp14 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f257,plain,
( ~ c3_1(a115)
| hskp14 ),
inference(consistent_polarity_flipping,[],[f108]) ).
fof(f258,plain,
( ~ c0_1(a110)
| hskp12 ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f259,plain,
( ~ c0_1(a109)
| hskp11 ),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f260,plain,
( ~ c3_1(a109)
| hskp11 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f261,plain,
( ~ c2_1(a106)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f113]) ).
fof(f263,plain,
( ~ c1_1(a103)
| hskp7 ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f264,plain,
( ~ c3_1(a103)
| hskp7 ),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f265,plain,
( ~ c1_1(a101)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f121]) ).
fof(f266,plain,
( ~ c2_1(a101)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f267,plain,
( ~ c1_1(a99)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f268,plain,
( ~ c3_1(a99)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f270,plain,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp13
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f273,plain,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| ~ hskp20
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f276,plain,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp26
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f277,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ hskp14
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f278,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ hskp16
| hskp8 ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f281,plain,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp19
| ~ hskp5 ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f286,plain,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ hskp12
| hskp8 ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f288,plain,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f290,plain,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| ~ hskp7 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f291,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f292,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f293,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| ~ hskp15 ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f295,plain,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| ~ hskp5 ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f298,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f299,plain,
( ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| ~ c1_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f301,definition,
( spl0_2
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f302,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f308,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f309,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f310,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f180,f308,f304,f301,f298]) ).
fof(f312,definition,
( spl0_5
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f313,plain,
( ! [X2] :
( c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f315,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f316,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,definition,
( spl0_7
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f319,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f320,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f179,f318,f304,f315,f312]) ).
fof(f322,definition,
( spl0_8
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f323,plain,
( ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f324,plain,
( spl0_8
| spl0_1
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f178,f308,f304,f298,f322]) ).
fof(f326,definition,
( spl0_9
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f327,plain,
( ! [X2] :
( c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f329,definition,
( spl0_10
<=> ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f330,plain,
( ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f331,plain,
( spl0_9
| spl0_5
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f177,f329,f304,f312,f326]) ).
fof(f333,definition,
( spl0_11
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f334,plain,
( ! [X2] :
( c0_1(X2)
| c3_1(X2)
| ~ c1_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f335,plain,
( spl0_11
| spl0_6
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f176,f301,f304,f315,f333]) ).
fof(f337,definition,
( spl0_12
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f338,plain,
( ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f339,plain,
( spl0_12
| spl0_8
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f175,f301,f304,f322,f337]) ).
fof(f341,definition,
( spl0_13
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f342,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f344,definition,
( spl0_14
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f345,plain,
( ! [X1] :
( c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f347,definition,
( spl0_15
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f348,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f349,plain,
( spl0_13
| spl0_14
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f174,f347,f304,f344,f341]) ).
fof(f351,definition,
( spl0_16
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f352,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f354,definition,
( spl0_17
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f355,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f356,plain,
( spl0_16
| spl0_10
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f173,f354,f304,f329,f351]) ).
fof(f358,definition,
( spl0_18
<=> ! [X2] :
( c1_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f359,plain,
( ! [X2] :
( c3_1(X2)
| c1_1(X2)
| c2_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f361,definition,
( spl0_19
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f362,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( spl0_18
| spl0_9
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f172,f361,f304,f326,f358]) ).
fof(f365,definition,
( spl0_20
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f369,definition,
( spl0_21
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f370,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,definition,
( spl0_22
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f377,definition,
( spl0_23
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f378,plain,
( ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f379,plain,
( spl0_22
| spl0_23
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f170,f369,f304,f377,f373]) ).
fof(f381,definition,
( spl0_24
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f385,definition,
( spl0_25
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f386,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f391,plain,
( spl0_22
| spl0_13
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f168,f308,f304,f341,f373]) ).
fof(f397,definition,
( spl0_28
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f401,definition,
( spl0_29
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f402,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f403,plain,
( ~ spl0_28
| spl0_19
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f295,f401,f304,f361,f397]) ).
fof(f405,definition,
( spl0_30
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f410,definition,
( spl0_31
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f413,plain,
( ~ spl0_31
| spl0_12
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f293,f315,f304,f337,f410]) ).
fof(f415,definition,
( spl0_32
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f418,plain,
( ~ spl0_32
| spl0_18
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f292,f369,f304,f358,f415]) ).
fof(f420,definition,
( spl0_33
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f423,plain,
( ~ spl0_33
| spl0_10
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f291,f347,f304,f329,f420]) ).
fof(f425,definition,
( spl0_34
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f429,definition,
( spl0_35
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f430,plain,
( ! [X1] :
( c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f431,plain,
( ~ spl0_34
| spl0_35
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f290,f344,f304,f429,f425]) ).
fof(f433,definition,
( spl0_36
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f434,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( spl0_15
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f160,f433,f304,f347]) ).
fof(f437,definition,
( spl0_37
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f441,plain,
( ~ spl0_30
| spl0_9
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f288,f354,f304,f326,f405]) ).
fof(f448,definition,
( spl0_39
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f456,definition,
( spl0_41
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f460,definition,
( spl0_42
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f461,plain,
( ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f462,plain,
( spl0_41
| spl0_42
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f155,f429,f304,f460,f456]) ).
fof(f464,definition,
( spl0_43
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f465,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f466,plain,
( spl0_22
| ~ spl0_33
| ~ spl0_3
| spl0_43 ),
inference(avatar_split_clause,[],[f286,f464,f304,f420,f373]) ).
fof(f473,definition,
( spl0_45
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f478,definition,
( spl0_46
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f497,definition,
( spl0_50
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f498,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f501,definition,
( spl0_51
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f504,plain,
( ~ spl0_28
| spl0_51
| ~ spl0_3
| spl0_50 ),
inference(avatar_split_clause,[],[f281,f497,f304,f501,f397]) ).
fof(f511,plain,
( spl0_22
| ~ spl0_24
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f278,f385,f304,f381,f373]) ).
fof(f512,plain,
( ~ spl0_30
| ~ spl0_37
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f277,f385,f304,f437,f405]) ).
fof(f514,definition,
( spl0_53
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f517,plain,
( ~ spl0_53
| spl0_45
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f276,f312,f304,f473,f514]) ).
fof(f521,definition,
( spl0_54
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f524,plain,
( ~ spl0_30
| ~ spl0_54
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f273,f377,f304,f521,f405]) ).
fof(f526,definition,
( spl0_55
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f529,plain,
( spl0_55
| ~ spl0_3
| spl0_50 ),
inference(avatar_split_clause,[],[f138,f497,f304,f526]) ).
fof(f539,plain,
( ~ spl0_32
| spl0_55
| spl0_18
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f270,f304,f358,f526,f415]) ).
fof(f545,plain,
( spl0_20
| spl0_18
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f133,f304,f358,f365]) ).
fof(f547,definition,
( spl0_59
<=> c3_1(a96) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f549,plain,
( ~ c3_1(a96)
| spl0_59 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f550,plain,
( ~ spl0_39
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f132,f547,f448]) ).
fof(f552,definition,
( spl0_60
<=> c2_1(a96) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f555,plain,
( ~ spl0_39
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f131,f552,f448]) ).
fof(f557,definition,
( spl0_61
<=> c1_1(a96) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f560,plain,
( ~ spl0_39
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f130,f557,f448]) ).
fof(f562,definition,
( spl0_62
<=> c1_1(a97) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f565,plain,
( ~ spl0_20
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f129,f562,f365]) ).
fof(f577,definition,
( spl0_65
<=> c3_1(a99) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f579,plain,
( ~ c3_1(a99)
| spl0_65 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f580,plain,
( spl0_32
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f268,f577,f415]) ).
fof(f582,definition,
( spl0_66
<=> c1_1(a99) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f585,plain,
( spl0_32
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f267,f582,f415]) ).
fof(f597,definition,
( spl0_69
<=> c2_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f599,plain,
( ~ c2_1(a101)
| spl0_69 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f600,plain,
( spl0_28
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f266,f597,f397]) ).
fof(f602,definition,
( spl0_70
<=> c1_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f605,plain,
( spl0_28
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f265,f602,f397]) ).
fof(f607,definition,
( spl0_71
<=> c3_1(a102) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f609,plain,
( ~ c3_1(a102)
| spl0_71 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,plain,
( ~ spl0_41
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f120,f607,f456]) ).
fof(f612,definition,
( spl0_72
<=> c3_1(a103) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f614,plain,
( ~ c3_1(a103)
| spl0_72 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f615,plain,
( spl0_34
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f264,f612,f425]) ).
fof(f617,definition,
( spl0_73
<=> c1_1(a103) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f620,plain,
( spl0_34
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f263,f617,f425]) ).
fof(f622,definition,
( spl0_74
<=> c3_1(a104) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f624,plain,
( ~ c3_1(a104)
| spl0_74 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f625,plain,
( ~ spl0_22
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f117,f622,f373]) ).
fof(f627,definition,
( spl0_75
<=> c2_1(a104) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f630,plain,
( ~ spl0_22
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f116,f627,f373]) ).
fof(f632,definition,
( spl0_76
<=> c0_1(a104) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f634,plain,
( ~ c0_1(a104)
| spl0_76 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( ~ spl0_22
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f115,f632,f373]) ).
fof(f642,definition,
( spl0_78
<=> c2_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f645,plain,
( spl0_30
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f261,f642,f405]) ).
fof(f647,definition,
( spl0_79
<=> c3_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f649,plain,
( ~ c3_1(a109)
| spl0_79 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f650,plain,
( spl0_53
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f260,f647,f514]) ).
fof(f652,definition,
( spl0_80
<=> c0_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f654,plain,
( ~ c0_1(a109)
| spl0_80 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f655,plain,
( spl0_53
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f259,f652,f514]) ).
fof(f657,definition,
( spl0_81
<=> c0_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f659,plain,
( ~ c0_1(a110)
| spl0_81 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f660,plain,
( spl0_33
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f258,f657,f420]) ).
fof(f662,definition,
( spl0_82
<=> c1_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f665,plain,
( ~ spl0_55
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f109,f662,f526]) ).
fof(f667,definition,
( spl0_83
<=> c3_1(a115) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f669,plain,
( ~ c3_1(a115)
| spl0_83 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f670,plain,
( spl0_37
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f257,f667,f437]) ).
fof(f672,definition,
( spl0_84
<=> c2_1(a115) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f675,plain,
( spl0_37
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f256,f672,f437]) ).
fof(f677,definition,
( spl0_85
<=> c0_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f679,plain,
( ~ c0_1(a116)
| spl0_85 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f680,plain,
( spl0_31
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f255,f677,f410]) ).
fof(f682,definition,
( spl0_86
<=> c3_1(a118) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f684,plain,
( ~ c3_1(a118)
| spl0_86 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f685,plain,
( spl0_24
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f254,f682,f381]) ).
fof(f687,definition,
( spl0_87
<=> c2_1(a118) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f690,plain,
( spl0_24
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f253,f687,f381]) ).
fof(f712,definition,
( spl0_92
<=> c3_1(a127) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f714,plain,
( ~ c3_1(a127)
| spl0_92 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f715,plain,
( ~ spl0_51
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f99,f712,f501]) ).
fof(f717,definition,
( spl0_93
<=> c2_1(a133) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f720,plain,
( spl0_54
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f248,f717,f521]) ).
fof(f722,definition,
( spl0_94
<=> c2_1(a145) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f725,plain,
( ~ spl0_46
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f97,f722,f478]) ).
fof(f727,definition,
( spl0_95
<=> c0_1(a145) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f729,plain,
( ~ c0_1(a145)
| spl0_95 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f730,plain,
( ~ spl0_46
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f96,f727,f478]) ).
fof(f751,definition,
( spl0_100
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f779,definition,
( spl0_106
<=> c3_1(a97) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f781,plain,
( c3_1(a97)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f782,plain,
( spl0_106
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f88,f365,f779]) ).
fof(f784,definition,
( spl0_107
<=> c2_1(a97) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f787,plain,
( spl0_107
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f87,f365,f784]) ).
fof(f794,definition,
( spl0_109
<=> c2_1(a99) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f797,plain,
( spl0_109
| spl0_32 ),
inference(avatar_split_clause,[],[f242,f415,f794]) ).
fof(f804,definition,
( spl0_111
<=> c3_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f806,plain,
( c3_1(a101)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f804]) ).
fof(f807,plain,
( spl0_111
| spl0_28 ),
inference(avatar_split_clause,[],[f241,f397,f804]) ).
fof(f809,definition,
( spl0_112
<=> c2_1(a102) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f812,plain,
( spl0_112
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f82,f456,f809]) ).
fof(f814,definition,
( spl0_113
<=> c1_1(a102) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f817,plain,
( spl0_113
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f81,f456,f814]) ).
fof(f819,definition,
( spl0_114
<=> c0_1(a103) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f821,plain,
( c0_1(a103)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f822,plain,
( spl0_114
| spl0_34 ),
inference(avatar_split_clause,[],[f240,f425,f819]) ).
fof(f834,definition,
( spl0_117
<=> c3_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f836,plain,
( c3_1(a106)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f837,plain,
( spl0_117
| spl0_30 ),
inference(avatar_split_clause,[],[f237,f405,f834]) ).
fof(f839,definition,
( spl0_118
<=> c1_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f842,plain,
( spl0_118
| spl0_30 ),
inference(avatar_split_clause,[],[f236,f405,f839]) ).
fof(f844,definition,
( spl0_119
<=> c2_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f847,plain,
( spl0_119
| spl0_53 ),
inference(avatar_split_clause,[],[f235,f514,f844]) ).
fof(f849,definition,
( spl0_120
<=> c3_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f852,plain,
( spl0_120
| spl0_33 ),
inference(avatar_split_clause,[],[f234,f420,f849]) ).
fof(f854,definition,
( spl0_121
<=> c2_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f857,plain,
( spl0_121
| spl0_33 ),
inference(avatar_split_clause,[],[f233,f420,f854]) ).
fof(f859,definition,
( spl0_122
<=> c3_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f861,plain,
( c3_1(a112)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f862,plain,
( spl0_122
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f72,f526,f859]) ).
fof(f864,definition,
( spl0_123
<=> c0_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f866,plain,
( c0_1(a112)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f864]) ).
fof(f867,plain,
( spl0_123
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f71,f526,f864]) ).
fof(f869,definition,
( spl0_124
<=> c0_1(a115) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f871,plain,
( c0_1(a115)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f869]) ).
fof(f872,plain,
( spl0_124
| spl0_37 ),
inference(avatar_split_clause,[],[f232,f437,f869]) ).
fof(f874,definition,
( spl0_125
<=> c3_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f876,plain,
( c3_1(a116)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f877,plain,
( spl0_125
| spl0_31 ),
inference(avatar_split_clause,[],[f231,f410,f874]) ).
fof(f879,definition,
( spl0_126
<=> c1_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f882,plain,
( spl0_126
| spl0_31 ),
inference(avatar_split_clause,[],[f230,f410,f879]) ).
fof(f884,definition,
( spl0_127
<=> c1_1(a118) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f887,plain,
( spl0_127
| spl0_24 ),
inference(avatar_split_clause,[],[f229,f381,f884]) ).
fof(f899,definition,
( spl0_130
<=> c2_1(a127) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f902,plain,
( spl0_130
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f64,f501,f899]) ).
fof(f904,definition,
( spl0_131
<=> c0_1(a127) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f906,plain,
( c0_1(a127)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f907,plain,
( spl0_131
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f63,f501,f904]) ).
fof(f909,definition,
( spl0_132
<=> c3_1(a133) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f911,plain,
( c3_1(a133)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f912,plain,
( spl0_132
| spl0_54 ),
inference(avatar_split_clause,[],[f226,f521,f909]) ).
fof(f914,definition,
( spl0_133
<=> c0_1(a133) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f916,plain,
( c0_1(a133)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f914]) ).
fof(f917,plain,
( spl0_133
| spl0_54 ),
inference(avatar_split_clause,[],[f225,f521,f914]) ).
fof(f919,definition,
( spl0_134
<=> c3_1(a145) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f921,plain,
( c3_1(a145)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f919]) ).
fof(f922,plain,
( spl0_134
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f60,f478,f919]) ).
fof(f949,definition,
( spl0_140
<=> c2_1(a94) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f952,plain,
( spl0_140
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f54,f473,f949]) ).
fof(f954,definition,
( spl0_141
<=> c1_1(a94) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f957,plain,
( spl0_141
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f53,f473,f954]) ).
fof(f959,definition,
( spl0_142
<=> c0_1(a94) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f961,plain,
( c0_1(a94)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f959]) ).
fof(f962,plain,
( spl0_142
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f52,f473,f959]) ).
fof(f994,definition,
( spl0_149
<=> c3_1(a165) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f996,plain,
( c3_1(a165)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f994]) ).
fof(f998,definition,
( spl0_150
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1001,plain,
( spl0_149
| spl0_150 ),
inference(avatar_split_clause,[],[f214,f998,f994]) ).
fof(f1003,definition,
( spl0_151
<=> c2_1(a165) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f1006,plain,
( spl0_151
| spl0_150 ),
inference(avatar_split_clause,[],[f213,f998,f1003]) ).
fof(f1008,definition,
( spl0_152
<=> c1_1(a165) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1011,plain,
( spl0_152
| spl0_150 ),
inference(avatar_split_clause,[],[f212,f998,f1008]) ).
fof(f1014,plain,
( ~ spl0_53
| ~ spl0_100
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f209,f998,f751,f514]) ).
fof(f1015,plain,
( ~ spl0_32
| spl0_20
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f208,f437,f365,f415]) ).
fof(f1016,plain,
( ~ spl0_53
| ~ spl0_33
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f207,f437,f420,f514]) ).
fof(f1017,plain,
( spl0_46
| ~ spl0_24
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f206,f437,f381,f478]) ).
fof(f1018,plain,
( spl0_22
| ~ spl0_32
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f205,f521,f415,f373]) ).
fof(f1019,plain,
( spl0_39
| ~ spl0_150
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f204,f521,f998,f448]) ).
fof(f1035,plain,
( spl0_3
| spl0_53 ),
inference(avatar_split_clause,[],[f194,f514,f304]) ).
fof(f1048,plain,
( spl0_3
| spl0_100 ),
inference(avatar_split_clause,[],[f184,f751,f304]) ).
fof(f1053,plain,
( spl0_3
| spl0_150 ),
inference(avatar_split_clause,[],[f181,f998,f304]) ).
fof(f1067,plain,
( ~ c1_1(a116)
| ~ c2_1(a116)
| ~ spl0_5
| spl0_85 ),
inference(resolution,[],[f313,f679]) ).
fof(f1084,definition,
( spl0_154
<=> c1_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f1091,definition,
( spl0_155
<=> c2_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1095,plain,
( c2_1(a112)
| c1_1(a112)
| ~ spl0_8
| ~ spl0_122 ),
inference(resolution,[],[f323,f861]) ).
fof(f1096,plain,
( spl0_82
| spl0_155
| ~ spl0_8
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1095,f859,f322,f1091,f662]) ).
fof(f1118,plain,
( c3_1(a104)
| ~ c1_1(a104)
| ~ spl0_11
| spl0_76 ),
inference(resolution,[],[f334,f634]) ).
fof(f1121,definition,
( spl0_156
<=> c1_1(a104) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f1132,definition,
( spl0_158
<=> c1_1(a115) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f1137,definition,
( spl0_159
<=> c1_1(a127) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1142,definition,
( spl0_160
<=> c1_1(a133) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1147,definition,
( spl0_161
<=> c1_1(a145) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1163,definition,
( spl0_163
<=> c2_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1182,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_13 ),
inference(resolution,[],[f342,f309]) ).
fof(f1190,plain,
( c2_1(a145)
| ~ c3_1(a145)
| ~ spl0_13
| spl0_95 ),
inference(resolution,[],[f342,f729]) ).
fof(f1202,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f1182]) ).
fof(f1229,plain,
( spl0_2
| ~ spl0_4
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1202,f341,f308,f301]) ).
fof(f1230,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_14 ),
inference(resolution,[],[f345,f309]) ).
fof(f1241,plain,
( ~ c2_1(a116)
| ~ c3_1(a116)
| ~ spl0_14
| spl0_85 ),
inference(resolution,[],[f345,f679]) ).
fof(f1243,plain,
( ~ c2_1(a110)
| ~ c3_1(a110)
| ~ spl0_14
| spl0_81 ),
inference(resolution,[],[f345,f659]) ).
fof(f1250,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f1230]) ).
fof(f1252,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_10 ),
inference(resolution,[],[f330,f309]) ).
fof(f1263,plain,
( ~ c1_1(a116)
| ~ c3_1(a116)
| ~ spl0_10
| spl0_85 ),
inference(resolution,[],[f330,f679]) ).
fof(f1272,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f1252]) ).
fof(f1273,plain,
( ~ spl0_125
| ~ spl0_126
| ~ spl0_10
| spl0_85 ),
inference(avatar_split_clause,[],[f1263,f677,f329,f879,f874]) ).
fof(f1292,plain,
( c2_1(a112)
| c1_1(a112)
| ~ spl0_12
| ~ spl0_123 ),
inference(resolution,[],[f338,f866]) ).
fof(f1294,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| c2_1(X0)
| c1_1(X0) )
| ~ spl0_12
| ~ spl0_16 ),
inference(resolution,[],[f352,f338]) ).
fof(f1315,plain,
( c2_1(a104)
| c1_1(a104)
| ~ spl0_16
| spl0_76 ),
inference(resolution,[],[f352,f634]) ).
fof(f1317,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0) )
| ~ spl0_12
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f1294]) ).
fof(f1327,definition,
( spl0_171
<=> c2_1(a103) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1379,plain,
( ~ c2_1(a99)
| c1_1(a99)
| ~ spl0_17
| spl0_65 ),
inference(resolution,[],[f355,f579]) ).
fof(f1390,plain,
( ~ c1_1(a106)
| ~ spl0_4
| ~ spl0_10
| ~ spl0_117 ),
inference(resolution,[],[f836,f1272]) ).
fof(f1391,plain,
( ~ spl0_118
| ~ spl0_4
| ~ spl0_10
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1390,f834,f329,f308,f839]) ).
fof(f1393,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_10 ),
inference(resolution,[],[f299,f330]) ).
fof(f1395,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(resolution,[],[f299,f334]) ).
fof(f1402,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f1395]) ).
fof(f1403,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f1393]) ).
fof(f1409,plain,
( spl0_19
| ~ spl0_1
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1402,f333,f298,f361]) ).
fof(f1410,plain,
( spl0_2
| ~ spl0_1
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1403,f329,f298,f301]) ).
fof(f1438,plain,
( c3_1(a109)
| ~ c2_1(a109)
| ~ spl0_9
| spl0_80 ),
inference(resolution,[],[f327,f654]) ).
fof(f1444,plain,
( ~ spl0_119
| spl0_79
| ~ spl0_9
| spl0_80 ),
inference(avatar_split_clause,[],[f1438,f652,f326,f647,f844]) ).
fof(f1452,plain,
( spl0_66
| ~ spl0_109
| ~ spl0_17
| spl0_65 ),
inference(avatar_split_clause,[],[f1379,f577,f354,f794,f582]) ).
fof(f1460,plain,
( c2_1(a115)
| ~ c1_1(a115)
| ~ spl0_1
| ~ spl0_124 ),
inference(resolution,[],[f299,f871]) ).
fof(f1470,plain,
( c2_1(a112)
| ~ c3_1(a112)
| ~ spl0_6
| ~ spl0_123 ),
inference(resolution,[],[f316,f866]) ).
fof(f1491,plain,
( ~ c2_1(a109)
| c1_1(a109)
| ~ spl0_17
| spl0_79 ),
inference(resolution,[],[f355,f649]) ).
fof(f1494,plain,
( ~ c2_1(a103)
| c1_1(a103)
| ~ spl0_17
| spl0_72 ),
inference(resolution,[],[f355,f614]) ).
fof(f1518,plain,
( c1_1(a115)
| c2_1(a115)
| ~ spl0_18
| spl0_83 ),
inference(resolution,[],[f359,f669]) ).
fof(f1524,plain,
( c1_1(a103)
| c2_1(a103)
| ~ spl0_18
| spl0_72 ),
inference(resolution,[],[f359,f614]) ).
fof(f1532,plain,
( c1_1(a104)
| c2_1(a104)
| ~ spl0_18
| spl0_74 ),
inference(resolution,[],[f359,f624]) ).
fof(f1533,plain,
( c1_1(a96)
| c2_1(a96)
| ~ spl0_18
| spl0_59 ),
inference(resolution,[],[f359,f549]) ).
fof(f1534,plain,
( spl0_60
| spl0_61
| ~ spl0_18
| spl0_59 ),
inference(avatar_split_clause,[],[f1533,f547,f358,f557,f552]) ).
fof(f1535,plain,
( spl0_75
| spl0_156
| ~ spl0_18
| spl0_74 ),
inference(avatar_split_clause,[],[f1532,f622,f358,f1121,f627]) ).
fof(f1546,plain,
( spl0_84
| spl0_158
| ~ spl0_18
| spl0_83 ),
inference(avatar_split_clause,[],[f1518,f667,f358,f1132,f672]) ).
fof(f1559,plain,
( ~ spl0_158
| spl0_84
| ~ spl0_1
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1460,f869,f298,f672,f1132]) ).
fof(f1586,plain,
( c2_1(a133)
| ~ c3_1(a133)
| ~ spl0_6
| ~ spl0_133 ),
inference(resolution,[],[f916,f316]) ).
fof(f1612,plain,
( c2_1(a145)
| ~ c1_1(a145)
| ~ spl0_2
| ~ spl0_134 ),
inference(resolution,[],[f302,f921]) ).
fof(f1625,plain,
( c2_1(a145)
| c1_1(a145)
| ~ spl0_8
| ~ spl0_134 ),
inference(resolution,[],[f323,f921]) ).
fof(f1626,plain,
( c2_1(a133)
| c1_1(a133)
| ~ spl0_8
| ~ spl0_132 ),
inference(resolution,[],[f323,f911]) ).
fof(f1670,plain,
( c3_1(a103)
| c1_1(a103)
| ~ spl0_15
| ~ spl0_114 ),
inference(resolution,[],[f348,f821]) ).
fof(f1681,plain,
( ~ c1_1(a118)
| c2_1(a118)
| ~ spl0_19
| spl0_86 ),
inference(resolution,[],[f362,f684]) ).
fof(f1693,plain,
( ~ c1_1(a104)
| c2_1(a104)
| ~ spl0_19
| spl0_74 ),
inference(resolution,[],[f362,f624]) ).
fof(f1698,plain,
( spl0_75
| ~ spl0_156
| ~ spl0_19
| spl0_74 ),
inference(avatar_split_clause,[],[f1693,f622,f361,f1121,f627]) ).
fof(f1705,plain,
( spl0_87
| ~ spl0_127
| ~ spl0_19
| spl0_86 ),
inference(avatar_split_clause,[],[f1681,f682,f361,f884,f687]) ).
fof(f1720,plain,
( ~ c3_1(a112)
| ~ c2_1(a112)
| ~ spl0_21
| ~ spl0_123 ),
inference(resolution,[],[f370,f866]) ).
fof(f1734,plain,
( c3_1(a115)
| c2_1(a115)
| ~ spl0_23
| ~ spl0_124 ),
inference(resolution,[],[f378,f871]) ).
fof(f1746,plain,
( c2_1(a101)
| c1_1(a101)
| ~ spl0_8
| ~ spl0_111 ),
inference(resolution,[],[f806,f323]) ).
fof(f1752,plain,
( spl0_84
| spl0_83
| ~ spl0_23
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1734,f869,f377,f667,f672]) ).
fof(f1768,plain,
( c3_1(a103)
| c2_1(a103)
| ~ spl0_23
| ~ spl0_114 ),
inference(resolution,[],[f378,f821]) ).
fof(f1807,plain,
( ~ c1_1(a127)
| ~ c2_1(a127)
| ~ spl0_29
| spl0_92 ),
inference(resolution,[],[f402,f714]) ).
fof(f1813,plain,
( ~ c1_1(a102)
| ~ c2_1(a102)
| ~ spl0_29
| spl0_71 ),
inference(resolution,[],[f402,f609]) ).
fof(f1821,plain,
( ~ spl0_112
| ~ spl0_113
| ~ spl0_29
| spl0_71 ),
inference(avatar_split_clause,[],[f1813,f607,f401,f814,f809]) ).
fof(f1848,plain,
( c1_1(a112)
| ~ c3_1(a112)
| ~ spl0_25
| ~ spl0_123 ),
inference(resolution,[],[f866,f386]) ).
fof(f1851,plain,
( ~ spl0_122
| spl0_82
| ~ spl0_25
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1848,f864,f385,f662,f859]) ).
fof(f1853,plain,
( ~ spl0_132
| spl0_93
| ~ spl0_6
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f1586,f914,f315,f717,f909]) ).
fof(f1876,plain,
( ~ spl0_161
| spl0_94
| ~ spl0_2
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f1612,f919,f301,f722,f1147]) ).
fof(f1888,plain,
( ~ spl0_156
| spl0_74
| ~ spl0_11
| spl0_76 ),
inference(avatar_split_clause,[],[f1118,f632,f333,f622,f1121]) ).
fof(f1904,plain,
( c2_1(a133)
| ~ c1_1(a133)
| ~ spl0_2
| ~ spl0_132 ),
inference(resolution,[],[f302,f911]) ).
fof(f1907,plain,
( c2_1(a116)
| ~ c1_1(a116)
| ~ spl0_2
| ~ spl0_125 ),
inference(resolution,[],[f302,f876]) ).
fof(f1936,plain,
( ~ c2_1(a94)
| ~ c1_1(a94)
| ~ spl0_7
| ~ spl0_142 ),
inference(resolution,[],[f319,f961]) ).
fof(f1948,plain,
( ~ spl0_141
| ~ spl0_140
| ~ spl0_7
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1936,f959,f318,f949,f954]) ).
fof(f1960,plain,
( ~ spl0_122
| spl0_155
| ~ spl0_6
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1470,f864,f315,f1091,f859]) ).
fof(f1963,plain,
( spl0_160
| spl0_93
| ~ spl0_8
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1626,f909,f322,f717,f1142]) ).
fof(f1964,plain,
( spl0_70
| spl0_69
| ~ spl0_8
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f1746,f804,f322,f597,f602]) ).
fof(f1965,plain,
( spl0_156
| spl0_75
| ~ spl0_16
| spl0_76 ),
inference(avatar_split_clause,[],[f1315,f632,f351,f627,f1121]) ).
fof(f1976,plain,
( ~ spl0_163
| ~ spl0_126
| ~ spl0_5
| spl0_85 ),
inference(avatar_split_clause,[],[f1067,f677,f312,f879,f1163]) ).
fof(f2018,plain,
( c1_1(a101)
| ~ spl0_12
| ~ spl0_16
| spl0_69 ),
inference(resolution,[],[f1317,f599]) ).
fof(f2024,plain,
( spl0_70
| ~ spl0_12
| ~ spl0_16
| spl0_69 ),
inference(avatar_split_clause,[],[f2018,f597,f351,f337,f602]) ).
fof(f2092,plain,
( ! [X0] :
( c3_1(X0)
| c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_9
| ~ spl0_15 ),
inference(resolution,[],[f348,f327]) ).
fof(f2106,plain,
( ! [X0] :
( c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_9
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f2092]) ).
fof(f2113,plain,
( spl0_17
| ~ spl0_9
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f2106,f347,f326,f354]) ).
fof(f2119,plain,
( ~ c1_1(a109)
| ~ c2_1(a109)
| ~ spl0_5
| spl0_80 ),
inference(resolution,[],[f654,f313]) ).
fof(f2212,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_6
| ~ spl0_35 ),
inference(resolution,[],[f430,f316]) ).
fof(f2213,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_35 ),
inference(resolution,[],[f430,f309]) ).
fof(f2229,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_4
| ~ spl0_35 ),
inference(duplicate_literal_removal,[],[f2213]) ).
fof(f2230,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_6
| ~ spl0_35 ),
inference(duplicate_literal_removal,[],[f2212]) ).
fof(f2236,plain,
( spl0_2
| ~ spl0_4
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f2229,f429,f308,f301]) ).
fof(f2237,plain,
( spl0_2
| ~ spl0_6
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f2230,f429,f315,f301]) ).
fof(f2238,plain,
( spl0_73
| spl0_72
| ~ spl0_15
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f1670,f819,f347,f612,f617]) ).
fof(f2246,plain,
( ~ spl0_160
| spl0_93
| ~ spl0_2
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1904,f909,f301,f717,f1142]) ).
fof(f2251,plain,
( spl0_82
| spl0_155
| ~ spl0_12
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1292,f864,f337,f1091,f662]) ).
fof(f2261,plain,
( spl0_154
| ~ spl0_119
| ~ spl0_17
| spl0_79 ),
inference(avatar_split_clause,[],[f1491,f647,f354,f844,f1084]) ).
fof(f2265,plain,
( ~ spl0_155
| ~ spl0_122
| ~ spl0_21
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1720,f864,f369,f859,f1091]) ).
fof(f2315,plain,
( ~ c3_1(a133)
| ~ c1_1(a133)
| ~ spl0_4
| ~ spl0_133 ),
inference(resolution,[],[f916,f309]) ).
fof(f2332,plain,
( c2_1(a106)
| ~ c1_1(a106)
| ~ spl0_2
| ~ spl0_117 ),
inference(resolution,[],[f302,f836]) ).
fof(f2344,plain,
( c2_1(a133)
| c1_1(a133)
| ~ spl0_12
| ~ spl0_133 ),
inference(resolution,[],[f338,f916]) ).
fof(f2356,plain,
( spl0_160
| spl0_93
| ~ spl0_12
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f2344,f914,f337,f717,f1142]) ).
fof(f2419,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_23
| ~ spl0_35 ),
inference(resolution,[],[f430,f378]) ).
fof(f2435,plain,
( c2_1(a104)
| ~ c1_1(a104)
| ~ spl0_35
| spl0_76 ),
inference(resolution,[],[f430,f634]) ).
fof(f2438,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_23
| ~ spl0_35 ),
inference(duplicate_literal_removal,[],[f2419]) ).
fof(f2439,plain,
( ~ spl0_156
| spl0_75
| ~ spl0_35
| spl0_76 ),
inference(avatar_split_clause,[],[f2435,f632,f429,f627,f1121]) ).
fof(f2442,plain,
( spl0_19
| ~ spl0_23
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f2438,f429,f377,f361]) ).
fof(f2445,plain,
( ~ spl0_120
| ~ spl0_121
| ~ spl0_14
| spl0_81 ),
inference(avatar_split_clause,[],[f1243,f657,f344,f854,f849]) ).
fof(f2447,plain,
( spl0_73
| ~ spl0_171
| ~ spl0_17
| spl0_72 ),
inference(avatar_split_clause,[],[f1494,f612,f354,f1327,f617]) ).
fof(f2448,plain,
( spl0_171
| spl0_73
| ~ spl0_18
| spl0_72 ),
inference(avatar_split_clause,[],[f1524,f612,f358,f617,f1327]) ).
fof(f2450,plain,
( spl0_171
| spl0_72
| ~ spl0_23
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f1768,f819,f377,f612,f1327]) ).
fof(f2508,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_14
| ~ spl0_21 ),
inference(resolution,[],[f345,f370]) ).
fof(f2521,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_14
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f2508]) ).
fof(f2530,plain,
( c1_1(a127)
| ~ c2_1(a127)
| ~ spl0_36
| ~ spl0_131 ),
inference(resolution,[],[f434,f906]) ).
fof(f2534,plain,
( c1_1(a103)
| ~ c2_1(a103)
| ~ spl0_36
| ~ spl0_114 ),
inference(resolution,[],[f434,f821]) ).
fof(f2551,plain,
( ~ c2_1(a97)
| ~ spl0_14
| ~ spl0_21
| ~ spl0_106 ),
inference(resolution,[],[f2521,f781]) ).
fof(f2553,plain,
( ~ spl0_107
| ~ spl0_14
| ~ spl0_21
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f2551,f779,f369,f344,f784]) ).
fof(f2559,plain,
( ~ spl0_160
| ~ spl0_132
| ~ spl0_4
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f2315,f914,f308,f909,f1142]) ).
fof(f2566,plain,
( ~ spl0_125
| ~ spl0_163
| ~ spl0_14
| spl0_85 ),
inference(avatar_split_clause,[],[f1241,f677,f344,f1163,f874]) ).
fof(f2662,plain,
( c3_1(a104)
| c2_1(a104)
| ~ spl0_42
| spl0_76 ),
inference(resolution,[],[f461,f634]) ).
fof(f2666,plain,
( spl0_75
| spl0_74
| ~ spl0_42
| spl0_76 ),
inference(avatar_split_clause,[],[f2662,f632,f460,f622,f627]) ).
fof(f2672,plain,
( ~ c1_1(a165)
| ~ c2_1(a165)
| ~ spl0_43
| ~ spl0_149 ),
inference(resolution,[],[f465,f996]) ).
fof(f2687,plain,
( ~ spl0_151
| ~ spl0_152
| ~ spl0_43
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f2672,f994,f464,f1008,f1003]) ).
fof(f2688,plain,
( spl0_43
| ~ spl0_4
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1250,f344,f308,f464]) ).
fof(f2695,plain,
( ~ spl0_126
| spl0_163
| ~ spl0_2
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f1907,f874,f301,f1163,f879]) ).
fof(f2699,plain,
( ~ spl0_118
| spl0_78
| ~ spl0_2
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f2332,f834,f301,f642,f839]) ).
fof(f2816,plain,
( c1_1(a97)
| ~ c2_1(a97)
| ~ spl0_50
| ~ spl0_106 ),
inference(resolution,[],[f498,f781]) ).
fof(f2820,plain,
( ~ spl0_107
| spl0_62
| ~ spl0_50
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f2816,f779,f497,f562,f784]) ).
fof(f2828,plain,
( ~ spl0_119
| ~ spl0_154
| ~ spl0_5
| spl0_80 ),
inference(avatar_split_clause,[],[f2119,f652,f312,f1084,f844]) ).
fof(f2833,plain,
( spl0_161
| spl0_94
| ~ spl0_8
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f1625,f919,f322,f722,f1147]) ).
fof(f2837,plain,
( ~ spl0_134
| spl0_94
| ~ spl0_13
| spl0_95 ),
inference(avatar_split_clause,[],[f1190,f727,f341,f722,f919]) ).
fof(f2848,plain,
( ~ spl0_130
| ~ spl0_159
| ~ spl0_29
| spl0_92 ),
inference(avatar_split_clause,[],[f1807,f712,f401,f1137,f899]) ).
fof(f2855,plain,
( ~ spl0_130
| spl0_159
| ~ spl0_36
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f2530,f904,f433,f1137,f899]) ).
fof(f2856,plain,
( ~ spl0_171
| spl0_73
| ~ spl0_36
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f2534,f819,f433,f617,f1327]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f310]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f320]) ).
cnf(s3,plain,
( spl0_1
| ~ spl0_3
| spl0_4
| spl0_8 ),
inference(sat_conversion,[],[f324]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_5
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f331]) ).
cnf(s5,plain,
( spl0_2
| ~ spl0_3
| spl0_6
| spl0_11 ),
inference(sat_conversion,[],[f335]) ).
cnf(s6,plain,
( spl0_2
| ~ spl0_3
| spl0_8
| spl0_12 ),
inference(sat_conversion,[],[f339]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f349]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_10
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f356]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_9
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f363]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_21
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f379]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_4
| spl0_13
| spl0_22 ),
inference(sat_conversion,[],[f391]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_19
| ~ spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f403]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_6
| spl0_12
| ~ spl0_31 ),
inference(sat_conversion,[],[f413]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_18
| spl0_21
| ~ spl0_32 ),
inference(sat_conversion,[],[f418]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_10
| spl0_15
| ~ spl0_33 ),
inference(sat_conversion,[],[f423]) ).
cnf(s20,plain,
( ~ spl0_3
| spl0_14
| ~ spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f431]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_15
| spl0_36 ),
inference(sat_conversion,[],[f435]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_9
| spl0_17
| ~ spl0_30 ),
inference(sat_conversion,[],[f441]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_35
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f462]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_22
| ~ spl0_33
| spl0_43 ),
inference(sat_conversion,[],[f466]) ).
cnf(s34,plain,
( ~ spl0_3
| ~ spl0_28
| spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f504]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_22
| ~ spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f511]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_25
| ~ spl0_30
| ~ spl0_37 ),
inference(sat_conversion,[],[f512]) ).
cnf(s39,plain,
( ~ spl0_3
| spl0_5
| spl0_45
| ~ spl0_53 ),
inference(sat_conversion,[],[f517]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_23
| ~ spl0_30
| ~ spl0_54 ),
inference(sat_conversion,[],[f524]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_50
| spl0_55 ),
inference(sat_conversion,[],[f529]) ).
cnf(s46,plain,
( ~ spl0_3
| spl0_18
| ~ spl0_32
| spl0_55 ),
inference(sat_conversion,[],[f539]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_18
| spl0_20 ),
inference(sat_conversion,[],[f545]) ).
cnf(s49,plain,
( ~ spl0_39
| ~ spl0_59 ),
inference(sat_conversion,[],[f550]) ).
cnf(s50,plain,
( ~ spl0_39
| ~ spl0_60 ),
inference(sat_conversion,[],[f555]) ).
cnf(s51,plain,
( ~ spl0_39
| ~ spl0_61 ),
inference(sat_conversion,[],[f560]) ).
cnf(s52,plain,
( ~ spl0_20
| ~ spl0_62 ),
inference(sat_conversion,[],[f565]) ).
cnf(s55,plain,
( spl0_32
| ~ spl0_65 ),
inference(sat_conversion,[],[f580]) ).
cnf(s56,plain,
( spl0_32
| ~ spl0_66 ),
inference(sat_conversion,[],[f585]) ).
cnf(s59,plain,
( spl0_28
| ~ spl0_69 ),
inference(sat_conversion,[],[f600]) ).
cnf(s60,plain,
( spl0_28
| ~ spl0_70 ),
inference(sat_conversion,[],[f605]) ).
cnf(s61,plain,
( ~ spl0_41
| ~ spl0_71 ),
inference(sat_conversion,[],[f610]) ).
cnf(s62,plain,
( spl0_34
| ~ spl0_72 ),
inference(sat_conversion,[],[f615]) ).
cnf(s63,plain,
( spl0_34
| ~ spl0_73 ),
inference(sat_conversion,[],[f620]) ).
cnf(s64,plain,
( ~ spl0_22
| ~ spl0_74 ),
inference(sat_conversion,[],[f625]) ).
cnf(s65,plain,
( ~ spl0_22
| ~ spl0_75 ),
inference(sat_conversion,[],[f630]) ).
cnf(s66,plain,
( ~ spl0_22
| ~ spl0_76 ),
inference(sat_conversion,[],[f635]) ).
cnf(s68,plain,
( spl0_30
| ~ spl0_78 ),
inference(sat_conversion,[],[f645]) ).
cnf(s69,plain,
( spl0_53
| ~ spl0_79 ),
inference(sat_conversion,[],[f650]) ).
cnf(s70,plain,
( spl0_53
| ~ spl0_80 ),
inference(sat_conversion,[],[f655]) ).
cnf(s71,plain,
( spl0_33
| ~ spl0_81 ),
inference(sat_conversion,[],[f660]) ).
cnf(s72,plain,
( ~ spl0_55
| ~ spl0_82 ),
inference(sat_conversion,[],[f665]) ).
cnf(s73,plain,
( spl0_37
| ~ spl0_83 ),
inference(sat_conversion,[],[f670]) ).
cnf(s74,plain,
( spl0_37
| ~ spl0_84 ),
inference(sat_conversion,[],[f675]) ).
cnf(s75,plain,
( spl0_31
| ~ spl0_85 ),
inference(sat_conversion,[],[f680]) ).
cnf(s76,plain,
( spl0_24
| ~ spl0_86 ),
inference(sat_conversion,[],[f685]) ).
cnf(s77,plain,
( spl0_24
| ~ spl0_87 ),
inference(sat_conversion,[],[f690]) ).
cnf(s82,plain,
( ~ spl0_51
| ~ spl0_92 ),
inference(sat_conversion,[],[f715]) ).
cnf(s83,plain,
( spl0_54
| ~ spl0_93 ),
inference(sat_conversion,[],[f720]) ).
cnf(s84,plain,
( ~ spl0_46
| ~ spl0_94 ),
inference(sat_conversion,[],[f725]) ).
cnf(s85,plain,
( ~ spl0_46
| ~ spl0_95 ),
inference(sat_conversion,[],[f730]) ).
cnf(s93,plain,
( ~ spl0_20
| spl0_106 ),
inference(sat_conversion,[],[f782]) ).
cnf(s94,plain,
( ~ spl0_20
| spl0_107 ),
inference(sat_conversion,[],[f787]) ).
cnf(s96,plain,
( spl0_32
| spl0_109 ),
inference(sat_conversion,[],[f797]) ).
cnf(s98,plain,
( spl0_28
| spl0_111 ),
inference(sat_conversion,[],[f807]) ).
cnf(s99,plain,
( ~ spl0_41
| spl0_112 ),
inference(sat_conversion,[],[f812]) ).
cnf(s100,plain,
( ~ spl0_41
| spl0_113 ),
inference(sat_conversion,[],[f817]) ).
cnf(s101,plain,
( spl0_34
| spl0_114 ),
inference(sat_conversion,[],[f822]) ).
cnf(s104,plain,
( spl0_30
| spl0_117 ),
inference(sat_conversion,[],[f837]) ).
cnf(s105,plain,
( spl0_30
| spl0_118 ),
inference(sat_conversion,[],[f842]) ).
cnf(s106,plain,
( spl0_53
| spl0_119 ),
inference(sat_conversion,[],[f847]) ).
cnf(s107,plain,
( spl0_33
| spl0_120 ),
inference(sat_conversion,[],[f852]) ).
cnf(s108,plain,
( spl0_33
| spl0_121 ),
inference(sat_conversion,[],[f857]) ).
cnf(s109,plain,
( ~ spl0_55
| spl0_122 ),
inference(sat_conversion,[],[f862]) ).
cnf(s110,plain,
( ~ spl0_55
| spl0_123 ),
inference(sat_conversion,[],[f867]) ).
cnf(s111,plain,
( spl0_37
| spl0_124 ),
inference(sat_conversion,[],[f872]) ).
cnf(s112,plain,
( spl0_31
| spl0_125 ),
inference(sat_conversion,[],[f877]) ).
cnf(s113,plain,
( spl0_31
| spl0_126 ),
inference(sat_conversion,[],[f882]) ).
cnf(s114,plain,
( spl0_24
| spl0_127 ),
inference(sat_conversion,[],[f887]) ).
cnf(s117,plain,
( ~ spl0_51
| spl0_130 ),
inference(sat_conversion,[],[f902]) ).
cnf(s118,plain,
( ~ spl0_51
| spl0_131 ),
inference(sat_conversion,[],[f907]) ).
cnf(s119,plain,
( spl0_54
| spl0_132 ),
inference(sat_conversion,[],[f912]) ).
cnf(s120,plain,
( spl0_54
| spl0_133 ),
inference(sat_conversion,[],[f917]) ).
cnf(s121,plain,
( ~ spl0_46
| spl0_134 ),
inference(sat_conversion,[],[f922]) ).
cnf(s127,plain,
( ~ spl0_45
| spl0_140 ),
inference(sat_conversion,[],[f952]) ).
cnf(s128,plain,
( ~ spl0_45
| spl0_141 ),
inference(sat_conversion,[],[f957]) ).
cnf(s129,plain,
( ~ spl0_45
| spl0_142 ),
inference(sat_conversion,[],[f962]) ).
cnf(s136,plain,
( spl0_149
| spl0_150 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s137,plain,
( spl0_150
| spl0_151 ),
inference(sat_conversion,[],[f1006]) ).
cnf(s138,plain,
( spl0_150
| spl0_152 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s141,plain,
( ~ spl0_53
| ~ spl0_100
| ~ spl0_150 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s142,plain,
( spl0_20
| ~ spl0_32
| ~ spl0_37 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s143,plain,
( ~ spl0_33
| ~ spl0_37
| ~ spl0_53 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s144,plain,
( ~ spl0_24
| ~ spl0_37
| spl0_46 ),
inference(sat_conversion,[],[f1017]) ).
cnf(s145,plain,
( spl0_22
| ~ spl0_32
| ~ spl0_54 ),
inference(sat_conversion,[],[f1018]) ).
cnf(s146,plain,
( spl0_39
| ~ spl0_54
| ~ spl0_150 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s162,plain,
( spl0_3
| spl0_53 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s175,plain,
( spl0_3
| spl0_100 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s180,plain,
( spl0_3
| spl0_150 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s184,plain,
( ~ spl0_8
| spl0_82
| ~ spl0_122
| spl0_155 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s203,plain,
( spl0_2
| ~ spl0_4
| ~ spl0_13 ),
inference(sat_conversion,[],[f1229]) ).
cnf(s205,plain,
( ~ spl0_10
| spl0_85
| ~ spl0_125
| ~ spl0_126 ),
inference(sat_conversion,[],[f1273]) ).
cnf(s232,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_117
| ~ spl0_118 ),
inference(sat_conversion,[],[f1391]) ).
cnf(s235,plain,
( ~ spl0_1
| ~ spl0_11
| spl0_19 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s236,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_10 ),
inference(sat_conversion,[],[f1410]) ).
cnf(s237,plain,
( ~ spl0_9
| spl0_79
| spl0_80
| ~ spl0_119 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s245,plain,
( ~ spl0_17
| spl0_65
| spl0_66
| ~ spl0_109 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s246,plain,
( ~ spl0_18
| spl0_59
| spl0_60
| spl0_61 ),
inference(sat_conversion,[],[f1534]) ).
cnf(s247,plain,
( ~ spl0_18
| spl0_74
| spl0_75
| spl0_156 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s258,plain,
( ~ spl0_18
| spl0_83
| spl0_84
| spl0_158 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s271,plain,
( ~ spl0_1
| spl0_84
| ~ spl0_124
| ~ spl0_158 ),
inference(sat_conversion,[],[f1559]) ).
cnf(s299,plain,
( ~ spl0_19
| spl0_74
| spl0_75
| ~ spl0_156 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s306,plain,
( ~ spl0_19
| spl0_86
| spl0_87
| ~ spl0_127 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s325,plain,
( ~ spl0_23
| spl0_83
| spl0_84
| ~ spl0_124 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s336,plain,
( ~ spl0_29
| spl0_71
| ~ spl0_112
| ~ spl0_113 ),
inference(sat_conversion,[],[f1821]) ).
cnf(s357,plain,
( ~ spl0_25
| spl0_82
| ~ spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f1851]) ).
cnf(s359,plain,
( ~ spl0_6
| spl0_93
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f1853]) ).
cnf(s382,plain,
( ~ spl0_2
| spl0_94
| ~ spl0_134
| ~ spl0_161 ),
inference(sat_conversion,[],[f1876]) ).
cnf(s394,plain,
( ~ spl0_11
| spl0_74
| spl0_76
| ~ spl0_156 ),
inference(sat_conversion,[],[f1888]) ).
cnf(s407,plain,
( ~ spl0_7
| ~ spl0_140
| ~ spl0_141
| ~ spl0_142 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s420,plain,
( ~ spl0_6
| ~ spl0_122
| ~ spl0_123
| spl0_155 ),
inference(sat_conversion,[],[f1960]) ).
cnf(s423,plain,
( ~ spl0_8
| spl0_93
| ~ spl0_132
| spl0_160 ),
inference(sat_conversion,[],[f1963]) ).
cnf(s424,plain,
( ~ spl0_8
| spl0_69
| spl0_70
| ~ spl0_111 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s425,plain,
( ~ spl0_16
| spl0_75
| spl0_76
| spl0_156 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s436,plain,
( ~ spl0_5
| spl0_85
| ~ spl0_126
| ~ spl0_163 ),
inference(sat_conversion,[],[f1976]) ).
cnf(s454,plain,
( ~ spl0_12
| ~ spl0_16
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f2024]) ).
cnf(s462,plain,
( ~ spl0_9
| ~ spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f2113]) ).
cnf(s474,plain,
( spl0_2
| ~ spl0_4
| ~ spl0_35 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s475,plain,
( spl0_2
| ~ spl0_6
| ~ spl0_35 ),
inference(sat_conversion,[],[f2237]) ).
cnf(s476,plain,
( ~ spl0_15
| spl0_72
| spl0_73
| ~ spl0_114 ),
inference(sat_conversion,[],[f2238]) ).
cnf(s484,plain,
( ~ spl0_2
| spl0_93
| ~ spl0_132
| ~ spl0_160 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s489,plain,
( ~ spl0_12
| spl0_82
| ~ spl0_123
| spl0_155 ),
inference(sat_conversion,[],[f2251]) ).
cnf(s499,plain,
( ~ spl0_17
| spl0_79
| ~ spl0_119
| spl0_154 ),
inference(sat_conversion,[],[f2261]) ).
cnf(s503,plain,
( ~ spl0_21
| ~ spl0_122
| ~ spl0_123
| ~ spl0_155 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s526,plain,
( ~ spl0_12
| spl0_93
| ~ spl0_133
| spl0_160 ),
inference(sat_conversion,[],[f2356]) ).
cnf(s539,plain,
( ~ spl0_35
| spl0_75
| spl0_76
| ~ spl0_156 ),
inference(sat_conversion,[],[f2439]) ).
cnf(s542,plain,
( spl0_19
| ~ spl0_23
| ~ spl0_35 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s545,plain,
( ~ spl0_14
| spl0_81
| ~ spl0_120
| ~ spl0_121 ),
inference(sat_conversion,[],[f2445]) ).
cnf(s547,plain,
( ~ spl0_17
| spl0_72
| spl0_73
| ~ spl0_171 ),
inference(sat_conversion,[],[f2447]) ).
cnf(s548,plain,
( ~ spl0_18
| spl0_72
| spl0_73
| spl0_171 ),
inference(sat_conversion,[],[f2448]) ).
cnf(s550,plain,
( ~ spl0_23
| spl0_72
| ~ spl0_114
| spl0_171 ),
inference(sat_conversion,[],[f2450]) ).
cnf(s554,plain,
( ~ spl0_14
| ~ spl0_21
| ~ spl0_106
| ~ spl0_107 ),
inference(sat_conversion,[],[f2553]) ).
cnf(s560,plain,
( ~ spl0_4
| ~ spl0_132
| ~ spl0_133
| ~ spl0_160 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s567,plain,
( ~ spl0_14
| spl0_85
| ~ spl0_125
| ~ spl0_163 ),
inference(sat_conversion,[],[f2566]) ).
cnf(s569,plain,
( ~ spl0_42
| spl0_74
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f2666]) ).
cnf(s572,plain,
( ~ spl0_43
| ~ spl0_149
| ~ spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f2687]) ).
cnf(s573,plain,
( ~ spl0_4
| ~ spl0_14
| spl0_43 ),
inference(sat_conversion,[],[f2688]) ).
cnf(s585,plain,
( ~ spl0_2
| ~ spl0_125
| ~ spl0_126
| spl0_163 ),
inference(sat_conversion,[],[f2695]) ).
cnf(s589,plain,
( ~ spl0_2
| spl0_78
| ~ spl0_117
| ~ spl0_118 ),
inference(sat_conversion,[],[f2699]) ).
cnf(s593,plain,
( ~ spl0_50
| spl0_62
| ~ spl0_106
| ~ spl0_107 ),
inference(sat_conversion,[],[f2820]) ).
cnf(s601,plain,
( ~ spl0_5
| spl0_80
| ~ spl0_119
| ~ spl0_154 ),
inference(sat_conversion,[],[f2828]) ).
cnf(s606,plain,
( ~ spl0_8
| spl0_94
| ~ spl0_134
| spl0_161 ),
inference(sat_conversion,[],[f2833]) ).
cnf(s614,plain,
( ~ spl0_13
| spl0_94
| spl0_95
| ~ spl0_134 ),
inference(sat_conversion,[],[f2837]) ).
cnf(s626,plain,
( ~ spl0_29
| spl0_92
| ~ spl0_130
| ~ spl0_159 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s633,plain,
( ~ spl0_36
| ~ spl0_130
| ~ spl0_131
| spl0_159 ),
inference(sat_conversion,[],[f2855]) ).
cnf(s634,plain,
( ~ spl0_36
| spl0_73
| ~ spl0_114
| ~ spl0_171 ),
inference(sat_conversion,[],[f2856]) ).
cnf(s643,plain,
spl0_3,
inference(rat,[],[s141,s162,s175,s180]) ).
cnf(s644,plain,
( spl0_14
| spl0_13
| spl0_35 ),
inference(rat,[],[s476,s62,s63,s101,s7,s20,s643]) ).
cnf(s645,plain,
( spl0_34
| ~ spl0_15 ),
inference(rat,[],[s476,s62,s63,s101]) ).
cnf(s646,plain,
( spl0_30
| ~ spl0_10
| ~ spl0_4 ),
inference(rat,[],[s232,s104,s105]) ).
cnf(s647,plain,
( spl0_32
| ~ spl0_17 ),
inference(rat,[],[s245,s55,s56,s96]) ).
cnf(s648,plain,
( spl0_18
| ~ spl0_32
| ~ spl0_14 ),
inference(rat,[],[s554,s93,s94,s18,s48,s643]) ).
cnf(s650,plain,
( spl0_54
| ~ spl0_12
| ~ spl0_4 ),
inference(rat,[],[s526,s560,s83,s119,s120]) ).
cnf(s654,plain,
( spl0_53
| ~ spl0_9 ),
inference(rat,[],[s237,s69,s70,s106]) ).
cnf(s656,plain,
( spl0_33
| ~ spl0_14 ),
inference(rat,[],[s545,s71,s107,s108]) ).
cnf(s657,plain,
( spl0_54
| ~ spl0_4
| spl0_2 ),
inference(rat,[],[s6,s423,s560,s650,s83,s119,s120,s643]) ).
cnf(s660,plain,
( spl0_150
| ~ spl0_43 ),
inference(rat,[],[s572,s136,s137,s138]) ).
cnf(s662,plain,
( spl0_24
| ~ spl0_19 ),
inference(rat,[],[s306,s76,s77,s114]) ).
cnf(s663,plain,
( spl0_10
| spl0_17
| spl0_18
| ~ spl0_33 ),
inference(rat,[],[s299,s425,s64,s65,s66,s37,s662,s9,s462,s19,s8,s357,s72,s109,s110,s43,s593,s52,s93,s94,s48,s643]) ).
cnf(s664,plain,
( ~ spl0_4
| spl0_2 ),
inference(rat,[],[s325,s73,s74,s111,s38,s42,s646,s663,s357,s72,s109,s110,s43,s593,s647,s52,s93,s94,s648,s48,s246,s49,s50,s51,s146,s660,s657,s656,s573,s644,s203,s474,s643]) ).
cnf(s665,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s664,s1,s643]) ).
cnf(s666,plain,
( spl0_30
| ~ spl0_2 ),
inference(rat,[],[s589,s68,s104,s105]) ).
cnf(s667,plain,
( spl0_31
| ~ spl0_14
| ~ spl0_2 ),
inference(rat,[],[s567,s585,s75,s112,s113]) ).
cnf(s668,plain,
( spl0_54
| ~ spl0_31
| ~ spl0_4 ),
inference(rat,[],[s17,s359,s650,s83,s119,s120,s643]) ).
cnf(s669,plain,
( ~ spl0_14
| ~ spl0_32
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s246,s49,s50,s51,s146,s668,s667,s660,s648,s573]) ).
cnf(s670,plain,
( spl0_34
| ~ spl0_23
| ~ spl0_17 ),
inference(rat,[],[s547,s550,s62,s63,s101]) ).
cnf(s671,plain,
( ~ spl0_54
| spl0_14
| ~ spl0_17
| ~ spl0_30 ),
inference(rat,[],[s325,s73,s74,s111,s38,s357,s72,s109,s110,s46,s247,s539,s20,s670,s64,s65,s66,s42,s145,s647,s643]) ).
cnf(s672,plain,
( spl0_54
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s407,s127,s128,s129,s39,s654,s2,s4,s436,s205,s585,s75,s112,s113,s359,s668,s83,s119,s120,s643]) ).
cnf(s673,plain,
( spl0_37
| ~ spl0_23 ),
inference(rat,[],[s325,s73,s74,s111]) ).
cnf(s674,plain,
( ~ spl0_14
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s23,s654,s647,s143,s669,s656,s673,s42,s672,s666,s643]) ).
cnf(s675,plain,
( ~ spl0_55
| ~ spl0_25 ),
inference(rat,[],[s357,s72,s109,s110]) ).
cnf(s676,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(rat,[],[s593,s52,s93,s94]) ).
cnf(s677,plain,
( spl0_34
| ~ spl0_36
| ~ spl0_23 ),
inference(rat,[],[s634,s550,s62,s63,s101]) ).
cnf(s678,plain,
( ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s614,s84,s85,s121,s144,s662,s542,s20,s677,s7,s21,s462,s23,s671,s674,s673,s42,s672,s666,s643]) ).
cnf(s679,plain,
( ~ spl0_46
| spl0_1 ),
inference(rat,[],[s606,s382,s84,s121,s3,s678,s665,s643]) ).
cnf(s680,plain,
( ~ spl0_41
| ~ spl0_29 ),
inference(rat,[],[s336,s61,s99,s100]) ).
cnf(s681,plain,
( spl0_54
| spl0_1 ),
inference(rat,[],[s484,s423,s83,s119,s3,s678,s665,s643]) ).
cnf(s682,plain,
spl0_1,
inference(rat,[],[s20,s656,s677,s143,s21,s654,s462,s23,s647,s142,s676,s542,s43,s662,s675,s144,s38,s673,s42,s681,s679,s666,s665,s643]) ).
cnf(s683,plain,
( spl0_37
| ~ spl0_18 ),
inference(rat,[],[s258,s271,s73,s74,s111,s682]) ).
cnf(s684,plain,
( ~ spl0_17
| ~ spl0_14
| spl0_10 ),
inference(rat,[],[s601,s4,s499,s654,s69,s70,s106,s143,s683,s648,s647,s656,s643]) ).
cnf(s686,plain,
( spl0_28
| ~ spl0_16
| spl0_2 ),
inference(rat,[],[s6,s454,s424,s59,s60,s98,s643]) ).
cnf(s687,plain,
( ~ spl0_11
| ~ spl0_18
| spl0_4 ),
inference(rat,[],[s247,s394,s64,s65,s66,s13,s614,s84,s85,s121,s144,s662,s235,s683,s643,s682]) ).
cnf(s688,plain,
( ~ spl0_22
| spl0_35
| ~ spl0_28
| ~ spl0_18 ),
inference(rat,[],[s15,s680,s299,s26,s247,s569,s64,s65,s66,s643]) ).
cnf(s689,plain,
( ~ spl0_39
| ~ spl0_18 ),
inference(rat,[],[s246,s49,s50,s51]) ).
cnf(s690,plain,
( ~ spl0_14
| spl0_2 ),
inference(rat,[],[s359,s83,s119,s120,s146,s689,s660,s27,s688,s475,s5,s687,s686,s663,s8,s684,s656,s236,s664,s643,s682]) ).
cnf(s691,plain,
( spl0_18
| ~ spl0_32
| spl0_2 ),
inference(rat,[],[s6,s184,s489,s503,s72,s109,s110,s18,s46,s643]) ).
cnf(s692,plain,
( ~ spl0_17
| spl0_2 ),
inference(rat,[],[s548,s547,s62,s63,s20,s475,s5,s687,s691,s647,s664,s690,s643]) ).
cnf(s693,plain,
( ~ spl0_18
| spl0_2 ),
inference(rat,[],[s634,s21,s548,s645,s62,s63,s101,s20,s475,s5,s687,s664,s690,s643]) ).
cnf(s694,plain,
( ~ spl0_6
| spl0_2 ),
inference(rat,[],[s299,s425,s15,s64,s65,s66,s626,s11,s633,s677,s21,s645,s503,s20,s420,s475,s690,s110,s109,s43,s118,s117,s82,s34,s676,s48,s693,s686,s8,s692,s236,s643,s682]) ).
cnf(s695,plain,
spl0_2,
inference(rat,[],[s425,s394,s64,s65,s66,s37,s662,s235,s5,s694,s675,s43,s676,s48,s693,s8,s692,s236,s643,s682]) ).
cnf(s696,plain,
spl0_30,
inference(rat,[],[s666,s695]) ).
cnf(s698,plain,
( ~ spl0_32
| ~ spl0_14 ),
inference(rat,[],[s43,s676,s675,s142,s38,s683,s648,s696,s643]) ).
cnf(s699,plain,
~ spl0_14,
inference(rat,[],[s526,s17,s484,s359,s83,s119,s120,s42,s673,s143,s654,s23,s647,s698,s667,s656,s643,s695,s696]) ).
cnf(s700,plain,
( spl0_12
| spl0_6 ),
inference(rat,[],[s407,s127,s128,s129,s39,s654,s4,s2,s436,s205,s585,s75,s112,s113,s17,s695,s643]) ).
cnf(s701,plain,
( ~ spl0_132
| spl0_93
| ~ spl0_133 ),
inference(rat,[],[s700,s526,s484,s359,s695]) ).
cnf(s702,plain,
spl0_54,
inference(rat,[],[s701,s83,s119,s120]) ).
cnf(s703,plain,
spl0_23,
inference(rat,[],[s42,s696,s643,s702]) ).
cnf(s704,plain,
~ spl0_17,
inference(rat,[],[s671,s696,s699,s702]) ).
cnf(s705,plain,
spl0_37,
inference(rat,[],[s673,s703]) ).
cnf(s706,plain,
spl0_9,
inference(rat,[],[s23,s696,s643,s704]) ).
cnf(s709,plain,
~ spl0_15,
inference(rat,[],[s462,s704,s706]) ).
cnf(s712,plain,
spl0_36,
inference(rat,[],[s21,s643,s709]) ).
cnf(s713,plain,
spl0_13,
inference(rat,[],[s7,s699,s643,s709]) ).
cnf(s716,plain,
spl0_34,
inference(rat,[],[s677,s703,s712]) ).
cnf(s721,plain,
spl0_35,
inference(rat,[],[s20,s699,s643,s716]) ).
cnf(s724,plain,
spl0_19,
inference(rat,[],[s542,s703,s721]) ).
cnf(s730,plain,
spl0_24,
inference(rat,[],[s662,s724]) ).
cnf(s732,plain,
spl0_46,
inference(rat,[],[s144,s705,s730]) ).
cnf(s737,plain,
spl0_134,
inference(rat,[],[s121,s732]) ).
cnf(s738,plain,
~ spl0_95,
inference(rat,[],[s85,s732]) ).
cnf(s739,plain,
~ spl0_94,
inference(rat,[],[s84,s732]) ).
cnf(s740,plain,
$false,
inference(rat,[],[s614,s737,s713,s738,s739]) ).
fof(f2865,plain,
$false,
inference(avatar_sat_refutation,[],[s740]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN454-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n003.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 16:06:57 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.32 % (1723667)Will run a generic schedule for satisfiability detection.
% 0.20/0.32 % (1723684)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=795355055:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.32 % (1723683)% WARNING: option uhcvi not known.
% 0.20/0.32 % (1723685)dis+10_1_sil=32000:sp=arity:random_seed=2979269480:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.32 % (1723683)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1928905056:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.32 % (1723682)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3917868194_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.32 % (1723686)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=588814303:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.32 % (1723687)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1514250777:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.32 % (1723688)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3706356385:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.32 % Detected minimum model sizes of [1]
% 0.20/0.32 % Detected maximum model sizes of [30]
% 0.20/0.32 % TRYING [1]
% 0.20/0.32 % TRYING [2]
% 0.20/0.32 % TRYING [3]
% 0.20/0.32 % TRYING [4]
% 0.20/0.32 % (1723688) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1723667-1723688"...
% 0.20/0.32 % (1723688)...printing done.
% 0.20/0.32 % (1723688)Refutation found. Thanks to Tanya!
% 0.20/0.32 % SZS status Unsatisfiable for theBenchmark
% 0.20/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.33 % (1723688)------------------------------
% 0.20/0.33 % (1723688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.33 % (1723688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.33 % (1723688)CaDiCaL version: 2.1.3
% 0.20/0.33 % (1723688)Termination reason: Refutation
% 0.20/0.33 % (1723688)Time elapsed: 0.035 s
% 0.20/0.33 % (1723688)Peak memory usage: 13 MB
% 0.20/0.33 % (1723688)Instructions burned: 57 (million)
% 0.20/0.33 % (1723667)Success in time 0.08 s
% 0.20/0.33 % Vampire exiting
%------------------------------------------------------------------------------