%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN459-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:09:14 PM UTC 2026
% Result : Unsatisfiable 0.19s 0.31s
% Output : Refutation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp25
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f11,negated_conjecture,
( ~ hskp15
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
fof(f24,negated_conjecture,
( ~ hskp2
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
fof(f27,negated_conjecture,
( hskp25
| hskp15
| hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
fof(f28,negated_conjecture,
( hskp23
| hskp9
| hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
fof(f30,negated_conjecture,
( hskp5
| hskp15
| hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
fof(f34,negated_conjecture,
( ~ hskp25
| c0_1(a230) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
( ~ hskp25
| c1_1(a230) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( ~ hskp25
| c2_1(a230) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( ~ hskp24
| c1_1(a215) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( ~ hskp24
| c2_1(a215) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
( ~ hskp24
| c3_1(a215) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( ~ hskp23
| c0_1(a189) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
fof(f41,negated_conjecture,
( ~ hskp23
| c1_1(a189) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
( ~ hskp23
| c3_1(a189) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
fof(f44,negated_conjecture,
( ~ hskp21
| c2_1(a257) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
fof(f47,negated_conjecture,
( ~ hskp19
| c3_1(a225) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp18
| c3_1(a223) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp17
| c1_1(a222) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp17
| c2_1(a222) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp15
| c2_1(a214) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
fof(f54,negated_conjecture,
( ~ hskp13
| c1_1(a209) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( ~ hskp13
| c3_1(a209) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( ~ hskp11
| c0_1(a202) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp10
| c0_1(a200) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp10
| c3_1(a200) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp9
| c2_1(a199) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp8
| c1_1(a198) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp8
| c3_1(a198) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp7
| c1_1(a197) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp6
| c0_1(a195) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp5
| c0_1(a194) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f68,negated_conjecture,
( ~ hskp1
| c0_1(a190) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp1
| c2_1(a190) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f72,negated_conjecture,
( ~ c1_1(a257)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ c3_1(a257)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f75,negated_conjecture,
( ~ c0_1(a225)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ c1_1(a225)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ c1_1(a223)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ c2_1(a223)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ c3_1(a222)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ c0_1(a221)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ c1_1(a221)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ c2_1(a221)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ c0_1(a214)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ c3_1(a214)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f86,negated_conjecture,
( ~ c0_1(a209)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ c0_1(a206)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ c2_1(a206)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ c3_1(a206)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c2_1(a202)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c3_1(a202)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ c1_1(a200)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c0_1(a199)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c1_1(a199)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c2_1(a198)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c0_1(a197)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c2_1(a197)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c1_1(a195)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c3_1(a195)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c1_1(a194)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c2_1(a194)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f105,negated_conjecture,
( ~ c1_1(a191)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c2_1(a191)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c3_1(a191)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c3_1(a190)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c0_1(a188)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c1_1(a188)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c3_1(a188)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c3_1(X0)
| hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f115,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp8
| hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp11
| hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp23
| hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp17
| hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f121,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp25
| hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f124,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp7
| hskp9 ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',clause127) ).
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/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f131,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',clause141) ).
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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',clause146) ).
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/sandbox/benchmark/theBenchmark.p',clause148) ).
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/sandbox/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause152) ).
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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X2)
| c1_1(X0)
| c0_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause157) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/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] :
( ~ c0_1(X2)
| c3_1(X2)
| c1_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] :
( ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c1_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(f175,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f176,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f177,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f163,f175,f171,f168,f165]) ).
fof(f179,definition,
( spl0_5
<=> ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f180,plain,
( ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f182,definition,
( spl0_6
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f183,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| ~ c1_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f184,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f162,f168,f171,f182,f179]) ).
fof(f186,definition,
( spl0_7
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f187,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| ~ c2_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f186]) ).
fof(f189,definition,
( spl0_8
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f190,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f192,definition,
( spl0_9
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f193,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f194,plain,
( spl0_7
| spl0_8
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f161,f192,f171,f189,f186]) ).
fof(f199,definition,
( spl0_11
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f200,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f203,definition,
( spl0_12
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f204,plain,
( ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f205,plain,
( spl0_12
| spl0_5
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f159,f199,f171,f179,f203]) ).
fof(f207,definition,
( spl0_13
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f208,plain,
( ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f211,definition,
( spl0_14
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f212,plain,
( ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f214,definition,
( spl0_15
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f215,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f217,definition,
( spl0_16
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f218,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f219,plain,
( spl0_14
| spl0_15
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f157,f217,f171,f214,f211]) ).
fof(f221,definition,
( spl0_17
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f222,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f224,definition,
( spl0_18
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f225,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f226,plain,
( spl0_14
| spl0_17
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f156,f224,f171,f221,f211]) ).
fof(f228,definition,
( spl0_19
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f229,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f231,definition,
( spl0_20
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f232,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f233,plain,
( spl0_19
| spl0_20
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f155,f203,f171,f231,f228]) ).
fof(f235,definition,
( spl0_21
<=> ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f236,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f237,plain,
( spl0_19
| spl0_15
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f154,f235,f171,f214,f228]) ).
fof(f239,definition,
( spl0_22
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f243,definition,
( spl0_23
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f244,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl0_24
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f250,plain,
( spl0_24
| spl0_15
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f152,f175,f171,f214,f247]) ).
fof(f252,definition,
( spl0_25
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f253,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f255,definition,
( spl0_26
<=> ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f256,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1)
| c2_1(X1) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f257,plain,
( spl0_25
| spl0_26
| spl0_14
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f151,f171,f211,f255,f252]) ).
fof(f259,definition,
( spl0_27
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f263,definition,
( spl0_28
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f264,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f267,definition,
( spl0_29
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f275,definition,
( spl0_31
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f278,plain,
( spl0_31
| spl0_12
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f148,f168,f171,f203,f275]) ).
fof(f284,plain,
( spl0_27
| spl0_15
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f146,f192,f171,f214,f259]) ).
fof(f286,definition,
( spl0_33
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f290,definition,
( spl0_34
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f291,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f292,plain,
( spl0_33
| spl0_15
| ~ spl0_3
| spl0_34 ),
inference(avatar_split_clause,[],[f145,f290,f171,f214,f286]) ).
fof(f294,definition,
( spl0_35
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f295,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f298,definition,
( spl0_36
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f301,plain,
( spl0_36
| spl0_17
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f143,f224,f171,f221,f298]) ).
fof(f303,definition,
( spl0_37
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f307,plain,
( spl0_29
| spl0_21
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f141,f192,f171,f235,f267]) ).
fof(f309,definition,
( spl0_38
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f313,plain,
( spl0_37
| spl0_12
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f139,f217,f171,f203,f303]) ).
fof(f315,definition,
( spl0_39
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f318,plain,
( spl0_39
| spl0_15
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f138,f203,f171,f214,f315]) ).
fof(f320,definition,
( spl0_40
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f321,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( spl0_39
| spl0_40
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f137,f192,f171,f320,f315]) ).
fof(f324,plain,
( spl0_29
| spl0_26
| spl0_23
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f135,f171,f243,f255,f267]) ).
fof(f326,definition,
( spl0_41
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f329,plain,
( spl0_41
| spl0_26
| spl0_20
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f134,f171,f231,f255,f326]) ).
fof(f331,definition,
( spl0_42
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f335,definition,
( spl0_43
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f336,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( spl0_42
| spl0_43
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f133,f207,f171,f335,f331]) ).
fof(f338,plain,
( spl0_41
| spl0_14
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f132,f179,f171,f211,f326]) ).
fof(f339,plain,
( spl0_33
| spl0_25
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f131,f189,f171,f252,f286]) ).
fof(f341,definition,
( spl0_44
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f349,definition,
( spl0_46
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f353,definition,
( spl0_47
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f354,plain,
( ! [X1] :
( c3_1(X1)
| c0_1(X1)
| c1_1(X1) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f355,plain,
( spl0_46
| spl0_47
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f129,f294,f171,f353,f349]) ).
fof(f357,definition,
( spl0_48
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f361,plain,
( spl0_42
| spl0_46
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f127,f175,f171,f349,f331]) ).
fof(f362,plain,
( spl0_39
| spl0_38
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f126,f168,f171,f309,f315]) ).
fof(f363,plain,
( spl0_37
| spl0_41
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f125,f224,f171,f326,f303]) ).
fof(f364,plain,
( spl0_31
| spl0_22
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f124,f192,f171,f239,f275]) ).
fof(f376,definition,
( spl0_51
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f379,plain,
( spl0_48
| spl0_51
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f121,f263,f171,f376,f357]) ).
fof(f381,definition,
( spl0_52
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f391,definition,
( spl0_54
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f395,definition,
( spl0_55
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f398,plain,
( spl0_54
| spl0_55
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f118,f165,f171,f395,f391]) ).
fof(f399,plain,
( spl0_48
| spl0_46
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f117,f165,f171,f349,f357]) ).
fof(f401,definition,
( spl0_56
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f404,plain,
( spl0_31
| spl0_56
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f116,f207,f171,f401,f275]) ).
fof(f405,plain,
( spl0_31
| spl0_52
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f115,f294,f171,f381,f275]) ).
fof(f411,plain,
( spl0_38
| spl0_47
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f112,f171,f353,f309]) ).
fof(f413,definition,
( spl0_58
<=> c3_1(a188) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f415,plain,
( ~ c3_1(a188)
| spl0_58 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f416,plain,
( ~ spl0_33
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f111,f413,f286]) ).
fof(f418,definition,
( spl0_59
<=> c1_1(a188) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f420,plain,
( ~ c1_1(a188)
| spl0_59 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f421,plain,
( ~ spl0_33
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f110,f418,f286]) ).
fof(f423,definition,
( spl0_60
<=> c0_1(a188) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f425,plain,
( ~ c0_1(a188)
| spl0_60 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f426,plain,
( ~ spl0_33
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f109,f423,f286]) ).
fof(f428,definition,
( spl0_61
<=> c3_1(a190) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f430,plain,
( ~ c3_1(a190)
| spl0_61 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f431,plain,
( ~ spl0_38
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f108,f428,f309]) ).
fof(f433,definition,
( spl0_62
<=> c3_1(a191) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f435,plain,
( ~ c3_1(a191)
| spl0_62 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f436,plain,
( ~ spl0_39
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f107,f433,f315]) ).
fof(f438,definition,
( spl0_63
<=> c2_1(a191) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f441,plain,
( ~ spl0_39
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f106,f438,f315]) ).
fof(f443,definition,
( spl0_64
<=> c1_1(a191) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f445,plain,
( ~ c1_1(a191)
| spl0_64 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f446,plain,
( ~ spl0_39
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f105,f443,f315]) ).
fof(f463,definition,
( spl0_68
<=> c2_1(a194) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f465,plain,
( ~ c2_1(a194)
| spl0_68 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f466,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f101,f463,f331]) ).
fof(f468,definition,
( spl0_69
<=> c1_1(a194) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f470,plain,
( ~ c1_1(a194)
| spl0_69 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f471,plain,
( ~ spl0_42
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f100,f468,f331]) ).
fof(f473,definition,
( spl0_70
<=> c3_1(a195) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f475,plain,
( ~ c3_1(a195)
| spl0_70 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f476,plain,
( ~ spl0_24
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f99,f473,f247]) ).
fof(f478,definition,
( spl0_71
<=> c1_1(a195) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f481,plain,
( ~ spl0_24
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f98,f478,f247]) ).
fof(f483,definition,
( spl0_72
<=> c2_1(a197) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f485,plain,
( ~ c2_1(a197)
| spl0_72 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f486,plain,
( ~ spl0_22
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f97,f483,f239]) ).
fof(f488,definition,
( spl0_73
<=> c0_1(a197) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f490,plain,
( ~ c0_1(a197)
| spl0_73 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f491,plain,
( ~ spl0_22
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f96,f488,f239]) ).
fof(f493,definition,
( spl0_74
<=> c2_1(a198) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f496,plain,
( ~ spl0_52
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f95,f493,f381]) ).
fof(f498,definition,
( spl0_75
<=> c1_1(a199) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f500,plain,
( ~ c1_1(a199)
| spl0_75 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f501,plain,
( ~ spl0_31
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f94,f498,f275]) ).
fof(f503,definition,
( spl0_76
<=> c0_1(a199) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f505,plain,
( ~ c0_1(a199)
| spl0_76 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f506,plain,
( ~ spl0_31
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f93,f503,f275]) ).
fof(f508,definition,
( spl0_77
<=> c1_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f510,plain,
( ~ c1_1(a200)
| spl0_77 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
( ~ spl0_41
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f92,f508,f326]) ).
fof(f513,definition,
( spl0_78
<=> c3_1(a202) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f515,plain,
( ~ c3_1(a202)
| spl0_78 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f516,plain,
( ~ spl0_56
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f91,f513,f401]) ).
fof(f518,definition,
( spl0_79
<=> c2_1(a202) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f521,plain,
( ~ spl0_56
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f90,f518,f401]) ).
fof(f523,definition,
( spl0_80
<=> c3_1(a206) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f525,plain,
( ~ c3_1(a206)
| spl0_80 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f526,plain,
( ~ spl0_27
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f89,f523,f259]) ).
fof(f528,definition,
( spl0_81
<=> c2_1(a206) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f530,plain,
( ~ c2_1(a206)
| spl0_81 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f531,plain,
( ~ spl0_27
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f88,f528,f259]) ).
fof(f533,definition,
( spl0_82
<=> c0_1(a206) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f535,plain,
( ~ c0_1(a206)
| spl0_82 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f536,plain,
( ~ spl0_27
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f87,f533,f259]) ).
fof(f538,definition,
( spl0_83
<=> c0_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f541,plain,
( ~ spl0_29
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f86,f538,f267]) ).
fof(f548,definition,
( spl0_85
<=> c3_1(a214) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f550,plain,
( ~ c3_1(a214)
| spl0_85 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f551,plain,
( ~ spl0_44
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f84,f548,f341]) ).
fof(f553,definition,
( spl0_86
<=> c0_1(a214) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f554,plain,
( c0_1(a214)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f555,plain,
( ~ c0_1(a214)
| spl0_86 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f556,plain,
( ~ spl0_44
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f83,f553,f341]) ).
fof(f558,definition,
( spl0_87
<=> c2_1(a221) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f560,plain,
( ~ c2_1(a221)
| spl0_87 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f561,plain,
( ~ spl0_48
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f82,f558,f357]) ).
fof(f563,definition,
( spl0_88
<=> c1_1(a221) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f565,plain,
( ~ c1_1(a221)
| spl0_88 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f566,plain,
( ~ spl0_48
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f81,f563,f357]) ).
fof(f568,definition,
( spl0_89
<=> c0_1(a221) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f570,plain,
( ~ c0_1(a221)
| spl0_89 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f571,plain,
( ~ spl0_48
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f80,f568,f357]) ).
fof(f573,definition,
( spl0_90
<=> c3_1(a222) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f575,plain,
( ~ c3_1(a222)
| spl0_90 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f576,plain,
( ~ spl0_55
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f79,f573,f395]) ).
fof(f578,definition,
( spl0_91
<=> c2_1(a223) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f580,plain,
( ~ c2_1(a223)
| spl0_91 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f581,plain,
( ~ spl0_54
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f78,f578,f391]) ).
fof(f583,definition,
( spl0_92
<=> c1_1(a223) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f585,plain,
( ~ c1_1(a223)
| spl0_92 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f586,plain,
( ~ spl0_54
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f77,f583,f391]) ).
fof(f588,definition,
( spl0_93
<=> c1_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f590,plain,
( ~ c1_1(a225)
| spl0_93 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f591,plain,
( ~ spl0_36
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f76,f588,f298]) ).
fof(f593,definition,
( spl0_94
<=> c0_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f595,plain,
( ~ c0_1(a225)
| spl0_94 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f596,plain,
( ~ spl0_36
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f75,f593,f298]) ).
fof(f603,definition,
( spl0_96
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f607,definition,
( spl0_97
<=> c3_1(a257) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f609,plain,
( ~ c3_1(a257)
| spl0_97 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,plain,
( ~ spl0_96
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f73,f607,f603]) ).
fof(f612,definition,
( spl0_98
<=> c1_1(a257) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f615,plain,
( ~ spl0_96
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f72,f612,f603]) ).
fof(f631,definition,
( spl0_102
<=> c2_1(a190) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f633,plain,
( c2_1(a190)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f634,plain,
( spl0_102
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f69,f309,f631]) ).
fof(f636,definition,
( spl0_103
<=> c0_1(a190) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f638,plain,
( c0_1(a190)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f639,plain,
( spl0_103
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f68,f309,f636]) ).
fof(f656,definition,
( spl0_107
<=> c0_1(a194) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f658,plain,
( c0_1(a194)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f659,plain,
( spl0_107
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f64,f331,f656]) ).
fof(f661,definition,
( spl0_108
<=> c0_1(a195) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f663,plain,
( c0_1(a195)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f664,plain,
( spl0_108
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f63,f247,f661]) ).
fof(f666,definition,
( spl0_109
<=> c1_1(a197) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f668,plain,
( c1_1(a197)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f669,plain,
( spl0_109
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f62,f239,f666]) ).
fof(f671,definition,
( spl0_110
<=> c3_1(a198) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f673,plain,
( c3_1(a198)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f674,plain,
( spl0_110
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f61,f381,f671]) ).
fof(f676,definition,
( spl0_111
<=> c1_1(a198) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f678,plain,
( c1_1(a198)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f679,plain,
( spl0_111
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f60,f381,f676]) ).
fof(f681,definition,
( spl0_112
<=> c2_1(a199) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f683,plain,
( c2_1(a199)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f684,plain,
( spl0_112
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f59,f275,f681]) ).
fof(f686,definition,
( spl0_113
<=> c3_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f688,plain,
( c3_1(a200)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f689,plain,
( spl0_113
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f58,f326,f686]) ).
fof(f691,definition,
( spl0_114
<=> c0_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f693,plain,
( c0_1(a200)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f694,plain,
( spl0_114
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f57,f326,f691]) ).
fof(f696,definition,
( spl0_115
<=> c0_1(a202) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f698,plain,
( c0_1(a202)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f699,plain,
( spl0_115
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f56,f401,f696]) ).
fof(f701,definition,
( spl0_116
<=> c3_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f703,plain,
( c3_1(a209)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f704,plain,
( spl0_116
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f55,f267,f701]) ).
fof(f706,definition,
( spl0_117
<=> c1_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f708,plain,
( c1_1(a209)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f709,plain,
( spl0_117
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f54,f267,f706]) ).
fof(f721,definition,
( spl0_120
<=> c2_1(a214) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f723,plain,
( c2_1(a214)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f724,plain,
( spl0_120
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f51,f341,f721]) ).
fof(f726,definition,
( spl0_121
<=> c2_1(a222) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f728,plain,
( c2_1(a222)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f729,plain,
( spl0_121
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f50,f395,f726]) ).
fof(f731,definition,
( spl0_122
<=> c1_1(a222) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f733,plain,
( c1_1(a222)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f734,plain,
( spl0_122
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f49,f395,f731]) ).
fof(f736,definition,
( spl0_123
<=> c3_1(a223) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f738,plain,
( c3_1(a223)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f739,plain,
( spl0_123
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f48,f391,f736]) ).
fof(f741,definition,
( spl0_124
<=> c3_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f743,plain,
( c3_1(a225)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f744,plain,
( spl0_124
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f47,f298,f741]) ).
fof(f756,definition,
( spl0_127
<=> c2_1(a257) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f758,plain,
( c2_1(a257)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f759,plain,
( spl0_127
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f44,f603,f756]) ).
fof(f766,definition,
( spl0_129
<=> c3_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f768,plain,
( c3_1(a189)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f769,plain,
( spl0_129
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f42,f349,f766]) ).
fof(f771,definition,
( spl0_130
<=> c1_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f773,plain,
( c1_1(a189)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f774,plain,
( spl0_130
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f41,f349,f771]) ).
fof(f776,definition,
( spl0_131
<=> c0_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f778,plain,
( c0_1(a189)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f779,plain,
( spl0_131
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f40,f349,f776]) ).
fof(f781,definition,
( spl0_132
<=> c3_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f783,plain,
( c3_1(a215)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f784,plain,
( spl0_132
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f39,f303,f781]) ).
fof(f786,definition,
( spl0_133
<=> c2_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f788,plain,
( c2_1(a215)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f789,plain,
( spl0_133
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f38,f303,f786]) ).
fof(f791,definition,
( spl0_134
<=> c1_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f793,plain,
( c1_1(a215)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f794,plain,
( spl0_134
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f37,f303,f791]) ).
fof(f796,definition,
( spl0_135
<=> c2_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f798,plain,
( c2_1(a230)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f799,plain,
( spl0_135
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f36,f376,f796]) ).
fof(f801,definition,
( spl0_136
<=> c1_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f803,plain,
( c1_1(a230)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f801]) ).
fof(f804,plain,
( spl0_136
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f35,f376,f801]) ).
fof(f806,definition,
( spl0_137
<=> c0_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f808,plain,
( c0_1(a230)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,plain,
( spl0_137
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f34,f376,f806]) ).
fof(f813,plain,
( spl0_96
| spl0_44
| spl0_42 ),
inference(avatar_split_clause,[],[f30,f331,f341,f603]) ).
fof(f815,plain,
( spl0_39
| spl0_31
| spl0_46 ),
inference(avatar_split_clause,[],[f28,f349,f275,f315]) ).
fof(f816,plain,
( spl0_39
| spl0_44
| spl0_51 ),
inference(avatar_split_clause,[],[f27,f376,f341,f315]) ).
fof(f819,plain,
( spl0_3
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f24,f315,f171]) ).
fof(f832,plain,
( spl0_3
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f11,f341,f171]) ).
fof(f842,plain,
( spl0_3
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f1,f376,f171]) ).
fof(f843,plain,
( c3_1(a194)
| c2_1(a194)
| ~ spl0_5
| ~ spl0_107 ),
inference(resolution,[],[f180,f658]) ).
fof(f844,plain,
( c3_1(a194)
| ~ spl0_5
| spl0_68
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f843,f465]) ).
fof(f846,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1) )
| ~ spl0_5
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f190,f180]) ).
fof(f847,plain,
( c2_1(a194)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_107 ),
inference(resolution,[],[f846,f658]) ).
fof(f850,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f193,f169]) ).
fof(f863,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f218,f169]) ).
fof(f864,plain,
( c3_1(a222)
| c0_1(a222)
| ~ spl0_13
| ~ spl0_121 ),
inference(resolution,[],[f208,f728]) ).
fof(f865,plain,
( c0_1(a222)
| ~ spl0_13
| spl0_90
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f864,f575]) ).
fof(f875,plain,
( ~ c0_1(a194)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_16
| spl0_68
| ~ spl0_107 ),
inference(resolution,[],[f844,f863]) ).
fof(f877,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| ~ spl0_16
| spl0_68
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f875,f658]) ).
fof(f878,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_16
| spl0_68
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f877]) ).
fof(f880,plain,
( ~ c0_1(a215)
| ~ c1_1(a215)
| ~ spl0_2
| ~ spl0_132 ),
inference(resolution,[],[f783,f169]) ).
fof(f882,definition,
( spl0_138
<=> c0_1(a215) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f894,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f215,f850]) ).
fof(f897,plain,
( ~ c1_1(a215)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_15
| ~ spl0_133 ),
inference(resolution,[],[f894,f788]) ).
fof(f898,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f897,f793]) ).
fof(f899,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f898]) ).
fof(f903,plain,
( ~ c0_1(a215)
| ~ c2_1(a215)
| ~ spl0_4
| ~ spl0_132 ),
inference(resolution,[],[f176,f783]) ).
fof(f908,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f225,f176]) ).
fof(f912,plain,
( ~ c0_1(a222)
| ~ spl0_4
| ~ spl0_18
| ~ spl0_121 ),
inference(resolution,[],[f908,f728]) ).
fof(f927,plain,
( c3_1(a190)
| c1_1(a190)
| ~ spl0_17
| ~ spl0_102 ),
inference(resolution,[],[f633,f222]) ).
fof(f928,plain,
( c1_1(a190)
| ~ spl0_17
| spl0_61
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f927,f430]) ).
fof(f932,plain,
( c1_1(a199)
| c0_1(a199)
| ~ spl0_19
| ~ spl0_112 ),
inference(resolution,[],[f229,f683]) ).
fof(f934,plain,
( c0_1(a199)
| ~ spl0_19
| spl0_75
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f932,f500]) ).
fof(f935,plain,
( $false
| ~ spl0_19
| spl0_75
| spl0_76
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f934,f505]) ).
fof(f936,plain,
( ~ spl0_19
| spl0_75
| spl0_76
| ~ spl0_112 ),
inference(avatar_contradiction_clause,[],[f935]) ).
fof(f937,plain,
( c3_1(a202)
| c2_1(a202)
| ~ spl0_5
| ~ spl0_115 ),
inference(resolution,[],[f698,f180]) ).
fof(f938,plain,
( c2_1(a202)
| ~ spl0_5
| spl0_78
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f937,f515]) ).
fof(f941,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f183,f222]) ).
fof(f947,plain,
( c3_1(a214)
| c1_1(a214)
| ~ spl0_17
| ~ spl0_120 ),
inference(resolution,[],[f723,f222]) ).
fof(f948,plain,
( c1_1(a214)
| ~ spl0_17
| spl0_85
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f947,f550]) ).
fof(f953,definition,
( spl0_139
<=> c3_1(a230) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f955,plain,
( c3_1(a230)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f960,plain,
( ~ c0_1(a230)
| ~ spl0_4
| ~ spl0_18
| ~ spl0_135 ),
inference(resolution,[],[f908,f798]) ).
fof(f964,plain,
( ~ c0_1(a190)
| ~ spl0_4
| ~ spl0_18
| ~ spl0_102 ),
inference(resolution,[],[f908,f633]) ).
fof(f969,plain,
( $false
| ~ spl0_4
| ~ spl0_18
| ~ spl0_135
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f960,f808]) ).
fof(f970,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_135
| ~ spl0_137 ),
inference(avatar_contradiction_clause,[],[f969]) ).
fof(f975,plain,
( c3_1(a190)
| ~ spl0_6
| ~ spl0_17
| ~ spl0_102 ),
inference(resolution,[],[f941,f633]) ).
fof(f976,plain,
( $false
| ~ spl0_6
| ~ spl0_17
| spl0_61
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f975,f430]) ).
fof(f977,plain,
( ~ spl0_6
| ~ spl0_17
| spl0_61
| ~ spl0_102 ),
inference(avatar_contradiction_clause,[],[f976]) ).
fof(f988,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f193,f166]) ).
fof(f995,plain,
( c3_1(a190)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_103 ),
inference(resolution,[],[f988,f638]) ).
fof(f996,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| spl0_61
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f995,f430]) ).
fof(f997,plain,
( ~ spl0_1
| ~ spl0_9
| spl0_61
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f996]) ).
fof(f1004,plain,
( c2_1(a223)
| c0_1(a223)
| ~ spl0_14
| ~ spl0_123 ),
inference(resolution,[],[f738,f212]) ).
fof(f1005,plain,
( c0_1(a223)
| ~ spl0_14
| spl0_91
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f1004,f580]) ).
fof(f1006,plain,
( c3_1(a230)
| ~ c0_1(a230)
| ~ spl0_9
| ~ spl0_136 ),
inference(resolution,[],[f193,f803]) ).
fof(f1008,plain,
( c3_1(a222)
| ~ c0_1(a222)
| ~ spl0_9
| ~ spl0_122 ),
inference(resolution,[],[f193,f733]) ).
fof(f1012,plain,
( c3_1(a190)
| ~ c0_1(a190)
| ~ spl0_9
| ~ spl0_17
| spl0_61
| ~ spl0_102 ),
inference(resolution,[],[f193,f928]) ).
fof(f1013,plain,
( ~ c0_1(a190)
| ~ spl0_9
| ~ spl0_17
| spl0_61
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f1012,f430]) ).
fof(f1015,plain,
( ~ c0_1(a222)
| ~ spl0_9
| spl0_90
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f1008,f575]) ).
fof(f1017,plain,
( $false
| ~ spl0_9
| ~ spl0_17
| spl0_61
| ~ spl0_102
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f1013,f638]) ).
fof(f1018,plain,
( ~ spl0_9
| ~ spl0_17
| spl0_61
| ~ spl0_102
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f1017]) ).
fof(f1021,plain,
( $false
| ~ spl0_9
| ~ spl0_13
| spl0_90
| ~ spl0_121
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f1015,f865]) ).
fof(f1022,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_90
| ~ spl0_121
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f1021]) ).
fof(f1024,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2) )
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f187,f222]) ).
fof(f1054,plain,
( c1_1(a257)
| ~ spl0_7
| ~ spl0_17
| ~ spl0_127 ),
inference(resolution,[],[f758,f1024]) ).
fof(f1056,plain,
( c3_1(a257)
| c1_1(a257)
| ~ spl0_17
| ~ spl0_127 ),
inference(resolution,[],[f758,f222]) ).
fof(f1057,plain,
( c1_1(a257)
| ~ spl0_17
| spl0_97
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f1056,f609]) ).
fof(f1071,plain,
( c1_1(a225)
| ~ c2_1(a225)
| ~ spl0_7
| ~ spl0_124 ),
inference(resolution,[],[f187,f743]) ).
fof(f1076,definition,
( spl0_140
<=> c1_1(a214) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1078,plain,
( c1_1(a214)
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f1076]) ).
fof(f1080,plain,
( ~ c2_1(a225)
| ~ spl0_7
| spl0_93
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f1071,f590]) ).
fof(f1083,plain,
( c2_1(a223)
| c1_1(a223)
| ~ spl0_12
| ~ spl0_14
| spl0_91
| ~ spl0_123 ),
inference(resolution,[],[f204,f1005]) ).
fof(f1085,plain,
( c2_1(a194)
| c1_1(a194)
| ~ spl0_12
| ~ spl0_107 ),
inference(resolution,[],[f204,f658]) ).
fof(f1089,plain,
( c1_1(a223)
| ~ spl0_12
| ~ spl0_14
| spl0_91
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f1083,f580]) ).
fof(f1094,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_13
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f225,f208]) ).
fof(f1101,plain,
( c3_1(a222)
| ~ spl0_13
| ~ spl0_18
| ~ spl0_121 ),
inference(resolution,[],[f1094,f728]) ).
fof(f1108,plain,
( $false
| ~ spl0_13
| ~ spl0_18
| spl0_90
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f1101,f575]) ).
fof(f1109,plain,
( ~ spl0_13
| ~ spl0_18
| spl0_90
| ~ spl0_121 ),
inference(avatar_contradiction_clause,[],[f1108]) ).
fof(f1119,plain,
( c2_1(a225)
| c0_1(a225)
| ~ spl0_14
| ~ spl0_124 ),
inference(resolution,[],[f212,f743]) ).
fof(f1124,plain,
( c2_1(a225)
| ~ spl0_14
| spl0_94
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f1119,f595]) ).
fof(f1128,plain,
( c3_1(a214)
| c0_1(a214)
| ~ spl0_13
| ~ spl0_120 ),
inference(resolution,[],[f723,f208]) ).
fof(f1131,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_7
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f236,f187]) ).
fof(f1136,plain,
( c1_1(a194)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_21
| spl0_68
| ~ spl0_107 ),
inference(resolution,[],[f1131,f844]) ).
fof(f1137,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_21
| spl0_68
| spl0_69
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f1136,f470]) ).
fof(f1138,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_21
| spl0_68
| spl0_69
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f1137]) ).
fof(f1148,definition,
( spl0_141
<=> c2_1(a209) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1149,plain,
( c2_1(a209)
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f1148]) ).
fof(f1168,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_14
| ~ spl0_26 ),
inference(resolution,[],[f256,f212]) ).
fof(f1178,plain,
( c1_1(a206)
| c2_1(a206)
| ~ spl0_26
| spl0_80 ),
inference(resolution,[],[f256,f525]) ).
fof(f1179,plain,
( c1_1(a191)
| c2_1(a191)
| ~ spl0_26
| spl0_62 ),
inference(resolution,[],[f256,f435]) ).
fof(f1182,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_14
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f1168]) ).
fof(f1184,plain,
( c2_1(a191)
| ~ spl0_26
| spl0_62
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f1179,f445]) ).
fof(f1185,plain,
( c1_1(a206)
| ~ spl0_26
| spl0_80
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f1178,f530]) ).
fof(f1190,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f232,f169]) ).
fof(f1191,plain,
( $false
| ~ spl0_7
| ~ spl0_14
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f1124,f1080]) ).
fof(f1192,plain,
( ~ spl0_7
| ~ spl0_14
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1195,definition,
( spl0_142
<=> c0_1(a222) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1210,definition,
( spl0_143
<=> c2_1(a200) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1235,plain,
( c1_1(a225)
| c0_1(a225)
| ~ spl0_14
| ~ spl0_19
| spl0_94
| ~ spl0_124 ),
inference(resolution,[],[f1124,f229]) ).
fof(f1236,plain,
( c0_1(a225)
| ~ spl0_14
| ~ spl0_19
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f1235,f590]) ).
fof(f1237,plain,
( $false
| ~ spl0_14
| ~ spl0_19
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f1236,f595]) ).
fof(f1238,plain,
( ~ spl0_14
| ~ spl0_19
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(avatar_contradiction_clause,[],[f1237]) ).
fof(f1253,plain,
( ~ spl0_142
| ~ spl0_4
| ~ spl0_18
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f912,f726,f224,f175,f1195]) ).
fof(f1254,plain,
( ~ spl0_103
| ~ spl0_4
| ~ spl0_18
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f964,f631,f224,f175,f636]) ).
fof(f1256,definition,
( spl0_145
<=> c1_1(a190) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1328,plain,
( ! [X2] :
( c1_1(X2)
| c0_1(X2) )
| ~ spl0_19
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f253,f229]) ).
fof(f1419,plain,
( spl0_86
| spl0_85
| ~ spl0_13
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1128,f721,f207,f548,f553]) ).
fof(f1445,plain,
( ! [X0] : ~ c0_1(X0)
| ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f988,f863]) ).
fof(f1450,definition,
( spl0_147
<=> c0_1(a223) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1460,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_86 ),
inference(resolution,[],[f1445,f554]) ).
fof(f1461,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_107 ),
inference(resolution,[],[f1445,f658]) ).
fof(f1462,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f1461]) ).
fof(f1463,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_86 ),
inference(avatar_contradiction_clause,[],[f1460]) ).
fof(f1486,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f808,f1445]) ).
fof(f1487,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_137 ),
inference(avatar_contradiction_clause,[],[f1486]) ).
fof(f1501,plain,
( spl0_92
| ~ spl0_12
| ~ spl0_14
| spl0_91
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1089,f736,f578,f211,f203,f583]) ).
fof(f1506,plain,
( spl0_25
| ~ spl0_14
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1182,f255,f211,f252]) ).
fof(f1519,plain,
( ~ spl0_137
| spl0_139
| ~ spl0_9
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1006,f801,f192,f953,f806]) ).
fof(f1552,plain,
( ~ c0_1(a230)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_136 ),
inference(resolution,[],[f803,f850]) ).
fof(f1553,plain,
( ~ spl0_137
| ~ spl0_2
| ~ spl0_9
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1552,f801,f192,f168,f806]) ).
fof(f1571,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1) )
| ~ spl0_2
| ~ spl0_9
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f336,f850]) ).
fof(f1575,plain,
( ~ c0_1(a189)
| ~ c1_1(a189)
| ~ spl0_2
| ~ spl0_129 ),
inference(resolution,[],[f768,f169]) ).
fof(f1576,plain,
( ~ c0_1(a189)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_130 ),
inference(resolution,[],[f773,f850]) ).
fof(f1577,plain,
( ~ spl0_131
| ~ spl0_2
| ~ spl0_9
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1576,f771,f192,f168,f776]) ).
fof(f1671,plain,
( ! [X2] :
( ~ c3_1(X2)
| c2_1(X2) )
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f212,f863]) ).
fof(f1673,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_2
| ~ spl0_16
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f244,f863]) ).
fof(f1683,plain,
( ! [X1] : ~ c3_1(X1)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1673,f1671]) ).
fof(f1697,plain,
( ! [X1] :
( c1_1(X1)
| c0_1(X1) )
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16
| ~ spl0_23
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f354,f1683]) ).
fof(f1717,plain,
( c0_1(a221)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16
| ~ spl0_23
| ~ spl0_47
| spl0_88 ),
inference(resolution,[],[f1697,f565]) ).
fof(f1722,plain,
( $false
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16
| ~ spl0_23
| ~ spl0_47
| spl0_88
| spl0_89 ),
inference(forward_subsumption_resolution,[],[f1717,f570]) ).
fof(f1723,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_16
| ~ spl0_23
| ~ spl0_47
| spl0_88
| spl0_89 ),
inference(avatar_contradiction_clause,[],[f1722]) ).
fof(f1756,plain,
( spl0_79
| ~ spl0_5
| spl0_78
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f938,f696,f513,f179,f518]) ).
fof(f1795,plain,
( spl0_63
| ~ spl0_26
| spl0_62
| spl0_64 ),
inference(avatar_split_clause,[],[f1184,f443,f433,f255,f438]) ).
fof(f1824,plain,
( c3_1(a222)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_43
| ~ spl0_122 ),
inference(resolution,[],[f733,f1571]) ).
fof(f1829,plain,
( spl0_90
| ~ spl0_2
| ~ spl0_9
| ~ spl0_43
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1824,f731,f335,f192,f168,f573]) ).
fof(f2192,plain,
( c0_1(a221)
| ~ spl0_19
| ~ spl0_25
| spl0_88 ),
inference(resolution,[],[f1328,f565]) ).
fof(f2194,plain,
( c0_1(a188)
| ~ spl0_19
| ~ spl0_25
| spl0_59 ),
inference(resolution,[],[f1328,f420]) ).
fof(f2195,plain,
( $false
| ~ spl0_19
| ~ spl0_25
| spl0_59
| spl0_60 ),
inference(forward_subsumption_resolution,[],[f2194,f425]) ).
fof(f2196,plain,
( ~ spl0_19
| ~ spl0_25
| spl0_59
| spl0_60 ),
inference(avatar_contradiction_clause,[],[f2195]) ).
fof(f2229,plain,
( ! [X2] :
( ~ c3_1(X2)
| c2_1(X2) )
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f212,f190]) ).
fof(f2234,plain,
( c2_1(a200)
| ~ spl0_8
| ~ spl0_14
| ~ spl0_113 ),
inference(resolution,[],[f2229,f688]) ).
fof(f2255,plain,
( c3_1(a190)
| ~ c0_1(a190)
| ~ spl0_18
| ~ spl0_102 ),
inference(resolution,[],[f225,f633]) ).
fof(f2266,plain,
( c3_1(a190)
| ~ spl0_18
| ~ spl0_102
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f2255,f638]) ).
fof(f2267,plain,
( spl0_61
| ~ spl0_18
| ~ spl0_102
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f2266,f636,f631,f224,f428]) ).
fof(f2299,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_8
| ~ spl0_14
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f244,f2229]) ).
fof(f2387,plain,
( ! [X1] :
( c1_1(X1)
| c0_1(X1) )
| ~ spl0_40
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f354,f321]) ).
fof(f2397,plain,
( c0_1(a199)
| ~ spl0_40
| ~ spl0_47
| spl0_75 ),
inference(resolution,[],[f2387,f500]) ).
fof(f2404,plain,
( c0_1(a221)
| ~ spl0_40
| ~ spl0_47
| spl0_88 ),
inference(resolution,[],[f2387,f565]) ).
fof(f2409,plain,
( $false
| ~ spl0_40
| ~ spl0_47
| spl0_88
| spl0_89 ),
inference(forward_subsumption_resolution,[],[f2404,f570]) ).
fof(f2410,plain,
( ~ spl0_40
| ~ spl0_47
| spl0_88
| spl0_89 ),
inference(avatar_contradiction_clause,[],[f2409]) ).
fof(f2415,plain,
( $false
| ~ spl0_40
| ~ spl0_47
| spl0_75
| spl0_76 ),
inference(forward_subsumption_resolution,[],[f2397,f505]) ).
fof(f2416,plain,
( ~ spl0_40
| ~ spl0_47
| spl0_75
| spl0_76 ),
inference(avatar_contradiction_clause,[],[f2415]) ).
fof(f2427,plain,
( c0_1(a214)
| c1_1(a214)
| ~ spl0_47
| spl0_85 ),
inference(resolution,[],[f354,f550]) ).
fof(f2434,plain,
( c0_1(a191)
| c1_1(a191)
| ~ spl0_47
| spl0_62 ),
inference(resolution,[],[f354,f435]) ).
fof(f2435,plain,
( c0_1(a188)
| c1_1(a188)
| ~ spl0_47
| spl0_58 ),
inference(resolution,[],[f354,f415]) ).
fof(f2437,plain,
( c0_1(a191)
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f2434,f445]) ).
fof(f2452,plain,
( spl0_98
| ~ spl0_7
| ~ spl0_17
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1054,f756,f221,f186,f612]) ).
fof(f2459,plain,
( ! [X1] :
( c3_1(X1)
| c0_1(X1) )
| ~ spl0_43
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f336,f354]) ).
fof(f2467,plain,
( c0_1(a188)
| ~ spl0_47
| spl0_58
| spl0_59 ),
inference(forward_subsumption_resolution,[],[f2435,f420]) ).
fof(f2471,plain,
( spl0_60
| ~ spl0_47
| spl0_58
| spl0_59 ),
inference(avatar_split_clause,[],[f2467,f418,f413,f353,f423]) ).
fof(f2486,plain,
( c1_1(a199)
| ~ spl0_7
| ~ spl0_17
| ~ spl0_112 ),
inference(resolution,[],[f1024,f683]) ).
fof(f2492,plain,
( $false
| ~ spl0_7
| ~ spl0_17
| spl0_75
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f2486,f500]) ).
fof(f2493,plain,
( ~ spl0_7
| ~ spl0_17
| spl0_75
| ~ spl0_112 ),
inference(avatar_contradiction_clause,[],[f2492]) ).
fof(f2498,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c1_1(X0) )
| ~ spl0_8
| ~ spl0_14
| ~ spl0_47 ),
inference(resolution,[],[f2229,f354]) ).
fof(f2507,plain,
( spl0_25
| ~ spl0_8
| ~ spl0_14
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f2498,f353,f211,f189,f252]) ).
fof(f2511,plain,
( c0_1(a222)
| ~ spl0_43
| ~ spl0_47
| spl0_90 ),
inference(resolution,[],[f2459,f575]) ).
fof(f2512,plain,
( c0_1(a214)
| ~ spl0_43
| ~ spl0_47
| spl0_85 ),
inference(resolution,[],[f2459,f550]) ).
fof(f2540,plain,
( spl0_142
| ~ spl0_43
| ~ spl0_47
| spl0_90 ),
inference(avatar_split_clause,[],[f2511,f573,f353,f335,f1195]) ).
fof(f2541,plain,
( spl0_86
| ~ spl0_43
| ~ spl0_47
| spl0_85 ),
inference(avatar_split_clause,[],[f2512,f548,f353,f335,f553]) ).
fof(f2543,definition,
( spl0_154
<=> c1_1(a206) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f2545,plain,
( c1_1(a206)
| ~ spl0_154 ),
inference(avatar_component_clause,[],[f2543]) ).
fof(f2553,plain,
( spl0_68
| ~ spl0_5
| ~ spl0_8
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f847,f656,f189,f179,f463]) ).
fof(f2569,plain,
( ~ spl0_130
| ~ spl0_131
| ~ spl0_2
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1575,f766,f168,f776,f771]) ).
fof(f2630,definition,
( spl0_156
<=> c2_1(a225) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f2633,plain,
( ~ spl0_156
| spl0_93
| ~ spl0_7
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1071,f741,f186,f588,f2630]) ).
fof(f2641,plain,
( spl0_98
| ~ spl0_17
| spl0_97
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1057,f756,f607,f221,f612]) ).
fof(f2690,plain,
( ~ c0_1(a215)
| ~ spl0_2
| ~ spl0_132
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f880,f793]) ).
fof(f2691,plain,
( ~ c0_1(a215)
| ~ spl0_4
| ~ spl0_132
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f903,f788]) ).
fof(f2702,plain,
( ~ spl0_138
| ~ spl0_2
| ~ spl0_132
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f2690,f791,f781,f168,f882]) ).
fof(f2703,plain,
( ~ spl0_138
| ~ spl0_4
| ~ spl0_132
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f2691,f786,f781,f175,f882]) ).
fof(f2731,plain,
( spl0_156
| ~ spl0_14
| spl0_94
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1124,f741,f593,f211,f2630]) ).
fof(f2732,plain,
( ~ c1_1(a215)
| ~ spl0_2
| ~ spl0_20
| ~ spl0_132 ),
inference(resolution,[],[f1190,f783]) ).
fof(f2746,plain,
( $false
| ~ spl0_2
| ~ spl0_20
| ~ spl0_132
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2732,f793]) ).
fof(f2747,plain,
( ~ spl0_2
| ~ spl0_20
| ~ spl0_132
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2746]) ).
fof(f2750,plain,
( spl0_89
| ~ spl0_19
| ~ spl0_25
| spl0_88 ),
inference(avatar_split_clause,[],[f2192,f563,f252,f228,f568]) ).
fof(f2793,plain,
( c3_1(a195)
| c1_1(a195)
| ~ spl0_1
| ~ spl0_108 ),
inference(resolution,[],[f166,f663]) ).
fof(f2797,plain,
( c3_1(a190)
| c1_1(a190)
| ~ spl0_1
| ~ spl0_103 ),
inference(resolution,[],[f166,f638]) ).
fof(f2815,plain,
( ~ c0_1(a200)
| ~ c2_1(a200)
| ~ spl0_4
| ~ spl0_113 ),
inference(resolution,[],[f176,f688]) ).
fof(f2929,plain,
( c2_1(a189)
| ~ c0_1(a189)
| ~ spl0_28
| ~ spl0_130 ),
inference(resolution,[],[f264,f773]) ).
fof(f2945,plain,
( c2_1(a189)
| ~ spl0_28
| ~ spl0_130
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f2929,f778]) ).
fof(f2977,plain,
( c2_1(a198)
| ~ c1_1(a198)
| ~ spl0_34
| ~ spl0_110 ),
inference(resolution,[],[f291,f673]) ).
fof(f3034,plain,
( c2_1(a197)
| c0_1(a197)
| ~ spl0_35
| ~ spl0_109 ),
inference(resolution,[],[f295,f668]) ).
fof(f3039,plain,
( c2_1(a206)
| c0_1(a206)
| ~ spl0_35
| ~ spl0_154 ),
inference(resolution,[],[f295,f2545]) ).
fof(f3040,plain,
( c0_1(a206)
| ~ spl0_35
| spl0_81
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f3039,f530]) ).
fof(f3042,plain,
( c0_1(a197)
| ~ spl0_35
| spl0_72
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f3034,f485]) ).
fof(f3045,plain,
( $false
| ~ spl0_35
| spl0_81
| spl0_82
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f3040,f535]) ).
fof(f3046,plain,
( ~ spl0_35
| spl0_81
| spl0_82
| ~ spl0_154 ),
inference(avatar_contradiction_clause,[],[f3045]) ).
fof(f3049,plain,
( $false
| ~ spl0_35
| spl0_72
| spl0_73
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f3042,f490]) ).
fof(f3050,plain,
( ~ spl0_35
| spl0_72
| spl0_73
| ~ spl0_109 ),
inference(avatar_contradiction_clause,[],[f3049]) ).
fof(f3064,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0) )
| ~ spl0_21
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f236,f291]) ).
fof(f3083,plain,
( ~ c2_1(a200)
| ~ spl0_4
| ~ spl0_113
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2815,f693]) ).
fof(f3085,plain,
( spl0_143
| ~ spl0_8
| ~ spl0_14
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f2234,f686,f211,f189,f1210]) ).
fof(f3086,plain,
( spl0_69
| spl0_68
| ~ spl0_12
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f1085,f656,f203,f463,f468]) ).
fof(f3087,plain,
( ~ spl0_143
| ~ spl0_4
| ~ spl0_113
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f3083,f691,f686,f175,f1210]) ).
fof(f3134,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1) )
| ~ spl0_1
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f354,f166]) ).
fof(f3150,plain,
( c2_1(a198)
| ~ spl0_34
| ~ spl0_110
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f2977,f678]) ).
fof(f3160,plain,
( spl0_74
| ~ spl0_34
| ~ spl0_110
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f3150,f676,f671,f290,f493]) ).
fof(f3200,plain,
( spl0_145
| spl0_61
| ~ spl0_1
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f2797,f636,f165,f428,f1256]) ).
fof(f3343,definition,
( spl0_158
<=> c2_1(a189) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f3350,plain,
( c1_1(a191)
| ~ spl0_1
| ~ spl0_47
| spl0_62 ),
inference(resolution,[],[f3134,f435]) ).
fof(f3351,plain,
( $false
| ~ spl0_1
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f3350,f445]) ).
fof(f3352,plain,
( ~ spl0_1
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(avatar_contradiction_clause,[],[f3351]) ).
fof(f3366,plain,
( ! [X2] :
( ~ c0_1(X2)
| c3_1(X2) )
| ~ spl0_4
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f180,f908]) ).
fof(f3382,plain,
( c3_1(a222)
| ~ c1_1(a222)
| ~ spl0_6
| ~ spl0_121 ),
inference(resolution,[],[f183,f728]) ).
fof(f3393,plain,
( c3_1(a191)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_18
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(resolution,[],[f2437,f3366]) ).
fof(f3394,plain,
( $false
| ~ spl0_4
| ~ spl0_5
| ~ spl0_18
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f3393,f435]) ).
fof(f3395,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_18
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(avatar_contradiction_clause,[],[f3394]) ).
fof(f3414,plain,
( c2_1(a223)
| c0_1(a223)
| ~ spl0_14
| ~ spl0_123 ),
inference(resolution,[],[f212,f738]) ).
fof(f3418,plain,
( c2_1(a209)
| c0_1(a209)
| ~ spl0_14
| ~ spl0_116 ),
inference(resolution,[],[f212,f703]) ).
fof(f3428,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_4
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f215,f908]) ).
fof(f3453,plain,
( c2_1(a189)
| ~ spl0_21
| ~ spl0_34
| ~ spl0_129 ),
inference(resolution,[],[f3064,f768]) ).
fof(f3456,plain,
( c2_1(a223)
| ~ spl0_21
| ~ spl0_34
| ~ spl0_123 ),
inference(resolution,[],[f3064,f738]) ).
fof(f3485,plain,
( spl0_158
| ~ spl0_21
| ~ spl0_34
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f3453,f766,f290,f235,f3343]) ).
fof(f3494,plain,
( spl0_147
| spl0_91
| ~ spl0_14
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f3414,f736,f211,f578,f1450]) ).
fof(f3498,plain,
( spl0_91
| ~ spl0_21
| ~ spl0_34
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f3456,f736,f290,f235,f578]) ).
fof(f3499,plain,
( ~ spl0_122
| spl0_90
| ~ spl0_6
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f3382,f726,f182,f573,f731]) ).
fof(f3519,plain,
( spl0_83
| spl0_141
| ~ spl0_14
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f3418,f701,f211,f1148,f538]) ).
fof(f3541,plain,
( ~ c1_1(a214)
| ~ spl0_4
| ~ spl0_15
| ~ spl0_18
| ~ spl0_120 ),
inference(resolution,[],[f3428,f723]) ).
fof(f3550,plain,
( ~ spl0_140
| ~ spl0_4
| ~ spl0_15
| ~ spl0_18
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f3541,f721,f224,f214,f175,f1076]) ).
fof(f3554,plain,
( c1_1(a223)
| ~ c0_1(a223)
| ~ spl0_16
| ~ spl0_123 ),
inference(resolution,[],[f218,f738]) ).
fof(f3559,plain,
( c1_1(a200)
| ~ c0_1(a200)
| ~ spl0_16
| ~ spl0_113 ),
inference(resolution,[],[f218,f688]) ).
fof(f3564,plain,
( ~ c0_1(a200)
| ~ spl0_16
| spl0_77
| ~ spl0_113 ),
inference(forward_subsumption_resolution,[],[f3559,f510]) ).
fof(f3566,plain,
( ~ c0_1(a223)
| ~ spl0_16
| spl0_92
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f3554,f585]) ).
fof(f3567,plain,
( $false
| ~ spl0_16
| spl0_77
| ~ spl0_113
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f3564,f693]) ).
fof(f3568,plain,
( ~ spl0_16
| spl0_77
| ~ spl0_113
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f3567]) ).
fof(f3570,plain,
( ~ spl0_147
| ~ spl0_16
| spl0_92
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f3566,f736,f583,f217,f1450]) ).
fof(f3594,plain,
( c1_1(a214)
| ~ spl0_47
| spl0_85
| spl0_86 ),
inference(forward_subsumption_resolution,[],[f2427,f555]) ).
fof(f3599,plain,
( spl0_140
| ~ spl0_47
| spl0_85
| spl0_86 ),
inference(avatar_split_clause,[],[f3594,f553,f548,f353,f1076]) ).
fof(f3604,plain,
( ~ c0_1(a189)
| ~ c2_1(a189)
| ~ spl0_4
| ~ spl0_129 ),
inference(resolution,[],[f176,f768]) ).
fof(f3617,plain,
( ~ c2_1(a189)
| ~ spl0_4
| ~ spl0_129
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f3604,f778]) ).
fof(f3618,plain,
( ~ spl0_158
| ~ spl0_4
| ~ spl0_129
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f3617,f776,f766,f175,f3343]) ).
fof(f3626,plain,
( c3_1(a191)
| c2_1(a191)
| ~ spl0_5
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(resolution,[],[f180,f2437]) ).
fof(f3627,plain,
( c2_1(a191)
| ~ spl0_5
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f3626,f435]) ).
fof(f3631,plain,
( spl0_63
| ~ spl0_5
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(avatar_split_clause,[],[f3627,f443,f433,f353,f179,f438]) ).
fof(f3633,plain,
( ~ c0_1(a215)
| ~ c1_1(a215)
| ~ spl0_11
| ~ spl0_133 ),
inference(resolution,[],[f200,f788]) ).
fof(f3640,plain,
( ~ c0_1(a190)
| ~ c1_1(a190)
| ~ spl0_11
| ~ spl0_102 ),
inference(resolution,[],[f200,f633]) ).
fof(f3642,plain,
( ~ c1_1(a190)
| ~ spl0_11
| ~ spl0_102
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f3640,f638]) ).
fof(f3643,plain,
( ~ spl0_145
| ~ spl0_11
| ~ spl0_102
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f3642,f636,f631,f199,f1256]) ).
fof(f3661,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_11
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f215,f200]) ).
fof(f3663,plain,
( ~ c1_1(a215)
| ~ spl0_11
| ~ spl0_15
| ~ spl0_133 ),
inference(resolution,[],[f3661,f788]) ).
fof(f3665,plain,
( ~ c1_1(a214)
| ~ spl0_11
| ~ spl0_15
| ~ spl0_120 ),
inference(resolution,[],[f3661,f723]) ).
fof(f3675,plain,
( $false
| ~ spl0_11
| ~ spl0_15
| ~ spl0_120
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f3665,f1078]) ).
fof(f3676,plain,
( ~ spl0_11
| ~ spl0_15
| ~ spl0_120
| ~ spl0_140 ),
inference(avatar_contradiction_clause,[],[f3675]) ).
fof(f3677,plain,
( $false
| ~ spl0_11
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f3663,f793]) ).
fof(f3678,plain,
( ~ spl0_11
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f3677]) ).
fof(f3681,plain,
( c0_1(a215)
| ~ c1_1(a215)
| ~ spl0_15
| ~ spl0_133 ),
inference(resolution,[],[f215,f788]) ).
fof(f3683,plain,
( c0_1(a214)
| ~ c1_1(a214)
| ~ spl0_15
| ~ spl0_120 ),
inference(resolution,[],[f215,f723]) ).
fof(f3685,plain,
( c0_1(a209)
| ~ c1_1(a209)
| ~ spl0_15
| ~ spl0_141 ),
inference(resolution,[],[f215,f1149]) ).
fof(f3692,plain,
( ~ c1_1(a214)
| ~ spl0_15
| spl0_86
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f3683,f555]) ).
fof(f3718,plain,
( spl0_158
| ~ spl0_28
| ~ spl0_130
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f2945,f776,f771,f263,f3343]) ).
fof(f3721,plain,
( ~ spl0_140
| ~ spl0_15
| spl0_86
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f3692,f721,f553,f214,f1076]) ).
fof(f3722,plain,
( c0_1(a215)
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f3681,f793]) ).
fof(f3724,plain,
( c0_1(a209)
| ~ spl0_15
| ~ spl0_117
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f3685,f708]) ).
fof(f3728,plain,
( spl0_138
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f3722,f791,f786,f214,f882]) ).
fof(f3729,plain,
( spl0_83
| ~ spl0_15
| ~ spl0_117
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f3724,f1148,f706,f214,f538]) ).
fof(f3743,plain,
( c2_1(a189)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_131 ),
inference(resolution,[],[f846,f778]) ).
fof(f3754,plain,
( spl0_158
| ~ spl0_5
| ~ spl0_8
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f3743,f776,f189,f179,f3343]) ).
fof(f3758,plain,
( c2_1(a189)
| ~ spl0_8
| ~ spl0_14
| ~ spl0_129 ),
inference(resolution,[],[f2229,f768]) ).
fof(f3768,plain,
( spl0_158
| ~ spl0_8
| ~ spl0_14
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f3758,f766,f211,f189,f3343]) ).
fof(f3775,plain,
( c0_1(a225)
| ~ spl0_8
| ~ spl0_14
| ~ spl0_23
| ~ spl0_124 ),
inference(resolution,[],[f2299,f743]) ).
fof(f3795,plain,
( spl0_154
| ~ spl0_26
| spl0_80
| spl0_81 ),
inference(avatar_split_clause,[],[f1185,f528,f523,f255,f2543]) ).
fof(f3829,plain,
( c0_1(a215)
| ~ c1_1(a215)
| ~ spl0_20
| ~ spl0_132 ),
inference(resolution,[],[f232,f783]) ).
fof(f3836,plain,
( c0_1(a209)
| ~ c1_1(a209)
| ~ spl0_20
| ~ spl0_116 ),
inference(resolution,[],[f232,f703]) ).
fof(f3897,plain,
( spl0_94
| ~ spl0_8
| ~ spl0_14
| ~ spl0_23
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f3775,f741,f243,f211,f189,f593]) ).
fof(f3910,plain,
( c1_1(a195)
| ~ spl0_1
| spl0_70
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f2793,f475]) ).
fof(f3912,plain,
( spl0_140
| ~ spl0_17
| spl0_85
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f948,f721,f548,f221,f1076]) ).
fof(f3914,plain,
( spl0_71
| ~ spl0_1
| spl0_70
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f3910,f661,f473,f165,f478]) ).
fof(f3951,plain,
( c1_1(a225)
| c0_1(a225)
| ~ spl0_40
| ~ spl0_124 ),
inference(resolution,[],[f321,f743]) ).
fof(f3959,plain,
( c0_1(a225)
| ~ spl0_40
| spl0_93
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f3951,f590]) ).
fof(f3960,plain,
( $false
| ~ spl0_40
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f3959,f595]) ).
fof(f3961,plain,
( ~ spl0_40
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(avatar_contradiction_clause,[],[f3960]) ).
fof(f3984,plain,
( ~ c0_1(a215)
| ~ spl0_11
| ~ spl0_133
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f3633,f793]) ).
fof(f3988,plain,
( c0_1(a215)
| ~ spl0_20
| ~ spl0_132
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f3829,f793]) ).
fof(f3989,plain,
( c0_1(a209)
| ~ spl0_20
| ~ spl0_116
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f3836,f708]) ).
fof(f4013,plain,
( ~ spl0_138
| ~ spl0_11
| ~ spl0_133
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f3984,f791,f786,f199,f882]) ).
fof(f4017,plain,
( spl0_138
| ~ spl0_20
| ~ spl0_132
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f3988,f791,f781,f231,f882]) ).
fof(f4018,plain,
( spl0_83
| ~ spl0_20
| ~ spl0_116
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f3989,f706,f701,f231,f538]) ).
fof(f4055,plain,
( ~ c0_1(a230)
| ~ c2_1(a230)
| ~ spl0_4
| ~ spl0_139 ),
inference(resolution,[],[f176,f955]) ).
fof(f4070,plain,
( ~ c2_1(a230)
| ~ spl0_4
| ~ spl0_137
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f4055,f808]) ).
fof(f4091,plain,
( c2_1(a200)
| c1_1(a200)
| ~ spl0_12
| ~ spl0_114 ),
inference(resolution,[],[f204,f693]) ).
fof(f4102,plain,
( c2_1(a225)
| c1_1(a225)
| ~ spl0_21
| ~ spl0_124 ),
inference(resolution,[],[f236,f743]) ).
fof(f4108,plain,
( c2_1(a225)
| ~ spl0_21
| spl0_93
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f4102,f590]) ).
fof(f4109,plain,
( spl0_156
| ~ spl0_21
| spl0_93
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f4108,f741,f588,f235,f2630]) ).
fof(f4111,plain,
( ! [X2] :
( c2_1(X2)
| c1_1(X2) )
| ~ spl0_12
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f253,f204]) ).
fof(f4116,plain,
( c1_1(a221)
| ~ spl0_12
| ~ spl0_25
| spl0_87 ),
inference(resolution,[],[f4111,f560]) ).
fof(f4119,plain,
( $false
| ~ spl0_12
| ~ spl0_25
| spl0_87
| spl0_88 ),
inference(forward_subsumption_resolution,[],[f4116,f565]) ).
fof(f4120,plain,
( ~ spl0_12
| ~ spl0_25
| spl0_87
| spl0_88 ),
inference(avatar_contradiction_clause,[],[f4119]) ).
fof(f4127,plain,
( ~ spl0_135
| ~ spl0_4
| ~ spl0_137
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f4070,f953,f806,f175,f796]) ).
fof(f4131,plain,
( c2_1(a200)
| ~ spl0_12
| spl0_77
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f4091,f510]) ).
fof(f4137,plain,
( spl0_143
| ~ spl0_12
| spl0_77
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f4131,f691,f508,f203,f1210]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f177]) ).
cnf(s2,plain,
( spl0_2
| ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f184]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f194]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_5
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f205]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_14
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f219]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_14
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f226]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_12
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f233]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_15
| spl0_19
| spl0_21 ),
inference(sat_conversion,[],[f237]) ).
cnf(s12,plain,
( ~ spl0_3
| spl0_4
| spl0_15
| spl0_24 ),
inference(sat_conversion,[],[f250]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_14
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f257]) ).
cnf(s16,plain,
( spl0_2
| ~ spl0_3
| spl0_12
| spl0_31 ),
inference(sat_conversion,[],[f278]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_9
| spl0_15
| spl0_27 ),
inference(sat_conversion,[],[f284]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_15
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f292]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_17
| spl0_18
| spl0_36 ),
inference(sat_conversion,[],[f301]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_9
| spl0_21
| spl0_29 ),
inference(sat_conversion,[],[f307]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_12
| spl0_16
| spl0_37 ),
inference(sat_conversion,[],[f313]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_12
| spl0_15
| spl0_39 ),
inference(sat_conversion,[],[f318]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_9
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f322]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_23
| spl0_26
| spl0_29 ),
inference(sat_conversion,[],[f324]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_20
| spl0_26
| spl0_41 ),
inference(sat_conversion,[],[f329]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_13
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f337]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_5
| spl0_14
| spl0_41 ),
inference(sat_conversion,[],[f338]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_8
| spl0_25
| spl0_33 ),
inference(sat_conversion,[],[f339]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_35
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f355]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_4
| spl0_42
| spl0_46 ),
inference(sat_conversion,[],[f361]) ).
cnf(s38,plain,
( spl0_2
| ~ spl0_3
| spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f362]) ).
cnf(s39,plain,
( ~ spl0_3
| spl0_18
| spl0_37
| spl0_41 ),
inference(sat_conversion,[],[f363]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_9
| spl0_22
| spl0_31 ),
inference(sat_conversion,[],[f364]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_28
| spl0_48
| spl0_51 ),
inference(sat_conversion,[],[f379]) ).
cnf(s46,plain,
( spl0_1
| ~ spl0_3
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f398]) ).
cnf(s47,plain,
( spl0_1
| ~ spl0_3
| spl0_46
| spl0_48 ),
inference(sat_conversion,[],[f399]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_13
| spl0_31
| spl0_56 ),
inference(sat_conversion,[],[f404]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_31
| spl0_35
| spl0_52 ),
inference(sat_conversion,[],[f405]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_38
| spl0_47 ),
inference(sat_conversion,[],[f411]) ).
cnf(s53,plain,
( ~ spl0_33
| ~ spl0_58 ),
inference(sat_conversion,[],[f416]) ).
cnf(s54,plain,
( ~ spl0_33
| ~ spl0_59 ),
inference(sat_conversion,[],[f421]) ).
cnf(s55,plain,
( ~ spl0_33
| ~ spl0_60 ),
inference(sat_conversion,[],[f426]) ).
cnf(s56,plain,
( ~ spl0_38
| ~ spl0_61 ),
inference(sat_conversion,[],[f431]) ).
cnf(s57,plain,
( ~ spl0_39
| ~ spl0_62 ),
inference(sat_conversion,[],[f436]) ).
cnf(s58,plain,
( ~ spl0_39
| ~ spl0_63 ),
inference(sat_conversion,[],[f441]) ).
cnf(s59,plain,
( ~ spl0_39
| ~ spl0_64 ),
inference(sat_conversion,[],[f446]) ).
cnf(s63,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(sat_conversion,[],[f466]) ).
cnf(s64,plain,
( ~ spl0_42
| ~ spl0_69 ),
inference(sat_conversion,[],[f471]) ).
cnf(s65,plain,
( ~ spl0_24
| ~ spl0_70 ),
inference(sat_conversion,[],[f476]) ).
cnf(s66,plain,
( ~ spl0_24
| ~ spl0_71 ),
inference(sat_conversion,[],[f481]) ).
cnf(s67,plain,
( ~ spl0_22
| ~ spl0_72 ),
inference(sat_conversion,[],[f486]) ).
cnf(s68,plain,
( ~ spl0_22
| ~ spl0_73 ),
inference(sat_conversion,[],[f491]) ).
cnf(s69,plain,
( ~ spl0_52
| ~ spl0_74 ),
inference(sat_conversion,[],[f496]) ).
cnf(s70,plain,
( ~ spl0_31
| ~ spl0_75 ),
inference(sat_conversion,[],[f501]) ).
cnf(s71,plain,
( ~ spl0_31
| ~ spl0_76 ),
inference(sat_conversion,[],[f506]) ).
cnf(s72,plain,
( ~ spl0_41
| ~ spl0_77 ),
inference(sat_conversion,[],[f511]) ).
cnf(s73,plain,
( ~ spl0_56
| ~ spl0_78 ),
inference(sat_conversion,[],[f516]) ).
cnf(s74,plain,
( ~ spl0_56
| ~ spl0_79 ),
inference(sat_conversion,[],[f521]) ).
cnf(s75,plain,
( ~ spl0_27
| ~ spl0_80 ),
inference(sat_conversion,[],[f526]) ).
cnf(s76,plain,
( ~ spl0_27
| ~ spl0_81 ),
inference(sat_conversion,[],[f531]) ).
cnf(s77,plain,
( ~ spl0_27
| ~ spl0_82 ),
inference(sat_conversion,[],[f536]) ).
cnf(s78,plain,
( ~ spl0_29
| ~ spl0_83 ),
inference(sat_conversion,[],[f541]) ).
cnf(s80,plain,
( ~ spl0_44
| ~ spl0_85 ),
inference(sat_conversion,[],[f551]) ).
cnf(s81,plain,
( ~ spl0_44
| ~ spl0_86 ),
inference(sat_conversion,[],[f556]) ).
cnf(s82,plain,
( ~ spl0_48
| ~ spl0_87 ),
inference(sat_conversion,[],[f561]) ).
cnf(s83,plain,
( ~ spl0_48
| ~ spl0_88 ),
inference(sat_conversion,[],[f566]) ).
cnf(s84,plain,
( ~ spl0_48
| ~ spl0_89 ),
inference(sat_conversion,[],[f571]) ).
cnf(s85,plain,
( ~ spl0_55
| ~ spl0_90 ),
inference(sat_conversion,[],[f576]) ).
cnf(s86,plain,
( ~ spl0_54
| ~ spl0_91 ),
inference(sat_conversion,[],[f581]) ).
cnf(s87,plain,
( ~ spl0_54
| ~ spl0_92 ),
inference(sat_conversion,[],[f586]) ).
cnf(s88,plain,
( ~ spl0_36
| ~ spl0_93 ),
inference(sat_conversion,[],[f591]) ).
cnf(s89,plain,
( ~ spl0_36
| ~ spl0_94 ),
inference(sat_conversion,[],[f596]) ).
cnf(s91,plain,
( ~ spl0_96
| ~ spl0_97 ),
inference(sat_conversion,[],[f610]) ).
cnf(s92,plain,
( ~ spl0_96
| ~ spl0_98 ),
inference(sat_conversion,[],[f615]) ).
cnf(s95,plain,
( ~ spl0_38
| spl0_102 ),
inference(sat_conversion,[],[f634]) ).
cnf(s96,plain,
( ~ spl0_38
| spl0_103 ),
inference(sat_conversion,[],[f639]) ).
cnf(s100,plain,
( ~ spl0_42
| spl0_107 ),
inference(sat_conversion,[],[f659]) ).
cnf(s101,plain,
( ~ spl0_24
| spl0_108 ),
inference(sat_conversion,[],[f664]) ).
cnf(s102,plain,
( ~ spl0_22
| spl0_109 ),
inference(sat_conversion,[],[f669]) ).
cnf(s103,plain,
( ~ spl0_52
| spl0_110 ),
inference(sat_conversion,[],[f674]) ).
cnf(s104,plain,
( ~ spl0_52
| spl0_111 ),
inference(sat_conversion,[],[f679]) ).
cnf(s105,plain,
( ~ spl0_31
| spl0_112 ),
inference(sat_conversion,[],[f684]) ).
cnf(s106,plain,
( ~ spl0_41
| spl0_113 ),
inference(sat_conversion,[],[f689]) ).
cnf(s107,plain,
( ~ spl0_41
| spl0_114 ),
inference(sat_conversion,[],[f694]) ).
cnf(s108,plain,
( ~ spl0_56
| spl0_115 ),
inference(sat_conversion,[],[f699]) ).
cnf(s109,plain,
( ~ spl0_29
| spl0_116 ),
inference(sat_conversion,[],[f704]) ).
cnf(s110,plain,
( ~ spl0_29
| spl0_117 ),
inference(sat_conversion,[],[f709]) ).
cnf(s113,plain,
( ~ spl0_44
| spl0_120 ),
inference(sat_conversion,[],[f724]) ).
cnf(s114,plain,
( ~ spl0_55
| spl0_121 ),
inference(sat_conversion,[],[f729]) ).
cnf(s115,plain,
( ~ spl0_55
| spl0_122 ),
inference(sat_conversion,[],[f734]) ).
cnf(s116,plain,
( ~ spl0_54
| spl0_123 ),
inference(sat_conversion,[],[f739]) ).
cnf(s117,plain,
( ~ spl0_36
| spl0_124 ),
inference(sat_conversion,[],[f744]) ).
cnf(s120,plain,
( ~ spl0_96
| spl0_127 ),
inference(sat_conversion,[],[f759]) ).
cnf(s122,plain,
( ~ spl0_46
| spl0_129 ),
inference(sat_conversion,[],[f769]) ).
cnf(s123,plain,
( ~ spl0_46
| spl0_130 ),
inference(sat_conversion,[],[f774]) ).
cnf(s124,plain,
( ~ spl0_46
| spl0_131 ),
inference(sat_conversion,[],[f779]) ).
cnf(s125,plain,
( ~ spl0_37
| spl0_132 ),
inference(sat_conversion,[],[f784]) ).
cnf(s126,plain,
( ~ spl0_37
| spl0_133 ),
inference(sat_conversion,[],[f789]) ).
cnf(s127,plain,
( ~ spl0_37
| spl0_134 ),
inference(sat_conversion,[],[f794]) ).
cnf(s128,plain,
( ~ spl0_51
| spl0_135 ),
inference(sat_conversion,[],[f799]) ).
cnf(s129,plain,
( ~ spl0_51
| spl0_136 ),
inference(sat_conversion,[],[f804]) ).
cnf(s130,plain,
( ~ spl0_51
| spl0_137 ),
inference(sat_conversion,[],[f809]) ).
cnf(s134,plain,
( spl0_42
| spl0_44
| spl0_96 ),
inference(sat_conversion,[],[f813]) ).
cnf(s136,plain,
( spl0_31
| spl0_39
| spl0_46 ),
inference(sat_conversion,[],[f815]) ).
cnf(s137,plain,
( spl0_39
| spl0_44
| spl0_51 ),
inference(sat_conversion,[],[f816]) ).
cnf(s140,plain,
( spl0_3
| ~ spl0_39 ),
inference(sat_conversion,[],[f819]) ).
cnf(s153,plain,
( spl0_3
| ~ spl0_44 ),
inference(sat_conversion,[],[f832]) ).
cnf(s163,plain,
( spl0_3
| ~ spl0_51 ),
inference(sat_conversion,[],[f842]) ).
cnf(s169,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_16
| spl0_68
| ~ spl0_107 ),
inference(sat_conversion,[],[f878]) ).
cnf(s172,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(sat_conversion,[],[f899]) ).
cnf(s176,plain,
( ~ spl0_19
| spl0_75
| spl0_76
| ~ spl0_112 ),
inference(sat_conversion,[],[f936]) ).
cnf(s182,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_135
| ~ spl0_137 ),
inference(sat_conversion,[],[f970]) ).
cnf(s183,plain,
( ~ spl0_6
| ~ spl0_17
| spl0_61
| ~ spl0_102 ),
inference(sat_conversion,[],[f977]) ).
cnf(s187,plain,
( ~ spl0_1
| ~ spl0_9
| spl0_61
| ~ spl0_103 ),
inference(sat_conversion,[],[f997]) ).
cnf(s191,plain,
( ~ spl0_9
| ~ spl0_17
| spl0_61
| ~ spl0_102
| ~ spl0_103 ),
inference(sat_conversion,[],[f1018]) ).
cnf(s193,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_90
| ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s207,plain,
( ~ spl0_13
| ~ spl0_18
| spl0_90
| ~ spl0_121 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s214,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_21
| spl0_68
| spl0_69
| ~ spl0_107 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s223,plain,
( ~ spl0_7
| ~ spl0_14
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s235,plain,
( ~ spl0_14
| ~ spl0_19
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s239,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_121
| ~ spl0_142 ),
inference(sat_conversion,[],[f1253]) ).
cnf(s241,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_102
| ~ spl0_103 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s286,plain,
( ~ spl0_13
| spl0_85
| spl0_86
| ~ spl0_120 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s301,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_107 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s302,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_86 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s308,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_137 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s326,plain,
( ~ spl0_12
| ~ spl0_14
| spl0_91
| spl0_92
| ~ spl0_123 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s328,plain,
( ~ spl0_14
| spl0_25
| ~ spl0_26 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s343,plain,
( ~ spl0_9
| ~ spl0_136
| ~ spl0_137
| spl0_139 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s355,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_136
| ~ spl0_137 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s368,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_130
| ~ spl0_131 ),
inference(sat_conversion,[],[f1577]) ).
cnf(s409,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_16
| ~ spl0_23
| ~ spl0_47
| spl0_88
| spl0_89 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s425,plain,
( ~ spl0_5
| spl0_78
| spl0_79
| ~ spl0_115 ),
inference(sat_conversion,[],[f1756]) ).
cnf(s433,plain,
( ~ spl0_26
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f1795]) ).
cnf(s447,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_43
| spl0_90
| ~ spl0_122 ),
inference(sat_conversion,[],[f1829]) ).
cnf(s577,plain,
( ~ spl0_19
| ~ spl0_25
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s597,plain,
( ~ spl0_18
| spl0_61
| ~ spl0_102
| ~ spl0_103 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s618,plain,
( ~ spl0_40
| ~ spl0_47
| spl0_88
| spl0_89 ),
inference(sat_conversion,[],[f2410]) ).
cnf(s621,plain,
( ~ spl0_40
| ~ spl0_47
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f2416]) ).
cnf(s631,plain,
( ~ spl0_7
| ~ spl0_17
| spl0_98
| ~ spl0_127 ),
inference(sat_conversion,[],[f2452]) ).
cnf(s639,plain,
( ~ spl0_47
| spl0_58
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f2471]) ).
cnf(s646,plain,
( ~ spl0_7
| ~ spl0_17
| spl0_75
| ~ spl0_112 ),
inference(sat_conversion,[],[f2493]) ).
cnf(s649,plain,
( ~ spl0_8
| ~ spl0_14
| spl0_25
| ~ spl0_47 ),
inference(sat_conversion,[],[f2507]) ).
cnf(s656,plain,
( ~ spl0_43
| ~ spl0_47
| spl0_90
| spl0_142 ),
inference(sat_conversion,[],[f2540]) ).
cnf(s657,plain,
( ~ spl0_43
| ~ spl0_47
| spl0_85
| spl0_86 ),
inference(sat_conversion,[],[f2541]) ).
cnf(s664,plain,
( ~ spl0_5
| ~ spl0_8
| spl0_68
| ~ spl0_107 ),
inference(sat_conversion,[],[f2553]) ).
cnf(s673,plain,
( ~ spl0_2
| ~ spl0_129
| ~ spl0_130
| ~ spl0_131 ),
inference(sat_conversion,[],[f2569]) ).
cnf(s708,plain,
( ~ spl0_7
| spl0_93
| ~ spl0_124
| ~ spl0_156 ),
inference(sat_conversion,[],[f2633]) ).
cnf(s715,plain,
( ~ spl0_17
| spl0_97
| spl0_98
| ~ spl0_127 ),
inference(sat_conversion,[],[f2641]) ).
cnf(s739,plain,
( ~ spl0_2
| ~ spl0_132
| ~ spl0_134
| ~ spl0_138 ),
inference(sat_conversion,[],[f2702]) ).
cnf(s740,plain,
( ~ spl0_4
| ~ spl0_132
| ~ spl0_133
| ~ spl0_138 ),
inference(sat_conversion,[],[f2703]) ).
cnf(s760,plain,
( ~ spl0_14
| spl0_94
| ~ spl0_124
| spl0_156 ),
inference(sat_conversion,[],[f2731]) ).
cnf(s766,plain,
( ~ spl0_2
| ~ spl0_20
| ~ spl0_132
| ~ spl0_134 ),
inference(sat_conversion,[],[f2747]) ).
cnf(s769,plain,
( ~ spl0_19
| ~ spl0_25
| spl0_88
| spl0_89 ),
inference(sat_conversion,[],[f2750]) ).
cnf(s850,plain,
( ~ spl0_35
| spl0_81
| spl0_82
| ~ spl0_154 ),
inference(sat_conversion,[],[f3046]) ).
cnf(s852,plain,
( ~ spl0_35
| spl0_72
| spl0_73
| ~ spl0_109 ),
inference(sat_conversion,[],[f3050]) ).
cnf(s884,plain,
( ~ spl0_8
| ~ spl0_14
| ~ spl0_113
| spl0_143 ),
inference(sat_conversion,[],[f3085]) ).
cnf(s886,plain,
( ~ spl0_12
| spl0_68
| spl0_69
| ~ spl0_107 ),
inference(sat_conversion,[],[f3086]) ).
cnf(s887,plain,
( ~ spl0_4
| ~ spl0_113
| ~ spl0_114
| ~ spl0_143 ),
inference(sat_conversion,[],[f3087]) ).
cnf(s941,plain,
( ~ spl0_34
| spl0_74
| ~ spl0_110
| ~ spl0_111 ),
inference(sat_conversion,[],[f3160]) ).
cnf(s977,plain,
( ~ spl0_1
| spl0_61
| ~ spl0_103
| spl0_145 ),
inference(sat_conversion,[],[f3200]) ).
cnf(s1073,plain,
( ~ spl0_1
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(sat_conversion,[],[f3352]) ).
cnf(s1093,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_18
| ~ spl0_47
| spl0_62
| spl0_64 ),
inference(sat_conversion,[],[f3395]) ).
cnf(s1109,plain,
( ~ spl0_21
| ~ spl0_34
| ~ spl0_129
| spl0_158 ),
inference(sat_conversion,[],[f3485]) ).
cnf(s1121,plain,
( ~ spl0_14
| spl0_91
| ~ spl0_123
| spl0_147 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s1125,plain,
( ~ spl0_21
| ~ spl0_34
| spl0_91
| ~ spl0_123 ),
inference(sat_conversion,[],[f3498]) ).
cnf(s1126,plain,
( ~ spl0_6
| spl0_90
| ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f3499]) ).
cnf(s1147,plain,
( ~ spl0_14
| spl0_83
| ~ spl0_116
| spl0_141 ),
inference(sat_conversion,[],[f3519]) ).
cnf(s1166,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_18
| ~ spl0_120
| ~ spl0_140 ),
inference(sat_conversion,[],[f3550]) ).
cnf(s1167,plain,
( ~ spl0_16
| spl0_77
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f3568]) ).
cnf(s1169,plain,
( ~ spl0_16
| spl0_92
| ~ spl0_123
| ~ spl0_147 ),
inference(sat_conversion,[],[f3570]) ).
cnf(s1210,plain,
( ~ spl0_47
| spl0_85
| spl0_86
| spl0_140 ),
inference(sat_conversion,[],[f3599]) ).
cnf(s1215,plain,
( ~ spl0_4
| ~ spl0_129
| ~ spl0_131
| ~ spl0_158 ),
inference(sat_conversion,[],[f3618]) ).
cnf(s1218,plain,
( ~ spl0_5
| ~ spl0_47
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f3631]) ).
cnf(s1219,plain,
( ~ spl0_11
| ~ spl0_102
| ~ spl0_103
| ~ spl0_145 ),
inference(sat_conversion,[],[f3643]) ).
cnf(s1225,plain,
( ~ spl0_11
| ~ spl0_15
| ~ spl0_120
| ~ spl0_140 ),
inference(sat_conversion,[],[f3676]) ).
cnf(s1226,plain,
( ~ spl0_11
| ~ spl0_15
| ~ spl0_133
| ~ spl0_134 ),
inference(sat_conversion,[],[f3678]) ).
cnf(s1248,plain,
( ~ spl0_28
| ~ spl0_130
| ~ spl0_131
| spl0_158 ),
inference(sat_conversion,[],[f3718]) ).
cnf(s1257,plain,
( ~ spl0_15
| spl0_86
| ~ spl0_120
| ~ spl0_140 ),
inference(sat_conversion,[],[f3721]) ).
cnf(s1268,plain,
( ~ spl0_15
| ~ spl0_133
| ~ spl0_134
| spl0_138 ),
inference(sat_conversion,[],[f3728]) ).
cnf(s1269,plain,
( ~ spl0_15
| spl0_83
| ~ spl0_117
| ~ spl0_141 ),
inference(sat_conversion,[],[f3729]) ).
cnf(s1275,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_131
| spl0_158 ),
inference(sat_conversion,[],[f3754]) ).
cnf(s1278,plain,
( ~ spl0_8
| ~ spl0_14
| ~ spl0_129
| spl0_158 ),
inference(sat_conversion,[],[f3768]) ).
cnf(s1286,plain,
( ~ spl0_26
| spl0_80
| spl0_81
| spl0_154 ),
inference(sat_conversion,[],[f3795]) ).
cnf(s1309,plain,
( ~ spl0_8
| ~ spl0_14
| ~ spl0_23
| spl0_94
| ~ spl0_124 ),
inference(sat_conversion,[],[f3897]) ).
cnf(s1317,plain,
( ~ spl0_17
| spl0_85
| ~ spl0_120
| spl0_140 ),
inference(sat_conversion,[],[f3912]) ).
cnf(s1320,plain,
( ~ spl0_1
| spl0_70
| spl0_71
| ~ spl0_108 ),
inference(sat_conversion,[],[f3914]) ).
cnf(s1334,plain,
( ~ spl0_40
| spl0_93
| spl0_94
| ~ spl0_124 ),
inference(sat_conversion,[],[f3961]) ).
cnf(s1368,plain,
( ~ spl0_11
| ~ spl0_133
| ~ spl0_134
| ~ spl0_138 ),
inference(sat_conversion,[],[f4013]) ).
cnf(s1372,plain,
( ~ spl0_20
| ~ spl0_132
| ~ spl0_134
| spl0_138 ),
inference(sat_conversion,[],[f4017]) ).
cnf(s1373,plain,
( ~ spl0_20
| spl0_83
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f4018]) ).
cnf(s1418,plain,
( ~ spl0_21
| spl0_93
| ~ spl0_124
| spl0_156 ),
inference(sat_conversion,[],[f4109]) ).
cnf(s1421,plain,
( ~ spl0_12
| ~ spl0_25
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f4120]) ).
cnf(s1430,plain,
( ~ spl0_4
| ~ spl0_135
| ~ spl0_137
| ~ spl0_139 ),
inference(sat_conversion,[],[f4127]) ).
cnf(s1445,plain,
( ~ spl0_12
| spl0_77
| ~ spl0_114
| spl0_143 ),
inference(sat_conversion,[],[f4137]) ).
cnf(s1446,plain,
spl0_3,
inference(rat,[],[s137,s140,s153,s163]) ).
cnf(s1447,plain,
( spl0_14
| spl0_12
| ~ spl0_11
| spl0_5 ),
inference(rat,[],[s1226,s126,s127,s7,s25,s1167,s72,s106,s107,s32,s1446]) ).
cnf(s1449,plain,
( ~ spl0_41
| ~ spl0_16 ),
inference(rat,[],[s1167,s72,s106,s107]) ).
cnf(s1450,plain,
( ~ spl0_38
| ~ spl0_18
| ~ spl0_4 ),
inference(rat,[],[s241,s95,s96]) ).
cnf(s1452,plain,
( ~ spl0_33
| ~ spl0_47 ),
inference(rat,[],[s639,s53,s54,s55]) ).
cnf(s1454,plain,
( ~ spl0_44
| ~ spl0_47
| ~ spl0_15
| ~ spl0_11 ),
inference(rat,[],[s1210,s1225,s80,s81,s113]) ).
cnf(s1460,plain,
( ~ spl0_55
| ~ spl0_6 ),
inference(rat,[],[s1126,s85,s114,s115]) ).
cnf(s1461,plain,
( ~ spl0_12
| spl0_91
| spl0_92
| ~ spl0_123
| spl0_5
| ~ spl0_4 ),
inference(rat,[],[s1445,s887,s72,s106,s107,s32,s326,s1446]) ).
cnf(s1462,plain,
( ~ spl0_11
| ~ spl0_20
| spl0_12
| spl0_91
| spl0_92
| ~ spl0_123
| spl0_5 ),
inference(rat,[],[s1372,s1368,s125,s126,s127,s25,s1169,s1121,s1447,s1446]) ).
cnf(s1463,plain,
( ~ spl0_20
| spl0_5
| spl0_12
| spl0_91
| spl0_92
| ~ spl0_123 ),
inference(rat,[],[s5,s1462,s1446]) ).
cnf(s1464,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s1463,s9,s176,s70,s71,s105,s16,s1461,s86,s87,s116,s46,s1460,s2,s1,s1446]) ).
cnf(s1465,plain,
( ~ spl0_18
| ~ spl0_5
| ~ spl0_4
| spl0_2 ),
inference(rat,[],[s1093,s57,s59,s38,s52,s1450,s1446]) ).
cnf(s1466,plain,
( spl0_37
| spl0_18
| ~ spl0_4 ),
inference(rat,[],[s25,s1445,s887,s1449,s72,s106,s107,s39,s1446]) ).
cnf(s1467,plain,
( spl0_12
| spl0_20
| spl0_2 ),
inference(rat,[],[s176,s70,s71,s105,s9,s16,s1446]) ).
cnf(s1468,plain,
( ~ spl0_42
| ~ spl0_12 ),
inference(rat,[],[s886,s63,s64,s100]) ).
cnf(s1469,plain,
( ~ spl0_46
| ~ spl0_28
| ~ spl0_4 ),
inference(rat,[],[s1215,s1248,s122,s123,s124]) ).
cnf(s1470,plain,
( ~ spl0_48
| ~ spl0_25
| ~ spl0_12 ),
inference(rat,[],[s1421,s82,s83]) ).
cnf(s1471,plain,
( spl0_17
| ~ spl0_26
| ~ spl0_12
| spl0_2
| spl0_1 ),
inference(rat,[],[s1430,s343,s3,s128,s129,s130,s1278,s43,s1215,s1469,s122,s124,s47,s1470,s223,s88,s89,s117,s328,s21,s8,s1465,s1464,s1,s1446]) ).
cnf(s1473,plain,
( ~ spl0_54
| ~ spl0_14
| ~ spl0_12 ),
inference(rat,[],[s326,s86,s87,s116]) ).
cnf(s1478,plain,
( ~ spl0_39
| ~ spl0_26 ),
inference(rat,[],[s433,s57,s58,s59]) ).
cnf(s1479,plain,
( ~ spl0_52
| ~ spl0_34 ),
inference(rat,[],[s941,s69,s103,s104]) ).
cnf(s1480,plain,
( ~ spl0_34
| spl0_158
| ~ spl0_129
| spl0_35
| spl0_15 ),
inference(rat,[],[s176,s70,s71,s105,s49,s1479,s10,s1109,s1446]) ).
cnf(s1481,plain,
( ~ spl0_96
| ~ spl0_7
| ~ spl0_17 ),
inference(rat,[],[s631,s92,s120]) ).
cnf(s1482,plain,
( ~ spl0_56
| ~ spl0_5 ),
inference(rat,[],[s425,s73,s74,s108]) ).
cnf(s1483,plain,
( ~ spl0_7
| ~ spl0_17
| spl0_56
| spl0_42 ),
inference(rat,[],[s646,s70,s105,s48,s286,s80,s81,s113,s134,s1481,s1446]) ).
cnf(s1484,plain,
( ~ spl0_46
| ~ spl0_8
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s1215,s1275,s122,s124]) ).
cnf(s1485,plain,
( ~ spl0_26
| spl0_2
| spl0_1 ),
inference(rat,[],[s618,s83,s84,s35,s47,s1484,s3,s1483,s850,s1286,s75,s76,s77,s27,s18,s191,s56,s95,s96,s38,s1478,s1471,s1268,s1468,s1467,s1372,s740,s126,s127,s125,s1466,s1465,s1,s1482,s1464,s1446]) ).
cnf(s1486,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s1445,s887,s72,s106,s107,s30,s1485,s1467,s1372,s740,s125,s126,s127,s1466,s1465,s1464,s1,s1446]) ).
cnf(s1487,plain,
( ~ spl0_17
| spl0_15
| spl0_47
| ~ spl0_5
| ~ spl0_4
| ~ spl0_26
| spl0_42 ),
inference(rat,[],[s850,s1286,s35,s75,s76,s77,s1484,s18,s3,s191,s1483,s1482,s96,s95,s56,s52,s1446]) ).
cnf(s1488,plain,
( spl0_47
| ~ spl0_5
| spl0_138
| ~ spl0_134
| ~ spl0_4
| ~ spl0_26
| ~ spl0_12
| spl0_1 ),
inference(rat,[],[s368,s123,s124,s27,s47,s1334,s1470,s88,s89,s117,s328,s21,s8,s1487,s1268,s126,s1466,s1450,s52,s1486,s1468,s1478,s1446]) ).
cnf(s1490,plain,
( ~ spl0_46
| ~ spl0_9
| ~ spl0_2 ),
inference(rat,[],[s368,s123,s124]) ).
cnf(s1493,plain,
( ~ spl0_55
| ~ spl0_13
| ~ spl0_9 ),
inference(rat,[],[s193,s85,s114,s115]) ).
cnf(s1494,plain,
( ~ spl0_54
| ~ spl0_21
| ~ spl0_34 ),
inference(rat,[],[s1125,s86,s116]) ).
cnf(s1495,plain,
( ~ spl0_55
| ~ spl0_9
| spl0_42
| ~ spl0_2 ),
inference(rat,[],[s31,s447,s1493,s85,s115,s1446]) ).
cnf(s1496,plain,
( spl0_15
| ~ spl0_54
| spl0_19
| spl0_33 ),
inference(rat,[],[s1494,s10,s19,s1446]) ).
cnf(s1497,plain,
( ~ spl0_51
| ~ spl0_18
| ~ spl0_4 ),
inference(rat,[],[s182,s128,s130]) ).
cnf(s1498,plain,
( ~ spl0_9
| ~ spl0_47
| ~ spl0_134
| ~ spl0_4
| spl0_39
| spl0_41
| spl0_42
| spl0_1 ),
inference(rat,[],[s1210,s1166,s80,s81,s113,s137,s1497,s39,s126,s172,s1496,s46,s1495,s176,s70,s71,s105,s136,s1490,s1486,s1452,s1446]) ).
cnf(s1499,plain,
( ~ spl0_31
| ~ spl0_40
| ~ spl0_47 ),
inference(rat,[],[s621,s70,s71]) ).
cnf(s1500,plain,
( ~ spl0_46
| ~ spl0_2 ),
inference(rat,[],[s673,s122,s123,s124]) ).
cnf(s1501,plain,
( spl0_47
| ~ spl0_5
| ~ spl0_26
| ~ spl0_12
| spl0_1 ),
inference(rat,[],[s740,s1488,s125,s126,s127,s1466,s1450,s52,s37,s1500,s1486,s1468,s1446]) ).
cnf(s1502,plain,
( ~ spl0_26
| spl0_41
| ~ spl0_12
| spl0_1 ),
inference(rat,[],[s1210,s1166,s80,s81,s113,s137,s1497,s39,s1496,s127,s46,s1498,s1495,s27,s1499,s1452,s1501,s32,s176,s328,s70,s71,s105,s136,s1478,s37,s1468,s1470,s47,s1500,s1486,s1446]) ).
cnf(s1503,plain,
( ~ spl0_37
| ~ spl0_20
| ~ spl0_2 ),
inference(rat,[],[s766,s125,s127]) ).
cnf(s1504,plain,
( spl0_41
| ~ spl0_12
| spl0_1 ),
inference(rat,[],[s31,s656,s52,s207,s239,s1450,s39,s1503,s85,s114,s46,s1473,s30,s13,s1502,s37,s1468,s1470,s47,s1500,s1486,s1446]) ).
cnf(s1505,plain,
( ~ spl0_12
| spl0_1 ),
inference(rat,[],[s1445,s887,s72,s106,s107,s1504,s37,s1468,s1500,s1486,s1446]) ).
cnf(s1506,plain,
( spl0_39
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s1210,s1166,s80,s81,s113,s137,s52,s1497,s1450,s1466,s1503,s9,s176,s70,s71,s105,s136,s26,s1500,s1486,s1505,s1446]) ).
cnf(s1507,plain,
( ~ spl0_7
| spl0_56
| spl0_42
| ~ spl0_14
| spl0_18 ),
inference(rat,[],[s760,s708,s88,s89,s117,s21,s1483,s1446]) ).
cnf(s1508,plain,
( ~ spl0_36
| ~ spl0_14
| ~ spl0_19 ),
inference(rat,[],[s235,s88,s89,s117]) ).
cnf(s1509,plain,
( ~ spl0_22
| ~ spl0_35 ),
inference(rat,[],[s852,s67,s68,s102]) ).
cnf(s1510,plain,
( spl0_47
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s176,s70,s71,s105,s40,s1509,s191,s21,s1508,s7,s1449,s1268,s9,s30,s740,s1503,s125,s126,s127,s1466,s1450,s56,s95,s96,s35,s52,s1500,s1486,s1505,s1478,s1506,s1446]) ).
cnf(s1511,plain,
( ~ spl0_20
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s1373,s78,s109,s110,s29,s409,s25,s1503,s84,s83,s47,s1500,s1486,s1478,s1447,s5,s1218,s1510,s59,s58,s57,s1506,s1505,s1446]) ).
cnf(s1512,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s33,s884,s887,s769,s106,s107,s9,s30,s1511,s1447,s5,s1218,s1452,s1510,s1478,s57,s58,s59,s1506,s84,s83,s47,s1500,s1486,s1505,s1446]) ).
cnf(s1513,plain,
( spl0_37
| spl0_18
| spl0_12 ),
inference(rat,[],[s1449,s39,s25,s1446]) ).
cnf(s1514,plain,
( spl0_47
| spl0_1 ),
inference(rat,[],[s176,s70,s71,s105,s40,s191,s21,s1508,s13,s1478,s26,s769,s1268,s9,s739,s1503,s125,s126,s127,s1513,s597,s1509,s56,s95,s96,s35,s52,s84,s83,s47,s1500,s1486,s1505,s1446]) ).
cnf(s1515,plain,
( spl0_39
| spl0_1 ),
inference(rat,[],[s355,s129,s130,s137,s1454,s5,s169,s25,s1503,s9,s176,s70,s71,s105,s27,s136,s26,s1505,s100,s63,s37,s1512,s618,s1514,s84,s83,s47,s1500,s1486,s1446]) ).
cnf(s1516,plain,
( spl0_25
| spl0_1 ),
inference(rat,[],[s649,s33,s1452,s1447,s5,s1218,s58,s59,s1514,s57,s1515,s1505,s1446]) ).
cnf(s1517,plain,
spl0_1,
inference(rat,[],[s1373,s78,s109,s110,s29,s409,s25,s1503,s9,s769,s1516,s1447,s5,s1218,s1478,s57,s58,s59,s1515,s1514,s1505,s83,s84,s47,s1500,s1486,s1446]) ).
cnf(s1518,plain,
( ~ spl0_14
| spl0_158
| ~ spl0_129
| spl0_15
| ~ spl0_26
| spl0_2
| ~ spl0_38
| spl0_42 ),
inference(rat,[],[s1418,s708,s88,s117,s21,s183,s2,s1482,s1507,s10,s3,s577,s1278,s328,s597,s95,s55,s54,s19,s1480,s850,s1286,s75,s77,s76,s18,s187,s56,s96,s1446,s1517]) ).
cnf(s1519,plain,
( ~ spl0_4
| ~ spl0_26
| spl0_2
| spl0_47
| spl0_42 ),
inference(rat,[],[s2,s183,s1487,s8,s1518,s1215,s122,s124,s35,s850,s1286,s75,s76,s77,s18,s1268,s740,s125,s126,s127,s1466,s597,s95,s187,s56,s96,s52,s1446,s1517]) ).
cnf(s1520,plain,
~ spl0_24,
inference(rat,[],[s1320,s65,s66,s101,s1517]) ).
cnf(s1523,plain,
( ~ spl0_96
| ~ spl0_17 ),
inference(rat,[],[s715,s91,s92,s120]) ).
cnf(s1524,plain,
( ~ spl0_17
| ~ spl0_15
| spl0_42 ),
inference(rat,[],[s1317,s1257,s80,s81,s113,s134,s1523]) ).
cnf(s1525,plain,
( ~ spl0_26
| spl0_2
| spl0_47
| spl0_42 ),
inference(rat,[],[s1334,s88,s89,s117,s21,s1524,s12,s27,s1519,s1478,s597,s95,s187,s56,s96,s52,s1446,s1520,s1517]) ).
cnf(s1526,plain,
( ~ spl0_4
| spl0_26
| spl0_18
| ~ spl0_12 ),
inference(rat,[],[s1445,s887,s72,s106,s107,s30,s1372,s740,s125,s126,s127,s1466,s1446]) ).
cnf(s1527,plain,
( spl0_26
| ~ spl0_38
| ~ spl0_12 ),
inference(rat,[],[s1147,s1269,s78,s109,s110,s29,s1309,s3,s223,s88,s89,s117,s21,s8,s1524,s12,s1526,s1468,s597,s95,s187,s56,s96,s1446,s1520,s1517]) ).
cnf(s1528,plain,
( spl0_47
| ~ spl0_12 ),
inference(rat,[],[s1286,s850,s75,s76,s77,s18,s1268,s740,s125,s126,s127,s1466,s35,s37,s1500,s1525,s1527,s187,s597,s56,s95,s96,s52,s1468,s1446,s1517]) ).
cnf(s1529,plain,
( spl0_39
| spl0_2
| ~ spl0_12 ),
inference(rat,[],[s1334,s88,s89,s117,s21,s1524,s19,s1479,s49,s1509,s40,s1499,s27,s187,s597,s56,s95,s96,s38,s1468,s1452,s1528,s1446,s1517]) ).
cnf(s1530,plain,
( ~ spl0_39
| ~ spl0_47 ),
inference(rat,[],[s1073,s57,s59,s1517]) ).
cnf(s1531,plain,
( ~ spl0_44
| ~ spl0_12 ),
inference(rat,[],[s31,s657,s286,s80,s81,s113,s1468,s1528,s1446]) ).
cnf(s1532,plain,
~ spl0_12,
inference(rat,[],[s355,s129,s130,s137,s1531,s27,s1499,s136,s1500,s1529,s1530,s1528,s1446]) ).
cnf(s1533,plain,
( ~ spl0_26
| spl0_2
| spl0_47 ),
inference(rat,[],[s1334,s88,s89,s117,s21,s646,s3,s664,s63,s100,s27,s1525,s1478,s597,s187,s5,s1219,s977,s56,s95,s96,s52,s105,s70,s16,s1446,s1532,s1517]) ).
cnf(s1534,plain,
( ~ spl0_29
| ~ spl0_20 ),
inference(rat,[],[s1373,s78,s109,s110]) ).
cnf(s1535,plain,
( spl0_42
| ~ spl0_23
| ~ spl0_15
| ~ spl0_38 ),
inference(rat,[],[s1309,s3,s89,s117,s1507,s21,s8,s1524,s597,s187,s1482,s5,s1219,s977,s56,s95,s96,s1446,s1532,s1517]) ).
cnf(s1536,plain,
( spl0_2
| spl0_47 ),
inference(rat,[],[s3,s214,s664,s63,s64,s100,s1535,s29,s23,s1534,s1533,s12,s740,s1372,s1467,s187,s5,s1219,s977,s127,s126,s125,s1513,s597,s56,s95,s96,s52,s1446,s1520,s1532,s1517]) ).
cnf(s1537,plain,
spl0_47,
inference(rat,[],[s176,s70,s71,s105,s40,s1509,s9,s35,s1503,s1500,s1536,s1513,s187,s597,s56,s95,s96,s52,s1446,s1532,s1517]) ).
cnf(s1539,plain,
~ spl0_39,
inference(rat,[],[s1530,s1537]) ).
cnf(s1540,plain,
spl0_15,
inference(rat,[],[s26,s1532,s1446,s1539]) ).
cnf(s1541,plain,
spl0_2,
inference(rat,[],[s27,s187,s1499,s56,s96,s16,s38,s1446,s1539,s1517,s1537,s1532]) ).
cnf(s1542,plain,
~ spl0_46,
inference(rat,[],[s1500,s1541]) ).
cnf(s1543,plain,
spl0_31,
inference(rat,[],[s136,s1539,s1542]) ).
cnf(s1544,plain,
spl0_112,
inference(rat,[],[s105,s1543]) ).
cnf(s1545,plain,
~ spl0_76,
inference(rat,[],[s71,s1543]) ).
cnf(s1546,plain,
~ spl0_75,
inference(rat,[],[s70,s1543]) ).
cnf(s1547,plain,
~ spl0_40,
inference(rat,[],[s1499,s1537,s1543]) ).
cnf(s1548,plain,
~ spl0_19,
inference(rat,[],[s176,s1544,s1546,s1545]) ).
cnf(s1549,plain,
spl0_9,
inference(rat,[],[s27,s1539,s1446,s1547]) ).
cnf(s1550,plain,
spl0_20,
inference(rat,[],[s9,s1532,s1446,s1548]) ).
cnf(s1551,plain,
~ spl0_37,
inference(rat,[],[s1503,s1541,s1550]) ).
cnf(s1553,plain,
spl0_16,
inference(rat,[],[s25,s1532,s1446,s1551]) ).
cnf(s1555,plain,
spl0_18,
inference(rat,[],[s1513,s1532,s1551]) ).
cnf(s1557,plain,
~ spl0_137,
inference(rat,[],[s308,s1549,s1541,s1517,s1553]) ).
cnf(s1558,plain,
~ spl0_86,
inference(rat,[],[s302,s1549,s1541,s1517,s1553]) ).
cnf(s1559,plain,
~ spl0_107,
inference(rat,[],[s301,s1549,s1541,s1517,s1553]) ).
cnf(s1564,plain,
~ spl0_51,
inference(rat,[],[s130,s1557]) ).
cnf(s1565,plain,
~ spl0_42,
inference(rat,[],[s100,s1559]) ).
cnf(s1567,plain,
spl0_44,
inference(rat,[],[s137,s1539,s1564]) ).
cnf(s1568,plain,
spl0_4,
inference(rat,[],[s37,s1542,s1446,s1565]) ).
cnf(s1571,plain,
spl0_120,
inference(rat,[],[s113,s1567]) ).
cnf(s1572,plain,
~ spl0_85,
inference(rat,[],[s80,s1567]) ).
cnf(s1576,plain,
~ spl0_140,
inference(rat,[],[s1166,s1555,s1540,s1568,s1571]) ).
cnf(s1579,plain,
$false,
inference(rat,[],[s1210,s1558,s1537,s1572,s1576]) ).
fof(f4138,plain,
$false,
inference(avatar_sat_refutation,[],[s1579]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN459-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:07:10 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.31 % (2368794)Will run a generic schedule for satisfiability detection.
% 0.19/0.31 % (2368802)dis+10_1_sil=32000:sp=arity:random_seed=3905841051:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.31 % (2368800)% WARNING: option uhcvi not known.
% 0.19/0.31 % (2368799)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=483973408_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.31 % (2368800)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2638270312:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.31 % (2368804)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2882914716:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.31 % (2368801)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2904556516:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.31 % (2368803)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4200098199:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.31 % (2368805)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=666799251:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.31 % Detected minimum model sizes of [1]
% 0.19/0.31 % Detected maximum model sizes of [26]
% 0.19/0.31 % TRYING [1]
% 0.19/0.31 % TRYING [2]
% 0.19/0.31 % TRYING [3]
% 0.19/0.31 % TRYING [4]
% 0.19/0.31 % (2368802) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2368794-2368802"...
% 0.19/0.31 % (2368802)...printing done.
% 0.19/0.31 % (2368802)Refutation found. Thanks to Tanya!
% 0.19/0.31 % SZS status Unsatisfiable for theBenchmark
% 0.19/0.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.32 % (2368802)------------------------------
% 0.19/0.32 % (2368802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.32 % (2368802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.32 % (2368802)CaDiCaL version: 2.1.3
% 0.19/0.32 % (2368802)Termination reason: Refutation
% 0.19/0.32 % (2368802)Time elapsed: 0.036 s
% 0.19/0.32 % (2368802)Peak memory usage: 13 MB
% 0.19/0.32 % (2368802)Instructions burned: 98 (million)
% 0.19/0.32 % (2368794)Success in time 0.072 s
% 0.19/0.32 % Vampire exiting
%------------------------------------------------------------------------------