%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN471-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:53:48 PM UTC 2026
% Result : Unsatisfiable 0.65s 1.00s
% Output : Refutation 2.84s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp9
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( ~ hskp31
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f9,negated_conjecture,
( ~ hskp24
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
fof(f32,negated_conjecture,
( ~ hskp1
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
fof(f34,negated_conjecture,
( hskp30
| hskp3
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f36,negated_conjecture,
( hskp1
| hskp31
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( hskp1
| hskp21
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( hskp10
| hskp28
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
( hskp10
| hskp9
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( hskp10
| hskp12
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f42,negated_conjecture,
( ~ hskp31
| c0_1(a672) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp31
| c2_1(a672) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f45,negated_conjecture,
( ~ hskp30
| c0_1(a637) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp30
| c1_1(a637) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp30
| c2_1(a637) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp29
| c0_1(a618) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp29
| c1_1(a618) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp29
| c3_1(a618) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp28
| c1_1(a595) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp28
| c2_1(a595) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp28
| c3_1(a595) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp25
| c1_1(a656) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( ~ hskp25
| c3_1(a656) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( ~ hskp24
| c1_1(a651) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp24
| c3_1(a651) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f59,negated_conjecture,
( ~ hskp21
| c0_1(a631) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp21
| c3_1(a631) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp20
| c0_1(a630) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp20
| c3_1(a630) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f64,negated_conjecture,
( ~ hskp18
| c3_1(a625) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp17
| c0_1(a624) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f67,negated_conjecture,
( ~ hskp16
| c1_1(a620) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp15
| c0_1(a619) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp14
| c0_1(a615) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp14
| c2_1(a615) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp13
| c1_1(a614) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp12
| c2_1(a609) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp11
| c1_1(a608) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp10
| c0_1(a605) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp10
| c2_1(a605) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp9
| c1_1(a604) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp9
| c2_1(a604) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp8
| c0_1(a603) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp7
| c2_1(a602) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp7
| c3_1(a602) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp6
| c3_1(a600) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp5
| c2_1(a599) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp5
| c3_1(a599) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ hskp3
| c1_1(a597) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ hskp3
| c2_1(a597) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ hskp2
| c2_1(a596) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ hskp1
| c0_1(a594) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp1
| c1_1(a594) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ hskp0
| c2_1(a593) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f93,negated_conjecture,
( ~ c0_1(a667)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f95,negated_conjecture,
( ~ c3_1(a667)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c0_1(a656)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c2_1(a651)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f100,negated_conjecture,
( ~ c0_1(a644)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c2_1(a644)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f103,negated_conjecture,
( ~ c1_1(a631)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c2_1(a630)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f107,negated_conjecture,
( ~ c0_1(a625)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c1_1(a625)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c2_1(a624)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c0_1(a620)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c2_1(a620)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f114,negated_conjecture,
( ~ c1_1(a615)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c2_1(a614)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c3_1(a614)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c1_1(a609)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c3_1(a609)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c0_1(a608)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c3_1(a608)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c3_1(a605)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c0_1(a604)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c1_1(a603)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f125,negated_conjecture,
( ~ c0_1(a602)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c1_1(a600)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c2_1(a600)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ c1_1(a599)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( ~ c0_1(a598)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ c1_1(a598)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( ~ c2_1(a598)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ c3_1(a597)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( ~ c0_1(a596)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
( ~ c1_1(a596)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
( ~ c3_1(a594)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
( ~ c0_1(a593)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( ~ c3_1(a593)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f142,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp10
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp28
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp17
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause144) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp14
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp15
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp14
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp13
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f154,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp4
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f156,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp29
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp10
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp28
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f161,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp28
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp5
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
fof(f166,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c2_1(X1)
| c3_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| c2_1(X1)
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
fof(f182,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f184,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause186) ).
fof(f188,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f190,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X0)
| c0_1(X2)
| c2_1(X2)
| c3_1(X2)
| c0_1(X1)
| c1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f191,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause191) ).
fof(f192,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X2)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause192) ).
fof(f194,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X2)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause196) ).
fof(f197,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c0_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause197) ).
fof(f198,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause198) ).
fof(f199,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| c0_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause200) ).
fof(f202,definition,
( spl0_1
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f203,plain,
( ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c2_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f206,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f212,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f213,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f214,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f200,f212,f208,f205,f202]) ).
fof(f216,definition,
( spl0_5
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f217,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f219,definition,
( spl0_6
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f220,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f222,definition,
( spl0_7
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f223,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f224,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f199,f222,f208,f219,f216]) ).
fof(f226,definition,
( spl0_8
<=> ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f227,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f228,plain,
( spl0_8
| spl0_1
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f198,f205,f208,f202,f226]) ).
fof(f230,definition,
( spl0_9
<=> ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f231,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| ~ c0_1(X2) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f233,definition,
( spl0_10
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f234,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f235,plain,
( spl0_9
| spl0_1
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f197,f233,f208,f202,f230]) ).
fof(f237,definition,
( spl0_11
<=> ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f238,plain,
( ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f240,definition,
( spl0_12
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f241,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f242,plain,
( spl0_11
| spl0_12
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f196,f212,f208,f240,f237]) ).
fof(f244,definition,
( spl0_13
<=> ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f245,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f247,definition,
( spl0_14
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f248,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f249,plain,
( spl0_13
| spl0_8
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f195,f247,f208,f226,f244]) ).
fof(f251,definition,
( spl0_15
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f252,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f253,plain,
( spl0_15
| spl0_10
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f194,f205,f208,f233,f251]) ).
fof(f255,definition,
( spl0_16
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f256,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f258,definition,
( spl0_17
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f259,plain,
( ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f262,definition,
( spl0_18
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f263,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f265,definition,
( spl0_19
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f266,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f267,plain,
( spl0_13
| spl0_18
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f192,f265,f208,f262,f244]) ).
fof(f269,definition,
( spl0_20
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f270,plain,
( ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f271,plain,
( spl0_20
| spl0_13
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f191,f212,f208,f244,f269]) ).
fof(f272,plain,
( spl0_16
| spl0_13
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f190,f226,f208,f244,f255]) ).
fof(f273,plain,
( spl0_15
| spl0_17
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f189,f247,f208,f258,f251]) ).
fof(f275,definition,
( spl0_21
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f276,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f277,plain,
( spl0_15
| spl0_13
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f188,f275,f208,f244,f251]) ).
fof(f279,definition,
( spl0_22
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f284,definition,
( spl0_23
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f287,plain,
( spl0_23
| spl0_19
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f186,f212,f208,f265,f284]) ).
fof(f289,definition,
( spl0_24
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f293,definition,
( spl0_25
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f294,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f295,plain,
( spl0_24
| spl0_25
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f185,f205,f208,f293,f289]) ).
fof(f297,definition,
( spl0_26
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f300,plain,
( spl0_26
| spl0_8
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f184,f205,f208,f226,f297]) ).
fof(f302,definition,
( spl0_27
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f307,definition,
( spl0_28
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f310,plain,
( spl0_28
| spl0_17
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f182,f212,f208,f258,f307]) ).
fof(f312,definition,
( spl0_29
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f317,definition,
( spl0_30
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f321,definition,
( spl0_31
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f322,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f323,plain,
( spl0_30
| spl0_31
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f180,f293,f208,f321,f317]) ).
fof(f325,definition,
( spl0_32
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f326,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f327,plain,
( spl0_24
| spl0_12
| ~ spl0_3
| spl0_32 ),
inference(avatar_split_clause,[],[f179,f325,f208,f240,f289]) ).
fof(f329,definition,
( spl0_33
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f332,plain,
( spl0_33
| spl0_5
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f178,f247,f208,f216,f329]) ).
fof(f334,definition,
( spl0_34
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f337,plain,
( spl0_34
| spl0_11
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f177,f222,f208,f237,f334]) ).
fof(f339,definition,
( spl0_35
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f342,plain,
( spl0_35
| spl0_11
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f176,f212,f208,f237,f339]) ).
fof(f343,plain,
( spl0_15
| spl0_20
| spl0_16
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f175,f208,f255,f269,f251]) ).
fof(f344,plain,
( spl0_26
| spl0_17
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f174,f293,f208,f258,f297]) ).
fof(f346,definition,
( spl0_36
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f349,plain,
( spl0_36
| spl0_9
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f173,f258,f208,f230,f346]) ).
fof(f351,definition,
( spl0_37
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f352,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f353,plain,
( spl0_30
| spl0_37
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f172,f247,f208,f351,f317]) ).
fof(f355,definition,
( spl0_38
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f356,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f358,definition,
( spl0_39
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f359,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f360,plain,
( spl0_30
| spl0_38
| ~ spl0_3
| spl0_39 ),
inference(avatar_split_clause,[],[f171,f358,f208,f355,f317]) ).
fof(f362,definition,
( spl0_40
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f365,plain,
( spl0_40
| spl0_18
| ~ spl0_3
| spl0_39 ),
inference(avatar_split_clause,[],[f170,f358,f208,f262,f362]) ).
fof(f367,definition,
( spl0_41
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f370,plain,
( spl0_41
| spl0_18
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f169,f230,f208,f262,f367]) ).
fof(f372,definition,
( spl0_42
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f375,plain,
( spl0_42
| spl0_16
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f168,f205,f208,f255,f372]) ).
fof(f377,definition,
( spl0_43
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f378,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f379,plain,
( spl0_41
| spl0_43
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f167,f230,f208,f377,f367]) ).
fof(f381,definition,
( spl0_44
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f385,definition,
( spl0_45
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f386,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f387,plain,
( spl0_44
| spl0_38
| ~ spl0_3
| spl0_45 ),
inference(avatar_split_clause,[],[f166,f385,f208,f355,f381]) ).
fof(f389,definition,
( spl0_46
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f394,definition,
( spl0_47
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f397,plain,
( spl0_47
| spl0_15
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f164,f275,f208,f251,f394]) ).
fof(f399,definition,
( spl0_48
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f402,plain,
( spl0_48
| spl0_16
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f163,f262,f208,f255,f399]) ).
fof(f403,plain,
( spl0_24
| spl0_48
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f162,f222,f208,f399,f289]) ).
fof(f405,definition,
( spl0_49
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f408,plain,
( spl0_49
| spl0_40
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f161,f212,f208,f362,f405]) ).
fof(f410,definition,
( spl0_50
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f415,definition,
( spl0_51
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f420,definition,
( spl0_52
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f423,plain,
( spl0_52
| spl0_40
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f158,f275,f208,f362,f420]) ).
fof(f424,plain,
( spl0_48
| spl0_34
| ~ spl0_3
| spl0_39 ),
inference(avatar_split_clause,[],[f157,f358,f208,f334,f399]) ).
fof(f426,definition,
( spl0_53
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f429,plain,
( spl0_53
| spl0_26
| ~ spl0_3
| spl0_39 ),
inference(avatar_split_clause,[],[f156,f358,f208,f297,f426]) ).
fof(f435,plain,
( spl0_51
| spl0_52
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f154,f293,f208,f420,f415]) ).
fof(f438,definition,
( spl0_55
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f439,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f440,plain,
( spl0_30
| spl0_33
| ~ spl0_3
| spl0_55 ),
inference(avatar_split_clause,[],[f152,f438,f208,f329,f317]) ).
fof(f441,plain,
( spl0_48
| spl0_27
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f151,f230,f208,f302,f399]) ).
fof(f443,definition,
( spl0_56
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f446,plain,
( spl0_50
| spl0_56
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f150,f226,f208,f443,f410]) ).
fof(f447,plain,
( spl0_46
| spl0_27
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f149,f219,f208,f302,f389]) ).
fof(f449,definition,
( spl0_57
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f452,plain,
( spl0_57
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f148,f275,f208,f449]) ).
fof(f453,plain,
( spl0_27
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f147,f275,f208,f302]) ).
fof(f461,definition,
( spl0_59
<=> ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f462,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f463,plain,
( spl0_24
| spl0_22
| ~ spl0_3
| spl0_59 ),
inference(avatar_split_clause,[],[f144,f461,f208,f279,f289]) ).
fof(f464,plain,
( spl0_42
| spl0_40
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f143,f355,f208,f362,f372]) ).
fof(f465,plain,
( spl0_48
| spl0_34
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f142,f355,f208,f334,f399]) ).
fof(f468,definition,
( spl0_60
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f478,definition,
( spl0_62
<=> c3_1(a593) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f480,plain,
( ~ c3_1(a593)
| spl0_62 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f481,plain,
( ~ spl0_47
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f137,f478,f394]) ).
fof(f483,definition,
( spl0_63
<=> c0_1(a593) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f485,plain,
( ~ c0_1(a593)
| spl0_63 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f486,plain,
( ~ spl0_47
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f136,f483,f394]) ).
fof(f488,definition,
( spl0_64
<=> c3_1(a594) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f490,plain,
( ~ c3_1(a594)
| spl0_64 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f491,plain,
( ~ spl0_41
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f135,f488,f367]) ).
fof(f493,definition,
( spl0_65
<=> c1_1(a596) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f495,plain,
( ~ c1_1(a596)
| spl0_65 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f496,plain,
( ~ spl0_49
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f134,f493,f405]) ).
fof(f498,definition,
( spl0_66
<=> c0_1(a596) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f500,plain,
( ~ c0_1(a596)
| spl0_66 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f501,plain,
( ~ spl0_49
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f133,f498,f405]) ).
fof(f503,definition,
( spl0_67
<=> c3_1(a597) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f505,plain,
( ~ c3_1(a597)
| spl0_67 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f506,plain,
( ~ spl0_60
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f132,f503,f468]) ).
fof(f508,definition,
( spl0_68
<=> c2_1(a598) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f510,plain,
( ~ c2_1(a598)
| spl0_68 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
( ~ spl0_52
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f131,f508,f420]) ).
fof(f513,definition,
( spl0_69
<=> c1_1(a598) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f515,plain,
( ~ c1_1(a598)
| spl0_69 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f516,plain,
( ~ spl0_52
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f130,f513,f420]) ).
fof(f518,definition,
( spl0_70
<=> c0_1(a598) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f520,plain,
( ~ c0_1(a598)
| spl0_70 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f521,plain,
( ~ spl0_52
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f129,f518,f420]) ).
fof(f523,definition,
( spl0_71
<=> c1_1(a599) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f525,plain,
( ~ c1_1(a599)
| spl0_71 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f526,plain,
( ~ spl0_48
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f128,f523,f399]) ).
fof(f528,definition,
( spl0_72
<=> c2_1(a600) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f530,plain,
( ~ c2_1(a600)
| spl0_72 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f531,plain,
( ~ spl0_53
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f127,f528,f426]) ).
fof(f533,definition,
( spl0_73
<=> c1_1(a600) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f535,plain,
( ~ c1_1(a600)
| spl0_73 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f536,plain,
( ~ spl0_53
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f126,f533,f426]) ).
fof(f538,definition,
( spl0_74
<=> c0_1(a602) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f539,plain,
( c0_1(a602)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( ~ c0_1(a602)
| spl0_74 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f541,plain,
( ~ spl0_42
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f125,f538,f372]) ).
fof(f548,definition,
( spl0_76
<=> c1_1(a603) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f550,plain,
( ~ c1_1(a603)
| spl0_76 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f551,plain,
( ~ spl0_46
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f123,f548,f389]) ).
fof(f553,definition,
( spl0_77
<=> c0_1(a604) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f555,plain,
( ~ c0_1(a604)
| spl0_77 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f556,plain,
( ~ spl0_35
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f122,f553,f339]) ).
fof(f558,definition,
( spl0_78
<=> c3_1(a605) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f560,plain,
( ~ c3_1(a605)
| spl0_78 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f561,plain,
( ~ spl0_34
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f121,f558,f334]) ).
fof(f563,definition,
( spl0_79
<=> c3_1(a608) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f565,plain,
( ~ c3_1(a608)
| spl0_79 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f566,plain,
( ~ spl0_44
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f120,f563,f381]) ).
fof(f568,definition,
( spl0_80
<=> c0_1(a608) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f570,plain,
( ~ c0_1(a608)
| spl0_80 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f571,plain,
( ~ spl0_44
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f119,f568,f381]) ).
fof(f573,definition,
( spl0_81
<=> c3_1(a609) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f575,plain,
( ~ c3_1(a609)
| spl0_81 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f576,plain,
( ~ spl0_30
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f118,f573,f317]) ).
fof(f578,definition,
( spl0_82
<=> c1_1(a609) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f580,plain,
( ~ c1_1(a609)
| spl0_82 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f581,plain,
( ~ spl0_30
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f117,f578,f317]) ).
fof(f583,definition,
( spl0_83
<=> c3_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f585,plain,
( ~ c3_1(a614)
| spl0_83 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f586,plain,
( ~ spl0_33
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f116,f583,f329]) ).
fof(f588,definition,
( spl0_84
<=> c2_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f591,plain,
( ~ spl0_33
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f115,f588,f329]) ).
fof(f593,definition,
( spl0_85
<=> c1_1(a615) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f595,plain,
( ~ c1_1(a615)
| spl0_85 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f596,plain,
( ~ spl0_27
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f114,f593,f302]) ).
fof(f608,definition,
( spl0_88
<=> c2_1(a620) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f610,plain,
( ~ c2_1(a620)
| spl0_88 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f611,plain,
( ~ spl0_50
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f111,f608,f410]) ).
fof(f613,definition,
( spl0_89
<=> c0_1(a620) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f615,plain,
( ~ c0_1(a620)
| spl0_89 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f616,plain,
( ~ spl0_50
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f110,f613,f410]) ).
fof(f618,definition,
( spl0_90
<=> c2_1(a624) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f620,plain,
( ~ c2_1(a624)
| spl0_90 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f621,plain,
( ~ spl0_22
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f109,f618,f279]) ).
fof(f623,definition,
( spl0_91
<=> c1_1(a625) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f625,plain,
( ~ c1_1(a625)
| spl0_91 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f626,plain,
( ~ spl0_24
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f108,f623,f289]) ).
fof(f628,definition,
( spl0_92
<=> c0_1(a625) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f630,plain,
( ~ c0_1(a625)
| spl0_92 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f631,plain,
( ~ spl0_24
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f107,f628,f289]) ).
fof(f643,definition,
( spl0_95
<=> c2_1(a630) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f645,plain,
( ~ c2_1(a630)
| spl0_95 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,plain,
( ~ spl0_36
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f104,f643,f346]) ).
fof(f648,definition,
( spl0_96
<=> c1_1(a631) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f650,plain,
( ~ c1_1(a631)
| spl0_96 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f651,plain,
( ~ spl0_29
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f103,f648,f312]) ).
fof(f658,definition,
( spl0_98
<=> c2_1(a644) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f660,plain,
( ~ c2_1(a644)
| spl0_98 ),
inference(avatar_component_clause,[],[f658]) ).
fof(f661,plain,
( ~ spl0_51
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f101,f658,f415]) ).
fof(f663,definition,
( spl0_99
<=> c0_1(a644) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f666,plain,
( ~ spl0_51
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f100,f663,f415]) ).
fof(f678,definition,
( spl0_102
<=> c2_1(a651) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f680,plain,
( ~ c2_1(a651)
| spl0_102 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,plain,
( ~ spl0_23
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f97,f678,f284]) ).
fof(f683,definition,
( spl0_103
<=> c0_1(a656) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f685,plain,
( ~ c0_1(a656)
| spl0_103 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f686,plain,
( ~ spl0_57
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f96,f683,f449]) ).
fof(f688,definition,
( spl0_104
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f692,definition,
( spl0_105
<=> c3_1(a667) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f694,plain,
( ~ c3_1(a667)
| spl0_105 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f695,plain,
( ~ spl0_104
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f95,f692,f688]) ).
fof(f702,definition,
( spl0_107
<=> c0_1(a667) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f705,plain,
( ~ spl0_104
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f93,f702,f688]) ).
fof(f726,definition,
( spl0_112
<=> c2_1(a593) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f728,plain,
( c2_1(a593)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f729,plain,
( spl0_112
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f89,f394,f726]) ).
fof(f731,definition,
( spl0_113
<=> c1_1(a594) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f733,plain,
( c1_1(a594)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f734,plain,
( spl0_113
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f88,f367,f731]) ).
fof(f736,definition,
( spl0_114
<=> c0_1(a594) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f738,plain,
( c0_1(a594)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f739,plain,
( spl0_114
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f87,f367,f736]) ).
fof(f741,definition,
( spl0_115
<=> c2_1(a596) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f743,plain,
( c2_1(a596)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f744,plain,
( spl0_115
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f86,f405,f741]) ).
fof(f746,definition,
( spl0_116
<=> c2_1(a597) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f748,plain,
( c2_1(a597)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f749,plain,
( spl0_116
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f85,f468,f746]) ).
fof(f751,definition,
( spl0_117
<=> c1_1(a597) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f753,plain,
( c1_1(a597)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f754,plain,
( spl0_117
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f84,f468,f751]) ).
fof(f756,definition,
( spl0_118
<=> c3_1(a599) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f758,plain,
( c3_1(a599)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f759,plain,
( spl0_118
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f83,f399,f756]) ).
fof(f761,definition,
( spl0_119
<=> c2_1(a599) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f763,plain,
( c2_1(a599)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f764,plain,
( spl0_119
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f82,f399,f761]) ).
fof(f766,definition,
( spl0_120
<=> c3_1(a600) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f768,plain,
( c3_1(a600)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f769,plain,
( spl0_120
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f81,f426,f766]) ).
fof(f771,definition,
( spl0_121
<=> c3_1(a602) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f773,plain,
( c3_1(a602)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f774,plain,
( spl0_121
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f80,f372,f771]) ).
fof(f776,definition,
( spl0_122
<=> c2_1(a602) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f778,plain,
( c2_1(a602)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f779,plain,
( spl0_122
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f79,f372,f776]) ).
fof(f781,definition,
( spl0_123
<=> c0_1(a603) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f783,plain,
( c0_1(a603)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f784,plain,
( spl0_123
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f78,f389,f781]) ).
fof(f786,definition,
( spl0_124
<=> c2_1(a604) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f788,plain,
( c2_1(a604)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f789,plain,
( spl0_124
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f77,f339,f786]) ).
fof(f791,definition,
( spl0_125
<=> c1_1(a604) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f793,plain,
( c1_1(a604)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f794,plain,
( spl0_125
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f76,f339,f791]) ).
fof(f796,definition,
( spl0_126
<=> c2_1(a605) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f798,plain,
( c2_1(a605)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f799,plain,
( spl0_126
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f75,f334,f796]) ).
fof(f801,definition,
( spl0_127
<=> c0_1(a605) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f803,plain,
( c0_1(a605)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f801]) ).
fof(f804,plain,
( spl0_127
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f74,f334,f801]) ).
fof(f806,definition,
( spl0_128
<=> c1_1(a608) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f808,plain,
( c1_1(a608)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,plain,
( spl0_128
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f73,f381,f806]) ).
fof(f811,definition,
( spl0_129
<=> c2_1(a609) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f813,plain,
( c2_1(a609)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f811]) ).
fof(f814,plain,
( spl0_129
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f72,f317,f811]) ).
fof(f816,definition,
( spl0_130
<=> c1_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f818,plain,
( c1_1(a614)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f819,plain,
( spl0_130
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f71,f329,f816]) ).
fof(f821,definition,
( spl0_131
<=> c2_1(a615) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f823,plain,
( c2_1(a615)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f824,plain,
( spl0_131
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f70,f302,f821]) ).
fof(f826,definition,
( spl0_132
<=> c0_1(a615) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f828,plain,
( c0_1(a615)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f829,plain,
( spl0_132
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f69,f302,f826]) ).
fof(f831,definition,
( spl0_133
<=> c0_1(a619) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f833,plain,
( c0_1(a619)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f834,plain,
( spl0_133
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f68,f443,f831]) ).
fof(f836,definition,
( spl0_134
<=> c1_1(a620) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f838,plain,
( c1_1(a620)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f839,plain,
( spl0_134
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f67,f410,f836]) ).
fof(f846,definition,
( spl0_136
<=> c0_1(a624) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f848,plain,
( c0_1(a624)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f846]) ).
fof(f849,plain,
( spl0_136
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f65,f279,f846]) ).
fof(f851,definition,
( spl0_137
<=> c3_1(a625) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f853,plain,
( c3_1(a625)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f851]) ).
fof(f854,plain,
( spl0_137
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f64,f289,f851]) ).
fof(f861,definition,
( spl0_139
<=> c3_1(a630) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f863,plain,
( c3_1(a630)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f861]) ).
fof(f864,plain,
( spl0_139
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f62,f346,f861]) ).
fof(f866,definition,
( spl0_140
<=> c0_1(a630) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f869,plain,
( spl0_140
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f61,f346,f866]) ).
fof(f871,definition,
( spl0_141
<=> c3_1(a631) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f873,plain,
( c3_1(a631)
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f871]) ).
fof(f874,plain,
( spl0_141
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f60,f312,f871]) ).
fof(f876,definition,
( spl0_142
<=> c0_1(a631) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f878,plain,
( c0_1(a631)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f879,plain,
( spl0_142
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f59,f312,f876]) ).
fof(f886,definition,
( spl0_144
<=> c3_1(a651) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f888,plain,
( c3_1(a651)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f889,plain,
( spl0_144
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f57,f284,f886]) ).
fof(f891,definition,
( spl0_145
<=> c1_1(a651) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f893,plain,
( c1_1(a651)
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f894,plain,
( spl0_145
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f56,f284,f891]) ).
fof(f896,definition,
( spl0_146
<=> c3_1(a656) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f899,plain,
( spl0_146
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f55,f449,f896]) ).
fof(f901,definition,
( spl0_147
<=> c1_1(a656) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f903,plain,
( c1_1(a656)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f904,plain,
( spl0_147
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f54,f449,f901]) ).
fof(f906,definition,
( spl0_148
<=> c3_1(a595) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f908,plain,
( c3_1(a595)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f906]) ).
fof(f909,plain,
( spl0_148
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f53,f362,f906]) ).
fof(f911,definition,
( spl0_149
<=> c2_1(a595) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f913,plain,
( c2_1(a595)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f911]) ).
fof(f914,plain,
( spl0_149
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f52,f362,f911]) ).
fof(f916,definition,
( spl0_150
<=> c1_1(a595) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f918,plain,
( c1_1(a595)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f919,plain,
( spl0_150
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f51,f362,f916]) ).
fof(f921,definition,
( spl0_151
<=> c3_1(a618) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f923,plain,
( c3_1(a618)
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f924,plain,
( spl0_151
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f50,f297,f921]) ).
fof(f926,definition,
( spl0_152
<=> c1_1(a618) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f928,plain,
( c1_1(a618)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f929,plain,
( spl0_152
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f49,f297,f926]) ).
fof(f931,definition,
( spl0_153
<=> c0_1(a618) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f933,plain,
( c0_1(a618)
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f931]) ).
fof(f934,plain,
( spl0_153
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f48,f297,f931]) ).
fof(f936,definition,
( spl0_154
<=> c2_1(a637) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f938,plain,
( c2_1(a637)
| ~ spl0_154 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f939,plain,
( spl0_154
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f47,f307,f936]) ).
fof(f941,definition,
( spl0_155
<=> c1_1(a637) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f943,plain,
( c1_1(a637)
| ~ spl0_155 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f944,plain,
( spl0_155
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f46,f307,f941]) ).
fof(f946,definition,
( spl0_156
<=> c0_1(a637) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f948,plain,
( c0_1(a637)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f949,plain,
( spl0_156
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f45,f307,f946]) ).
fof(f955,definition,
( spl0_158
<=> hskp31 ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f960,definition,
( spl0_159
<=> c2_1(a672) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f962,plain,
( c2_1(a672)
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f963,plain,
( spl0_159
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f43,f955,f960]) ).
fof(f965,definition,
( spl0_160
<=> c0_1(a672) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f967,plain,
( c0_1(a672)
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f968,plain,
( spl0_160
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f42,f955,f965]) ).
fof(f970,plain,
( spl0_24
| spl0_30
| spl0_34 ),
inference(avatar_split_clause,[],[f40,f334,f317,f289]) ).
fof(f971,plain,
( spl0_30
| spl0_35
| spl0_34 ),
inference(avatar_split_clause,[],[f39,f334,f339,f317]) ).
fof(f972,plain,
( spl0_49
| spl0_40
| spl0_34 ),
inference(avatar_split_clause,[],[f38,f334,f362,f405]) ).
fof(f973,plain,
( spl0_52
| spl0_29
| spl0_41 ),
inference(avatar_split_clause,[],[f37,f367,f312,f420]) ).
fof(f974,plain,
( spl0_23
| spl0_158
| spl0_41 ),
inference(avatar_split_clause,[],[f36,f367,f955,f284]) ).
fof(f976,plain,
( spl0_104
| spl0_60
| spl0_28 ),
inference(avatar_split_clause,[],[f34,f307,f468,f688]) ).
fof(f978,plain,
( spl0_3
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f32,f367,f208]) ).
fof(f1001,plain,
( spl0_3
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f9,f284,f208]) ).
fof(f1008,plain,
( spl0_3
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f2,f955,f208]) ).
fof(f1009,plain,
( spl0_23
| spl0_35 ),
inference(avatar_split_clause,[],[f1,f339,f284]) ).
fof(f1010,plain,
( ! [X2] :
( ~ c3_1(X2)
| ~ c2_1(X2) )
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f227,f213]) ).
fof(f1011,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f234,f223]) ).
fof(f1012,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f245,f220]) ).
fof(f1013,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f248,f213]) ).
fof(f1014,plain,
( ! [X1] :
( c3_1(X1)
| c2_1(X1) )
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f259,f256]) ).
fof(f1015,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f276,f213]) ).
fof(f1016,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f294,f206]) ).
fof(f1017,plain,
( ! [X1] :
( c3_1(X1)
| c0_1(X1) )
| ~ spl0_16
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f356,f256]) ).
fof(f1018,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f359,f223]) ).
fof(f1019,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_12
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f439,f241]) ).
fof(f1033,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f263,f220]) ).
fof(f1035,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_6
| ~ spl0_13
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f356,f1012]) ).
fof(f1036,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f248,f259]) ).
fof(f1037,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f276,f259]) ).
fof(f1054,plain,
( ~ c0_1(a594)
| ~ spl0_2
| ~ spl0_25
| ~ spl0_113 ),
inference(resolution,[],[f1016,f733]) ).
fof(f1055,plain,
( $false
| ~ spl0_2
| ~ spl0_25
| ~ spl0_113
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f1054,f738]) ).
fof(f1056,plain,
( ~ spl0_2
| ~ spl0_25
| ~ spl0_113
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f1055]) ).
fof(f1061,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f322,f206]) ).
fof(f1073,plain,
( ~ c3_1(a618)
| ~ spl0_7
| ~ spl0_39
| ~ spl0_152 ),
inference(resolution,[],[f1018,f928]) ).
fof(f1074,plain,
( ~ c3_1(a656)
| ~ spl0_7
| ~ spl0_39
| ~ spl0_147 ),
inference(resolution,[],[f1018,f903]) ).
fof(f1085,plain,
( c1_1(a599)
| ~ spl0_12
| ~ spl0_55
| ~ spl0_119 ),
inference(resolution,[],[f1019,f763]) ).
fof(f1086,plain,
( c1_1(a596)
| ~ spl0_12
| ~ spl0_55
| ~ spl0_115 ),
inference(resolution,[],[f1019,f743]) ).
fof(f1087,plain,
( $false
| ~ spl0_12
| ~ spl0_55
| spl0_65
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f1086,f495]) ).
fof(f1088,plain,
( ~ spl0_12
| ~ spl0_55
| spl0_65
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f1087]) ).
fof(f1089,plain,
( $false
| ~ spl0_12
| ~ spl0_55
| spl0_71
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f1085,f525]) ).
fof(f1090,plain,
( ~ spl0_12
| ~ spl0_55
| spl0_71
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f1089]) ).
fof(f1112,plain,
( ! [X2] :
( c1_1(X2)
| c0_1(X2) )
| ~ spl0_15
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f252,f378]) ).
fof(f1144,plain,
( c3_1(a605)
| ~ spl0_17
| ~ spl0_21
| ~ spl0_127 ),
inference(resolution,[],[f1037,f803]) ).
fof(f1147,plain,
( c3_1(a594)
| ~ spl0_17
| ~ spl0_21
| ~ spl0_114 ),
inference(resolution,[],[f1037,f738]) ).
fof(f1150,plain,
( $false
| ~ spl0_17
| ~ spl0_21
| spl0_78
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f1144,f560]) ).
fof(f1151,plain,
( ~ spl0_17
| ~ spl0_21
| spl0_78
| ~ spl0_127 ),
inference(avatar_contradiction_clause,[],[f1150]) ).
fof(f1163,plain,
( c0_1(a596)
| ~ spl0_15
| ~ spl0_43
| spl0_65 ),
inference(resolution,[],[f1112,f495]) ).
fof(f1171,plain,
( $false
| ~ spl0_15
| ~ spl0_43
| spl0_65
| spl0_66 ),
inference(forward_subsumption_resolution,[],[f1163,f500]) ).
fof(f1172,plain,
( ~ spl0_15
| ~ spl0_43
| spl0_65
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f1171]) ).
fof(f1175,plain,
( ! [X2] :
( c2_1(X2)
| c0_1(X2) )
| ~ spl0_11
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f252,f238]) ).
fof(f1177,plain,
( c0_1(a644)
| ~ spl0_11
| ~ spl0_15
| spl0_98 ),
inference(resolution,[],[f1175,f660]) ).
fof(f1178,plain,
( c0_1(a598)
| ~ spl0_11
| ~ spl0_15
| spl0_68 ),
inference(resolution,[],[f1175,f510]) ).
fof(f1212,plain,
( ~ c2_1(a637)
| ~ c0_1(a637)
| ~ spl0_2
| ~ spl0_155 ),
inference(resolution,[],[f206,f943]) ).
fof(f1214,plain,
( ~ c2_1(a595)
| ~ c0_1(a595)
| ~ spl0_2
| ~ spl0_150 ),
inference(resolution,[],[f206,f918]) ).
fof(f1219,plain,
( ~ c2_1(a594)
| ~ c0_1(a594)
| ~ spl0_2
| ~ spl0_113 ),
inference(resolution,[],[f206,f733]) ).
fof(f1220,plain,
( ~ c2_1(a594)
| ~ spl0_2
| ~ spl0_113
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f1219,f738]) ).
fof(f1223,plain,
( ~ c0_1(a595)
| ~ spl0_2
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f1214,f913]) ).
fof(f1225,plain,
( ~ c0_1(a637)
| ~ spl0_2
| ~ spl0_154
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f1212,f938]) ).
fof(f1237,plain,
( ! [X1] : ~ c2_1(X1)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_13
| ~ spl0_21
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1035,f1015]) ).
fof(f1262,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_13
| ~ spl0_21
| ~ spl0_38
| ~ spl0_116 ),
inference(resolution,[],[f1237,f748]) ).
fof(f1263,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_13
| ~ spl0_21
| ~ spl0_38
| ~ spl0_116 ),
inference(avatar_contradiction_clause,[],[f1262]) ).
fof(f1273,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f234,f241]) ).
fof(f1275,plain,
( spl0_99
| ~ spl0_11
| ~ spl0_15
| spl0_98 ),
inference(avatar_split_clause,[],[f1177,f658,f251,f237,f663]) ).
fof(f1276,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0) )
| ~ spl0_11
| ~ spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f248,f1175]) ).
fof(f1283,plain,
( spl0_64
| ~ spl0_17
| ~ spl0_21
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f1147,f736,f275,f258,f488]) ).
fof(f1345,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f326,f231]) ).
fof(f1438,plain,
( c3_1(a593)
| ~ spl0_10
| ~ spl0_12
| ~ spl0_112 ),
inference(resolution,[],[f1273,f728]) ).
fof(f1446,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1) )
| ~ spl0_11
| ~ spl0_15
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f294,f1175]) ).
fof(f1453,plain,
( c2_1(a651)
| ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| ~ spl0_144 ),
inference(resolution,[],[f1276,f888]) ).
fof(f1487,plain,
( c2_1(a651)
| ~ spl0_11
| ~ spl0_15
| ~ spl0_25
| ~ spl0_145 ),
inference(resolution,[],[f1446,f893]) ).
fof(f1539,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2) )
| ~ spl0_6
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f231,f1012]) ).
fof(f1547,plain,
( c1_1(a599)
| ~ spl0_6
| ~ spl0_9
| ~ spl0_13
| ~ spl0_118 ),
inference(resolution,[],[f1539,f758]) ).
fof(f1579,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1) )
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f263,f266]) ).
fof(f1612,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0) )
| ~ spl0_6
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f248,f1012]) ).
fof(f1613,plain,
( ! [X2] :
( c2_1(X2)
| c0_1(X2) )
| ~ spl0_6
| ~ spl0_13
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f256,f1012]) ).
fof(f1616,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_6
| ~ spl0_18
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f378,f1033]) ).
fof(f1618,plain,
( ! [X1] : c0_1(X1)
| ~ spl0_6
| ~ spl0_13
| ~ spl0_16
| ~ spl0_18
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f1616,f1613]) ).
fof(f1647,plain,
( $false
| ~ spl0_6
| ~ spl0_13
| ~ spl0_16
| ~ spl0_18
| ~ spl0_43
| spl0_77 ),
inference(resolution,[],[f1618,f555]) ).
fof(f1652,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_16
| ~ spl0_18
| ~ spl0_43
| spl0_77 ),
inference(avatar_contradiction_clause,[],[f1647]) ).
fof(f1718,plain,
( c0_1(a604)
| ~ spl0_6
| ~ spl0_18
| ~ spl0_125 ),
inference(resolution,[],[f1033,f793]) ).
fof(f1722,plain,
( $false
| ~ spl0_6
| ~ spl0_18
| spl0_77
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f1718,f555]) ).
fof(f1723,plain,
( ~ spl0_6
| ~ spl0_18
| spl0_77
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f1722]) ).
fof(f1750,plain,
( c2_1(a630)
| ~ spl0_6
| ~ spl0_13
| ~ spl0_14
| ~ spl0_139 ),
inference(resolution,[],[f1612,f863]) ).
fof(f1753,plain,
( $false
| ~ spl0_6
| ~ spl0_13
| ~ spl0_14
| spl0_95
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f1750,f645]) ).
fof(f1754,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_14
| spl0_95
| ~ spl0_139 ),
inference(avatar_contradiction_clause,[],[f1753]) ).
fof(f1759,plain,
( spl0_71
| ~ spl0_6
| ~ spl0_9
| ~ spl0_13
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f1547,f756,f244,f230,f219,f523]) ).
fof(f1803,plain,
( ! [X1] : c3_1(X1)
| ~ spl0_16
| ~ spl0_17
| ~ spl0_21
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1017,f1037]) ).
fof(f1805,plain,
( ! [X0] : ~ c1_1(X0)
| ~ spl0_7
| ~ spl0_18
| ~ spl0_19
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1018,f1579]) ).
fof(f1806,plain,
( ~ spl0_151
| ~ spl0_7
| ~ spl0_39
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f1073,f926,f358,f222,f921]) ).
fof(f1818,plain,
( $false
| ~ spl0_16
| ~ spl0_17
| ~ spl0_21
| ~ spl0_38
| spl0_81 ),
inference(resolution,[],[f1803,f575]) ).
fof(f1821,plain,
( $false
| ~ spl0_16
| ~ spl0_17
| ~ spl0_21
| ~ spl0_38
| spl0_67 ),
inference(resolution,[],[f1803,f505]) ).
fof(f1830,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_21
| ~ spl0_38
| spl0_67 ),
inference(avatar_contradiction_clause,[],[f1821]) ).
fof(f1833,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_21
| ~ spl0_38
| spl0_81 ),
inference(avatar_contradiction_clause,[],[f1818]) ).
fof(f1850,plain,
( $false
| ~ spl0_7
| ~ spl0_18
| ~ spl0_19
| ~ spl0_39
| ~ spl0_125 ),
inference(resolution,[],[f1805,f793]) ).
fof(f1857,plain,
( ~ spl0_7
| ~ spl0_18
| ~ spl0_19
| ~ spl0_39
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f1850]) ).
fof(f1866,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1) )
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f263,f1037]) ).
fof(f1869,plain,
( ! [X1] : ~ c1_1(X1)
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1866,f1018]) ).
fof(f1878,plain,
( $false
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_39
| ~ spl0_125 ),
inference(resolution,[],[f1869,f793]) ).
fof(f1885,plain,
( ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_39
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f1878]) ).
fof(f1896,plain,
( ! [X0] : ~ c0_1(X0)
| ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1013,f1037]) ).
fof(f1929,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f833,f1896]) ).
fof(f1930,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f1929]) ).
fof(f1931,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_160 ),
inference(resolution,[],[f1896,f967]) ).
fof(f1938,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_132 ),
inference(resolution,[],[f1896,f828]) ).
fof(f1939,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_123 ),
inference(resolution,[],[f1896,f783]) ).
fof(f1940,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_74 ),
inference(resolution,[],[f1896,f539]) ).
fof(f1947,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f1940]) ).
fof(f1948,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f1939]) ).
fof(f1949,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_132 ),
inference(avatar_contradiction_clause,[],[f1938]) ).
fof(f1956,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_160 ),
inference(avatar_contradiction_clause,[],[f1931]) ).
fof(f1959,definition,
( spl0_161
<=> c2_1(a625) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1961,plain,
( ~ c2_1(a625)
| spl0_161 ),
inference(avatar_component_clause,[],[f1959]) ).
fof(f1973,plain,
( ~ c0_1(a651)
| ~ spl0_2
| ~ spl0_25
| ~ spl0_145 ),
inference(resolution,[],[f1016,f893]) ).
fof(f2000,plain,
( ! [X2] :
( c1_1(X2)
| c3_1(X2) )
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f270,f1037]) ).
fof(f2001,plain,
( ! [X2] : c3_1(X2)
| ~ spl0_17
| ~ spl0_18
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2000,f1866]) ).
fof(f2002,plain,
( ~ c0_1(a614)
| ~ spl0_2
| ~ spl0_25
| ~ spl0_130 ),
inference(resolution,[],[f818,f1016]) ).
fof(f2005,plain,
( $false
| ~ spl0_17
| ~ spl0_18
| ~ spl0_20
| ~ spl0_21
| spl0_83 ),
inference(resolution,[],[f2001,f585]) ).
fof(f2006,plain,
( $false
| ~ spl0_17
| ~ spl0_18
| ~ spl0_20
| ~ spl0_21
| spl0_81 ),
inference(resolution,[],[f2001,f575]) ).
fof(f2021,plain,
( ~ spl0_17
| ~ spl0_18
| ~ spl0_20
| ~ spl0_21
| spl0_81 ),
inference(avatar_contradiction_clause,[],[f2006]) ).
fof(f2022,plain,
( ~ spl0_17
| ~ spl0_18
| ~ spl0_20
| ~ spl0_21
| spl0_83 ),
inference(avatar_contradiction_clause,[],[f2005]) ).
fof(f2025,plain,
( ! [X2] :
( ~ c1_1(X2)
| c2_1(X2) )
| ~ spl0_11
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f238,f294]) ).
fof(f2028,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f223,f1866]) ).
fof(f2050,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f206,f1036]) ).
fof(f2051,plain,
( ! [X2] :
( ~ c1_1(X2)
| c2_1(X2) )
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f238,f1036]) ).
fof(f2052,plain,
( ! [X2] : ~ c1_1(X2)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2051,f2028]) ).
fof(f2057,plain,
( $false
| ~ spl0_7
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_125 ),
inference(resolution,[],[f2052,f793]) ).
fof(f2066,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f2057]) ).
fof(f2071,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_7
| ~ spl0_12
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f241,f2028]) ).
fof(f2072,plain,
( ! [X1] : c3_1(X1)
| ~ spl0_7
| ~ spl0_12
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2071,f1014]) ).
fof(f2075,plain,
( $false
| ~ spl0_7
| ~ spl0_12
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| spl0_81 ),
inference(resolution,[],[f2072,f575]) ).
fof(f2080,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| spl0_81 ),
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2081,plain,
( ! [X2] :
( ~ c2_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f217,f378]) ).
fof(f2100,plain,
( c2_1(a614)
| ~ spl0_16
| ~ spl0_17
| spl0_83 ),
inference(resolution,[],[f1014,f585]) ).
fof(f2112,plain,
( c3_1(a614)
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_130 ),
inference(resolution,[],[f1866,f818]) ).
fof(f2117,plain,
( $false
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| spl0_83
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f2112,f585]) ).
fof(f2118,plain,
( ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| spl0_83
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f2117]) ).
fof(f2119,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2) )
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f231,f245]) ).
fof(f2132,plain,
( c2_1(a620)
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_134 ),
inference(resolution,[],[f2051,f838]) ).
fof(f2136,plain,
( $false
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| spl0_88
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2132,f610]) ).
fof(f2137,plain,
( ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| spl0_88
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2136]) ).
fof(f2156,plain,
( c0_1(a602)
| ~ spl0_5
| ~ spl0_43
| ~ spl0_122 ),
inference(resolution,[],[f2081,f778]) ).
fof(f2159,plain,
( c0_1(a593)
| ~ spl0_5
| ~ spl0_43
| ~ spl0_112 ),
inference(resolution,[],[f2081,f728]) ).
fof(f2161,plain,
( $false
| ~ spl0_5
| ~ spl0_43
| spl0_63
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f2159,f485]) ).
fof(f2162,plain,
( ~ spl0_5
| ~ spl0_43
| spl0_63
| ~ spl0_112 ),
inference(avatar_contradiction_clause,[],[f2161]) ).
fof(f2165,plain,
( $false
| ~ spl0_5
| ~ spl0_43
| spl0_74
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f2156,f540]) ).
fof(f2166,plain,
( ~ spl0_5
| ~ spl0_43
| spl0_74
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f2165]) ).
fof(f2191,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f217,f2051]) ).
fof(f2209,plain,
( c1_1(a600)
| ~ spl0_9
| ~ spl0_13
| ~ spl0_120 ),
inference(resolution,[],[f2119,f768]) ).
fof(f2210,plain,
( c1_1(a599)
| ~ spl0_9
| ~ spl0_13
| ~ spl0_118 ),
inference(resolution,[],[f2119,f758]) ).
fof(f2215,plain,
( $false
| ~ spl0_9
| ~ spl0_13
| spl0_71
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f2210,f525]) ).
fof(f2216,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_71
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f2215]) ).
fof(f2229,plain,
( ! [X2] :
( c0_1(X2)
| c3_1(X2) )
| ~ spl0_5
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f270,f2191]) ).
fof(f2231,plain,
( ! [X2] :
( ~ c0_1(X2)
| c1_1(X2) )
| ~ spl0_9
| ~ spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f231,f1037]) ).
fof(f2232,plain,
( ! [X2] : c3_1(X2)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2229,f1037]) ).
fof(f2245,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f575,f2232]) ).
fof(f2246,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| spl0_81 ),
inference(avatar_contradiction_clause,[],[f2245]) ).
fof(f2250,plain,
( ! [X1] : ~ c0_1(X1)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2050,f2231]) ).
fof(f2259,plain,
( c2_1(a651)
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_145 ),
inference(resolution,[],[f893,f2051]) ).
fof(f2260,plain,
( $false
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| spl0_102
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2259,f680]) ).
fof(f2261,plain,
( ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| spl0_102
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f2260]) ).
fof(f2262,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_160 ),
inference(forward_subsumption_resolution,[],[f967,f2250]) ).
fof(f2263,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_160 ),
inference(avatar_contradiction_clause,[],[f2262]) ).
fof(f2332,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f439,f2000]) ).
fof(f2382,plain,
( c3_1(a609)
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| spl0_82 ),
inference(resolution,[],[f2000,f580]) ).
fof(f2405,plain,
( c1_1(a631)
| ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| ~ spl0_142 ),
inference(resolution,[],[f2231,f878]) ).
fof(f2409,plain,
( $false
| ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| spl0_96
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f2405,f650]) ).
fof(f2410,plain,
( ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| spl0_96
| ~ spl0_142 ),
inference(avatar_contradiction_clause,[],[f2409]) ).
fof(f2412,plain,
( spl0_62
| ~ spl0_10
| ~ spl0_12
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1438,f726,f240,f233,f478]) ).
fof(f2439,plain,
( ~ c2_1(a637)
| ~ spl0_7
| ~ spl0_10
| ~ spl0_155 ),
inference(resolution,[],[f1011,f943]) ).
fof(f2440,plain,
( ~ c2_1(a595)
| ~ spl0_7
| ~ spl0_10
| ~ spl0_150 ),
inference(resolution,[],[f1011,f918]) ).
fof(f2445,plain,
( ~ c2_1(a604)
| ~ spl0_7
| ~ spl0_10
| ~ spl0_125 ),
inference(resolution,[],[f1011,f793]) ).
fof(f2462,plain,
( $false
| ~ spl0_7
| ~ spl0_10
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f2440,f913]) ).
fof(f2463,plain,
( ~ spl0_7
| ~ spl0_10
| ~ spl0_149
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f2462]) ).
fof(f2464,plain,
( $false
| ~ spl0_7
| ~ spl0_10
| ~ spl0_154
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f2439,f938]) ).
fof(f2465,plain,
( ~ spl0_7
| ~ spl0_10
| ~ spl0_154
| ~ spl0_155 ),
inference(avatar_contradiction_clause,[],[f2464]) ).
fof(f2501,plain,
( ~ c3_1(a651)
| ~ spl0_7
| ~ spl0_39
| ~ spl0_145 ),
inference(resolution,[],[f1018,f893]) ).
fof(f2511,plain,
( $false
| ~ spl0_7
| ~ spl0_39
| ~ spl0_144
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2501,f888]) ).
fof(f2512,plain,
( ~ spl0_7
| ~ spl0_39
| ~ spl0_144
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f2511]) ).
fof(f2516,plain,
( spl0_84
| ~ spl0_16
| ~ spl0_17
| spl0_83 ),
inference(avatar_split_clause,[],[f2100,f583,f258,f255,f588]) ).
fof(f2521,plain,
( ~ c2_1(a595)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_148 ),
inference(resolution,[],[f1010,f908]) ).
fof(f2531,plain,
( ~ c2_1(a602)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_121 ),
inference(resolution,[],[f1010,f773]) ).
fof(f2533,plain,
( ~ c2_1(a599)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_118 ),
inference(resolution,[],[f1010,f758]) ).
fof(f2538,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_118
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f2533,f763]) ).
fof(f2539,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_118
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f2538]) ).
fof(f2575,plain,
( c3_1(a620)
| c2_1(a620)
| ~ spl0_1
| ~ spl0_134 ),
inference(resolution,[],[f203,f838]) ).
fof(f2576,plain,
( c3_1(a614)
| c2_1(a614)
| ~ spl0_1
| ~ spl0_130 ),
inference(resolution,[],[f203,f818]) ).
fof(f2583,plain,
( c0_1(a595)
| ~ c3_1(a595)
| ~ spl0_6
| ~ spl0_150 ),
inference(resolution,[],[f220,f918]) ).
fof(f2584,plain,
( c0_1(a651)
| ~ c3_1(a651)
| ~ spl0_6
| ~ spl0_145 ),
inference(resolution,[],[f220,f893]) ).
fof(f2585,plain,
( c0_1(a620)
| ~ c3_1(a620)
| ~ spl0_6
| ~ spl0_134 ),
inference(resolution,[],[f220,f838]) ).
fof(f2587,plain,
( c0_1(a604)
| ~ c3_1(a604)
| ~ spl0_6
| ~ spl0_125 ),
inference(resolution,[],[f220,f793]) ).
fof(f2604,plain,
( ~ c0_1(a595)
| ~ spl0_2
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f1214,f913]) ).
fof(f2612,plain,
( ~ c3_1(a651)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2584,f2250]) ).
fof(f2616,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_144
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2612,f888]) ).
fof(f2617,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_144
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f2616]) ).
fof(f2620,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f234,f203]) ).
fof(f2621,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f238,f217]) ).
fof(f2623,plain,
( spl0_81
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| spl0_82 ),
inference(avatar_split_clause,[],[f2382,f578,f275,f269,f258,f573]) ).
fof(f2627,definition,
( spl0_163
<=> c0_1(a614) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f2629,plain,
( c0_1(a614)
| ~ spl0_163 ),
inference(avatar_component_clause,[],[f2627]) ).
fof(f2638,plain,
( ~ c3_1(a604)
| ~ spl0_6
| spl0_77
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f2587,f555]) ).
fof(f2639,plain,
( ~ c3_1(a620)
| ~ spl0_6
| spl0_89
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2585,f615]) ).
fof(f2640,plain,
( c0_1(a651)
| ~ spl0_6
| ~ spl0_144
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2584,f888]) ).
fof(f2641,plain,
( c0_1(a595)
| ~ spl0_6
| ~ spl0_148
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f2583,f908]) ).
fof(f2659,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f2604,f2641]) ).
fof(f2660,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f2659]) ).
fof(f2668,plain,
( ~ c0_1(a672)
| ~ spl0_2
| ~ spl0_31
| ~ spl0_159 ),
inference(resolution,[],[f1061,f962]) ).
fof(f2690,plain,
( $false
| ~ spl0_2
| ~ spl0_31
| ~ spl0_159
| ~ spl0_160 ),
inference(forward_subsumption_resolution,[],[f2668,f967]) ).
fof(f2691,plain,
( ~ spl0_2
| ~ spl0_31
| ~ spl0_159
| ~ spl0_160 ),
inference(avatar_contradiction_clause,[],[f2690]) ).
fof(f2692,plain,
( ! [X1] : ~ c0_1(X1)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1016,f2231]) ).
fof(f2696,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_25
| ~ spl0_144
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f1973,f2640]) ).
fof(f2697,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_25
| ~ spl0_144
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f2696]) ).
fof(f2698,plain,
( $false
| ~ spl0_2
| ~ spl0_25
| ~ spl0_130
| ~ spl0_163 ),
inference(forward_subsumption_resolution,[],[f2002,f2629]) ).
fof(f2699,plain,
( ~ spl0_2
| ~ spl0_25
| ~ spl0_130
| ~ spl0_163 ),
inference(avatar_contradiction_clause,[],[f2698]) ).
fof(f2718,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| ~ spl0_25
| ~ spl0_160 ),
inference(resolution,[],[f2692,f967]) ).
fof(f2719,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| ~ spl0_25
| ~ spl0_160 ),
inference(avatar_contradiction_clause,[],[f2718]) ).
fof(f2767,plain,
( c1_1(a599)
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| ~ spl0_119 ),
inference(resolution,[],[f2332,f763]) ).
fof(f2769,plain,
( c1_1(a596)
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| ~ spl0_115 ),
inference(resolution,[],[f2332,f743]) ).
fof(f2776,plain,
( $false
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| spl0_65
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f2769,f495]) ).
fof(f2777,plain,
( ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| spl0_65
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f2776]) ).
fof(f2778,plain,
( $false
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| spl0_71
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f2767,f525]) ).
fof(f2779,plain,
( ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| spl0_71
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f2778]) ).
fof(f2792,plain,
( c0_1(a614)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_130 ),
inference(resolution,[],[f2621,f818]) ).
fof(f2793,plain,
( c0_1(a604)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_125 ),
inference(resolution,[],[f2621,f793]) ).
fof(f2819,plain,
( c0_1(a625)
| ~ c2_1(a625)
| ~ spl0_8
| ~ spl0_137 ),
inference(resolution,[],[f227,f853]) ).
fof(f2826,plain,
( c0_1(a599)
| ~ c2_1(a599)
| ~ spl0_8
| ~ spl0_118 ),
inference(resolution,[],[f227,f758]) ).
fof(f2834,plain,
( ~ c2_1(a599)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_31
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f2826,f1061]) ).
fof(f2850,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_31
| ~ spl0_118
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f2834,f763]) ).
fof(f2851,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_31
| ~ spl0_118
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f2850]) ).
fof(f2868,definition,
( spl0_165
<=> c3_1(a637) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f2869,plain,
( ~ c3_1(a637)
| spl0_165 ),
inference(avatar_component_clause,[],[f2868]) ).
fof(f2872,plain,
( c2_1(a620)
| ~ spl0_1
| ~ spl0_6
| spl0_89
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2575,f2639]) ).
fof(f2873,plain,
( c2_1(a614)
| ~ spl0_1
| spl0_83
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f2576,f585]) ).
fof(f2885,plain,
( ~ c2_1(a625)
| ~ spl0_8
| spl0_92
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f2819,f630]) ).
fof(f2891,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| spl0_88
| spl0_89
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2872,f610]) ).
fof(f2892,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_88
| spl0_89
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2891]) ).
fof(f2913,plain,
( spl0_163
| ~ spl0_5
| ~ spl0_11
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f2792,f816,f237,f216,f2627]) ).
fof(f2914,plain,
( spl0_77
| ~ spl0_5
| ~ spl0_11
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f2793,f791,f237,f216,f553]) ).
fof(f2919,plain,
( ~ spl0_124
| ~ spl0_7
| ~ spl0_10
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f2445,f791,f233,f222,f786]) ).
fof(f2920,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_11
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f245,f2621]) ).
fof(f2922,plain,
( spl0_73
| ~ spl0_9
| ~ spl0_13
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f2209,f766,f244,f230,f533]) ).
fof(f2923,plain,
( spl0_71
| ~ spl0_9
| ~ spl0_13
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f2210,f756,f244,f230,f523]) ).
fof(f2937,plain,
( ! [X2] :
( c0_1(X2)
| c3_1(X2) )
| ~ spl0_5
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f270,f2621]) ).
fof(f2993,plain,
( ~ c0_1(a618)
| ~ spl0_9
| ~ spl0_32
| ~ spl0_151 ),
inference(resolution,[],[f1345,f923]) ).
fof(f3006,plain,
( $false
| ~ spl0_9
| ~ spl0_32
| ~ spl0_151
| ~ spl0_153 ),
inference(forward_subsumption_resolution,[],[f2993,f933]) ).
fof(f3007,plain,
( ~ spl0_9
| ~ spl0_32
| ~ spl0_151
| ~ spl0_153 ),
inference(avatar_contradiction_clause,[],[f3006]) ).
fof(f3032,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2) )
| ~ spl0_18
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f270,f263]) ).
fof(f3057,plain,
( c0_1(a593)
| ~ spl0_18
| ~ spl0_20
| spl0_62 ),
inference(resolution,[],[f3032,f480]) ).
fof(f3064,plain,
( $false
| ~ spl0_18
| ~ spl0_20
| spl0_62
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f3057,f485]) ).
fof(f3065,plain,
( ~ spl0_18
| ~ spl0_20
| spl0_62
| spl0_63 ),
inference(avatar_contradiction_clause,[],[f3064]) ).
fof(f3077,plain,
( ~ spl0_122
| ~ spl0_4
| ~ spl0_8
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f2531,f771,f226,f212,f776]) ).
fof(f3082,plain,
( ~ spl0_161
| ~ spl0_8
| spl0_92
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f2885,f851,f628,f226,f1959]) ).
fof(f3086,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0) )
| ~ spl0_16
| ~ spl0_17
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f462,f1014]) ).
fof(f3124,plain,
( ~ c0_1(a618)
| ~ spl0_4
| ~ spl0_14
| ~ spl0_151 ),
inference(resolution,[],[f1013,f923]) ).
fof(f3130,plain,
( ~ c0_1(a630)
| ~ spl0_4
| ~ spl0_14
| ~ spl0_139 ),
inference(resolution,[],[f1013,f863]) ).
fof(f3146,definition,
( spl0_166
<=> c3_1(a604) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f3148,plain,
( ~ c3_1(a604)
| spl0_166 ),
inference(avatar_component_clause,[],[f3146]) ).
fof(f3150,plain,
( ~ spl0_166
| ~ spl0_6
| spl0_77
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f2638,f791,f553,f219,f3146]) ).
fof(f3154,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2) )
| ~ spl0_1
| ~ spl0_10
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f270,f2620]) ).
fof(f3164,plain,
( c0_1(a593)
| ~ spl0_16
| ~ spl0_38
| spl0_62 ),
inference(resolution,[],[f1017,f480]) ).
fof(f3166,plain,
( c0_1(a667)
| ~ spl0_16
| ~ spl0_38
| spl0_105 ),
inference(resolution,[],[f1017,f694]) ).
fof(f3184,plain,
( c3_1(a604)
| ~ spl0_1
| ~ spl0_10
| ~ spl0_125 ),
inference(resolution,[],[f2620,f793]) ).
fof(f3186,plain,
( c3_1(a594)
| ~ spl0_1
| ~ spl0_10
| ~ spl0_113 ),
inference(resolution,[],[f2620,f733]) ).
fof(f3190,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| ~ spl0_125
| spl0_166 ),
inference(forward_subsumption_resolution,[],[f3184,f3148]) ).
fof(f3191,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_125
| spl0_166 ),
inference(avatar_contradiction_clause,[],[f3190]) ).
fof(f3197,plain,
( c2_1(a608)
| ~ spl0_16
| ~ spl0_17
| spl0_79 ),
inference(resolution,[],[f565,f1014]) ).
fof(f3206,plain,
( c2_1(a600)
| ~ spl0_16
| ~ spl0_17
| ~ spl0_59
| spl0_73 ),
inference(resolution,[],[f3086,f535]) ).
fof(f3229,plain,
( c0_1(a656)
| ~ c3_1(a656)
| ~ spl0_6
| ~ spl0_147 ),
inference(resolution,[],[f220,f903]) ).
fof(f3238,plain,
( ~ c3_1(a656)
| ~ spl0_6
| spl0_103
| ~ spl0_147 ),
inference(forward_subsumption_resolution,[],[f3229,f685]) ).
fof(f3292,plain,
( spl0_63
| ~ spl0_16
| ~ spl0_38
| spl0_62 ),
inference(avatar_split_clause,[],[f3164,f478,f355,f255,f483]) ).
fof(f3296,plain,
( $false
| ~ spl0_16
| ~ spl0_17
| ~ spl0_59
| spl0_72
| spl0_73 ),
inference(forward_subsumption_resolution,[],[f3206,f530]) ).
fof(f3297,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_59
| spl0_72
| spl0_73 ),
inference(avatar_contradiction_clause,[],[f3296]) ).
fof(f3299,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1) )
| ~ spl0_25
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f352,f294]) ).
fof(f3311,plain,
( c2_1(a594)
| ~ spl0_16
| ~ spl0_17
| spl0_64 ),
inference(resolution,[],[f490,f1014]) ).
fof(f3333,plain,
( ~ spl0_156
| ~ spl0_2
| ~ spl0_154
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f1225,f941,f936,f205,f946]) ).
fof(f3359,plain,
( $false
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| spl0_64
| ~ spl0_113
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f3311,f1220]) ).
fof(f3360,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| spl0_64
| ~ spl0_113
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f3359]) ).
fof(f3363,plain,
( ~ spl0_153
| ~ spl0_4
| ~ spl0_14
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f3124,f921,f247,f212,f931]) ).
fof(f3390,plain,
( c2_1(a624)
| ~ spl0_14
| ~ spl0_17
| ~ spl0_136 ),
inference(resolution,[],[f1036,f848]) ).
fof(f3396,plain,
( $false
| ~ spl0_14
| ~ spl0_17
| spl0_90
| ~ spl0_136 ),
inference(forward_subsumption_resolution,[],[f3390,f620]) ).
fof(f3397,plain,
( ~ spl0_14
| ~ spl0_17
| spl0_90
| ~ spl0_136 ),
inference(avatar_contradiction_clause,[],[f3396]) ).
fof(f3406,plain,
( c3_1(a604)
| ~ spl0_18
| ~ spl0_19
| ~ spl0_125 ),
inference(resolution,[],[f1579,f793]) ).
fof(f3412,plain,
( $false
| ~ spl0_18
| ~ spl0_19
| ~ spl0_125
| spl0_166 ),
inference(forward_subsumption_resolution,[],[f3406,f3148]) ).
fof(f3413,plain,
( ~ spl0_18
| ~ spl0_19
| ~ spl0_125
| spl0_166 ),
inference(avatar_contradiction_clause,[],[f3412]) ).
fof(f3437,plain,
( c2_1(a618)
| ~ spl0_25
| ~ spl0_37
| ~ spl0_153 ),
inference(resolution,[],[f3299,f933]) ).
fof(f3448,plain,
( ~ c0_1(a618)
| ~ c2_1(a618)
| ~ spl0_4
| ~ spl0_151 ),
inference(resolution,[],[f213,f923]) ).
fof(f3458,plain,
( ~ c0_1(a599)
| ~ c2_1(a599)
| ~ spl0_4
| ~ spl0_118 ),
inference(resolution,[],[f213,f758]) ).
fof(f3459,plain,
( ~ c0_1(a599)
| ~ spl0_4
| ~ spl0_118
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f3458,f763]) ).
fof(f3463,plain,
( ~ c2_1(a618)
| ~ spl0_4
| ~ spl0_151
| ~ spl0_153 ),
inference(forward_subsumption_resolution,[],[f3448,f933]) ).
fof(f3467,plain,
( $false
| ~ spl0_4
| ~ spl0_25
| ~ spl0_37
| ~ spl0_151
| ~ spl0_153 ),
inference(forward_subsumption_resolution,[],[f3463,f3437]) ).
fof(f3468,plain,
( ~ spl0_4
| ~ spl0_25
| ~ spl0_37
| ~ spl0_151
| ~ spl0_153 ),
inference(avatar_contradiction_clause,[],[f3467]) ).
fof(f3473,plain,
( c0_1(a595)
| ~ c2_1(a595)
| ~ spl0_5
| ~ spl0_150 ),
inference(resolution,[],[f217,f918]) ).
fof(f3474,plain,
( c0_1(a656)
| ~ c2_1(a656)
| ~ spl0_5
| ~ spl0_147 ),
inference(resolution,[],[f217,f903]) ).
fof(f3478,plain,
( c0_1(a608)
| ~ c2_1(a608)
| ~ spl0_5
| ~ spl0_128 ),
inference(resolution,[],[f217,f808]) ).
fof(f3479,plain,
( c0_1(a604)
| ~ c2_1(a604)
| ~ spl0_5
| ~ spl0_125 ),
inference(resolution,[],[f217,f793]) ).
fof(f3480,plain,
( c0_1(a597)
| ~ c2_1(a597)
| ~ spl0_5
| ~ spl0_117 ),
inference(resolution,[],[f217,f753]) ).
fof(f3484,plain,
( ~ c2_1(a604)
| ~ spl0_5
| spl0_77
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f3479,f555]) ).
fof(f3485,plain,
( ~ c2_1(a608)
| ~ spl0_5
| spl0_80
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f3478,f570]) ).
fof(f3488,plain,
( ~ c2_1(a656)
| ~ spl0_5
| spl0_103
| ~ spl0_147 ),
inference(forward_subsumption_resolution,[],[f3474,f685]) ).
fof(f3491,plain,
( $false
| ~ spl0_5
| spl0_77
| ~ spl0_124
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f3484,f788]) ).
fof(f3492,plain,
( ~ spl0_5
| spl0_77
| ~ spl0_124
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f3491]) ).
fof(f3493,plain,
( $false
| ~ spl0_5
| ~ spl0_16
| ~ spl0_17
| spl0_79
| spl0_80
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f3485,f3197]) ).
fof(f3494,plain,
( ~ spl0_5
| ~ spl0_16
| ~ spl0_17
| spl0_79
| spl0_80
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f3493]) ).
fof(f3504,plain,
( ~ c3_1(a637)
| ~ c2_1(a637)
| ~ spl0_7
| ~ spl0_155 ),
inference(resolution,[],[f223,f943]) ).
fof(f3506,plain,
( ~ c3_1(a595)
| ~ c2_1(a595)
| ~ spl0_7
| ~ spl0_150 ),
inference(resolution,[],[f223,f918]) ).
fof(f3512,plain,
( ~ c3_1(a604)
| ~ c2_1(a604)
| ~ spl0_7
| ~ spl0_125 ),
inference(resolution,[],[f223,f793]) ).
fof(f3525,plain,
( ~ c3_1(a637)
| ~ spl0_7
| ~ spl0_154
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f3504,f938]) ).
fof(f3526,plain,
( ~ spl0_165
| ~ spl0_7
| ~ spl0_154
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f3525,f941,f936,f222,f2868]) ).
fof(f3537,plain,
( c1_1(a625)
| c0_1(a625)
| ~ spl0_13
| ~ spl0_137 ),
inference(resolution,[],[f245,f853]) ).
fof(f3541,plain,
( c1_1(a599)
| c0_1(a599)
| ~ spl0_13
| ~ spl0_118 ),
inference(resolution,[],[f245,f758]) ).
fof(f3542,plain,
( c0_1(a599)
| ~ spl0_13
| spl0_71
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f3541,f525]) ).
fof(f3545,plain,
( c0_1(a625)
| ~ spl0_13
| spl0_91
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f3537,f625]) ).
fof(f3548,plain,
( $false
| ~ spl0_4
| ~ spl0_13
| spl0_71
| ~ spl0_118
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f3542,f3459]) ).
fof(f3549,plain,
( ~ spl0_4
| ~ spl0_13
| spl0_71
| ~ spl0_118
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f3548]) ).
fof(f3562,plain,
( c2_1(a625)
| c0_1(a625)
| ~ spl0_15
| spl0_91 ),
inference(resolution,[],[f252,f625]) ).
fof(f3573,plain,
( c2_1(a598)
| c0_1(a598)
| ~ spl0_15
| spl0_69 ),
inference(resolution,[],[f252,f515]) ).
fof(f3576,plain,
( c0_1(a598)
| ~ spl0_15
| spl0_68
| spl0_69 ),
inference(forward_subsumption_resolution,[],[f3573,f510]) ).
fof(f3577,plain,
( $false
| ~ spl0_15
| spl0_68
| spl0_69
| spl0_70 ),
inference(forward_subsumption_resolution,[],[f3576,f520]) ).
fof(f3578,plain,
( ~ spl0_15
| spl0_68
| spl0_69
| spl0_70 ),
inference(avatar_contradiction_clause,[],[f3577]) ).
fof(f3580,plain,
( spl0_70
| ~ spl0_11
| ~ spl0_15
| spl0_68 ),
inference(avatar_split_clause,[],[f1178,f508,f251,f237,f518]) ).
fof(f3604,plain,
( ~ c2_1(a595)
| ~ spl0_7
| ~ spl0_148
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f3506,f908]) ).
fof(f3607,plain,
( ! [X2] :
( ~ c0_1(X2)
| c1_1(X2) )
| ~ spl0_9
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f231,f386]) ).
fof(f3609,plain,
( $false
| ~ spl0_7
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f3604,f913]) ).
fof(f3610,plain,
( ~ spl0_7
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f3609]) ).
fof(f3616,plain,
( spl0_84
| ~ spl0_1
| spl0_83
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f2873,f816,f583,f202,f588]) ).
fof(f3623,plain,
( ! [X2] : c0_1(X2)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_13
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2937,f2920]) ).
fof(f3625,plain,
( ~ c2_1(a595)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f3473,f1223]) ).
fof(f3640,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f3625,f913]) ).
fof(f3641,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_149
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f3640]) ).
fof(f3649,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| ~ spl0_13
| ~ spl0_20
| spl0_103 ),
inference(resolution,[],[f3623,f685]) ).
fof(f3654,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| ~ spl0_13
| ~ spl0_20
| spl0_66 ),
inference(resolution,[],[f3623,f500]) ).
fof(f3665,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_13
| ~ spl0_20
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f3654]) ).
fof(f3670,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_13
| ~ spl0_20
| spl0_103 ),
inference(avatar_contradiction_clause,[],[f3649]) ).
fof(f3675,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| spl0_64
| ~ spl0_113 ),
inference(forward_subsumption_resolution,[],[f3186,f490]) ).
fof(f3676,plain,
( ~ spl0_1
| ~ spl0_10
| spl0_64
| ~ spl0_113 ),
inference(avatar_contradiction_clause,[],[f3675]) ).
fof(f3678,definition,
( spl0_169
<=> c2_1(a656) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f3690,plain,
( ~ spl0_146
| ~ spl0_6
| spl0_103
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f3238,f901,f683,f219,f896]) ).
fof(f3694,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f276,f3154]) ).
fof(f3735,plain,
( c0_1(a602)
| ~ spl0_6
| ~ spl0_18
| ~ spl0_43
| ~ spl0_122 ),
inference(resolution,[],[f1616,f778]) ).
fof(f3744,plain,
( $false
| ~ spl0_6
| ~ spl0_18
| ~ spl0_43
| spl0_74
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f3735,f540]) ).
fof(f3745,plain,
( ~ spl0_6
| ~ spl0_18
| ~ spl0_43
| spl0_74
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f3744]) ).
fof(f3750,plain,
( c2_1(a656)
| ~ spl0_11
| ~ spl0_25
| ~ spl0_147 ),
inference(resolution,[],[f2025,f903]) ).
fof(f3751,plain,
( c2_1(a651)
| ~ spl0_11
| ~ spl0_25
| ~ spl0_145 ),
inference(resolution,[],[f2025,f893]) ).
fof(f3769,plain,
( spl0_169
| ~ spl0_11
| ~ spl0_25
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f3750,f901,f293,f237,f3678]) ).
fof(f3820,plain,
( c1_1(a615)
| ~ spl0_9
| ~ spl0_45
| ~ spl0_132 ),
inference(resolution,[],[f3607,f828]) ).
fof(f3824,plain,
( c1_1(a603)
| ~ spl0_9
| ~ spl0_45
| ~ spl0_123 ),
inference(resolution,[],[f3607,f783]) ).
fof(f3831,plain,
( $false
| ~ spl0_9
| ~ spl0_45
| spl0_76
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f3824,f550]) ).
fof(f3832,plain,
( ~ spl0_9
| ~ spl0_45
| spl0_76
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f3831]) ).
fof(f3833,plain,
( $false
| ~ spl0_9
| ~ spl0_45
| spl0_85
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f3820,f595]) ).
fof(f3834,plain,
( ~ spl0_9
| ~ spl0_45
| spl0_85
| ~ spl0_132 ),
inference(avatar_contradiction_clause,[],[f3833]) ).
fof(f3844,plain,
( c3_1(a609)
| ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| ~ spl0_129 ),
inference(resolution,[],[f3694,f813]) ).
fof(f3845,plain,
( c3_1(a605)
| ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| ~ spl0_126 ),
inference(resolution,[],[f3694,f798]) ).
fof(f3853,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| spl0_78
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f3845,f560]) ).
fof(f3854,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| spl0_78
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f3853]) ).
fof(f3855,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| spl0_81
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f3844,f575]) ).
fof(f3856,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| spl0_81
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f3855]) ).
fof(f3861,plain,
( ~ spl0_149
| ~ spl0_4
| ~ spl0_8
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f2521,f906,f226,f212,f911]) ).
fof(f3867,plain,
( ~ spl0_140
| ~ spl0_4
| ~ spl0_14
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f3130,f861,f247,f212,f866]) ).
fof(f3873,plain,
( ~ c2_1(a597)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_21
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f3480,f1015]) ).
fof(f3876,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_4
| ~ spl0_21
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f294,f1015]) ).
fof(f3880,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_4
| ~ spl0_21
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f356,f1015]) ).
fof(f3881,plain,
( ~ spl0_116
| ~ spl0_4
| ~ spl0_5
| ~ spl0_21
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f3873,f751,f275,f216,f212,f746]) ).
fof(f3882,plain,
( ! [X1] : ~ c2_1(X1)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_21
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3880,f1010]) ).
fof(f3908,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_21
| ~ spl0_38
| ~ spl0_126 ),
inference(resolution,[],[f3882,f798]) ).
fof(f3910,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_21
| ~ spl0_38
| ~ spl0_115 ),
inference(resolution,[],[f3882,f743]) ).
fof(f3915,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_21
| ~ spl0_38
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f3910]) ).
fof(f3917,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_21
| ~ spl0_38
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f3908]) ).
fof(f3928,plain,
( ~ spl0_169
| ~ spl0_5
| spl0_103
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f3488,f901,f683,f216,f3678]) ).
fof(f3960,plain,
( ~ c0_1(a672)
| ~ spl0_4
| ~ spl0_21
| ~ spl0_159 ),
inference(resolution,[],[f1015,f962]) ).
fof(f3961,plain,
( ~ c0_1(a615)
| ~ spl0_4
| ~ spl0_21
| ~ spl0_131 ),
inference(resolution,[],[f1015,f823]) ).
fof(f3964,plain,
( ~ c0_1(a605)
| ~ spl0_4
| ~ spl0_21
| ~ spl0_126 ),
inference(resolution,[],[f1015,f798]) ).
fof(f3969,plain,
( $false
| ~ spl0_4
| ~ spl0_21
| ~ spl0_126
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f3964,f803]) ).
fof(f3970,plain,
( ~ spl0_4
| ~ spl0_21
| ~ spl0_126
| ~ spl0_127 ),
inference(avatar_contradiction_clause,[],[f3969]) ).
fof(f3973,plain,
( $false
| ~ spl0_4
| ~ spl0_21
| ~ spl0_131
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f3961,f828]) ).
fof(f3974,plain,
( ~ spl0_4
| ~ spl0_21
| ~ spl0_131
| ~ spl0_132 ),
inference(avatar_contradiction_clause,[],[f3973]) ).
fof(f3975,plain,
( $false
| ~ spl0_4
| ~ spl0_21
| ~ spl0_159
| ~ spl0_160 ),
inference(forward_subsumption_resolution,[],[f3960,f967]) ).
fof(f3976,plain,
( ~ spl0_4
| ~ spl0_21
| ~ spl0_159
| ~ spl0_160 ),
inference(avatar_contradiction_clause,[],[f3975]) ).
fof(f3977,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1) )
| ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f263,f3876]) ).
fof(f4028,plain,
( c3_1(a608)
| ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25
| ~ spl0_128 ),
inference(resolution,[],[f3977,f808]) ).
fof(f4030,plain,
( c3_1(a597)
| ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25
| ~ spl0_117 ),
inference(resolution,[],[f3977,f753]) ).
fof(f4032,plain,
( spl0_67
| ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f4030,f751,f293,f275,f262,f212,f503]) ).
fof(f4033,plain,
( $false
| ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25
| spl0_79
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f4028,f565]) ).
fof(f4034,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25
| spl0_79
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f4033]) ).
fof(f4066,plain,
( c0_1(a625)
| ~ spl0_15
| spl0_91
| spl0_161 ),
inference(forward_subsumption_resolution,[],[f3562,f1961]) ).
fof(f4071,plain,
( spl0_70
| ~ spl0_15
| spl0_68
| spl0_69 ),
inference(avatar_split_clause,[],[f3576,f513,f508,f251,f518]) ).
fof(f4078,plain,
( spl0_107
| ~ spl0_16
| ~ spl0_38
| spl0_105 ),
inference(avatar_split_clause,[],[f3166,f692,f355,f255,f702]) ).
fof(f4080,plain,
( ~ spl0_146
| ~ spl0_7
| ~ spl0_39
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1074,f901,f358,f222,f896]) ).
fof(f4086,plain,
( ~ c3_1(a604)
| ~ spl0_7
| ~ spl0_124
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f3512,f788]) ).
fof(f4093,plain,
( $false
| ~ spl0_15
| spl0_91
| spl0_92
| spl0_161 ),
inference(forward_subsumption_resolution,[],[f4066,f630]) ).
fof(f4094,plain,
( ~ spl0_15
| spl0_91
| spl0_92
| spl0_161 ),
inference(avatar_contradiction_clause,[],[f4093]) ).
fof(f4097,plain,
( ~ spl0_166
| ~ spl0_7
| ~ spl0_124
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f4086,f791,f786,f222,f3146]) ).
fof(f4109,plain,
( spl0_92
| ~ spl0_13
| spl0_91
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f3545,f851,f623,f244,f628]) ).
fof(f4155,plain,
( c3_1(a609)
| c1_1(a609)
| ~ spl0_12
| ~ spl0_129 ),
inference(resolution,[],[f241,f813]) ).
fof(f4163,plain,
( c1_1(a609)
| ~ spl0_12
| spl0_81
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f4155,f575]) ).
fof(f4165,plain,
( $false
| ~ spl0_12
| spl0_81
| spl0_82
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f4163,f580]) ).
fof(f4166,plain,
( ~ spl0_12
| spl0_81
| spl0_82
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f4165]) ).
fof(f4173,plain,
( spl0_102
| ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1453,f886,f251,f247,f237,f678]) ).
fof(f4176,plain,
( spl0_102
| ~ spl0_11
| ~ spl0_15
| ~ spl0_25
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f1487,f891,f293,f251,f237,f678]) ).
fof(f4180,plain,
( spl0_102
| ~ spl0_11
| ~ spl0_25
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f3751,f891,f293,f237,f678]) ).
fof(f4235,plain,
( c1_1(a631)
| ~ c0_1(a631)
| ~ spl0_9
| ~ spl0_141 ),
inference(resolution,[],[f231,f873]) ).
fof(f4244,plain,
( ~ c0_1(a631)
| ~ spl0_9
| spl0_96
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f4235,f650]) ).
fof(f4246,plain,
( $false
| ~ spl0_9
| spl0_96
| ~ spl0_141
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f4244,f878]) ).
fof(f4247,plain,
( ~ spl0_9
| spl0_96
| ~ spl0_141
| ~ spl0_142 ),
inference(avatar_contradiction_clause,[],[f4246]) ).
fof(f4307,plain,
( c3_1(a637)
| ~ c0_1(a637)
| ~ spl0_19
| ~ spl0_155 ),
inference(resolution,[],[f266,f943]) ).
fof(f4318,plain,
( c3_1(a594)
| ~ c0_1(a594)
| ~ spl0_19
| ~ spl0_113 ),
inference(resolution,[],[f266,f733]) ).
fof(f4319,plain,
( ~ c0_1(a594)
| ~ spl0_19
| spl0_64
| ~ spl0_113 ),
inference(forward_subsumption_resolution,[],[f4318,f490]) ).
fof(f4321,plain,
( ~ c0_1(a637)
| ~ spl0_19
| ~ spl0_155
| spl0_165 ),
inference(forward_subsumption_resolution,[],[f4307,f2869]) ).
fof(f4322,plain,
( $false
| ~ spl0_19
| spl0_64
| ~ spl0_113
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f4319,f738]) ).
fof(f4323,plain,
( ~ spl0_19
| spl0_64
| ~ spl0_113
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f4322]) ).
fof(f4324,plain,
( $false
| ~ spl0_19
| ~ spl0_155
| ~ spl0_156
| spl0_165 ),
inference(forward_subsumption_resolution,[],[f4321,f948]) ).
fof(f4325,plain,
( ~ spl0_19
| ~ spl0_155
| ~ spl0_156
| spl0_165 ),
inference(avatar_contradiction_clause,[],[f4324]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f214]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f224]) ).
cnf(s3,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_8 ),
inference(sat_conversion,[],[f228]) ).
cnf(s4,plain,
( spl0_1
| ~ spl0_3
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f235]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_4
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f242]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_8
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f249]) ).
cnf(s7,plain,
( spl0_2
| ~ spl0_3
| spl0_10
| spl0_15 ),
inference(sat_conversion,[],[f253]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_13
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f267]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_4
| spl0_13
| spl0_20 ),
inference(sat_conversion,[],[f271]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_8
| spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f272]) ).
cnf(s12,plain,
( ~ spl0_3
| spl0_14
| spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f273]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_13
| spl0_15
| spl0_21 ),
inference(sat_conversion,[],[f277]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_4
| spl0_19
| spl0_23 ),
inference(sat_conversion,[],[f287]) ).
cnf(s16,plain,
( spl0_2
| ~ spl0_3
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f295]) ).
cnf(s17,plain,
( spl0_2
| ~ spl0_3
| spl0_8
| spl0_26 ),
inference(sat_conversion,[],[f300]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_4
| spl0_17
| spl0_28 ),
inference(sat_conversion,[],[f310]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_25
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f323]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_12
| spl0_24
| spl0_32 ),
inference(sat_conversion,[],[f327]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_5
| spl0_14
| spl0_33 ),
inference(sat_conversion,[],[f332]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_7
| spl0_11
| spl0_34 ),
inference(sat_conversion,[],[f337]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_4
| spl0_11
| spl0_35 ),
inference(sat_conversion,[],[f342]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_15
| spl0_16
| spl0_20 ),
inference(sat_conversion,[],[f343]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_17
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f344]) ).
cnf(s28,plain,
( ~ spl0_3
| spl0_9
| spl0_17
| spl0_36 ),
inference(sat_conversion,[],[f349]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_14
| spl0_30
| spl0_37 ),
inference(sat_conversion,[],[f353]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_30
| spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f360]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_18
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f365]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_9
| spl0_18
| spl0_41 ),
inference(sat_conversion,[],[f370]) ).
cnf(s33,plain,
( spl0_2
| ~ spl0_3
| spl0_16
| spl0_42 ),
inference(sat_conversion,[],[f375]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_9
| spl0_41
| spl0_43 ),
inference(sat_conversion,[],[f379]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_38
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f387]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_15
| spl0_21
| spl0_47 ),
inference(sat_conversion,[],[f397]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_16
| spl0_18
| spl0_48 ),
inference(sat_conversion,[],[f402]) ).
cnf(s39,plain,
( ~ spl0_3
| spl0_7
| spl0_24
| spl0_48 ),
inference(sat_conversion,[],[f403]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_4
| spl0_40
| spl0_49 ),
inference(sat_conversion,[],[f408]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_21
| spl0_40
| spl0_52 ),
inference(sat_conversion,[],[f423]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_34
| spl0_39
| spl0_48 ),
inference(sat_conversion,[],[f424]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_26
| spl0_39
| spl0_53 ),
inference(sat_conversion,[],[f429]) ).
cnf(s47,plain,
( ~ spl0_3
| spl0_25
| spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f435]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_30
| spl0_33
| spl0_55 ),
inference(sat_conversion,[],[f440]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_9
| spl0_27
| spl0_48 ),
inference(sat_conversion,[],[f441]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_8
| spl0_50
| spl0_56 ),
inference(sat_conversion,[],[f446]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_6
| spl0_27
| spl0_46 ),
inference(sat_conversion,[],[f447]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_21
| spl0_57 ),
inference(sat_conversion,[],[f452]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_21
| spl0_27 ),
inference(sat_conversion,[],[f453]) ).
cnf(s57,plain,
( ~ spl0_3
| spl0_22
| spl0_24
| spl0_59 ),
inference(sat_conversion,[],[f463]) ).
cnf(s58,plain,
( ~ spl0_3
| spl0_38
| spl0_40
| spl0_42 ),
inference(sat_conversion,[],[f464]) ).
cnf(s59,plain,
( ~ spl0_3
| spl0_34
| spl0_38
| spl0_48 ),
inference(sat_conversion,[],[f465]) ).
cnf(s64,plain,
( ~ spl0_47
| ~ spl0_62 ),
inference(sat_conversion,[],[f481]) ).
cnf(s65,plain,
( ~ spl0_47
| ~ spl0_63 ),
inference(sat_conversion,[],[f486]) ).
cnf(s66,plain,
( ~ spl0_41
| ~ spl0_64 ),
inference(sat_conversion,[],[f491]) ).
cnf(s67,plain,
( ~ spl0_49
| ~ spl0_65 ),
inference(sat_conversion,[],[f496]) ).
cnf(s68,plain,
( ~ spl0_49
| ~ spl0_66 ),
inference(sat_conversion,[],[f501]) ).
cnf(s69,plain,
( ~ spl0_60
| ~ spl0_67 ),
inference(sat_conversion,[],[f506]) ).
cnf(s70,plain,
( ~ spl0_52
| ~ spl0_68 ),
inference(sat_conversion,[],[f511]) ).
cnf(s71,plain,
( ~ spl0_52
| ~ spl0_69 ),
inference(sat_conversion,[],[f516]) ).
cnf(s72,plain,
( ~ spl0_52
| ~ spl0_70 ),
inference(sat_conversion,[],[f521]) ).
cnf(s73,plain,
( ~ spl0_48
| ~ spl0_71 ),
inference(sat_conversion,[],[f526]) ).
cnf(s74,plain,
( ~ spl0_53
| ~ spl0_72 ),
inference(sat_conversion,[],[f531]) ).
cnf(s75,plain,
( ~ spl0_53
| ~ spl0_73 ),
inference(sat_conversion,[],[f536]) ).
cnf(s76,plain,
( ~ spl0_42
| ~ spl0_74 ),
inference(sat_conversion,[],[f541]) ).
cnf(s78,plain,
( ~ spl0_46
| ~ spl0_76 ),
inference(sat_conversion,[],[f551]) ).
cnf(s79,plain,
( ~ spl0_35
| ~ spl0_77 ),
inference(sat_conversion,[],[f556]) ).
cnf(s80,plain,
( ~ spl0_34
| ~ spl0_78 ),
inference(sat_conversion,[],[f561]) ).
cnf(s81,plain,
( ~ spl0_44
| ~ spl0_79 ),
inference(sat_conversion,[],[f566]) ).
cnf(s82,plain,
( ~ spl0_44
| ~ spl0_80 ),
inference(sat_conversion,[],[f571]) ).
cnf(s83,plain,
( ~ spl0_30
| ~ spl0_81 ),
inference(sat_conversion,[],[f576]) ).
cnf(s84,plain,
( ~ spl0_30
| ~ spl0_82 ),
inference(sat_conversion,[],[f581]) ).
cnf(s85,plain,
( ~ spl0_33
| ~ spl0_83 ),
inference(sat_conversion,[],[f586]) ).
cnf(s86,plain,
( ~ spl0_33
| ~ spl0_84 ),
inference(sat_conversion,[],[f591]) ).
cnf(s87,plain,
( ~ spl0_27
| ~ spl0_85 ),
inference(sat_conversion,[],[f596]) ).
cnf(s90,plain,
( ~ spl0_50
| ~ spl0_88 ),
inference(sat_conversion,[],[f611]) ).
cnf(s91,plain,
( ~ spl0_50
| ~ spl0_89 ),
inference(sat_conversion,[],[f616]) ).
cnf(s92,plain,
( ~ spl0_22
| ~ spl0_90 ),
inference(sat_conversion,[],[f621]) ).
cnf(s93,plain,
( ~ spl0_24
| ~ spl0_91 ),
inference(sat_conversion,[],[f626]) ).
cnf(s94,plain,
( ~ spl0_24
| ~ spl0_92 ),
inference(sat_conversion,[],[f631]) ).
cnf(s97,plain,
( ~ spl0_36
| ~ spl0_95 ),
inference(sat_conversion,[],[f646]) ).
cnf(s98,plain,
( ~ spl0_29
| ~ spl0_96 ),
inference(sat_conversion,[],[f651]) ).
cnf(s100,plain,
( ~ spl0_51
| ~ spl0_98 ),
inference(sat_conversion,[],[f661]) ).
cnf(s101,plain,
( ~ spl0_51
| ~ spl0_99 ),
inference(sat_conversion,[],[f666]) ).
cnf(s104,plain,
( ~ spl0_23
| ~ spl0_102 ),
inference(sat_conversion,[],[f681]) ).
cnf(s105,plain,
( ~ spl0_57
| ~ spl0_103 ),
inference(sat_conversion,[],[f686]) ).
cnf(s106,plain,
( ~ spl0_104
| ~ spl0_105 ),
inference(sat_conversion,[],[f695]) ).
cnf(s108,plain,
( ~ spl0_104
| ~ spl0_107 ),
inference(sat_conversion,[],[f705]) ).
cnf(s112,plain,
( ~ spl0_47
| spl0_112 ),
inference(sat_conversion,[],[f729]) ).
cnf(s113,plain,
( ~ spl0_41
| spl0_113 ),
inference(sat_conversion,[],[f734]) ).
cnf(s114,plain,
( ~ spl0_41
| spl0_114 ),
inference(sat_conversion,[],[f739]) ).
cnf(s115,plain,
( ~ spl0_49
| spl0_115 ),
inference(sat_conversion,[],[f744]) ).
cnf(s116,plain,
( ~ spl0_60
| spl0_116 ),
inference(sat_conversion,[],[f749]) ).
cnf(s117,plain,
( ~ spl0_60
| spl0_117 ),
inference(sat_conversion,[],[f754]) ).
cnf(s118,plain,
( ~ spl0_48
| spl0_118 ),
inference(sat_conversion,[],[f759]) ).
cnf(s119,plain,
( ~ spl0_48
| spl0_119 ),
inference(sat_conversion,[],[f764]) ).
cnf(s120,plain,
( ~ spl0_53
| spl0_120 ),
inference(sat_conversion,[],[f769]) ).
cnf(s121,plain,
( ~ spl0_42
| spl0_121 ),
inference(sat_conversion,[],[f774]) ).
cnf(s122,plain,
( ~ spl0_42
| spl0_122 ),
inference(sat_conversion,[],[f779]) ).
cnf(s123,plain,
( ~ spl0_46
| spl0_123 ),
inference(sat_conversion,[],[f784]) ).
cnf(s124,plain,
( ~ spl0_35
| spl0_124 ),
inference(sat_conversion,[],[f789]) ).
cnf(s125,plain,
( ~ spl0_35
| spl0_125 ),
inference(sat_conversion,[],[f794]) ).
cnf(s126,plain,
( ~ spl0_34
| spl0_126 ),
inference(sat_conversion,[],[f799]) ).
cnf(s127,plain,
( ~ spl0_34
| spl0_127 ),
inference(sat_conversion,[],[f804]) ).
cnf(s128,plain,
( ~ spl0_44
| spl0_128 ),
inference(sat_conversion,[],[f809]) ).
cnf(s129,plain,
( ~ spl0_30
| spl0_129 ),
inference(sat_conversion,[],[f814]) ).
cnf(s130,plain,
( ~ spl0_33
| spl0_130 ),
inference(sat_conversion,[],[f819]) ).
cnf(s131,plain,
( ~ spl0_27
| spl0_131 ),
inference(sat_conversion,[],[f824]) ).
cnf(s132,plain,
( ~ spl0_27
| spl0_132 ),
inference(sat_conversion,[],[f829]) ).
cnf(s133,plain,
( ~ spl0_56
| spl0_133 ),
inference(sat_conversion,[],[f834]) ).
cnf(s134,plain,
( ~ spl0_50
| spl0_134 ),
inference(sat_conversion,[],[f839]) ).
cnf(s136,plain,
( ~ spl0_22
| spl0_136 ),
inference(sat_conversion,[],[f849]) ).
cnf(s137,plain,
( ~ spl0_24
| spl0_137 ),
inference(sat_conversion,[],[f854]) ).
cnf(s139,plain,
( ~ spl0_36
| spl0_139 ),
inference(sat_conversion,[],[f864]) ).
cnf(s140,plain,
( ~ spl0_36
| spl0_140 ),
inference(sat_conversion,[],[f869]) ).
cnf(s141,plain,
( ~ spl0_29
| spl0_141 ),
inference(sat_conversion,[],[f874]) ).
cnf(s142,plain,
( ~ spl0_29
| spl0_142 ),
inference(sat_conversion,[],[f879]) ).
cnf(s144,plain,
( ~ spl0_23
| spl0_144 ),
inference(sat_conversion,[],[f889]) ).
cnf(s145,plain,
( ~ spl0_23
| spl0_145 ),
inference(sat_conversion,[],[f894]) ).
cnf(s146,plain,
( ~ spl0_57
| spl0_146 ),
inference(sat_conversion,[],[f899]) ).
cnf(s147,plain,
( ~ spl0_57
| spl0_147 ),
inference(sat_conversion,[],[f904]) ).
cnf(s148,plain,
( ~ spl0_40
| spl0_148 ),
inference(sat_conversion,[],[f909]) ).
cnf(s149,plain,
( ~ spl0_40
| spl0_149 ),
inference(sat_conversion,[],[f914]) ).
cnf(s150,plain,
( ~ spl0_40
| spl0_150 ),
inference(sat_conversion,[],[f919]) ).
cnf(s151,plain,
( ~ spl0_26
| spl0_151 ),
inference(sat_conversion,[],[f924]) ).
cnf(s152,plain,
( ~ spl0_26
| spl0_152 ),
inference(sat_conversion,[],[f929]) ).
cnf(s153,plain,
( ~ spl0_26
| spl0_153 ),
inference(sat_conversion,[],[f934]) ).
cnf(s154,plain,
( ~ spl0_28
| spl0_154 ),
inference(sat_conversion,[],[f939]) ).
cnf(s155,plain,
( ~ spl0_28
| spl0_155 ),
inference(sat_conversion,[],[f944]) ).
cnf(s156,plain,
( ~ spl0_28
| spl0_156 ),
inference(sat_conversion,[],[f949]) ).
cnf(s158,plain,
( ~ spl0_158
| spl0_159 ),
inference(sat_conversion,[],[f963]) ).
cnf(s159,plain,
( ~ spl0_158
| spl0_160 ),
inference(sat_conversion,[],[f968]) ).
cnf(s161,plain,
( spl0_24
| spl0_30
| spl0_34 ),
inference(sat_conversion,[],[f970]) ).
cnf(s162,plain,
( spl0_30
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f971]) ).
cnf(s163,plain,
( spl0_34
| spl0_40
| spl0_49 ),
inference(sat_conversion,[],[f972]) ).
cnf(s164,plain,
( spl0_29
| spl0_41
| spl0_52 ),
inference(sat_conversion,[],[f973]) ).
cnf(s165,plain,
( spl0_23
| spl0_41
| spl0_158 ),
inference(sat_conversion,[],[f974]) ).
cnf(s167,plain,
( spl0_28
| spl0_60
| spl0_104 ),
inference(sat_conversion,[],[f976]) ).
cnf(s169,plain,
( spl0_3
| ~ spl0_41 ),
inference(sat_conversion,[],[f978]) ).
cnf(s192,plain,
( spl0_3
| ~ spl0_23 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s199,plain,
( spl0_3
| ~ spl0_158 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s200,plain,
( spl0_23
| spl0_35 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s209,plain,
( ~ spl0_2
| ~ spl0_25
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s219,plain,
( ~ spl0_12
| ~ spl0_55
| spl0_65
| ~ spl0_115 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s220,plain,
( ~ spl0_12
| ~ spl0_55
| spl0_71
| ~ spl0_119 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s233,plain,
( ~ spl0_17
| ~ spl0_21
| spl0_78
| ~ spl0_127 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s237,plain,
( ~ spl0_15
| ~ spl0_43
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s254,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_13
| ~ spl0_21
| ~ spl0_38
| ~ spl0_116 ),
inference(sat_conversion,[],[f1263]) ).
cnf(s264,plain,
( ~ spl0_11
| ~ spl0_15
| spl0_98
| spl0_99 ),
inference(sat_conversion,[],[f1275]) ).
cnf(s267,plain,
( ~ spl0_17
| ~ spl0_21
| spl0_64
| ~ spl0_114 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s384,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_16
| ~ spl0_18
| ~ spl0_43
| spl0_77 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s412,plain,
( ~ spl0_6
| ~ spl0_18
| spl0_77
| ~ spl0_125 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s422,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_14
| spl0_95
| ~ spl0_139 ),
inference(sat_conversion,[],[f1754]) ).
cnf(s424,plain,
( ~ spl0_6
| ~ spl0_9
| ~ spl0_13
| spl0_71
| ~ spl0_118 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s443,plain,
( ~ spl0_7
| ~ spl0_39
| ~ spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f1806]) ).
cnf(s450,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_21
| ~ spl0_38
| spl0_67 ),
inference(sat_conversion,[],[f1830]) ).
cnf(s453,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_21
| ~ spl0_38
| spl0_81 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s461,plain,
( ~ spl0_7
| ~ spl0_18
| ~ spl0_19
| ~ spl0_39
| ~ spl0_125 ),
inference(sat_conversion,[],[f1857]) ).
cnf(s473,plain,
( ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_39
| ~ spl0_125 ),
inference(sat_conversion,[],[f1885]) ).
cnf(s496,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_133 ),
inference(sat_conversion,[],[f1930]) ).
cnf(s500,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_74 ),
inference(sat_conversion,[],[f1947]) ).
cnf(s501,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_123 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s502,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_132 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s509,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_160 ),
inference(sat_conversion,[],[f1956]) ).
cnf(s527,plain,
( ~ spl0_17
| ~ spl0_18
| ~ spl0_20
| ~ spl0_21
| spl0_81 ),
inference(sat_conversion,[],[f2021]) ).
cnf(s528,plain,
( ~ spl0_17
| ~ spl0_18
| ~ spl0_20
| ~ spl0_21
| spl0_83 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s545,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| ~ spl0_125 ),
inference(sat_conversion,[],[f2066]) ).
cnf(s552,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| spl0_81 ),
inference(sat_conversion,[],[f2080]) ).
cnf(s562,plain,
( ~ spl0_17
| ~ spl0_18
| ~ spl0_21
| spl0_83
| ~ spl0_130 ),
inference(sat_conversion,[],[f2118]) ).
cnf(s567,plain,
( ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| spl0_88
| ~ spl0_134 ),
inference(sat_conversion,[],[f2137]) ).
cnf(s568,plain,
( ~ spl0_5
| ~ spl0_43
| spl0_63
| ~ spl0_112 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s570,plain,
( ~ spl0_5
| ~ spl0_43
| spl0_74
| ~ spl0_122 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s584,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_71
| ~ spl0_118 ),
inference(sat_conversion,[],[f2216]) ).
cnf(s596,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| spl0_81 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s597,plain,
( ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| spl0_102
| ~ spl0_145 ),
inference(sat_conversion,[],[f2261]) ).
cnf(s598,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_160 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s649,plain,
( ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| spl0_96
| ~ spl0_142 ),
inference(sat_conversion,[],[f2410]) ).
cnf(s652,plain,
( ~ spl0_10
| ~ spl0_12
| spl0_62
| ~ spl0_112 ),
inference(sat_conversion,[],[f2412]) ).
cnf(s669,plain,
( ~ spl0_7
| ~ spl0_10
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f2463]) ).
cnf(s670,plain,
( ~ spl0_7
| ~ spl0_10
| ~ spl0_154
| ~ spl0_155 ),
inference(sat_conversion,[],[f2465]) ).
cnf(s678,plain,
( ~ spl0_7
| ~ spl0_39
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f2512]) ).
cnf(s680,plain,
( ~ spl0_16
| ~ spl0_17
| spl0_83
| spl0_84 ),
inference(sat_conversion,[],[f2516]) ).
cnf(s684,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f2539]) ).
cnf(s697,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_17
| ~ spl0_21
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f2617]) ).
cnf(s699,plain,
( ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| spl0_81
| spl0_82 ),
inference(sat_conversion,[],[f2623]) ).
cnf(s706,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f2660]) ).
cnf(s710,plain,
( ~ spl0_2
| ~ spl0_31
| ~ spl0_159
| ~ spl0_160 ),
inference(sat_conversion,[],[f2691]) ).
cnf(s713,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_25
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f2697]) ).
cnf(s715,plain,
( ~ spl0_2
| ~ spl0_25
| ~ spl0_130
| ~ spl0_163 ),
inference(sat_conversion,[],[f2699]) ).
cnf(s723,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_17
| ~ spl0_21
| ~ spl0_25
| ~ spl0_160 ),
inference(sat_conversion,[],[f2719]) ).
cnf(s726,plain,
( ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| spl0_65
| ~ spl0_115 ),
inference(sat_conversion,[],[f2777]) ).
cnf(s727,plain,
( ~ spl0_17
| ~ spl0_20
| ~ spl0_21
| ~ spl0_55
| spl0_71
| ~ spl0_119 ),
inference(sat_conversion,[],[f2779]) ).
cnf(s740,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_31
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f2851]) ).
cnf(s749,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_88
| spl0_89
| ~ spl0_134 ),
inference(sat_conversion,[],[f2892]) ).
cnf(s760,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_130
| spl0_163 ),
inference(sat_conversion,[],[f2913]) ).
cnf(s761,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_77
| ~ spl0_125 ),
inference(sat_conversion,[],[f2914]) ).
cnf(s764,plain,
( ~ spl0_7
| ~ spl0_10
| ~ spl0_124
| ~ spl0_125 ),
inference(sat_conversion,[],[f2919]) ).
cnf(s766,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_73
| ~ spl0_120 ),
inference(sat_conversion,[],[f2922]) ).
cnf(s767,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_71
| ~ spl0_118 ),
inference(sat_conversion,[],[f2923]) ).
cnf(s791,plain,
( ~ spl0_9
| ~ spl0_32
| ~ spl0_151
| ~ spl0_153 ),
inference(sat_conversion,[],[f3007]) ).
cnf(s806,plain,
( ~ spl0_18
| ~ spl0_20
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f3065]) ).
cnf(s813,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f3077]) ).
cnf(s816,plain,
( ~ spl0_8
| spl0_92
| ~ spl0_137
| ~ spl0_161 ),
inference(sat_conversion,[],[f3082]) ).
cnf(s828,plain,
( ~ spl0_6
| spl0_77
| ~ spl0_125
| ~ spl0_166 ),
inference(sat_conversion,[],[f3150]) ).
cnf(s831,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_125
| spl0_166 ),
inference(sat_conversion,[],[f3191]) ).
cnf(s856,plain,
( ~ spl0_16
| ~ spl0_38
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f3292]) ).
cnf(s857,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_59
| spl0_72
| spl0_73 ),
inference(sat_conversion,[],[f3297]) ).
cnf(s868,plain,
( ~ spl0_2
| ~ spl0_154
| ~ spl0_155
| ~ spl0_156 ),
inference(sat_conversion,[],[f3333]) ).
cnf(s883,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| spl0_64
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f3360]) ).
cnf(s884,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_151
| ~ spl0_153 ),
inference(sat_conversion,[],[f3363]) ).
cnf(s890,plain,
( ~ spl0_14
| ~ spl0_17
| spl0_90
| ~ spl0_136 ),
inference(sat_conversion,[],[f3397]) ).
cnf(s892,plain,
( ~ spl0_18
| ~ spl0_19
| ~ spl0_125
| spl0_166 ),
inference(sat_conversion,[],[f3413]) ).
cnf(s899,plain,
( ~ spl0_4
| ~ spl0_25
| ~ spl0_37
| ~ spl0_151
| ~ spl0_153 ),
inference(sat_conversion,[],[f3468]) ).
cnf(s901,plain,
( ~ spl0_5
| spl0_77
| ~ spl0_124
| ~ spl0_125 ),
inference(sat_conversion,[],[f3492]) ).
cnf(s902,plain,
( ~ spl0_5
| ~ spl0_16
| ~ spl0_17
| spl0_79
| spl0_80
| ~ spl0_128 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s910,plain,
( ~ spl0_7
| ~ spl0_154
| ~ spl0_155
| ~ spl0_165 ),
inference(sat_conversion,[],[f3526]) ).
cnf(s911,plain,
( ~ spl0_4
| ~ spl0_13
| spl0_71
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f3549]) ).
cnf(s915,plain,
( ~ spl0_15
| spl0_68
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f3578]) ).
cnf(s916,plain,
( ~ spl0_11
| ~ spl0_15
| spl0_68
| spl0_70 ),
inference(sat_conversion,[],[f3580]) ).
cnf(s930,plain,
( ~ spl0_7
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f3610]) ).
cnf(s932,plain,
( ~ spl0_1
| spl0_83
| spl0_84
| ~ spl0_130 ),
inference(sat_conversion,[],[f3616]) ).
cnf(s943,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f3641]) ).
cnf(s950,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_13
| ~ spl0_20
| spl0_66 ),
inference(sat_conversion,[],[f3665]) ).
cnf(s955,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_13
| ~ spl0_20
| spl0_103 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s959,plain,
( ~ spl0_1
| ~ spl0_10
| spl0_64
| ~ spl0_113 ),
inference(sat_conversion,[],[f3676]) ).
cnf(s964,plain,
( ~ spl0_6
| spl0_103
| ~ spl0_146
| ~ spl0_147 ),
inference(sat_conversion,[],[f3690]) ).
cnf(s985,plain,
( ~ spl0_6
| ~ spl0_18
| ~ spl0_43
| spl0_74
| ~ spl0_122 ),
inference(sat_conversion,[],[f3745]) ).
cnf(s991,plain,
( ~ spl0_11
| ~ spl0_25
| ~ spl0_147
| spl0_169 ),
inference(sat_conversion,[],[f3769]) ).
cnf(s996,plain,
( ~ spl0_9
| ~ spl0_45
| spl0_76
| ~ spl0_123 ),
inference(sat_conversion,[],[f3832]) ).
cnf(s997,plain,
( ~ spl0_9
| ~ spl0_45
| spl0_85
| ~ spl0_132 ),
inference(sat_conversion,[],[f3834]) ).
cnf(s1001,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| spl0_78
| ~ spl0_126 ),
inference(sat_conversion,[],[f3854]) ).
cnf(s1002,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| spl0_81
| ~ spl0_129 ),
inference(sat_conversion,[],[f3856]) ).
cnf(s1004,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_148
| ~ spl0_149 ),
inference(sat_conversion,[],[f3861]) ).
cnf(s1011,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_139
| ~ spl0_140 ),
inference(sat_conversion,[],[f3867]) ).
cnf(s1018,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_21
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f3881]) ).
cnf(s1031,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_21
| ~ spl0_38
| ~ spl0_115 ),
inference(sat_conversion,[],[f3915]) ).
cnf(s1033,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_21
| ~ spl0_38
| ~ spl0_126 ),
inference(sat_conversion,[],[f3917]) ).
cnf(s1043,plain,
( ~ spl0_5
| spl0_103
| ~ spl0_147
| ~ spl0_169 ),
inference(sat_conversion,[],[f3928]) ).
cnf(s1048,plain,
( ~ spl0_4
| ~ spl0_21
| ~ spl0_126
| ~ spl0_127 ),
inference(sat_conversion,[],[f3970]) ).
cnf(s1050,plain,
( ~ spl0_4
| ~ spl0_21
| ~ spl0_131
| ~ spl0_132 ),
inference(sat_conversion,[],[f3974]) ).
cnf(s1051,plain,
( ~ spl0_4
| ~ spl0_21
| ~ spl0_159
| ~ spl0_160 ),
inference(sat_conversion,[],[f3976]) ).
cnf(s1057,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25
| spl0_67
| ~ spl0_117 ),
inference(sat_conversion,[],[f4032]) ).
cnf(s1058,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_21
| ~ spl0_25
| spl0_79
| ~ spl0_128 ),
inference(sat_conversion,[],[f4034]) ).
cnf(s1074,plain,
( ~ spl0_15
| spl0_68
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f4071]) ).
cnf(s1077,plain,
( ~ spl0_16
| ~ spl0_38
| spl0_105
| spl0_107 ),
inference(sat_conversion,[],[f4078]) ).
cnf(s1078,plain,
( ~ spl0_7
| ~ spl0_39
| ~ spl0_146
| ~ spl0_147 ),
inference(sat_conversion,[],[f4080]) ).
cnf(s1086,plain,
( ~ spl0_15
| spl0_91
| spl0_92
| spl0_161 ),
inference(sat_conversion,[],[f4094]) ).
cnf(s1088,plain,
( ~ spl0_7
| ~ spl0_124
| ~ spl0_125
| ~ spl0_166 ),
inference(sat_conversion,[],[f4097]) ).
cnf(s1090,plain,
( ~ spl0_13
| spl0_91
| spl0_92
| ~ spl0_137 ),
inference(sat_conversion,[],[f4109]) ).
cnf(s1096,plain,
( ~ spl0_12
| spl0_81
| spl0_82
| ~ spl0_129 ),
inference(sat_conversion,[],[f4166]) ).
cnf(s1099,plain,
( ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| spl0_102
| ~ spl0_144 ),
inference(sat_conversion,[],[f4173]) ).
cnf(s1104,plain,
( ~ spl0_11
| ~ spl0_15
| ~ spl0_25
| spl0_102
| ~ spl0_145 ),
inference(sat_conversion,[],[f4176]) ).
cnf(s1108,plain,
( ~ spl0_11
| ~ spl0_25
| spl0_102
| ~ spl0_145 ),
inference(sat_conversion,[],[f4180]) ).
cnf(s1115,plain,
( ~ spl0_9
| spl0_96
| ~ spl0_141
| ~ spl0_142 ),
inference(sat_conversion,[],[f4247]) ).
cnf(s1116,plain,
( ~ spl0_19
| spl0_64
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f4323]) ).
cnf(s1117,plain,
( ~ spl0_19
| ~ spl0_155
| ~ spl0_156
| spl0_165 ),
inference(sat_conversion,[],[f4325]) ).
cnf(s1118,plain,
spl0_3,
inference(rat,[],[s165,s169,s192,s199]) ).
cnf(s1119,plain,
( ~ spl0_42
| ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s813,s121,s122]) ).
cnf(s1120,plain,
( spl0_18
| spl0_13
| spl0_9 ),
inference(rat,[],[s1116,s66,s113,s114,s9,s32,s1118]) ).
cnf(s1121,plain,
( ~ spl0_41
| ~ spl0_19 ),
inference(rat,[],[s1116,s66,s113,s114]) ).
cnf(s1122,plain,
( ~ spl0_35
| ~ spl0_10
| ~ spl0_7 ),
inference(rat,[],[s764,s124,s125]) ).
cnf(s1124,plain,
( ~ spl0_40
| ~ spl0_10
| ~ spl0_7 ),
inference(rat,[],[s669,s149,s150]) ).
cnf(s1125,plain,
( spl0_40
| spl0_21
| ~ spl0_16
| spl0_42 ),
inference(rat,[],[s856,s64,s65,s37,s1074,s70,s71,s72,s58,s43,s1118]) ).
cnf(s1127,plain,
( ~ spl0_57
| ~ spl0_6 ),
inference(rat,[],[s964,s105,s146,s147]) ).
cnf(s1128,plain,
( ~ spl0_40
| ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s1004,s148,s149]) ).
cnf(s1129,plain,
( ~ spl0_21
| ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s163,s115,s126,s1031,s1033,s58,s1128,s1119,s1118]) ).
cnf(s1130,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s1125,s1129,s1128,s33,s1119,s3,s1,s1118]) ).
cnf(s1131,plain,
( ~ spl0_8
| spl0_21
| ~ spl0_4 ),
inference(rat,[],[s684,s118,s119,s38,s806,s64,s65,s26,s37,s1074,s70,s71,s72,s1125,s43,s1128,s1119,s1118]) ).
cnf(s1132,plain,
( ~ spl0_40
| spl0_6
| ~ spl0_2 ),
inference(rat,[],[s2,s930,s943,s148,s149,s150,s1118]) ).
cnf(s1133,plain,
( ~ spl0_48
| ~ spl0_13
| ~ spl0_4 ),
inference(rat,[],[s911,s73,s118,s119]) ).
cnf(s1134,plain,
( spl0_16
| spl0_48
| spl0_62
| spl0_63
| spl0_15 ),
inference(rat,[],[s806,s38,s26,s1118]) ).
cnf(s1135,plain,
( spl0_14
| spl0_5
| ~ spl0_16
| spl0_15 ),
inference(rat,[],[s680,s85,s86,s23,s12,s1118]) ).
cnf(s1136,plain,
( ~ spl0_36
| ~ spl0_14
| ~ spl0_4 ),
inference(rat,[],[s1011,s139,s140]) ).
cnf(s1137,plain,
( ~ spl0_33
| ~ spl0_17
| ~ spl0_16 ),
inference(rat,[],[s680,s85,s86]) ).
cnf(s1138,plain,
( ~ spl0_53
| ~ spl0_59
| ~ spl0_17
| ~ spl0_16 ),
inference(rat,[],[s857,s74,s75]) ).
cnf(s1139,plain,
( ~ spl0_26
| ~ spl0_14
| ~ spl0_4 ),
inference(rat,[],[s884,s151,s153]) ).
cnf(s1140,plain,
( ~ spl0_24
| ~ spl0_13 ),
inference(rat,[],[s1090,s93,s94,s137]) ).
cnf(s1141,plain,
( spl0_5
| ~ spl0_16
| ~ spl0_13
| spl0_15
| spl0_6
| ~ spl0_146
| ~ spl0_147
| ~ spl0_4 ),
inference(rat,[],[s890,s92,s136,s57,s1138,s28,s766,s75,s120,s45,s1139,s1136,s1135,s1078,s2,s1140,s1118]) ).
cnf(s1142,plain,
( ~ spl0_41
| ~ spl0_17
| ~ spl0_16
| ~ spl0_2 ),
inference(rat,[],[s883,s66,s113,s114]) ).
cnf(s1143,plain,
( ~ spl0_17
| spl0_43
| ~ spl0_5
| spl0_38
| ~ spl0_16
| spl0_85
| ~ spl0_132
| ~ spl0_2 ),
inference(rat,[],[s902,s81,s82,s128,s35,s997,s34,s1142,s1118]) ).
cnf(s1144,plain,
( spl0_21
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s766,s75,s120,s45,s28,s1139,s1136,s12,s1143,s1078,s570,s39,s1141,s1140,s76,s122,s856,s1125,s1134,s1133,s64,s65,s13,s37,s1074,s70,s71,s72,s43,s1132,s1127,s146,s147,s87,s132,s53,s54,s1118]) ).
cnf(s1145,plain,
( ~ spl0_34
| ~ spl0_21
| ~ spl0_4 ),
inference(rat,[],[s1048,s126,s127]) ).
cnf(s1146,plain,
( ~ spl0_17
| spl0_38
| ~ spl0_16
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s122,s58,s985,s1124,s34,s32,s4,s24,s697,s567,s144,s145,s90,s134,s165,s51,s52,s159,s133,s123,s132,s1142,s509,s496,s500,s501,s502,s6,s1133,s59,s1145,s1129,s1144,s1130,s1118]) ).
cnf(s1147,plain,
( ~ spl0_44
| ~ spl0_18
| ~ spl0_25
| ~ spl0_21
| ~ spl0_4 ),
inference(rat,[],[s1058,s81,s128]) ).
cnf(s1148,plain,
( ~ spl0_46
| ~ spl0_45
| ~ spl0_9 ),
inference(rat,[],[s996,s78,s123]) ).
cnf(s1149,plain,
( ~ spl0_27
| ~ spl0_21
| ~ spl0_4 ),
inference(rat,[],[s1050,s131,s132]) ).
cnf(s1151,plain,
( ~ spl0_23
| ~ spl0_7
| ~ spl0_39 ),
inference(rat,[],[s678,s144,s145]) ).
cnf(s1152,plain,
( ~ spl0_158
| ~ spl0_21
| ~ spl0_4 ),
inference(rat,[],[s1051,s158,s159]) ).
cnf(s1153,plain,
( spl0_6
| ~ spl0_25
| ~ spl0_9
| spl0_38
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s24,s1108,s1151,s104,s145,s165,s1121,s9,s31,s1147,s35,s1148,s52,s1132,s1149,s1152,s1133,s59,s1145,s1144,s1118]) ).
cnf(s1154,plain,
( ~ spl0_23
| ~ spl0_6
| ~ spl0_25
| ~ spl0_2 ),
inference(rat,[],[s713,s144,s145]) ).
cnf(s1155,plain,
( spl0_38
| ~ spl0_16
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s209,s113,s114,s165,s1154,s1153,s27,s28,s1139,s1136,s6,s1133,s1146,s59,s1129,s1145,s1152,s1144,s1130,s1118]) ).
cnf(s1156,plain,
( spl0_9
| spl0_17
| spl0_27
| spl0_8
| ~ spl0_4 ),
inference(rat,[],[s6,s1136,s1133,s28,s50,s1118]) ).
cnf(s1157,plain,
( ~ spl0_41
| ~ spl0_25
| ~ spl0_2 ),
inference(rat,[],[s209,s113,s114]) ).
cnf(s1158,plain,
( ~ spl0_104
| ~ spl0_38
| ~ spl0_16 ),
inference(rat,[],[s1077,s106,s108]) ).
cnf(s1159,plain,
( ~ spl0_60
| ~ spl0_18
| ~ spl0_25
| ~ spl0_21
| ~ spl0_4 ),
inference(rat,[],[s1057,s69,s117]) ).
cnf(s1160,plain,
( ~ spl0_28
| ~ spl0_2 ),
inference(rat,[],[s868,s154,s155,s156]) ).
cnf(s1161,plain,
( ~ spl0_25
| ~ spl0_60
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s1151,s31,s2,s1132,s1154,s165,s1159,s1157,s1152,s1018,s116,s1144,s117,s1118]) ).
cnf(s1162,plain,
( ~ spl0_16
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s443,s44,s2,s1133,s254,s6,s1139,s151,s152,s27,s1161,s450,s1018,s69,s116,s117,s167,s1158,s1155,s1160,s1129,s1145,s1144,s1130,s1118]) ).
cnf(s1163,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s791,s151,s153,s27,s473,s22,s1157,s125,s1096,s165,s200,s83,s84,s129,s1151,s161,s39,s38,s50,s44,s1140,s1133,s11,s1162,s1152,s1149,s1145,s1129,s1144,s1130,s1118]) ).
cnf(s1164,plain,
( ~ spl0_38
| ~ spl0_21
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s69,s167,s450,s1158,s19,s1160,s1130,s1163,s1118]) ).
cnf(s1169,plain,
( ~ spl0_23
| ~ spl0_7
| spl0_40
| ~ spl0_14
| ~ spl0_21
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s552,s83,s5,s31,s30,s597,s1151,s104,s145,s19,s1160,s1130,s1163,s1164,s1118]) ).
cnf(s1170,plain,
( ~ spl0_7
| spl0_40
| ~ spl0_14
| ~ spl0_21
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s598,s4,s159,s1122,s165,s200,s1169,s1142,s19,s1160,s1163,s1130,s1118]) ).
cnf(s1171,plain,
( ~ spl0_34
| ~ spl0_21
| ~ spl0_17 ),
inference(rat,[],[s233,s80,s127]) ).
cnf(s1172,plain,
( ~ spl0_7
| ~ spl0_14
| spl0_1
| ~ spl0_21
| ~ spl0_16 ),
inference(rat,[],[s930,s148,s149,s150,s1170]) ).
cnf(s1173,plain,
( spl0_6
| ~ spl0_14
| ~ spl0_21
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s49,s83,s727,s596,s10,s767,s34,s570,s76,s122,s58,s2,s1132,s1137,s1142,s119,s118,s73,s59,s1164,s24,s1172,s1171,s19,s1160,s1130,s1163,s1118]) ).
cnf(s1174,plain,
( ~ spl0_20
| spl0_71
| ~ spl0_119
| ~ spl0_21
| spl0_33
| ~ spl0_17 ),
inference(rat,[],[s699,s83,s84,s49,s727,s1118]) ).
cnf(s1175,plain,
( ~ spl0_14
| ~ spl0_21
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s597,s104,s145,s200,s79,s384,s1173,s24,s1172,s32,s34,s767,s10,s1174,s119,s1137,s73,s118,s59,s1171,s1164,s1142,s19,s1160,s1163,s1130,s1118]) ).
cnf(s1176,plain,
( ~ spl0_42
| ~ spl0_5
| ~ spl0_43 ),
inference(rat,[],[s570,s76,s122]) ).
cnf(s1177,plain,
( ~ spl0_21
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s943,s149,s150,s58,s1176,s23,s1175,s34,s767,s10,s1174,s73,s118,s119,s59,s1171,s1164,s1137,s1142,s19,s1160,s1163,s1130,s1118]) ).
cnf(s1178,plain,
( ~ spl0_23
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17 ),
inference(rat,[],[s597,s104,s145]) ).
cnf(s1179,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s892,s1088,s124,s125,s15,s200,s1178,s5,s1096,s83,s84,s129,s31,s30,s1078,s19,s1160,s1163,s147,s146,s856,s64,s65,s37,s915,s70,s71,s72,s43,s1132,s1127,s53,s1130,s1177,s1118]) ).
cnf(s1180,plain,
( ~ spl0_5
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s1143,s1176,s19,s1160,s1163,s132,s87,s54,s1125,s856,s64,s65,s37,s915,s70,s71,s72,s43,s1132,s1127,s53,s1130,s1177,s1118]) ).
cnf(s1181,plain,
( ~ spl0_16
| spl0_1 ),
inference(rat,[],[s1179,s2,s23,s1180,s1127,s53,s1177,s1137,s19,s1160,s1130,s1163,s1118]) ).
cnf(s1182,plain,
( ~ spl0_23
| spl0_40
| ~ spl0_7
| ~ spl0_14
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s85,s528,s1174,s10,s767,s4,s1122,s73,s118,s119,s25,s44,s31,s1178,s1151,s1171,s19,s1160,s1130,s1163,s1118]) ).
cnf(s1183,plain,
( spl0_23
| ~ spl0_7
| ~ spl0_14
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s159,s598,s165,s4,s1121,s1122,s15,s200,s19,s1160,s1130,s1163,s1118]) ).
cnf(s1184,plain,
( ~ spl0_23
| ~ spl0_7
| spl0_1
| ~ spl0_14
| ~ spl0_21 ),
inference(rat,[],[s930,s148,s149,s150,s1182]) ).
cnf(s1185,plain,
( ~ spl0_7
| ~ spl0_14
| spl0_1
| ~ spl0_21 ),
inference(rat,[],[s1184,s1183]) ).
cnf(s1186,plain,
( ~ spl0_14
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s32,s598,s412,s159,s2,s165,s901,s1121,s79,s124,s125,s15,s200,s1178,s24,s1185,s1171,s19,s1160,s1130,s1163,s1118]) ).
cnf(s1187,plain,
( ~ spl0_20
| spl0_71
| ~ spl0_119
| ~ spl0_18
| ~ spl0_21
| ~ spl0_17 ),
inference(rat,[],[s85,s528,s1174]) ).
cnf(s1188,plain,
( ~ spl0_41
| ~ spl0_21
| ~ spl0_17 ),
inference(rat,[],[s267,s66,s114]) ).
cnf(s1189,plain,
( spl0_39
| spl0_40
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s34,s237,s767,s26,s10,s1187,s73,s118,s119,s44,s31,s1181,s1171,s1188,s19,s1160,s1130,s68,s67,s40,s1163,s1118]) ).
cnf(s1190,plain,
( ~ spl0_39
| ~ spl0_7
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s10,s699,s767,s83,s84,s73,s118,s21,s38,s710,s723,s4,s461,s158,s159,s1122,s125,s165,s15,s200,s1151,s1181,s1188,s19,s1160,s1130,s1163,s1118]) ).
cnf(s1191,plain,
( ~ spl0_7
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s930,s148,s149,s150,s1189,s1190]) ).
cnf(s1192,plain,
( ~ spl0_18
| spl0_55
| ~ spl0_20
| ~ spl0_21
| ~ spl0_17 ),
inference(rat,[],[s49,s85,s83,s528,s527,s1118]) ).
cnf(s1193,plain,
( spl0_13
| spl0_25
| ~ spl0_49
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s699,s83,s84,s21,s740,s118,s119,s38,s1192,s726,s10,s11,s19,s1160,s1130,s1163,s1181,s115,s67,s1118]) ).
cnf(s1194,plain,
( ~ spl0_13
| ~ spl0_5
| ~ spl0_49
| ~ spl0_11
| spl0_7
| spl0_41
| spl0_16 ),
inference(rat,[],[s34,s767,s237,s73,s118,s26,s39,s950,s1140,s68,s67,s1118]) ).
cnf(s1195,plain,
( ~ spl0_5
| ~ spl0_49
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s760,s715,s130,s1174,s73,s119,s38,s1192,s726,s1193,s10,s1194,s1181,s1188,s24,s1191,s1171,s19,s1160,s1130,s1163,s115,s67,s1118]) ).
cnf(s1196,plain,
( ~ spl0_49
| ~ spl0_21
| spl0_1 ),
inference(rat,[],[s159,s165,s723,s1154,s1193,s424,s73,s118,s32,s38,s562,s85,s130,s2,s23,s1195,s1181,s1186,s1188,s19,s1160,s1130,s1163,s1191,s1118]) ).
cnf(s1197,plain,
( ~ spl0_40
| ~ spl0_2 ),
inference(rat,[],[s706,s1132,s148,s149,s150]) ).
cnf(s1198,plain,
spl0_1,
inference(rat,[],[s5,s950,s652,s2,s4,s1078,s767,s31,s73,s118,s806,s1134,s64,s65,s112,s26,s13,s37,s915,s70,s71,s72,s1127,s146,s147,s43,s53,s1196,s68,s40,s1197,s1181,s1163,s1130,s1118]) ).
cnf(s1199,plain,
( ~ spl0_25
| spl0_6
| ~ spl0_16
| ~ spl0_9
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s167,s1158,s1161,s1153,s1160]) ).
cnf(s1200,plain,
( ~ spl0_26
| ~ spl0_7
| spl0_34
| spl0_8
| ~ spl0_4 ),
inference(rat,[],[s1133,s44,s6,s443,s1139,s151,s152,s1118]) ).
cnf(s1201,plain,
( ~ spl0_7
| ~ spl0_9
| spl0_158
| spl0_34
| spl0_8
| ~ spl0_2
| spl0_17 ),
inference(rat,[],[s1133,s11,s44,s1199,s1151,s1154,s165,s1157,s27,s1200,s19,s1160,s1118]) ).
cnf(s1202,plain,
( ~ spl0_13
| spl0_7
| ~ spl0_4 ),
inference(rat,[],[s39,s1140,s1133,s1118]) ).
cnf(s1203,plain,
( ~ spl0_2
| spl0_17
| ~ spl0_21 ),
inference(rat,[],[s1199,s11,s1154,s165,s1157,s27,s1139,s6,s1202,s1201,s1156,s1152,s1149,s1145,s1129,s19,s1160,s1118]) ).
cnf(s1204,plain,
( ~ spl0_4
| spl0_2
| ~ spl0_21 ),
inference(rat,[],[s1202,s6,s1200,s1139,s17,s1145,s1129,s1118]) ).
cnf(s1205,plain,
( ~ spl0_30
| ~ spl0_12 ),
inference(rat,[],[s1096,s83,s84,s129]) ).
cnf(s1206,plain,
~ spl0_33,
inference(rat,[],[s932,s85,s86,s130,s1198]) ).
cnf(s1207,plain,
( ~ spl0_48
| ~ spl0_12 ),
inference(rat,[],[s220,s73,s119,s49,s1205,s1206,s1118]) ).
cnf(s1208,plain,
( ~ spl0_49
| ~ spl0_12 ),
inference(rat,[],[s219,s67,s115,s49,s1205,s1206,s1118]) ).
cnf(s1209,plain,
( ~ spl0_40
| ~ spl0_7 ),
inference(rat,[],[s930,s148,s149,s150]) ).
cnf(s1210,plain,
( ~ spl0_7
| ~ spl0_154
| ~ spl0_155
| ~ spl0_156
| spl0_4
| spl0_2 ),
inference(rat,[],[s816,s6,s1086,s1140,s93,s94,s137,s16,s1099,s1104,s5,s1208,s40,s1209,s104,s144,s145,s15,s7,s1117,s670,s910,s1118]) ).
cnf(s1211,plain,
( ~ spl0_30
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21 ),
inference(rat,[],[s1002,s83,s129,s1198]) ).
cnf(s1212,plain,
( ~ spl0_35
| ~ spl0_5
| ~ spl0_11 ),
inference(rat,[],[s761,s79,s125]) ).
cnf(s1213,plain,
( ~ spl0_10
| spl0_35
| ~ spl0_20
| ~ spl0_21 ),
inference(rat,[],[s1001,s80,s126,s162,s1211,s1198]) ).
cnf(s1214,plain,
( spl0_35
| ~ spl0_11
| ~ spl0_20
| ~ spl0_14
| spl0_2
| ~ spl0_21 ),
inference(rat,[],[s1099,s104,s144,s7,s200,s1213,s1118]) ).
cnf(s1215,plain,
( ~ spl0_23
| ~ spl0_15
| ~ spl0_11
| ~ spl0_14 ),
inference(rat,[],[s1099,s104,s144]) ).
cnf(s1216,plain,
( ~ spl0_52
| ~ spl0_15
| ~ spl0_11 ),
inference(rat,[],[s916,s70,s72]) ).
cnf(s1217,plain,
( ~ spl0_11
| spl0_13
| ~ spl0_14
| spl0_17
| ~ spl0_21 ),
inference(rat,[],[s1115,s98,s141,s142,s164,s1216,s7,s1121,s831,s9,s1120,s828,s412,s2,s1212,s79,s125,s1214,s1210,s154,s155,s156,s19,s10,s1204,s1203,s1118,s1198]) ).
cnf(s1218,plain,
( ~ spl0_52
| ~ spl0_15 ),
inference(rat,[],[s1074,s70,s71,s72]) ).
cnf(s1219,plain,
( spl0_13
| ~ spl0_14
| spl0_17
| ~ spl0_21 ),
inference(rat,[],[s1115,s98,s141,s142,s164,s1218,s1121,s9,s1120,s412,s2,s7,s901,s1001,s79,s124,s125,s80,s126,s25,s24,s1217,s10,s1210,s154,s155,s156,s19,s1204,s1203,s1118,s1198]) ).
cnf(s1220,plain,
( ~ spl0_14
| spl0_17
| ~ spl0_21 ),
inference(rat,[],[s1108,s104,s145,s200,s1212,s2,s422,s97,s139,s28,s5,s584,s1207,s73,s118,s39,s16,s1140,s1219,s1210,s154,s155,s156,s19,s1204,s1203,s1118]) ).
cnf(s1221,plain,
( ~ spl0_35
| ~ spl0_5 ),
inference(rat,[],[s901,s79,s124,s125]) ).
cnf(s1222,plain,
( spl0_17
| ~ spl0_21 ),
inference(rat,[],[s264,s100,s101,s47,s1108,s104,s145,s25,s200,s1221,s1218,s23,s12,s1220,s1204,s1203,s1206,s1118]) ).
cnf(s1223,plain,
( ~ spl0_14
| ~ spl0_4
| ~ spl0_21 ),
inference(rat,[],[s749,s90,s91,s134,s51,s52,s133,s123,s496,s501,s1222,s1129,s1149,s1198,s1118]) ).
cnf(s1224,plain,
( ~ spl0_4
| ~ spl0_21 ),
inference(rat,[],[s1151,s44,s1202,s1133,s6,s1223,s165,s1152,s1129,s1171,s1188,s1222,s1118]) ).
cnf(s1225,plain,
( ~ spl0_14
| ~ spl0_2
| ~ spl0_21 ),
inference(rat,[],[s2,s545,s412,s32,s598,s159,s1221,s79,s125,s165,s200,s1178,s1188,s5,s1224,s1208,s163,s1197,s1171,s1222,s1118]) ).
cnf(s1226,plain,
( ~ spl0_43
| ~ spl0_2
| ~ spl0_21 ),
inference(rat,[],[s453,s26,s58,s237,s1176,s68,s67,s163,s1197,s699,s83,s84,s162,s1221,s23,s1225,s1171,s1222,s1118,s1206]) ).
cnf(s1227,plain,
( ~ spl0_48
| ~ spl0_9
| ~ spl0_13 ),
inference(rat,[],[s767,s73,s118]) ).
cnf(s1228,plain,
( ~ spl0_2
| ~ spl0_21 ),
inference(rat,[],[s1151,s39,s44,s1227,s34,s1226,s1140,s10,s699,s83,s84,s162,s200,s1221,s23,s1225,s1171,s1188,s1222,s1224,s1118,s1206]) ).
cnf(s1229,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_21 ),
inference(rat,[],[s649,s98,s142,s164,s1218,s32,s7,s545,s1122,s125,s200,s1178,s5,s1208,s163,s1209,s1171,s1188,s1222,s1224,s1228,s1118]) ).
cnf(s1230,plain,
( ~ spl0_14
| ~ spl0_21 ),
inference(rat,[],[s649,s98,s142,s164,s1218,s7,s831,s32,s828,s412,s2,s1221,s79,s125,s200,s1178,s24,s1229,s1171,s1188,s1222,s1228,s1118,s1198]) ).
cnf(s1231,plain,
( ~ spl0_17
| ~ spl0_21 ),
inference(rat,[],[s1140,s10,s16,s699,s1108,s83,s84,s104,s145,s162,s25,s200,s1221,s23,s1230,s1228,s1224,s1171,s1206,s1118]) ).
cnf(s1232,plain,
~ spl0_21,
inference(rat,[],[s1231,s1222]) ).
cnf(s1233,plain,
spl0_27,
inference(rat,[],[s54,s1118,s1232]) ).
cnf(s1234,plain,
spl0_57,
inference(rat,[],[s53,s1118,s1232]) ).
cnf(s1235,plain,
spl0_132,
inference(rat,[],[s132,s1233]) ).
cnf(s1237,plain,
~ spl0_85,
inference(rat,[],[s87,s1233]) ).
cnf(s1238,plain,
spl0_147,
inference(rat,[],[s147,s1234]) ).
cnf(s1239,plain,
spl0_146,
inference(rat,[],[s146,s1234]) ).
cnf(s1240,plain,
~ spl0_103,
inference(rat,[],[s105,s1234]) ).
cnf(s1241,plain,
~ spl0_6,
inference(rat,[],[s1127,s1234]) ).
cnf(s1242,plain,
( spl0_23
| ~ spl0_2 ),
inference(rat,[],[s892,s31,s1088,s1078,s2,s1221,s124,s125,s15,s200,s1197,s1144,s1118,s1239,s1238,s1241,s1232]) ).
cnf(s1243,plain,
~ spl0_2,
inference(rat,[],[s856,s1143,s26,s568,s955,s23,s1178,s1242,s64,s65,s112,s13,s37,s5,s1218,s1208,s19,s43,s40,s1144,s1197,s1160,s1237,s1235,s1118,s1240,s1206,s1232]) ).
cnf(s1244,plain,
( ~ spl0_4
| spl0_17 ),
inference(rat,[],[s1209,s43,s1202,s1218,s6,s12,s1139,s17,s1131,s1232,s1118,s1243]) ).
cnf(s1245,plain,
( ~ spl0_154
| spl0_4
| ~ spl0_155
| ~ spl0_156 ),
inference(rat,[],[s816,s6,s1086,s1215,s13,s1140,s93,s94,s137,s16,s991,s25,s200,s1043,s1221,s2,s1210,s1241,s1240,s1238,s1243,s1232,s1118]) ).
cnf(s1246,plain,
( spl0_4
| spl0_17 ),
inference(rat,[],[s1245,s154,s155,s156,s19,s1118]) ).
cnf(s1247,plain,
spl0_17,
inference(rat,[],[s1246,s1244]) ).
cnf(s1248,plain,
~ spl0_4,
inference(rat,[],[s959,s66,s113,s34,s568,s791,s65,s112,s22,s37,s7,s1205,s1218,s29,s43,s899,s1209,s16,s1202,s1140,s6,s23,s1139,s151,s153,s17,s1131,s1198,s1118,s1232,s1243,s1206]) ).
cnf(s1249,plain,
( ~ spl0_7
| ~ spl0_14 ),
inference(rat,[],[s200,s1122,s1178,s7,s5,s1218,s1208,s43,s40,s1209,s1247,s1118,s1243,s1248,s1232]) ).
cnf(s1250,plain,
~ spl0_14,
inference(rat,[],[s1178,s25,s200,s1221,s2,s1249,s1247,s1118,s1248,s1241]) ).
cnf(s1251,plain,
spl0_5,
inference(rat,[],[s23,s1206,s1118,s1250]) ).
cnf(s1252,plain,
~ spl0_35,
inference(rat,[],[s1221,s1251]) ).
cnf(s1253,plain,
~ spl0_169,
inference(rat,[],[s1043,s1240,s1238,s1251]) ).
cnf(s1255,plain,
spl0_11,
inference(rat,[],[s25,s1248,s1118,s1252]) ).
cnf(s1256,plain,
~ spl0_25,
inference(rat,[],[s991,s1238,s1255,s1253]) ).
cnf(s1260,plain,
spl0_24,
inference(rat,[],[s16,s1243,s1118,s1256]) ).
cnf(s1261,plain,
spl0_137,
inference(rat,[],[s137,s1260]) ).
cnf(s1262,plain,
~ spl0_92,
inference(rat,[],[s94,s1260]) ).
cnf(s1263,plain,
~ spl0_91,
inference(rat,[],[s93,s1260]) ).
cnf(s1264,plain,
~ spl0_13,
inference(rat,[],[s1140,s1260]) ).
cnf(s1265,plain,
spl0_15,
inference(rat,[],[s13,s1232,s1118,s1264]) ).
cnf(s1267,plain,
spl0_8,
inference(rat,[],[s6,s1118,s1250,s1264]) ).
cnf(s1269,plain,
spl0_161,
inference(rat,[],[s1086,s1262,s1263,s1265]) ).
cnf(s1271,plain,
$false,
inference(rat,[],[s816,s1262,s1261,s1269,s1267]) ).
fof(f4326,plain,
$false,
inference(avatar_sat_refutation,[],[s1271]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN471-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n002.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 16:13:49 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.65/1.00 % (481873)Input is clausal, will run a generic CNF schedule.
% 0.65/1.00 % (481881)lrs+10_1_sil=8000:sp=occurrence:random_seed=1600240658:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.65/1.00 % (481881)First to succeed.
% 0.65/1.00 % (481881)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-481873"
% 0.65/1.00 % (481884)dis-21_1_sil=8000:lcm=predicate:random_seed=3772195672:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 0.65/1.00 % (481879)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1341364304:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.65/1.00 % (481878)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=701015235:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.65/1.00 % (481880)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2858556972:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.65/1.00 % (481882)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=442666806:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.65/1.00 % (481883)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=436482701:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.65/1.00 % (481884)Also succeeded, but the first one will report.
% 0.65/1.00 % (481882)Also succeeded, but the first one will report.
% 0.65/1.00 % (481883)Also succeeded, but the first one will report.
% 0.65/1.00 % (481881)Refutation found. Thanks to Tanya!
% 0.65/1.00 % SZS status Unsatisfiable for theBenchmark
% 0.65/1.00 % SZS output start Proof for theBenchmark
% See solution above
% 2.84/1.10 % (481881)------------------------------
% 2.84/1.10 % (481881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.84/1.10 % (481881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/1.10 % (481881)CaDiCaL version: 2.1.3
% 2.84/1.10 % (481881)Termination reason: Refutation
% 2.84/1.10 % (481881)Time elapsed: 0.038 s
% 2.84/1.10 % (481881)Peak memory usage: 91 MB
% 2.84/1.10 % (481881)Instructions burned: 104 (million)
% 2.84/1.10 % (481881)------------------------------
% 2.84/1.10 % (481881)------------------------------
% 2.84/1.10 % (481873)Success in time 0.333 s
% 2.84/1.10 % Vampire exiting
%------------------------------------------------------------------------------