%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN459-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 : n005.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:52:33 PM UTC 2026
% Result : Unsatisfiable 3.15s 1.10s
% Output : Refutation 3.71s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp25
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f11,negated_conjecture,
( ~ hskp15
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
fof(f24,negated_conjecture,
( ~ hskp2
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
fof(f27,negated_conjecture,
( hskp25
| hskp15
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
fof(f28,negated_conjecture,
( hskp23
| hskp9
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
fof(f34,negated_conjecture,
( ~ hskp25
| c0_1(a230) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
( ~ hskp25
| c1_1(a230) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( ~ hskp25
| c2_1(a230) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( ~ hskp24
| c1_1(a215) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( ~ hskp24
| c2_1(a215) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
( ~ hskp24
| c3_1(a215) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( ~ hskp23
| c0_1(a189) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f41,negated_conjecture,
( ~ hskp23
| c1_1(a189) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
( ~ hskp23
| c3_1(a189) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f47,negated_conjecture,
( ~ hskp19
| c3_1(a225) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f51,negated_conjecture,
( ~ hskp15
| c2_1(a214) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp14
| c2_1(a210) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp14
| c3_1(a210) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp13
| c1_1(a209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( ~ hskp13
| c3_1(a209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f57,negated_conjecture,
( ~ hskp10
| c0_1(a200) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp10
| c3_1(a200) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp9
| c2_1(a199) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp8
| c1_1(a198) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp8
| c3_1(a198) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp7
| c1_1(a197) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp6
| c0_1(a195) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp5
| c0_1(a194) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp4
| c1_1(a193) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( ~ hskp3
| c0_1(a192) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( ~ hskp3
| c1_1(a192) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp1
| c0_1(a190) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp1
| c2_1(a190) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f75,negated_conjecture,
( ~ c0_1(a225)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ c1_1(a225)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f80,negated_conjecture,
( ~ c0_1(a221)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ c1_1(a221)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ c2_1(a221)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ c0_1(a214)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ c3_1(a214)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ c1_1(a210)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ c0_1(a209)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ c0_1(a206)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ c2_1(a206)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ c3_1(a206)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f92,negated_conjecture,
( ~ c1_1(a200)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c0_1(a199)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c1_1(a199)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c2_1(a198)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c0_1(a197)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c2_1(a197)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c1_1(a195)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c3_1(a195)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c1_1(a194)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c2_1(a194)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ c0_1(a193)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c3_1(a193)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c3_1(a192)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c1_1(a191)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c2_1(a191)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c3_1(a191)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c3_1(a190)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f110,negated_conjecture,
( ~ c1_1(a188)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c3_1(a188)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c3_1(X0)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp3
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp8
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f117,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp23
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f119,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp3
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f121,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp25
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f123,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp7
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp7
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp10
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp1
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp23
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp16
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f133,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X0)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| ~ c2_1(X0)
| ~ c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f137,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f141,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f145,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c0_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X0)
| c2_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| c2_1(X0)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
fof(f153,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X2)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f159,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c0_1(X2)
| c2_1(X1)
| c3_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f161,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c2_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X2)
| c3_1(X1)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f165,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f166,plain,
( ! [X2] :
( c1_1(X2)
| c3_1(X2)
| ~ c0_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f168,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f169,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f168]) ).
fof(f171,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f174,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f175,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f176,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f163,f174,f171,f168,f165]) ).
fof(f178,definition,
( spl0_5
<=> ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f179,plain,
( ! [X2] :
( c3_1(X2)
| ~ c0_1(X2)
| c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f181,definition,
( spl0_6
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f182,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f183,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f162,f168,f171,f181,f178]) ).
fof(f185,definition,
( spl0_7
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f186,plain,
( ! [X2] :
( c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f188,definition,
( spl0_8
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f189,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,definition,
( spl0_9
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f192,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( spl0_7
| spl0_8
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f161,f191,f171,f188,f185]) ).
fof(f198,definition,
( spl0_11
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f199,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f202,definition,
( spl0_12
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f203,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| ~ c0_1(X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f204,plain,
( spl0_12
| spl0_5
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f159,f198,f171,f178,f202]) ).
fof(f206,definition,
( spl0_13
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f207,plain,
( ! [X2] :
( c3_1(X2)
| ~ c2_1(X2)
| c0_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f210,definition,
( spl0_14
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f211,plain,
( ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f213,definition,
( spl0_15
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f214,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,definition,
( spl0_16
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f217,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f220,definition,
( spl0_17
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f221,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,definition,
( spl0_18
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f224,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f225,plain,
( spl0_14
| spl0_17
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f156,f223,f171,f220,f210]) ).
fof(f227,definition,
( spl0_19
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f228,plain,
( ! [X2] :
( c1_1(X2)
| ~ c2_1(X2)
| c0_1(X2) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f230,definition,
( spl0_20
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f231,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f232,plain,
( spl0_19
| spl0_20
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f155,f202,f171,f230,f227]) ).
fof(f234,definition,
( spl0_21
<=> ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f235,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f236,plain,
( spl0_19
| spl0_15
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f154,f234,f171,f213,f227]) ).
fof(f238,definition,
( spl0_22
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f241,definition,
( spl0_23
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f242,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f243,plain,
( spl0_22
| spl0_23
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f153,f198,f171,f241,f238]) ).
fof(f245,definition,
( spl0_24
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f249,definition,
( spl0_25
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f250,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f252,definition,
( spl0_26
<=> ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f253,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( spl0_25
| spl0_26
| spl0_14
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f151,f171,f210,f252,f249]) ).
fof(f256,definition,
( spl0_27
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f259,definition,
( spl0_28
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f260,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f261,plain,
( spl0_27
| spl0_28
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f150,f181,f171,f259,f256]) ).
fof(f263,definition,
( spl0_29
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f266,definition,
( spl0_30
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f267,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f268,plain,
( spl0_29
| spl0_5
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f149,f266,f171,f178,f263]) ).
fof(f270,definition,
( spl0_31
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f272,plain,
( spl0_31
| spl0_12
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f148,f168,f171,f202,f270]) ).
fof(f274,definition,
( spl0_32
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f276,plain,
( spl0_32
| spl0_23
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f147,f185,f171,f241,f274]) ).
fof(f277,plain,
( spl0_27
| spl0_15
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f146,f191,f171,f213,f256]) ).
fof(f279,definition,
( spl0_33
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f282,definition,
( spl0_34
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f283,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f284,plain,
( spl0_33
| spl0_15
| ~ spl0_3
| spl0_34 ),
inference(avatar_split_clause,[],[f145,f282,f171,f213,f279]) ).
fof(f286,definition,
( spl0_35
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f287,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f290,definition,
( spl0_36
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f292,plain,
( spl0_36
| spl0_17
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f143,f223,f171,f220,f290]) ).
fof(f294,definition,
( spl0_37
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f296,plain,
( spl0_37
| spl0_17
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f142,f259,f171,f220,f294]) ).
fof(f297,plain,
( spl0_29
| spl0_21
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f141,f191,f171,f234,f263]) ).
fof(f299,definition,
( spl0_38
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f302,plain,
( spl0_37
| spl0_12
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f139,f216,f171,f202,f294]) ).
fof(f304,definition,
( spl0_39
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f306,plain,
( spl0_39
| spl0_15
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f138,f202,f171,f213,f304]) ).
fof(f308,definition,
( spl0_40
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f309,plain,
( ! [X1] :
( c1_1(X1)
| ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f310,plain,
( spl0_39
| spl0_40
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f137,f191,f171,f308,f304]) ).
fof(f312,plain,
( spl0_29
| spl0_26
| spl0_23
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f135,f171,f241,f252,f263]) ).
fof(f314,definition,
( spl0_41
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f316,plain,
( spl0_41
| spl0_26
| spl0_20
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f134,f171,f230,f252,f314]) ).
fof(f318,definition,
( spl0_42
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f321,definition,
( spl0_43
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f322,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f323,plain,
( spl0_42
| spl0_43
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f133,f206,f171,f321,f318]) ).
fof(f327,definition,
( spl0_44
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f330,definition,
( spl0_45
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f331,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f334,definition,
( spl0_46
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f337,definition,
( spl0_47
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f338,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f339,plain,
( spl0_46
| spl0_47
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f129,f286,f171,f337,f334]) ).
fof(f341,definition,
( spl0_48
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f343,plain,
( spl0_27
| spl0_48
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f128,f174,f171,f341,f256]) ).
fof(f344,plain,
( spl0_42
| spl0_46
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f127,f174,f171,f334,f318]) ).
fof(f345,plain,
( spl0_39
| spl0_38
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f126,f168,f171,f299,f304]) ).
fof(f346,plain,
( spl0_37
| spl0_41
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f125,f223,f171,f314,f294]) ).
fof(f347,plain,
( spl0_31
| spl0_22
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f124,f191,f171,f238,f270]) ).
fof(f349,definition,
( spl0_49
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f351,plain,
( spl0_49
| spl0_22
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f123,f191,f171,f238,f349]) ).
fof(f357,definition,
( spl0_51
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f359,plain,
( spl0_48
| spl0_51
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f121,f259,f171,f357,f341]) ).
fof(f361,definition,
( spl0_52
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f365,definition,
( spl0_53
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f367,plain,
( spl0_27
| spl0_53
| ~ spl0_3
| spl0_45 ),
inference(avatar_split_clause,[],[f119,f330,f171,f365,f256]) ).
fof(f375,plain,
( spl0_48
| spl0_46
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f117,f165,f171,f334,f341]) ).
fof(f380,plain,
( spl0_31
| spl0_52
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f115,f286,f171,f361,f270]) ).
fof(f381,plain,
( spl0_49
| spl0_53
| ~ spl0_3
| spl0_40 ),
inference(avatar_split_clause,[],[f114,f308,f171,f365,f349]) ).
fof(f383,definition,
( spl0_57
<=> ! [X0] :
( c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f384,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f385,plain,
( spl0_24
| spl0_57
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f113,f171,f383,f245]) ).
fof(f386,plain,
( spl0_38
| spl0_47
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f112,f171,f337,f299]) ).
fof(f389,definition,
( spl0_58
<=> c3_1(a188) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f391,plain,
( ~ spl0_33
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f111,f389,f279]) ).
fof(f393,definition,
( spl0_59
<=> c1_1(a188) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f394,plain,
( ~ c1_1(a188)
| spl0_59 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f395,plain,
( ~ spl0_33
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f110,f393,f279]) ).
fof(f402,definition,
( spl0_61
<=> c3_1(a190) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f403,plain,
( ~ c3_1(a190)
| spl0_61 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( ~ spl0_38
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f108,f402,f299]) ).
fof(f407,definition,
( spl0_62
<=> c3_1(a191) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f408,plain,
( ~ c3_1(a191)
| spl0_62 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f409,plain,
( ~ spl0_39
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f107,f407,f304]) ).
fof(f411,definition,
( spl0_63
<=> c2_1(a191) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f413,plain,
( ~ spl0_39
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f106,f411,f304]) ).
fof(f415,definition,
( spl0_64
<=> c1_1(a191) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f416,plain,
( ~ c1_1(a191)
| spl0_64 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f417,plain,
( ~ spl0_39
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f105,f415,f304]) ).
fof(f420,definition,
( spl0_65
<=> c3_1(a192) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f422,plain,
( ~ spl0_53
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f104,f420,f365]) ).
fof(f425,definition,
( spl0_66
<=> c3_1(a193) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f426,plain,
( ~ c3_1(a193)
| spl0_66 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( ~ spl0_49
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f103,f425,f349]) ).
fof(f429,definition,
( spl0_67
<=> c0_1(a193) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f431,plain,
( ~ spl0_49
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f102,f429,f349]) ).
fof(f434,definition,
( spl0_68
<=> c2_1(a194) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f435,plain,
( ~ c2_1(a194)
| spl0_68 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f436,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f101,f434,f318]) ).
fof(f438,definition,
( spl0_69
<=> c1_1(a194) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f439,plain,
( ~ c1_1(a194)
| spl0_69 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f440,plain,
( ~ spl0_42
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f100,f438,f318]) ).
fof(f443,definition,
( spl0_70
<=> c3_1(a195) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f445,plain,
( ~ spl0_24
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f99,f443,f245]) ).
fof(f447,definition,
( spl0_71
<=> c1_1(a195) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f448,plain,
( ~ c1_1(a195)
| spl0_71 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f449,plain,
( ~ spl0_24
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f98,f447,f245]) ).
fof(f452,definition,
( spl0_72
<=> c2_1(a197) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f454,plain,
( ~ spl0_22
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f97,f452,f238]) ).
fof(f456,definition,
( spl0_73
<=> c0_1(a197) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f458,plain,
( ~ spl0_22
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f96,f456,f238]) ).
fof(f461,definition,
( spl0_74
<=> c2_1(a198) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f463,plain,
( ~ spl0_52
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f95,f461,f361]) ).
fof(f466,definition,
( spl0_75
<=> c1_1(a199) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f467,plain,
( ~ c1_1(a199)
| spl0_75 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f468,plain,
( ~ spl0_31
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f94,f466,f270]) ).
fof(f470,definition,
( spl0_76
<=> c0_1(a199) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f472,plain,
( ~ spl0_31
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f93,f470,f270]) ).
fof(f475,definition,
( spl0_77
<=> c1_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f476,plain,
( ~ c1_1(a200)
| spl0_77 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f477,plain,
( ~ spl0_41
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f92,f475,f314]) ).
fof(f489,definition,
( spl0_80
<=> c3_1(a206) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f490,plain,
( ~ c3_1(a206)
| spl0_80 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( ~ spl0_27
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f89,f489,f256]) ).
fof(f493,definition,
( spl0_81
<=> c2_1(a206) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f495,plain,
( ~ spl0_27
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f88,f493,f256]) ).
fof(f497,definition,
( spl0_82
<=> c0_1(a206) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f499,plain,
( ~ spl0_27
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f87,f497,f256]) ).
fof(f502,definition,
( spl0_83
<=> c0_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f504,plain,
( ~ spl0_29
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f86,f502,f263]) ).
fof(f507,definition,
( spl0_84
<=> c1_1(a210) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f508,plain,
( ~ c1_1(a210)
| spl0_84 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( ~ spl0_32
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f85,f507,f274]) ).
fof(f512,definition,
( spl0_85
<=> c3_1(a214) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f513,plain,
( ~ c3_1(a214)
| spl0_85 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( ~ spl0_44
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f84,f512,f327]) ).
fof(f516,definition,
( spl0_86
<=> c0_1(a214) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f518,plain,
( ~ spl0_44
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f83,f516,f327]) ).
fof(f521,definition,
( spl0_87
<=> c2_1(a221) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f523,plain,
( ~ spl0_48
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f82,f521,f341]) ).
fof(f525,definition,
( spl0_88
<=> c1_1(a221) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f526,plain,
( ~ c1_1(a221)
| spl0_88 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f527,plain,
( ~ spl0_48
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f81,f525,f341]) ).
fof(f529,definition,
( spl0_89
<=> c0_1(a221) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f531,plain,
( ~ spl0_48
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f80,f529,f341]) ).
fof(f548,definition,
( spl0_93
<=> c1_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f549,plain,
( ~ c1_1(a225)
| spl0_93 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f550,plain,
( ~ spl0_36
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f76,f548,f290]) ).
fof(f552,definition,
( spl0_94
<=> c0_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f554,plain,
( ~ spl0_36
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f75,f552,f290]) ).
fof(f583,definition,
( spl0_102
<=> c2_1(a190) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f585,plain,
( spl0_102
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f69,f299,f583]) ).
fof(f587,definition,
( spl0_103
<=> c0_1(a190) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f589,plain,
( spl0_103
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f68,f299,f587]) ).
fof(f591,definition,
( spl0_104
<=> c1_1(a192) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f592,plain,
( c1_1(a192)
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( spl0_104
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f67,f365,f591]) ).
fof(f595,definition,
( spl0_105
<=> c0_1(a192) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f597,plain,
( spl0_105
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f66,f365,f595]) ).
fof(f599,definition,
( spl0_106
<=> c1_1(a193) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f600,plain,
( c1_1(a193)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f601,plain,
( spl0_106
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f65,f349,f599]) ).
fof(f603,definition,
( spl0_107
<=> c0_1(a194) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f605,plain,
( spl0_107
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f64,f318,f603]) ).
fof(f607,definition,
( spl0_108
<=> c0_1(a195) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f609,plain,
( spl0_108
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f63,f245,f607]) ).
fof(f611,definition,
( spl0_109
<=> c1_1(a197) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f612,plain,
( c1_1(a197)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f613,plain,
( spl0_109
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f62,f238,f611]) ).
fof(f615,definition,
( spl0_110
<=> c3_1(a198) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f616,plain,
( c3_1(a198)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f617,plain,
( spl0_110
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f61,f361,f615]) ).
fof(f619,definition,
( spl0_111
<=> c1_1(a198) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f620,plain,
( c1_1(a198)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f621,plain,
( spl0_111
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f60,f361,f619]) ).
fof(f623,definition,
( spl0_112
<=> c2_1(a199) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f625,plain,
( spl0_112
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f59,f270,f623]) ).
fof(f627,definition,
( spl0_113
<=> c3_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f628,plain,
( c3_1(a200)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( spl0_113
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f58,f314,f627]) ).
fof(f631,definition,
( spl0_114
<=> c0_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f633,plain,
( spl0_114
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f57,f314,f631]) ).
fof(f639,definition,
( spl0_116
<=> c3_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f640,plain,
( c3_1(a209)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f641,plain,
( spl0_116
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f55,f263,f639]) ).
fof(f643,definition,
( spl0_117
<=> c1_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f644,plain,
( c1_1(a209)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f645,plain,
( spl0_117
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f54,f263,f643]) ).
fof(f647,definition,
( spl0_118
<=> c3_1(a210) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f648,plain,
( c3_1(a210)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f649,plain,
( spl0_118
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f53,f274,f647]) ).
fof(f651,definition,
( spl0_119
<=> c2_1(a210) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f653,plain,
( spl0_119
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f52,f274,f651]) ).
fof(f655,definition,
( spl0_120
<=> c2_1(a214) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f657,plain,
( spl0_120
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f51,f327,f655]) ).
fof(f671,definition,
( spl0_124
<=> c3_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f672,plain,
( c3_1(a225)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f673,plain,
( spl0_124
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f47,f290,f671]) ).
fof(f691,definition,
( spl0_129
<=> c3_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f692,plain,
( c3_1(a189)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f694,plain,
( spl0_129
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f42,f334,f691]) ).
fof(f696,definition,
( spl0_130
<=> c1_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f697,plain,
( c1_1(a189)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f698,plain,
( spl0_130
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f41,f334,f696]) ).
fof(f700,definition,
( spl0_131
<=> c0_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f702,plain,
( spl0_131
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f40,f334,f700]) ).
fof(f704,definition,
( spl0_132
<=> c3_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f705,plain,
( c3_1(a215)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f707,plain,
( spl0_132
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f39,f294,f704]) ).
fof(f709,definition,
( spl0_133
<=> c2_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f711,plain,
( spl0_133
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f38,f294,f709]) ).
fof(f713,definition,
( spl0_134
<=> c1_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f714,plain,
( c1_1(a215)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f715,plain,
( spl0_134
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f37,f294,f713]) ).
fof(f717,definition,
( spl0_135
<=> c2_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f720,plain,
( spl0_135
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f36,f357,f717]) ).
fof(f722,definition,
( spl0_136
<=> c1_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f723,plain,
( c1_1(a230)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f724,plain,
( spl0_136
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f35,f357,f722]) ).
fof(f726,definition,
( spl0_137
<=> c0_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f728,plain,
( spl0_137
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f34,f357,f726]) ).
fof(f736,plain,
( spl0_39
| spl0_31
| spl0_46 ),
inference(avatar_split_clause,[],[f28,f334,f270,f304]) ).
fof(f737,plain,
( spl0_39
| spl0_44
| spl0_51 ),
inference(avatar_split_clause,[],[f27,f357,f327,f304]) ).
fof(f741,plain,
( spl0_3
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f24,f304,f171]) ).
fof(f754,plain,
( spl0_3
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f11,f327,f171]) ).
fof(f764,plain,
( spl0_3
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f1,f357,f171]) ).
fof(f773,definition,
( spl0_138
<=> c0_1(a191) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f776,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_5
| ~ spl0_8 ),
inference(resolution,[],[f189,f179]) ).
fof(f777,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_5
| ~ spl0_8 ),
inference(duplicate_literal_removal,[],[f776]) ).
fof(f779,plain,
( ~ c0_1(a194)
| ~ spl0_5
| ~ spl0_8
| spl0_68 ),
inference(resolution,[],[f777,f435]) ).
fof(f805,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_12 ),
inference(resolution,[],[f203,f192]) ).
fof(f806,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_12 ),
inference(resolution,[],[f203,f169]) ).
fof(f809,plain,
( c2_1(a191)
| ~ c0_1(a191)
| ~ spl0_12
| spl0_64 ),
inference(resolution,[],[f203,f416]) ).
fof(f811,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_2
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f806]) ).
fof(f812,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_9
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f805]) ).
fof(f817,plain,
( spl0_5
| ~ spl0_9
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f812,f202,f191,f178]) ).
fof(f818,plain,
( ~ spl0_107
| ~ spl0_5
| ~ spl0_8
| spl0_68 ),
inference(avatar_split_clause,[],[f779,f434,f188,f178,f603]) ).
fof(f819,plain,
( c2_1(a199)
| ~ c0_1(a199)
| ~ spl0_12
| spl0_75 ),
inference(resolution,[],[f467,f203]) ).
fof(f820,plain,
( ~ spl0_76
| spl0_112
| ~ spl0_12
| spl0_75 ),
inference(avatar_split_clause,[],[f819,f466,f202,f623,f470]) ).
fof(f821,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(resolution,[],[f166,f199]) ).
fof(f831,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f821]) ).
fof(f836,plain,
( spl0_18
| ~ spl0_1
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f831,f198,f165,f223]) ).
fof(f861,definition,
( spl0_141
<=> c2_1(a188) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f888,plain,
( c3_1(a188)
| ~ c2_1(a188)
| ~ spl0_17
| spl0_59 ),
inference(resolution,[],[f221,f394]) ).
fof(f894,definition,
( spl0_142
<=> c3_1(a199) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f895,plain,
( c3_1(a199)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f894]) ).
fof(f918,definition,
( spl0_143
<=> c3_1(a221) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f933,plain,
( c3_1(a188)
| c2_1(a188)
| ~ spl0_26
| spl0_59 ),
inference(resolution,[],[f253,f394]) ).
fof(f938,plain,
( c3_1(a221)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f918]) ).
fof(f948,definition,
( spl0_144
<=> c2_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f970,plain,
( spl0_8
| ~ spl0_2
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f811,f202,f168,f188]) ).
fof(f974,definition,
( spl0_145
<=> c2_1(a193) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1018,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_20
| ~ spl0_25 ),
inference(resolution,[],[f250,f231]) ).
fof(f1027,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_20
| ~ spl0_25 ),
inference(duplicate_literal_removal,[],[f1018]) ).
fof(f1048,plain,
( ~ spl0_141
| spl0_58
| ~ spl0_17
| spl0_59 ),
inference(avatar_split_clause,[],[f888,f393,f220,f389,f861]) ).
fof(f1063,plain,
( c0_1(a215)
| ~ c2_1(a215)
| ~ spl0_23
| ~ spl0_132 ),
inference(resolution,[],[f705,f242]) ).
fof(f1068,definition,
( spl0_147
<=> c0_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1075,plain,
( spl0_141
| spl0_58
| ~ spl0_26
| spl0_59 ),
inference(avatar_split_clause,[],[f933,f393,f252,f389,f861]) ).
fof(f1091,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f182,f166]) ).
fof(f1096,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_6 ),
inference(duplicate_literal_removal,[],[f1091]) ).
fof(f1097,plain,
( spl0_18
| ~ spl0_1
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1096,f181,f165,f223]) ).
fof(f1098,plain,
( ~ c2_1(a199)
| ~ c3_1(a199)
| ~ spl0_7
| spl0_75 ),
inference(resolution,[],[f186,f467]) ).
fof(f1108,plain,
( ~ spl0_142
| ~ spl0_112
| ~ spl0_7
| spl0_75 ),
inference(avatar_split_clause,[],[f1098,f466,f185,f623,f894]) ).
fof(f1114,definition,
( spl0_148
<=> c0_1(a210) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1133,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_17 ),
inference(resolution,[],[f221,f192]) ).
fof(f1135,plain,
( c3_1(a199)
| ~ c2_1(a199)
| ~ spl0_17
| spl0_75 ),
inference(resolution,[],[f221,f467]) ).
fof(f1140,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1133]) ).
fof(f1144,plain,
( ~ spl0_112
| spl0_142
| ~ spl0_17
| spl0_75 ),
inference(avatar_split_clause,[],[f1135,f466,f220,f894,f623]) ).
fof(f1145,plain,
( spl0_18
| ~ spl0_9
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1140,f220,f191,f223]) ).
fof(f1149,definition,
( spl0_149
<=> c2_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1153,plain,
( c2_1(a225)
| c0_1(a225)
| ~ spl0_14
| ~ spl0_124 ),
inference(resolution,[],[f672,f211]) ).
fof(f1156,plain,
( spl0_94
| spl0_149
| ~ spl0_14
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1153,f671,f210,f1149,f552]) ).
fof(f1161,plain,
( c2_1(a225)
| ~ c3_1(a225)
| ~ spl0_21
| spl0_93 ),
inference(resolution,[],[f235,f549]) ).
fof(f1171,plain,
( ~ spl0_124
| spl0_149
| ~ spl0_21
| spl0_93 ),
inference(avatar_split_clause,[],[f1161,f548,f234,f1149,f671]) ).
fof(f1185,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_26 ),
inference(resolution,[],[f253,f192]) ).
fof(f1191,plain,
( c3_1(a191)
| c2_1(a191)
| ~ spl0_26
| spl0_64 ),
inference(resolution,[],[f253,f416]) ).
fof(f1193,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f1185]) ).
fof(f1196,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_21
| ~ spl0_28 ),
inference(resolution,[],[f260,f235]) ).
fof(f1204,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_21
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f1196]) ).
fof(f1207,plain,
( spl0_8
| ~ spl0_21
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f1204,f259,f234,f188]) ).
fof(f1211,definition,
( spl0_150
<=> c3_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1212,plain,
( c3_1(a230)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1222,plain,
( ~ c3_1(a215)
| ~ c2_1(a215)
| ~ spl0_30
| ~ spl0_134 ),
inference(resolution,[],[f267,f714]) ).
fof(f1226,plain,
( ~ spl0_133
| ~ spl0_132
| ~ spl0_30
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f1222,f713,f266,f704,f709]) ).
fof(f1236,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_12
| ~ spl0_34 ),
inference(resolution,[],[f283,f203]) ).
fof(f1241,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_12
| ~ spl0_34 ),
inference(duplicate_literal_removal,[],[f1236]) ).
fof(f1245,plain,
( spl0_8
| ~ spl0_12
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1241,f282,f202,f188]) ).
fof(f1258,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_26
| ~ spl0_35 ),
inference(resolution,[],[f287,f253]) ).
fof(f1265,plain,
( c2_1(a197)
| c0_1(a197)
| ~ spl0_35
| ~ spl0_109 ),
inference(resolution,[],[f287,f612]) ).
fof(f1270,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_26
| ~ spl0_35 ),
inference(duplicate_literal_removal,[],[f1258]) ).
fof(f1275,plain,
( spl0_57
| ~ spl0_26
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f1270,f286,f252,f383]) ).
fof(f1277,plain,
( ~ c3_1(a225)
| c0_1(a225)
| ~ spl0_40
| spl0_93 ),
inference(resolution,[],[f309,f549]) ).
fof(f1281,plain,
( ~ c3_1(a221)
| c0_1(a221)
| ~ spl0_40
| spl0_88 ),
inference(resolution,[],[f309,f526]) ).
fof(f1285,plain,
( spl0_89
| ~ spl0_143
| ~ spl0_40
| spl0_88 ),
inference(avatar_split_clause,[],[f1281,f525,f308,f918,f529]) ).
fof(f1293,plain,
( ~ c0_1(a230)
| ~ c2_1(a230)
| ~ spl0_4
| ~ spl0_150 ),
inference(resolution,[],[f1212,f175]) ).
fof(f1294,plain,
( ~ spl0_135
| ~ spl0_137
| ~ spl0_4
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f1293,f1211,f174,f726,f717]) ).
fof(f1296,plain,
( ~ c2_1(a225)
| c0_1(a225)
| ~ spl0_19
| spl0_93 ),
inference(resolution,[],[f228,f549]) ).
fof(f1298,plain,
( ~ c2_1(a199)
| c0_1(a199)
| ~ spl0_19
| spl0_75 ),
inference(resolution,[],[f228,f467]) ).
fof(f1310,plain,
( spl0_94
| ~ spl0_149
| ~ spl0_19
| spl0_93 ),
inference(avatar_split_clause,[],[f1296,f548,f227,f1149,f552]) ).
fof(f1346,definition,
( spl0_152
<=> c0_1(a198) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1351,plain,
( ~ c0_1(a189)
| ~ c2_1(a189)
| ~ spl0_4
| ~ spl0_129 ),
inference(resolution,[],[f692,f175]) ).
fof(f1353,definition,
( spl0_153
<=> c2_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1364,plain,
( c2_1(a189)
| ~ c0_1(a189)
| ~ spl0_8
| ~ spl0_129 ),
inference(resolution,[],[f189,f692]) ).
fof(f1375,plain,
( spl0_14
| ~ spl0_20
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1027,f249,f230,f210]) ).
fof(f1402,plain,
( ~ c3_1(a230)
| ~ c0_1(a230)
| ~ spl0_2
| ~ spl0_136 ),
inference(resolution,[],[f169,f723]) ).
fof(f1403,plain,
( ~ c3_1(a215)
| ~ c0_1(a215)
| ~ spl0_2
| ~ spl0_134 ),
inference(resolution,[],[f169,f714]) ).
fof(f1404,plain,
( ~ c3_1(a189)
| ~ c0_1(a189)
| ~ spl0_2
| ~ spl0_130 ),
inference(resolution,[],[f169,f697]) ).
fof(f1414,plain,
( ~ spl0_131
| ~ spl0_129
| ~ spl0_2
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1404,f696,f168,f691,f700]) ).
fof(f1416,plain,
( ~ spl0_137
| ~ spl0_150
| ~ spl0_2
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1402,f722,f168,f1211,f726]) ).
fof(f1433,plain,
( spl0_5
| ~ spl0_9
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1193,f252,f191,f178]) ).
fof(f1457,plain,
( ~ c0_1(a210)
| ~ c2_1(a210)
| ~ spl0_4
| ~ spl0_118 ),
inference(resolution,[],[f648,f175]) ).
fof(f1458,plain,
( ~ spl0_119
| ~ spl0_148
| ~ spl0_4
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f1457,f647,f174,f1114,f651]) ).
fof(f1459,plain,
( ~ c0_1(a215)
| ~ c2_1(a215)
| ~ spl0_4
| ~ spl0_132 ),
inference(resolution,[],[f705,f175]) ).
fof(f1460,plain,
( ~ spl0_133
| ~ spl0_147
| ~ spl0_4
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1459,f704,f174,f1068,f709]) ).
fof(f1522,plain,
( ~ c2_1(a215)
| ~ c0_1(a215)
| ~ spl0_11
| ~ spl0_134 ),
inference(resolution,[],[f199,f714]) ).
fof(f1551,definition,
( spl0_155
<=> c2_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1565,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_11
| ~ spl0_17 ),
inference(resolution,[],[f221,f199]) ).
fof(f1572,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_11
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1565]) ).
fof(f1575,plain,
( spl0_18
| ~ spl0_11
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1572,f220,f198,f223]) ).
fof(f1602,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_16
| ~ spl0_28 ),
inference(resolution,[],[f260,f217]) ).
fof(f1610,plain,
( c2_1(a198)
| ~ c0_1(a198)
| ~ spl0_28
| ~ spl0_111 ),
inference(resolution,[],[f260,f620]) ).
fof(f1616,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_16
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f1602]) ).
fof(f1619,plain,
( ~ spl0_152
| spl0_74
| ~ spl0_28
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f1610,f619,f259,f461,f1346]) ).
fof(f1653,plain,
( c3_1(a193)
| c0_1(a193)
| ~ spl0_43
| ~ spl0_106 ),
inference(resolution,[],[f322,f600]) ).
fof(f1659,plain,
( spl0_67
| spl0_66
| ~ spl0_43
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f1653,f599,f321,f425,f429]) ).
fof(f1687,plain,
( c3_1(a192)
| ~ c0_1(a192)
| ~ spl0_9
| ~ spl0_104 ),
inference(resolution,[],[f592,f192]) ).
fof(f1691,plain,
( ~ spl0_105
| spl0_65
| ~ spl0_9
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f1687,f591,f191,f420,f595]) ).
fof(f1710,plain,
( c0_1(a209)
| ~ c2_1(a209)
| ~ spl0_15
| ~ spl0_117 ),
inference(resolution,[],[f214,f644]) ).
fof(f1716,plain,
( ~ spl0_155
| spl0_83
| ~ spl0_15
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1710,f643,f213,f502,f1551]) ).
fof(f1726,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15
| ~ spl0_40 ),
inference(resolution,[],[f309,f214]) ).
fof(f1732,plain,
( ~ c3_1(a210)
| c0_1(a210)
| ~ spl0_40
| spl0_84 ),
inference(resolution,[],[f309,f508]) ).
fof(f1733,plain,
( ~ c3_1(a199)
| c0_1(a199)
| ~ spl0_40
| spl0_75 ),
inference(resolution,[],[f309,f467]) ).
fof(f1736,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15
| ~ spl0_40 ),
inference(duplicate_literal_removal,[],[f1726]) ).
fof(f1740,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_45 ),
inference(resolution,[],[f331,f166]) ).
fof(f1755,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_45 ),
inference(duplicate_literal_removal,[],[f1740]) ).
fof(f1762,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15
| ~ spl0_47 ),
inference(resolution,[],[f338,f214]) ).
fof(f1767,plain,
( c3_1(a199)
| c0_1(a199)
| ~ spl0_47
| spl0_75 ),
inference(resolution,[],[f338,f467]) ).
fof(f1770,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15
| ~ spl0_47 ),
inference(duplicate_literal_removal,[],[f1762]) ).
fof(f1775,plain,
( spl0_13
| ~ spl0_15
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1770,f337,f213,f206]) ).
fof(f1790,plain,
( ~ spl0_153
| ~ spl0_131
| ~ spl0_4
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1351,f691,f174,f700,f1353]) ).
fof(f1804,plain,
( spl0_8
| ~ spl0_16
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f1616,f259,f216,f188]) ).
fof(f1824,plain,
( spl0_76
| spl0_142
| ~ spl0_47
| spl0_75 ),
inference(avatar_split_clause,[],[f1767,f466,f337,f894,f470]) ).
fof(f1834,plain,
( ~ c0_1(a200)
| ~ c3_1(a200)
| ~ spl0_16
| spl0_77 ),
inference(resolution,[],[f476,f217]) ).
fof(f1835,plain,
( ~ spl0_113
| ~ spl0_114
| ~ spl0_16
| spl0_77 ),
inference(avatar_split_clause,[],[f1834,f475,f216,f631,f627]) ).
fof(f1842,plain,
( ~ c0_1(a200)
| ~ c2_1(a200)
| ~ spl0_4
| ~ spl0_113 ),
inference(resolution,[],[f628,f175]) ).
fof(f1843,plain,
( ~ spl0_144
| ~ spl0_114
| ~ spl0_4
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f1842,f627,f174,f631,f948]) ).
fof(f1850,plain,
( c2_1(a189)
| ~ c0_1(a189)
| ~ spl0_28
| ~ spl0_130 ),
inference(resolution,[],[f697,f260]) ).
fof(f1851,plain,
( ~ spl0_131
| spl0_153
| ~ spl0_28
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1850,f696,f259,f1353,f700]) ).
fof(f1864,plain,
( c2_1(a200)
| ~ c0_1(a200)
| ~ spl0_8
| ~ spl0_113 ),
inference(resolution,[],[f189,f628]) ).
fof(f1867,plain,
( ~ spl0_114
| spl0_144
| ~ spl0_8
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f1864,f627,f188,f948,f631]) ).
fof(f1878,plain,
( c2_1(a198)
| c0_1(a198)
| ~ spl0_14
| ~ spl0_110 ),
inference(resolution,[],[f211,f616]) ).
fof(f1906,plain,
( ~ c0_1(a190)
| ~ c2_1(a190)
| ~ spl0_18
| spl0_61 ),
inference(resolution,[],[f224,f403]) ).
fof(f1913,plain,
( ~ spl0_102
| ~ spl0_103
| ~ spl0_18
| spl0_61 ),
inference(avatar_split_clause,[],[f1906,f402,f223,f587,f583]) ).
fof(f1917,plain,
( c0_1(a209)
| ~ c3_1(a209)
| ~ spl0_20
| ~ spl0_117 ),
inference(resolution,[],[f231,f644]) ).
fof(f1922,plain,
( ~ spl0_116
| spl0_83
| ~ spl0_20
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1917,f643,f230,f502,f639]) ).
fof(f1946,plain,
( c2_1(a221)
| ~ c3_1(a221)
| ~ spl0_21
| spl0_88 ),
inference(resolution,[],[f235,f526]) ).
fof(f1957,plain,
( c0_1(a225)
| ~ c2_1(a225)
| ~ spl0_23
| ~ spl0_124 ),
inference(resolution,[],[f242,f672]) ).
fof(f1960,plain,
( c0_1(a199)
| ~ c2_1(a199)
| ~ spl0_23
| ~ spl0_142 ),
inference(resolution,[],[f242,f895]) ).
fof(f1965,plain,
( ~ spl0_149
| spl0_94
| ~ spl0_23
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1957,f671,f241,f552,f1149]) ).
fof(f1971,plain,
( spl0_5
| ~ spl0_1
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1755,f330,f165,f178]) ).
fof(f1980,plain,
( ~ spl0_138
| spl0_63
| ~ spl0_12
| spl0_64 ),
inference(avatar_split_clause,[],[f809,f415,f202,f411,f773]) ).
fof(f1994,plain,
( spl0_152
| spl0_74
| ~ spl0_14
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f1878,f615,f210,f461,f1346]) ).
fof(f2020,plain,
( c2_1(a209)
| c0_1(a209)
| ~ spl0_14
| ~ spl0_116 ),
inference(resolution,[],[f640,f211]) ).
fof(f2028,plain,
( c3_1(a230)
| ~ c0_1(a230)
| ~ spl0_9
| ~ spl0_136 ),
inference(resolution,[],[f723,f192]) ).
fof(f2029,plain,
( ~ spl0_137
| spl0_150
| ~ spl0_9
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f2028,f722,f191,f1211,f726]) ).
fof(f2037,plain,
( c3_1(a195)
| ~ c0_1(a195)
| ~ spl0_1
| spl0_71 ),
inference(resolution,[],[f166,f448]) ).
fof(f2040,plain,
( c3_1(a191)
| ~ c0_1(a191)
| ~ spl0_1
| spl0_64 ),
inference(resolution,[],[f166,f416]) ).
fof(f2043,plain,
( ~ spl0_138
| spl0_62
| ~ spl0_1
| spl0_64 ),
inference(avatar_split_clause,[],[f2040,f415,f165,f407,f773]) ).
fof(f2046,plain,
( ~ spl0_108
| spl0_70
| ~ spl0_1
| spl0_71 ),
inference(avatar_split_clause,[],[f2037,f447,f165,f443,f607]) ).
fof(f2055,plain,
( spl0_23
| ~ spl0_15
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1736,f308,f213,f241]) ).
fof(f2056,plain,
( ~ spl0_133
| spl0_147
| ~ spl0_23
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1063,f704,f241,f1068,f709]) ).
fof(f2059,plain,
( ~ spl0_112
| spl0_76
| ~ spl0_23
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1960,f894,f241,f470,f623]) ).
fof(f2060,plain,
( spl0_94
| ~ spl0_124
| ~ spl0_40
| spl0_93 ),
inference(avatar_split_clause,[],[f1277,f548,f308,f671,f552]) ).
fof(f2063,plain,
( spl0_148
| ~ spl0_118
| ~ spl0_40
| spl0_84 ),
inference(avatar_split_clause,[],[f1732,f507,f308,f647,f1114]) ).
fof(f2064,plain,
( spl0_76
| ~ spl0_142
| ~ spl0_40
| spl0_75 ),
inference(avatar_split_clause,[],[f1733,f466,f308,f894,f470]) ).
fof(f2077,plain,
( ~ c0_1(a191)
| c2_1(a191)
| ~ spl0_5
| spl0_62 ),
inference(resolution,[],[f179,f408]) ).
fof(f2080,plain,
( spl0_63
| ~ spl0_138
| ~ spl0_5
| spl0_62 ),
inference(avatar_split_clause,[],[f2077,f407,f178,f773,f411]) ).
fof(f2087,plain,
( c2_1(a200)
| ~ c0_1(a200)
| ~ spl0_12
| spl0_77 ),
inference(resolution,[],[f203,f476]) ).
fof(f2090,plain,
( c2_1(a194)
| ~ c0_1(a194)
| ~ spl0_12
| spl0_69 ),
inference(resolution,[],[f203,f439]) ).
fof(f2095,plain,
( ~ spl0_107
| spl0_68
| ~ spl0_12
| spl0_69 ),
inference(avatar_split_clause,[],[f2090,f438,f202,f434,f603]) ).
fof(f2097,plain,
( ~ spl0_114
| spl0_144
| ~ spl0_12
| spl0_77 ),
inference(avatar_split_clause,[],[f2087,f475,f202,f948,f631]) ).
fof(f2102,plain,
( ~ c2_1(a214)
| c0_1(a214)
| ~ spl0_13
| spl0_85 ),
inference(resolution,[],[f207,f513]) ).
fof(f2109,plain,
( spl0_86
| ~ spl0_120
| ~ spl0_13
| spl0_85 ),
inference(avatar_split_clause,[],[f2102,f512,f206,f655,f516]) ).
fof(f2129,plain,
( spl0_63
| spl0_62
| ~ spl0_26
| spl0_64 ),
inference(avatar_split_clause,[],[f1191,f415,f252,f407,f411]) ).
fof(f2141,plain,
( ~ c2_1(a193)
| c0_1(a193)
| ~ spl0_13
| spl0_66 ),
inference(resolution,[],[f426,f207]) ).
fof(f2143,plain,
( spl0_67
| ~ spl0_145
| ~ spl0_13
| spl0_66 ),
inference(avatar_split_clause,[],[f2141,f425,f206,f974,f429]) ).
fof(f2148,plain,
( c0_1(a215)
| ~ c2_1(a215)
| ~ spl0_15
| ~ spl0_134 ),
inference(resolution,[],[f214,f714]) ).
fof(f2153,plain,
( c0_1(a193)
| ~ c2_1(a193)
| ~ spl0_15
| ~ spl0_106 ),
inference(resolution,[],[f214,f600]) ).
fof(f2154,plain,
( ~ spl0_145
| spl0_67
| ~ spl0_15
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f2153,f599,f213,f429,f974]) ).
fof(f2156,plain,
( ~ spl0_133
| spl0_147
| ~ spl0_15
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f2148,f713,f213,f1068,f709]) ).
fof(f2159,plain,
( c0_1(a215)
| ~ c3_1(a215)
| ~ spl0_20
| ~ spl0_134 ),
inference(resolution,[],[f231,f714]) ).
fof(f2162,plain,
( c0_1(a198)
| ~ c3_1(a198)
| ~ spl0_20
| ~ spl0_111 ),
inference(resolution,[],[f231,f620]) ).
fof(f2166,plain,
( ~ spl0_110
| spl0_152
| ~ spl0_20
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f2162,f619,f230,f1346,f615]) ).
fof(f2167,plain,
( ~ spl0_132
| spl0_147
| ~ spl0_20
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f2159,f713,f230,f1068,f704]) ).
fof(f2178,plain,
( c2_1(a221)
| c0_1(a221)
| ~ spl0_25
| spl0_88 ),
inference(resolution,[],[f250,f526]) ).
fof(f2179,plain,
( c2_1(a191)
| c0_1(a191)
| ~ spl0_25
| spl0_64 ),
inference(resolution,[],[f250,f416]) ).
fof(f2182,plain,
( spl0_138
| spl0_63
| ~ spl0_25
| spl0_64 ),
inference(avatar_split_clause,[],[f2179,f415,f249,f411,f773]) ).
fof(f2183,plain,
( spl0_89
| spl0_87
| ~ spl0_25
| spl0_88 ),
inference(avatar_split_clause,[],[f2178,f525,f249,f521,f529]) ).
fof(f2197,plain,
( c3_1(a221)
| c2_1(a221)
| ~ spl0_26
| spl0_88 ),
inference(resolution,[],[f253,f526]) ).
fof(f2200,plain,
( spl0_87
| spl0_143
| ~ spl0_26
| spl0_88 ),
inference(avatar_split_clause,[],[f2197,f525,f252,f918,f521]) ).
fof(f2203,plain,
( c2_1(a221)
| c0_1(a221)
| ~ spl0_14
| ~ spl0_143 ),
inference(resolution,[],[f938,f211]) ).
fof(f2204,plain,
( spl0_89
| spl0_87
| ~ spl0_14
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f2203,f918,f210,f521,f529]) ).
fof(f2215,plain,
( c3_1(a221)
| c0_1(a221)
| ~ spl0_47
| spl0_88 ),
inference(resolution,[],[f338,f526]) ).
fof(f2216,plain,
( c3_1(a191)
| c0_1(a191)
| ~ spl0_47
| spl0_64 ),
inference(resolution,[],[f338,f416]) ).
fof(f2225,plain,
( c0_1(a193)
| c2_1(a193)
| ~ spl0_57
| spl0_66 ),
inference(resolution,[],[f384,f426]) ).
fof(f2227,plain,
( c0_1(a206)
| c2_1(a206)
| ~ spl0_57
| spl0_80 ),
inference(resolution,[],[f384,f490]) ).
fof(f2233,plain,
( spl0_81
| spl0_82
| ~ spl0_57
| spl0_80 ),
inference(avatar_split_clause,[],[f2227,f489,f383,f497,f493]) ).
fof(f2234,plain,
( spl0_145
| spl0_67
| ~ spl0_57
| spl0_66 ),
inference(avatar_split_clause,[],[f2225,f425,f383,f429,f974]) ).
fof(f2238,plain,
( ~ spl0_147
| ~ spl0_132
| ~ spl0_2
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f1403,f713,f168,f704,f1068]) ).
fof(f2242,plain,
( ~ spl0_131
| spl0_153
| ~ spl0_8
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1364,f691,f188,f1353,f700]) ).
fof(f2246,plain,
( ~ spl0_147
| ~ spl0_133
| ~ spl0_11
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f1522,f713,f198,f709,f1068]) ).
fof(f2253,plain,
( spl0_76
| ~ spl0_112
| ~ spl0_19
| spl0_75 ),
inference(avatar_split_clause,[],[f1298,f466,f227,f623,f470]) ).
fof(f2266,plain,
( ~ spl0_143
| spl0_87
| ~ spl0_21
| spl0_88 ),
inference(avatar_split_clause,[],[f1946,f525,f234,f521,f918]) ).
fof(f2269,plain,
( spl0_73
| spl0_72
| ~ spl0_35
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f1265,f611,f286,f452,f456]) ).
fof(f2272,plain,
( spl0_83
| spl0_155
| ~ spl0_14
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f2020,f639,f210,f1551,f502]) ).
fof(f2273,plain,
( spl0_89
| spl0_143
| ~ spl0_47
| spl0_88 ),
inference(avatar_split_clause,[],[f2215,f525,f337,f918,f529]) ).
fof(f2278,plain,
( spl0_138
| spl0_62
| ~ spl0_47
| spl0_64 ),
inference(avatar_split_clause,[],[f2216,f415,f337,f407,f773]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f176]) ).
cnf(s2,plain,
( spl0_2
| ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f183]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f193]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_5
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f204]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_14
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f225]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_12
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f232]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_15
| spl0_19
| spl0_21 ),
inference(sat_conversion,[],[f236]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_11
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f243]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_14
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f254]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_6
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f261]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_5
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f268]) ).
cnf(s16,plain,
( spl0_2
| ~ spl0_3
| spl0_12
| spl0_31 ),
inference(sat_conversion,[],[f272]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_7
| spl0_23
| spl0_32 ),
inference(sat_conversion,[],[f276]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_9
| spl0_15
| spl0_27 ),
inference(sat_conversion,[],[f277]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_15
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f284]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_17
| spl0_18
| spl0_36 ),
inference(sat_conversion,[],[f292]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_17
| spl0_28
| spl0_37 ),
inference(sat_conversion,[],[f296]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_9
| spl0_21
| spl0_29 ),
inference(sat_conversion,[],[f297]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_12
| spl0_16
| spl0_37 ),
inference(sat_conversion,[],[f302]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_12
| spl0_15
| spl0_39 ),
inference(sat_conversion,[],[f306]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_9
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f310]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_23
| spl0_26
| spl0_29 ),
inference(sat_conversion,[],[f312]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_20
| spl0_26
| spl0_41 ),
inference(sat_conversion,[],[f316]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_13
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f323]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_35
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f339]) ).
cnf(s36,plain,
( ~ spl0_3
| spl0_4
| spl0_27
| spl0_48 ),
inference(sat_conversion,[],[f343]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_4
| spl0_42
| spl0_46 ),
inference(sat_conversion,[],[f344]) ).
cnf(s38,plain,
( spl0_2
| ~ spl0_3
| spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f345]) ).
cnf(s39,plain,
( ~ spl0_3
| spl0_18
| spl0_37
| spl0_41 ),
inference(sat_conversion,[],[f346]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_9
| spl0_22
| spl0_31 ),
inference(sat_conversion,[],[f347]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_9
| spl0_22
| spl0_49 ),
inference(sat_conversion,[],[f351]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_28
| spl0_48
| spl0_51 ),
inference(sat_conversion,[],[f359]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_27
| spl0_45
| spl0_53 ),
inference(sat_conversion,[],[f367]) ).
cnf(s47,plain,
( spl0_1
| ~ spl0_3
| spl0_46
| spl0_48 ),
inference(sat_conversion,[],[f375]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_31
| spl0_35
| spl0_52 ),
inference(sat_conversion,[],[f380]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_40
| spl0_49
| spl0_53 ),
inference(sat_conversion,[],[f381]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_24
| spl0_57 ),
inference(sat_conversion,[],[f385]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_38
| spl0_47 ),
inference(sat_conversion,[],[f386]) ).
cnf(s53,plain,
( ~ spl0_33
| ~ spl0_58 ),
inference(sat_conversion,[],[f391]) ).
cnf(s54,plain,
( ~ spl0_33
| ~ spl0_59 ),
inference(sat_conversion,[],[f395]) ).
cnf(s56,plain,
( ~ spl0_38
| ~ spl0_61 ),
inference(sat_conversion,[],[f404]) ).
cnf(s57,plain,
( ~ spl0_39
| ~ spl0_62 ),
inference(sat_conversion,[],[f409]) ).
cnf(s58,plain,
( ~ spl0_39
| ~ spl0_63 ),
inference(sat_conversion,[],[f413]) ).
cnf(s59,plain,
( ~ spl0_39
| ~ spl0_64 ),
inference(sat_conversion,[],[f417]) ).
cnf(s60,plain,
( ~ spl0_53
| ~ spl0_65 ),
inference(sat_conversion,[],[f422]) ).
cnf(s61,plain,
( ~ spl0_49
| ~ spl0_66 ),
inference(sat_conversion,[],[f427]) ).
cnf(s62,plain,
( ~ spl0_49
| ~ spl0_67 ),
inference(sat_conversion,[],[f431]) ).
cnf(s63,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(sat_conversion,[],[f436]) ).
cnf(s64,plain,
( ~ spl0_42
| ~ spl0_69 ),
inference(sat_conversion,[],[f440]) ).
cnf(s65,plain,
( ~ spl0_24
| ~ spl0_70 ),
inference(sat_conversion,[],[f445]) ).
cnf(s66,plain,
( ~ spl0_24
| ~ spl0_71 ),
inference(sat_conversion,[],[f449]) ).
cnf(s67,plain,
( ~ spl0_22
| ~ spl0_72 ),
inference(sat_conversion,[],[f454]) ).
cnf(s68,plain,
( ~ spl0_22
| ~ spl0_73 ),
inference(sat_conversion,[],[f458]) ).
cnf(s69,plain,
( ~ spl0_52
| ~ spl0_74 ),
inference(sat_conversion,[],[f463]) ).
cnf(s70,plain,
( ~ spl0_31
| ~ spl0_75 ),
inference(sat_conversion,[],[f468]) ).
cnf(s71,plain,
( ~ spl0_31
| ~ spl0_76 ),
inference(sat_conversion,[],[f472]) ).
cnf(s72,plain,
( ~ spl0_41
| ~ spl0_77 ),
inference(sat_conversion,[],[f477]) ).
cnf(s75,plain,
( ~ spl0_27
| ~ spl0_80 ),
inference(sat_conversion,[],[f491]) ).
cnf(s76,plain,
( ~ spl0_27
| ~ spl0_81 ),
inference(sat_conversion,[],[f495]) ).
cnf(s77,plain,
( ~ spl0_27
| ~ spl0_82 ),
inference(sat_conversion,[],[f499]) ).
cnf(s78,plain,
( ~ spl0_29
| ~ spl0_83 ),
inference(sat_conversion,[],[f504]) ).
cnf(s79,plain,
( ~ spl0_32
| ~ spl0_84 ),
inference(sat_conversion,[],[f509]) ).
cnf(s80,plain,
( ~ spl0_44
| ~ spl0_85 ),
inference(sat_conversion,[],[f514]) ).
cnf(s81,plain,
( ~ spl0_44
| ~ spl0_86 ),
inference(sat_conversion,[],[f518]) ).
cnf(s82,plain,
( ~ spl0_48
| ~ spl0_87 ),
inference(sat_conversion,[],[f523]) ).
cnf(s83,plain,
( ~ spl0_48
| ~ spl0_88 ),
inference(sat_conversion,[],[f527]) ).
cnf(s84,plain,
( ~ spl0_48
| ~ spl0_89 ),
inference(sat_conversion,[],[f531]) ).
cnf(s88,plain,
( ~ spl0_36
| ~ spl0_93 ),
inference(sat_conversion,[],[f550]) ).
cnf(s89,plain,
( ~ spl0_36
| ~ spl0_94 ),
inference(sat_conversion,[],[f554]) ).
cnf(s95,plain,
( ~ spl0_38
| spl0_102 ),
inference(sat_conversion,[],[f585]) ).
cnf(s96,plain,
( ~ spl0_38
| spl0_103 ),
inference(sat_conversion,[],[f589]) ).
cnf(s97,plain,
( ~ spl0_53
| spl0_104 ),
inference(sat_conversion,[],[f593]) ).
cnf(s98,plain,
( ~ spl0_53
| spl0_105 ),
inference(sat_conversion,[],[f597]) ).
cnf(s99,plain,
( ~ spl0_49
| spl0_106 ),
inference(sat_conversion,[],[f601]) ).
cnf(s100,plain,
( ~ spl0_42
| spl0_107 ),
inference(sat_conversion,[],[f605]) ).
cnf(s101,plain,
( ~ spl0_24
| spl0_108 ),
inference(sat_conversion,[],[f609]) ).
cnf(s102,plain,
( ~ spl0_22
| spl0_109 ),
inference(sat_conversion,[],[f613]) ).
cnf(s103,plain,
( ~ spl0_52
| spl0_110 ),
inference(sat_conversion,[],[f617]) ).
cnf(s104,plain,
( ~ spl0_52
| spl0_111 ),
inference(sat_conversion,[],[f621]) ).
cnf(s105,plain,
( ~ spl0_31
| spl0_112 ),
inference(sat_conversion,[],[f625]) ).
cnf(s106,plain,
( ~ spl0_41
| spl0_113 ),
inference(sat_conversion,[],[f629]) ).
cnf(s107,plain,
( ~ spl0_41
| spl0_114 ),
inference(sat_conversion,[],[f633]) ).
cnf(s109,plain,
( ~ spl0_29
| spl0_116 ),
inference(sat_conversion,[],[f641]) ).
cnf(s110,plain,
( ~ spl0_29
| spl0_117 ),
inference(sat_conversion,[],[f645]) ).
cnf(s111,plain,
( ~ spl0_32
| spl0_118 ),
inference(sat_conversion,[],[f649]) ).
cnf(s112,plain,
( ~ spl0_32
| spl0_119 ),
inference(sat_conversion,[],[f653]) ).
cnf(s113,plain,
( ~ spl0_44
| spl0_120 ),
inference(sat_conversion,[],[f657]) ).
cnf(s117,plain,
( ~ spl0_36
| spl0_124 ),
inference(sat_conversion,[],[f673]) ).
cnf(s122,plain,
( ~ spl0_46
| spl0_129 ),
inference(sat_conversion,[],[f694]) ).
cnf(s123,plain,
( ~ spl0_46
| spl0_130 ),
inference(sat_conversion,[],[f698]) ).
cnf(s124,plain,
( ~ spl0_46
| spl0_131 ),
inference(sat_conversion,[],[f702]) ).
cnf(s125,plain,
( ~ spl0_37
| spl0_132 ),
inference(sat_conversion,[],[f707]) ).
cnf(s126,plain,
( ~ spl0_37
| spl0_133 ),
inference(sat_conversion,[],[f711]) ).
cnf(s127,plain,
( ~ spl0_37
| spl0_134 ),
inference(sat_conversion,[],[f715]) ).
cnf(s128,plain,
( ~ spl0_51
| spl0_135 ),
inference(sat_conversion,[],[f720]) ).
cnf(s129,plain,
( ~ spl0_51
| spl0_136 ),
inference(sat_conversion,[],[f724]) ).
cnf(s130,plain,
( ~ spl0_51
| spl0_137 ),
inference(sat_conversion,[],[f728]) ).
cnf(s136,plain,
( spl0_31
| spl0_39
| spl0_46 ),
inference(sat_conversion,[],[f736]) ).
cnf(s137,plain,
( spl0_39
| spl0_44
| spl0_51 ),
inference(sat_conversion,[],[f737]) ).
cnf(s140,plain,
( spl0_3
| ~ spl0_39 ),
inference(sat_conversion,[],[f741]) ).
cnf(s153,plain,
( spl0_3
| ~ spl0_44 ),
inference(sat_conversion,[],[f754]) ).
cnf(s163,plain,
( spl0_3
| ~ spl0_51 ),
inference(sat_conversion,[],[f764]) ).
cnf(s170,plain,
( spl0_5
| ~ spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f817]) ).
cnf(s171,plain,
( ~ spl0_5
| ~ spl0_8
| spl0_68
| ~ spl0_107 ),
inference(sat_conversion,[],[f818]) ).
cnf(s172,plain,
( ~ spl0_12
| spl0_75
| ~ spl0_76
| spl0_112 ),
inference(sat_conversion,[],[f820]) ).
cnf(s174,plain,
( ~ spl0_1
| ~ spl0_11
| spl0_18 ),
inference(sat_conversion,[],[f836]) ).
cnf(s196,plain,
( ~ spl0_2
| spl0_8
| ~ spl0_12 ),
inference(sat_conversion,[],[f970]) ).
cnf(s218,plain,
( ~ spl0_17
| spl0_58
| spl0_59
| ~ spl0_141 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s232,plain,
( ~ spl0_26
| spl0_58
| spl0_59
| spl0_141 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s236,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_18 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s241,plain,
( ~ spl0_7
| spl0_75
| ~ spl0_112
| ~ spl0_142 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s249,plain,
( ~ spl0_17
| spl0_75
| ~ spl0_112
| spl0_142 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s250,plain,
( ~ spl0_9
| ~ spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s253,plain,
( ~ spl0_14
| spl0_94
| ~ spl0_124
| spl0_149 ),
inference(sat_conversion,[],[f1156]) ).
cnf(s257,plain,
( ~ spl0_21
| spl0_93
| ~ spl0_124
| spl0_149 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s261,plain,
( spl0_8
| ~ spl0_21
| ~ spl0_28 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s263,plain,
( ~ spl0_30
| ~ spl0_132
| ~ spl0_133
| ~ spl0_134 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s265,plain,
( spl0_8
| ~ spl0_12
| ~ spl0_34 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s269,plain,
( ~ spl0_26
| ~ spl0_35
| spl0_57 ),
inference(sat_conversion,[],[f1275]) ).
cnf(s271,plain,
( ~ spl0_40
| spl0_88
| spl0_89
| ~ spl0_143 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s276,plain,
( ~ spl0_4
| ~ spl0_135
| ~ spl0_137
| ~ spl0_150 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s283,plain,
( ~ spl0_19
| spl0_93
| spl0_94
| ~ spl0_149 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s314,plain,
( spl0_14
| ~ spl0_20
| ~ spl0_25 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s325,plain,
( ~ spl0_2
| ~ spl0_129
| ~ spl0_130
| ~ spl0_131 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s327,plain,
( ~ spl0_2
| ~ spl0_136
| ~ spl0_137
| ~ spl0_150 ),
inference(sat_conversion,[],[f1416]) ).
cnf(s347,plain,
( spl0_5
| ~ spl0_9
| ~ spl0_26 ),
inference(sat_conversion,[],[f1433]) ).
cnf(s372,plain,
( ~ spl0_4
| ~ spl0_118
| ~ spl0_119
| ~ spl0_148 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s373,plain,
( ~ spl0_4
| ~ spl0_132
| ~ spl0_133
| ~ spl0_147 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s399,plain,
( ~ spl0_11
| ~ spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s403,plain,
( ~ spl0_28
| spl0_74
| ~ spl0_111
| ~ spl0_152 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s406,plain,
( ~ spl0_43
| spl0_66
| spl0_67
| ~ spl0_106 ),
inference(sat_conversion,[],[f1659]) ).
cnf(s422,plain,
( ~ spl0_9
| spl0_65
| ~ spl0_104
| ~ spl0_105 ),
inference(sat_conversion,[],[f1691]) ).
cnf(s427,plain,
( ~ spl0_15
| spl0_83
| ~ spl0_117
| ~ spl0_155 ),
inference(sat_conversion,[],[f1716]) ).
cnf(s436,plain,
( spl0_13
| ~ spl0_15
| ~ spl0_47 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s452,plain,
( ~ spl0_4
| ~ spl0_129
| ~ spl0_131
| ~ spl0_153 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s466,plain,
( spl0_8
| ~ spl0_16
| ~ spl0_28 ),
inference(sat_conversion,[],[f1804]) ).
cnf(s489,plain,
( ~ spl0_47
| spl0_75
| spl0_76
| spl0_142 ),
inference(sat_conversion,[],[f1824]) ).
cnf(s496,plain,
( ~ spl0_16
| spl0_77
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s499,plain,
( ~ spl0_4
| ~ spl0_113
| ~ spl0_114
| ~ spl0_144 ),
inference(sat_conversion,[],[f1843]) ).
cnf(s500,plain,
( ~ spl0_28
| ~ spl0_130
| ~ spl0_131
| spl0_153 ),
inference(sat_conversion,[],[f1851]) ).
cnf(s505,plain,
( ~ spl0_8
| ~ spl0_113
| ~ spl0_114
| spl0_144 ),
inference(sat_conversion,[],[f1867]) ).
cnf(s516,plain,
( ~ spl0_18
| spl0_61
| ~ spl0_102
| ~ spl0_103 ),
inference(sat_conversion,[],[f1913]) ).
cnf(s519,plain,
( ~ spl0_20
| spl0_83
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f1922]) ).
cnf(s538,plain,
( ~ spl0_23
| spl0_94
| ~ spl0_124
| ~ spl0_149 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s545,plain,
( ~ spl0_1
| spl0_5
| ~ spl0_45 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s555,plain,
( ~ spl0_12
| spl0_63
| spl0_64
| ~ spl0_138 ),
inference(sat_conversion,[],[f1980]) ).
cnf(s573,plain,
( ~ spl0_14
| spl0_74
| ~ spl0_110
| spl0_152 ),
inference(sat_conversion,[],[f1994]) ).
cnf(s591,plain,
( ~ spl0_9
| ~ spl0_136
| ~ spl0_137
| spl0_150 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s592,plain,
( ~ spl0_1
| spl0_62
| spl0_64
| ~ spl0_138 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s594,plain,
( ~ spl0_1
| spl0_70
| spl0_71
| ~ spl0_108 ),
inference(sat_conversion,[],[f2046]) ).
cnf(s604,plain,
( ~ spl0_15
| spl0_23
| ~ spl0_40 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s605,plain,
( ~ spl0_23
| ~ spl0_132
| ~ spl0_133
| spl0_147 ),
inference(sat_conversion,[],[f2056]) ).
cnf(s608,plain,
( ~ spl0_23
| spl0_76
| ~ spl0_112
| ~ spl0_142 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s609,plain,
( ~ spl0_40
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s612,plain,
( ~ spl0_40
| spl0_84
| ~ spl0_118
| spl0_148 ),
inference(sat_conversion,[],[f2063]) ).
cnf(s613,plain,
( ~ spl0_40
| spl0_75
| spl0_76
| ~ spl0_142 ),
inference(sat_conversion,[],[f2064]) ).
cnf(s616,plain,
( ~ spl0_5
| spl0_62
| spl0_63
| ~ spl0_138 ),
inference(sat_conversion,[],[f2080]) ).
cnf(s618,plain,
( ~ spl0_12
| spl0_68
| spl0_69
| ~ spl0_107 ),
inference(sat_conversion,[],[f2095]) ).
cnf(s620,plain,
( ~ spl0_12
| spl0_77
| ~ spl0_114
| spl0_144 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s622,plain,
( ~ spl0_13
| spl0_85
| spl0_86
| ~ spl0_120 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s642,plain,
( ~ spl0_26
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f2129]) ).
cnf(s652,plain,
( ~ spl0_13
| spl0_66
| spl0_67
| ~ spl0_145 ),
inference(sat_conversion,[],[f2143]) ).
cnf(s653,plain,
( ~ spl0_15
| spl0_67
| ~ spl0_106
| ~ spl0_145 ),
inference(sat_conversion,[],[f2154]) ).
cnf(s655,plain,
( ~ spl0_15
| ~ spl0_133
| ~ spl0_134
| spl0_147 ),
inference(sat_conversion,[],[f2156]) ).
cnf(s657,plain,
( ~ spl0_20
| ~ spl0_110
| ~ spl0_111
| spl0_152 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s658,plain,
( ~ spl0_20
| ~ spl0_132
| ~ spl0_134
| spl0_147 ),
inference(sat_conversion,[],[f2167]) ).
cnf(s659,plain,
( ~ spl0_25
| spl0_63
| spl0_64
| spl0_138 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s660,plain,
( ~ spl0_25
| spl0_87
| spl0_88
| spl0_89 ),
inference(sat_conversion,[],[f2183]) ).
cnf(s663,plain,
( ~ spl0_26
| spl0_87
| spl0_88
| spl0_143 ),
inference(sat_conversion,[],[f2200]) ).
cnf(s666,plain,
( ~ spl0_14
| spl0_87
| spl0_89
| ~ spl0_143 ),
inference(sat_conversion,[],[f2204]) ).
cnf(s669,plain,
( ~ spl0_57
| spl0_80
| spl0_81
| spl0_82 ),
inference(sat_conversion,[],[f2233]) ).
cnf(s670,plain,
( ~ spl0_57
| spl0_66
| spl0_67
| spl0_145 ),
inference(sat_conversion,[],[f2234]) ).
cnf(s676,plain,
( ~ spl0_2
| ~ spl0_132
| ~ spl0_134
| ~ spl0_147 ),
inference(sat_conversion,[],[f2238]) ).
cnf(s681,plain,
( ~ spl0_8
| ~ spl0_129
| ~ spl0_131
| spl0_153 ),
inference(sat_conversion,[],[f2242]) ).
cnf(s685,plain,
( ~ spl0_11
| ~ spl0_133
| ~ spl0_134
| ~ spl0_147 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s692,plain,
( ~ spl0_19
| spl0_75
| spl0_76
| ~ spl0_112 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s705,plain,
( ~ spl0_21
| spl0_87
| spl0_88
| ~ spl0_143 ),
inference(sat_conversion,[],[f2266]) ).
cnf(s708,plain,
( ~ spl0_35
| spl0_72
| spl0_73
| ~ spl0_109 ),
inference(sat_conversion,[],[f2269]) ).
cnf(s711,plain,
( ~ spl0_14
| spl0_83
| ~ spl0_116
| spl0_155 ),
inference(sat_conversion,[],[f2272]) ).
cnf(s712,plain,
( ~ spl0_47
| spl0_88
| spl0_89
| spl0_143 ),
inference(sat_conversion,[],[f2273]) ).
cnf(s717,plain,
( ~ spl0_47
| spl0_62
| spl0_64
| spl0_138 ),
inference(sat_conversion,[],[f2278]) ).
cnf(s718,plain,
spl0_3,
inference(rat,[],[s137,s140,s153,s163]) ).
cnf(s719,plain,
( spl0_14
| ~ spl0_20
| spl0_26 ),
inference(rat,[],[s314,s13,s718]) ).
cnf(s720,plain,
( ~ spl0_37
| ~ spl0_20
| ~ spl0_11 ),
inference(rat,[],[s658,s685,s125,s126,s127]) ).
cnf(s721,plain,
( ~ spl0_29
| ~ spl0_20 ),
inference(rat,[],[s519,s78,s109,s110]) ).
cnf(s722,plain,
( spl0_8
| spl0_7
| spl0_5
| spl0_2 ),
inference(rat,[],[s249,s608,s22,s29,s466,s721,s25,s720,s9,s692,s70,s71,s105,s5,s16,s347,s170,s3,s718]) ).
cnf(s723,plain,
( ~ spl0_41
| ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s499,s505,s106,s107]) ).
cnf(s725,plain,
( ~ spl0_38
| ~ spl0_18 ),
inference(rat,[],[s516,s56,s95,s96]) ).
cnf(s726,plain,
( spl0_12
| ~ spl0_20
| spl0_41
| spl0_5
| spl0_2 ),
inference(rat,[],[s29,s642,s608,s57,s58,s59,s489,s38,s52,s725,s39,s720,s70,s71,s105,s5,s16,s721,s718]) ).
cnf(s727,plain,
( spl0_38
| ~ spl0_12
| spl0_2 ),
inference(rat,[],[s717,s555,s57,s58,s59,s38,s52,s718]) ).
cnf(s728,plain,
( ~ spl0_20
| spl0_41
| spl0_5
| spl0_2 ),
inference(rat,[],[s263,s125,s126,s127,s39,s725,s727,s726,s15,s721,s718]) ).
cnf(s729,plain,
( ~ spl0_39
| ~ spl0_26 ),
inference(rat,[],[s642,s57,s58,s59]) ).
cnf(s730,plain,
( spl0_7
| spl0_5
| ~ spl0_4
| spl0_2 ),
inference(rat,[],[s612,s372,s79,s111,s112,s17,s605,s373,s125,s126,s39,s725,s27,s38,s729,s347,s30,s728,s723,s722,s718]) ).
cnf(s731,plain,
( ~ spl0_20
| spl0_5
| ~ spl0_4
| spl0_2 ),
inference(rat,[],[s720,s25,s5,s496,s620,s499,s72,s106,s107,s728,s718]) ).
cnf(s732,plain,
( spl0_12
| spl0_20
| spl0_2 ),
inference(rat,[],[s692,s70,s71,s105,s9,s16,s718]) ).
cnf(s733,plain,
( ~ spl0_41
| ~ spl0_12
| ~ spl0_4 ),
inference(rat,[],[s620,s499,s72,s106,s107]) ).
cnf(s734,plain,
( ~ spl0_36
| ~ spl0_40 ),
inference(rat,[],[s609,s88,s89,s117]) ).
cnf(s735,plain,
( ~ spl0_33
| ~ spl0_17
| ~ spl0_26 ),
inference(rat,[],[s218,s232,s53,s54]) ).
cnf(s736,plain,
( ~ spl0_46
| ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s681,s452,s122,s124]) ).
cnf(s737,plain,
( spl0_75
| spl0_76
| ~ spl0_112
| ~ spl0_47
| ~ spl0_7 ),
inference(rat,[],[s241,s489]) ).
cnf(s738,plain,
( spl0_15
| spl0_33
| ~ spl0_26
| spl0_9
| ~ spl0_12
| ~ spl0_7
| ~ spl0_4 ),
inference(rat,[],[s70,s737,s71,s105,s35,s136,s736,s265,s19,s269,s669,s75,s76,s77,s18,s729,s718]) ).
cnf(s739,plain,
( spl0_5
| spl0_2
| ~ spl0_4 ),
inference(rat,[],[s373,s605,s125,s126,s604,s39,s738,s735,s21,s734,s27,s729,s30,s733,s725,s727,s170,s732,s731,s730,s718]) ).
cnf(s740,plain,
( spl0_9
| spl0_76
| spl0_75
| ~ spl0_26
| spl0_18
| ~ spl0_12
| ~ spl0_4 ),
inference(rat,[],[s265,s736,s19,s35,s735,s269,s489,s21,s669,s613,s734,s75,s76,s77,s27,s18,s729,s655,s373,s125,s127,s126,s39,s733,s718]) ).
cnf(s741,plain,
( ~ spl0_48
| ~ spl0_21
| ~ spl0_26 ),
inference(rat,[],[s663,s705,s82,s83]) ).
cnf(s742,plain,
( ~ spl0_9
| spl0_15
| ~ spl0_26
| spl0_18
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s276,s591,s128,s129,s130,s43,s261,s736,s47,s741,s10,s283,s253,s88,s89,s117,s21,s8,s250,s718]) ).
cnf(s743,plain,
( spl0_75
| spl0_9
| ~ spl0_26
| spl0_18
| ~ spl0_12
| ~ spl0_4 ),
inference(rat,[],[s3,s241,s736,s249,s136,s172,s71,s740,s21,s734,s27,s729,s718]) ).
cnf(s744,plain,
( spl0_20
| spl0_2
| spl0_1 ),
inference(rat,[],[s136,s736,s70,s265,s743,s19,s735,s21,s734,s27,s742,s655,s373,s125,s126,s127,s729,s39,s30,s725,s733,s727,s732,s1,s718]) ).
cnf(s745,plain,
( ~ spl0_37
| ~ spl0_20
| ~ spl0_4 ),
inference(rat,[],[s373,s658,s125,s126,s127]) ).
cnf(s746,plain,
( ~ spl0_12
| spl0_37
| ~ spl0_4
| spl0_2 ),
inference(rat,[],[s39,s725,s733,s727,s718]) ).
cnf(s747,plain,
( spl0_38
| ~ spl0_5
| spl0_2 ),
inference(rat,[],[s616,s717,s57,s58,s59,s38,s52,s718]) ).
cnf(s748,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s496,s72,s106,s107,s39,s725,s747,s25,s746,s745,s744,s739,s1,s718]) ).
cnf(s749,plain,
( spl0_18
| ~ spl0_9
| spl0_14 ),
inference(rat,[],[s250,s8,s718]) ).
cnf(s750,plain,
( ~ spl0_37
| ~ spl0_15
| ~ spl0_2 ),
inference(rat,[],[s676,s655,s125,s126,s127]) ).
cnf(s755,plain,
( ~ spl0_27
| ~ spl0_57 ),
inference(rat,[],[s669,s75,s76,s77]) ).
cnf(s758,plain,
( ~ spl0_51
| ~ spl0_9
| ~ spl0_2 ),
inference(rat,[],[s327,s591,s129,s130]) ).
cnf(s759,plain,
( spl0_46
| ~ spl0_26
| spl0_1 ),
inference(rat,[],[s622,s80,s81,s113,s137,s758,s436,s52,s725,s749,s27,s271,s666,s10,s663,s692,s741,s82,s83,s84,s70,s71,s105,s47,s136,s748,s729,s718]) ).
cnf(s760,plain,
( ~ spl0_46
| ~ spl0_2 ),
inference(rat,[],[s325,s122,s123,s124]) ).
cnf(s761,plain,
( ~ spl0_36
| ~ spl0_19
| ~ spl0_14 ),
inference(rat,[],[s283,s253,s88,s89,s117]) ).
cnf(s762,plain,
( ~ spl0_22
| ~ spl0_35 ),
inference(rat,[],[s708,s67,s68,s102]) ).
cnf(s763,plain,
( ~ spl0_12
| ~ spl0_41
| spl0_46 ),
inference(rat,[],[s618,s63,s64,s100,s37,s733,s718]) ).
cnf(s764,plain,
( spl0_20
| spl0_1 ),
inference(rat,[],[s11,s605,s399,s676,s21,s125,s126,s127,s761,s25,s9,s763,s496,s72,s106,s107,s30,s725,s52,s762,s35,s712,s666,s13,s660,s759,s82,s84,s83,s47,s760,s748,s718]) ).
cnf(s765,plain,
( ~ spl0_37
| spl0_1 ),
inference(rat,[],[s658,s676,s125,s127,s748,s764]) ).
cnf(s766,plain,
( spl0_46
| spl0_1 ),
inference(rat,[],[s25,s496,s763,s72,s106,s107,s39,s765,s725,s52,s712,s666,s13,s660,s82,s83,s84,s759,s47,s718]) ).
cnf(s767,plain,
spl0_1,
inference(rat,[],[s766,s760,s748]) ).
cnf(s768,plain,
( ~ spl0_42
| ~ spl0_8
| ~ spl0_5 ),
inference(rat,[],[s171,s63,s100]) ).
cnf(s772,plain,
( ~ spl0_49
| ~ spl0_43 ),
inference(rat,[],[s406,s61,s62,s99]) ).
cnf(s773,plain,
( ~ spl0_47
| ~ spl0_26
| ~ spl0_2 ),
inference(rat,[],[s422,s60,s97,s98,s50,s772,s31,s768,s196,s26,s436,s622,s80,s81,s113,s137,s758,s347,s27,s613,s489,s71,s70,s136,s729,s760,s718]) ).
cnf(s774,plain,
( spl0_47
| ~ spl0_2
| spl0_41 ),
inference(rat,[],[s605,s676,s125,s126,s127,s11,s39,s174,s762,s725,s35,s52,s760,s718,s767]) ).
cnf(s775,plain,
( ~ spl0_31
| spl0_76
| ~ spl0_23
| ~ spl0_47 ),
inference(rat,[],[s489,s608,s70,s105]) ).
cnf(s777,plain,
( ~ spl0_31
| ~ spl0_23
| ~ spl0_47 ),
inference(rat,[],[s775,s71]) ).
cnf(s778,plain,
( spl0_64
| ~ spl0_47
| spl0_62 ),
inference(rat,[],[s592,s717,s767]) ).
cnf(s779,plain,
( ~ spl0_2
| spl0_41 ),
inference(rat,[],[s778,s57,s59,s136,s777,s29,s721,s30,s773,s774,s760,s718]) ).
cnf(s780,plain,
( ~ spl0_53
| ~ spl0_9 ),
inference(rat,[],[s422,s60,s97,s98]) ).
cnf(s781,plain,
~ spl0_24,
inference(rat,[],[s594,s65,s66,s101,s767]) ).
cnf(s782,plain,
spl0_57,
inference(rat,[],[s51,s718,s781]) ).
cnf(s783,plain,
~ spl0_27,
inference(rat,[],[s755,s782]) ).
cnf(s785,plain,
( ~ spl0_48
| ~ spl0_47
| spl0_18
| spl0_39 ),
inference(rat,[],[s27,s749,s271,s666,s712,s82,s83,s84,s718]) ).
cnf(s786,plain,
( spl0_15
| ~ spl0_5
| spl0_18 ),
inference(rat,[],[s31,s652,s768,s670,s261,s772,s61,s62,s10,s50,s761,s734,s21,s780,s250,s749,s18,s14,s236,s718,s782,s783,s767]) ).
cnf(s787,plain,
( ~ spl0_26
| spl0_41 ),
inference(rat,[],[s27,s749,s271,s666,s663,s82,s83,s84,s36,s373,s655,s786,s125,s126,s127,s2,s39,s236,s725,s38,s729,s779,s718,s783,s767]) ).
cnf(s788,plain,
( ~ spl0_36
| spl0_41 ),
inference(rat,[],[s538,s253,s89,s117,s719,s29,s721,s30,s787,s718]) ).
cnf(s789,plain,
( ~ spl0_52
| spl0_41 ),
inference(rat,[],[s657,s403,s69,s103,s104,s14,s236,s725,s747,s728,s30,s787,s779,s783,s718,s767]) ).
cnf(s790,plain,
( spl0_31
| spl0_41 ),
inference(rat,[],[s762,s49,s40,s250,s21,s788,s725,s747,s728,s30,s787,s779,s789,s718]) ).
cnf(s791,plain,
spl0_41,
inference(rat,[],[s249,s608,s70,s71,s105,s790,s21,s788,s725,s747,s29,s728,s721,s30,s787,s779,s718]) ).
cnf(s792,plain,
spl0_114,
inference(rat,[],[s107,s791]) ).
cnf(s793,plain,
spl0_113,
inference(rat,[],[s106,s791]) ).
cnf(s794,plain,
~ spl0_77,
inference(rat,[],[s72,s791]) ).
cnf(s795,plain,
~ spl0_16,
inference(rat,[],[s496,s792,s793,s794]) ).
cnf(s796,plain,
( spl0_15
| spl0_12 ),
inference(rat,[],[s786,s725,s545,s52,s45,s778,s780,s57,s59,s18,s26,s783,s718,s767]) ).
cnf(s797,plain,
~ spl0_2,
inference(rat,[],[s796,s750,s25,s763,s760,s718,s795,s791]) ).
cnf(s798,plain,
( ~ spl0_49
| ~ spl0_15 ),
inference(rat,[],[s670,s653,s61,s62,s99,s782]) ).
cnf(s799,plain,
( ~ spl0_9
| spl0_18 ),
inference(rat,[],[s734,s21,s50,s250,s780,s798,s786,s2,s236,s718,s797,s767]) ).
cnf(s800,plain,
( ~ spl0_47
| spl0_39 ),
inference(rat,[],[s733,s16,s36,s777,s785,s604,s27,s799,s786,s2,s236,s725,s38,s791,s718,s797,s783,s767]) ).
cnf(s801,plain,
~ spl0_26,
inference(rat,[],[s663,s271,s82,s83,s84,s36,s452,s500,s122,s123,s124,s35,s800,s762,s41,s27,s799,s798,s786,s14,s2,s236,s725,s38,s729,s718,s783,s797,s767]) ).
cnf(s802,plain,
spl0_38,
inference(rat,[],[s778,s57,s59,s38,s52,s718,s797]) ).
cnf(s806,plain,
~ spl0_18,
inference(rat,[],[s725,s802]) ).
cnf(s808,plain,
~ spl0_6,
inference(rat,[],[s236,s767,s806]) ).
cnf(s809,plain,
~ spl0_9,
inference(rat,[],[s799,s806]) ).
cnf(s810,plain,
spl0_5,
inference(rat,[],[s2,s718,s797,s808]) ).
cnf(s811,plain,
spl0_28,
inference(rat,[],[s14,s783,s718,s808]) ).
cnf(s812,plain,
spl0_15,
inference(rat,[],[s18,s783,s718,s809]) ).
cnf(s813,plain,
~ spl0_49,
inference(rat,[],[s798,s812]) ).
cnf(s814,plain,
spl0_22,
inference(rat,[],[s41,s809,s718,s813]) ).
cnf(s818,plain,
~ spl0_35,
inference(rat,[],[s762,s814]) ).
cnf(s819,plain,
( ~ spl0_31
| ~ spl0_40 ),
inference(rat,[],[s249,s608,s70,s71,s105,s604,s21,s734,s806,s718,s812]) ).
cnf(s820,plain,
spl0_39,
inference(rat,[],[s573,s403,s69,s103,s104,s49,s819,s13,s660,s82,s83,s84,s36,s452,s500,s122,s123,s124,s35,s27,s800,s811,s718,s818,s801,s783,s809]) ).
cnf(s821,plain,
~ spl0_64,
inference(rat,[],[s59,s820]) ).
cnf(s822,plain,
~ spl0_63,
inference(rat,[],[s58,s820]) ).
cnf(s823,plain,
~ spl0_62,
inference(rat,[],[s57,s820]) ).
cnf(s824,plain,
~ spl0_138,
inference(rat,[],[s616,s823,s810,s822]) ).
cnf(s826,plain,
~ spl0_25,
inference(rat,[],[s659,s821,s822,s824]) ).
cnf(s828,plain,
spl0_14,
inference(rat,[],[s13,s801,s718,s826]) ).
cnf(s839,plain,
~ spl0_29,
inference(rat,[],[s711,s427,s78,s109,s110,s828,s812]) ).
cnf(s840,plain,
spl0_23,
inference(rat,[],[s29,s801,s718,s839]) ).
cnf(s841,plain,
spl0_21,
inference(rat,[],[s23,s809,s718,s839]) ).
cnf(s845,plain,
~ spl0_36,
inference(rat,[],[s538,s257,s88,s89,s117,s840,s841]) ).
cnf(s846,plain,
spl0_17,
inference(rat,[],[s21,s806,s718,s845]) ).
cnf(s848,plain,
~ spl0_31,
inference(rat,[],[s249,s608,s70,s71,s105,s846,s840]) ).
cnf(s850,plain,
spl0_52,
inference(rat,[],[s49,s818,s718,s848]) ).
cnf(s851,plain,
spl0_111,
inference(rat,[],[s104,s850]) ).
cnf(s852,plain,
spl0_110,
inference(rat,[],[s103,s850]) ).
cnf(s853,plain,
~ spl0_74,
inference(rat,[],[s69,s850]) ).
cnf(s854,plain,
~ spl0_152,
inference(rat,[],[s403,s853,s811,s851]) ).
cnf(s856,plain,
$false,
inference(rat,[],[s573,s853,s828,s852,s854]) ).
fof(f2279,plain,
$false,
inference(avatar_sat_refutation,[],[s856]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN459-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.06/0.17 % Computer : n005.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 16:06:17 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.21 Running first-order theorem proving
% 0.06/0.21 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
% 3.15/1.10 % (903523)Input is clausal, will run a generic CNF schedule.
% 3.15/1.10 % (903529)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1438184001:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.15/1.10 % (903533)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4009479286:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.15/1.10 % (903531)lrs+10_1_sil=8000:sp=occurrence:random_seed=3368519069:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.15/1.10 % (903532)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3674722945:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.15/1.10 % (903528)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=2570784317:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.15/1.10 % (903530)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=124202836:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.15/1.10 % (903534)dis-21_1_sil=8000:lcm=predicate:random_seed=3055349405:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.15/1.10 % (903534)First to succeed.
% 3.15/1.10 % (903533)Also succeeded, but the first one will report.
% 3.15/1.10 % (903532)Also succeeded, but the first one will report.
% 3.15/1.10 % (903534)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-903523"
% 3.15/1.10 % (903531)Also succeeded, but the first one will report.
% 3.15/1.10 % (903529)Refutation not found, incomplete strategy
% 3.15/1.10 % (903529)------------------------------
% 3.15/1.10 % (903529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.15/1.10 % (903529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.15/1.10 % (903529)CaDiCaL version: 2.1.3
% 3.15/1.10 % (903529)Termination reason: Refutation not found, incomplete strategy
% 3.15/1.10 % (903529)Time elapsed: 0.328 s
% 3.15/1.10 % (903529)Peak memory usage: 129 MB
% 3.15/1.10 % (903529)Instructions burned: 894 (million)
% 3.15/1.10 % (903534)Refutation found. Thanks to Tanya!
% 3.15/1.10 % SZS status Unsatisfiable for theBenchmark
% 3.15/1.10 % SZS output start Proof for theBenchmark
% See solution above
% 3.71/1.28 % (903534)------------------------------
% 3.71/1.28 % (903534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.28 % (903534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.71/1.28 % (903534)CaDiCaL version: 2.1.3
% 3.71/1.28 % (903534)Termination reason: Refutation
% 3.71/1.28 % (903534)Time elapsed: 0.035 s
% 3.71/1.28 % (903534)Peak memory usage: 90 MB
% 3.71/1.28 % (903534)Instructions burned: 55 (million)
% 3.71/1.28 % (903534)------------------------------
% 3.71/1.28 % (903534)------------------------------
% 3.71/1.28 % (903523)Success in time 0.451 s
% 3.71/1.28 % Vampire exiting
%------------------------------------------------------------------------------