%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN500-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:58:34 PM UTC 2026
% Result : Unsatisfiable 1.10s 1.14s
% Output : Refutation 3.97s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp27
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f4,negated_conjecture,
( ~ hskp27
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f22,negated_conjecture,
( ~ hskp9
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
fof(f32,negated_conjecture,
( hskp14
| hskp20
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
fof(f33,negated_conjecture,
( hskp29
| hskp24
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f35,negated_conjecture,
( hskp1
| hskp27
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( hskp17
| hskp22
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( hskp11
| hskp0
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( hskp11
| hskp21
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
( ~ hskp29
| c0_1(a77) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( ~ hskp29
| c2_1(a77) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f42,negated_conjecture,
( ~ hskp28
| c0_1(a23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp28
| c1_1(a23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp28
| c2_1(a23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp27
| c1_1(a13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp27
| c2_1(a13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp27
| c3_1(a13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f51,negated_conjecture,
( ~ hskp25
| c0_1(a73) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp25
| c2_1(a73) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp24
| c1_1(a64) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp24
| c3_1(a64) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f56,negated_conjecture,
( ~ hskp22
| c1_1(a48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp21
| c2_1(a47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp21
| c3_1(a47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp20
| c0_1(a43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp20
| c1_1(a43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp19
| c2_1(a40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp18
| c0_1(a39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp18
| c3_1(a39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp17
| c0_1(a33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f67,negated_conjecture,
( ~ hskp15
| c2_1(a28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp15
| c3_1(a28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp14
| c0_1(a25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp14
| c1_1(a25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp13
| c3_1(a22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp11
| c1_1(a19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp11
| c2_1(a19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp8
| c3_1(a14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f76,negated_conjecture,
( ~ hskp6
| c0_1(a10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp6
| c3_1(a10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp5
| c1_1(a8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp3
| c2_1(a5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp2
| c3_1(a3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp1
| c0_1(a2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp0
| c1_1(a1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp0
| c3_1(a1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ c3_1(a73)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ c0_1(a64)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f88,negated_conjecture,
( ~ c0_1(a48)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ c3_1(a48)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c0_1(a47)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c3_1(a43)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ c0_1(a40)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c3_1(a40)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c1_1(a39)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c1_1(a33)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c3_1(a33)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f98,negated_conjecture,
( ~ c1_1(a28)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c2_1(a25)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c0_1(a22)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c1_1(a22)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ c0_1(a20)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c2_1(a20)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c3_1(a20)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c0_1(a19)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c1_1(a18)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c2_1(a18)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c3_1(a18)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c0_1(a15)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c1_1(a15)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c2_1(a15)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c0_1(a14)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f116,negated_conjecture,
( ~ c2_1(a10)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c2_1(a8)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c3_1(a8)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c0_1(a7)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c1_1(a7)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c3_1(a7)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c0_1(a5)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c1_1(a5)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c1_1(a3)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ c2_1(a3)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c1_1(a2)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c2_1(a2)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ c2_1(a1)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f130,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp1
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f133,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f136,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp1
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f139,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp15
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f141,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp11
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp24
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f145,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp17
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp3
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp18
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp11
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause149) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp6
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f158,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f166,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c0_1(X0)
| c0_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f177,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X2)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X2)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f185,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause185) ).
fof(f186,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X2)
| c1_1(X0)
| c0_1(X1)
| c2_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f190,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f191,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X2)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause191) ).
fof(f192,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X2)
| c2_1(X0)
| c1_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| c3_1(X0)
| c1_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause194) ).
fof(f196,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause196) ).
fof(f198,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c2_1(X1)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause198) ).
fof(f199,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c2_1(X2)
| c1_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause200) ).
fof(f202,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| c1_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f203,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| ~ c0_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,definition,
( spl0_2
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f206,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f211,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f212,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f213,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f200,f211,f208,f205,f202]) ).
fof(f215,definition,
( spl0_5
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f216,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f217,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f199,f215,f208,f205,f202]) ).
fof(f219,definition,
( spl0_6
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f220,plain,
( ! [X2] :
( c3_1(X2)
| ~ c2_1(X2)
| c1_1(X2) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f222,definition,
( spl0_7
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f223,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f225,definition,
( spl0_8
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f226,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f227,plain,
( spl0_6
| spl0_7
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f198,f225,f208,f222,f219]) ).
fof(f229,definition,
( spl0_9
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f230,plain,
( ! [X2] :
( c2_1(X2)
| ~ c0_1(X2)
| c1_1(X2) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f232,definition,
( spl0_10
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f233,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f236,definition,
( spl0_11
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f237,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| ~ c1_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f239,definition,
( spl0_12
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f240,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( spl0_11
| spl0_2
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f196,f239,f208,f205,f236]) ).
fof(f243,definition,
( spl0_13
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f244,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| c2_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl0_14
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f248,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f249,plain,
( spl0_6
| spl0_14
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f194,f215,f208,f247,f219]) ).
fof(f251,definition,
( spl0_15
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f252,plain,
( ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,definition,
( spl0_16
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f255,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f256,plain,
( spl0_15
| spl0_2
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f193,f254,f208,f205,f251]) ).
fof(f257,plain,
( spl0_9
| spl0_1
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f192,f222,f208,f202,f229]) ).
fof(f259,definition,
( spl0_17
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f260,plain,
( ! [X2] :
( c3_1(X2)
| ~ c2_1(X2)
| c0_1(X2) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f261,plain,
( spl0_17
| spl0_13
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f191,f211,f208,f243,f259]) ).
fof(f263,definition,
( spl0_18
<=> ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f264,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f266,definition,
( spl0_19
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f267,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f268,plain,
( spl0_18
| spl0_19
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f190,f215,f208,f266,f263]) ).
fof(f270,definition,
( spl0_20
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f271,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( spl0_20
| spl0_11
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f189,f222,f208,f236,f270]) ).
fof(f274,definition,
( spl0_21
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f275,plain,
( ! [X2] :
( c2_1(X2)
| c0_1(X2)
| c1_1(X2) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f277,definition,
( spl0_22
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f278,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f279,plain,
( spl0_21
| spl0_2
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f188,f277,f208,f205,f274]) ).
fof(f280,plain,
( spl0_18
| spl0_19
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f187,f219,f208,f266,f263]) ).
fof(f282,definition,
( spl0_23
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f283,plain,
( ! [X1] :
( c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f284,plain,
( spl0_18
| spl0_23
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f186,f205,f208,f282,f263]) ).
fof(f286,definition,
( spl0_24
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f287,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f288,plain,
( spl0_21
| spl0_14
| ~ spl0_3
| spl0_24 ),
inference(avatar_split_clause,[],[f185,f286,f208,f247,f274]) ).
fof(f289,plain,
( spl0_21
| spl0_11
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f184,f247,f208,f236,f274]) ).
fof(f291,definition,
( spl0_25
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f292,plain,
( ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f294,definition,
( spl0_26
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f295,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f297,definition,
( spl0_27
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f298,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f299,plain,
( spl0_25
| spl0_26
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f183,f297,f208,f294,f291]) ).
fof(f301,definition,
( spl0_28
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f302,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f303,plain,
( spl0_28
| spl0_6
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f182,f239,f208,f219,f301]) ).
fof(f304,plain,
( spl0_18
| spl0_6
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f181,f243,f208,f219,f263]) ).
fof(f306,definition,
( spl0_29
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f307,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c1_1(X2) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f308,plain,
( spl0_29
| spl0_20
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f180,f243,f208,f270,f306]) ).
fof(f310,definition,
( spl0_30
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f312,plain,
( spl0_30
| spl0_19
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f179,f232,f208,f266,f310]) ).
fof(f314,definition,
( spl0_31
<=> ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f315,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1)
| c2_1(X1) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f316,plain,
( spl0_21
| spl0_31
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f178,f297,f208,f314,f274]) ).
fof(f318,definition,
( spl0_32
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f320,plain,
( spl0_32
| spl0_13
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f177,f225,f208,f243,f318]) ).
fof(f322,definition,
( spl0_33
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f329,definition,
( spl0_35
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f331,plain,
( spl0_35
| spl0_1
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f175,f254,f208,f202,f329]) ).
fof(f333,definition,
( spl0_36
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f335,plain,
( spl0_36
| spl0_15
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f174,f211,f208,f251,f333]) ).
fof(f337,definition,
( spl0_37
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f339,plain,
( spl0_37
| spl0_11
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f173,f254,f208,f236,f337]) ).
fof(f340,plain,
( spl0_35
| spl0_11
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f172,f266,f208,f236,f329]) ).
fof(f342,definition,
( spl0_38
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f344,plain,
( spl0_38
| spl0_25
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f171,f277,f208,f291,f342]) ).
fof(f345,plain,
( spl0_32
| spl0_25
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f170,f225,f208,f291,f318]) ).
fof(f347,definition,
( spl0_39
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f349,plain,
( spl0_39
| spl0_13
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f169,f239,f208,f243,f347]) ).
fof(f351,definition,
( spl0_40
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f353,plain,
( spl0_40
| spl0_26
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f168,f205,f208,f294,f351]) ).
fof(f354,plain,
( spl0_33
| spl0_9
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f167,f205,f208,f229,f322]) ).
fof(f356,definition,
( spl0_41
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f358,plain,
( spl0_41
| spl0_11
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f166,f243,f208,f236,f356]) ).
fof(f360,definition,
( spl0_42
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f363,definition,
( spl0_43
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f364,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f367,definition,
( spl0_44
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f376,definition,
( spl0_46
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f378,plain,
( spl0_46
| spl0_18
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f161,f205,f208,f263,f376]) ).
fof(f380,definition,
( spl0_47
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f382,plain,
( spl0_47
| spl0_18
| ~ spl0_3
| spl0_43 ),
inference(avatar_split_clause,[],[f160,f363,f208,f263,f380]) ).
fof(f384,definition,
( spl0_48
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f386,plain,
( spl0_48
| spl0_6
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f159,f297,f208,f219,f384]) ).
fof(f387,plain,
( spl0_39
| spl0_31
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f158,f202,f208,f314,f347]) ).
fof(f389,definition,
( spl0_49
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f392,plain,
( spl0_46
| spl0_29
| ~ spl0_3
| spl0_24 ),
inference(avatar_split_clause,[],[f156,f286,f208,f306,f376]) ).
fof(f393,plain,
( spl0_48
| spl0_29
| ~ spl0_3
| spl0_43 ),
inference(avatar_split_clause,[],[f155,f363,f208,f306,f384]) ).
fof(f395,definition,
( spl0_50
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f397,plain,
( spl0_50
| spl0_21
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f154,f297,f208,f274,f395]) ).
fof(f399,definition,
( spl0_51
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f401,plain,
( spl0_51
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f153,f225,f208,f399]) ).
fof(f403,definition,
( spl0_52
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f405,plain,
( spl0_46
| spl0_52
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f152,f239,f208,f403,f376]) ).
fof(f409,definition,
( spl0_53
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f411,plain,
( spl0_36
| spl0_53
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f149,f202,f208,f409,f333]) ).
fof(f412,plain,
( spl0_30
| spl0_37
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f148,f202,f208,f337,f310]) ).
fof(f413,plain,
( spl0_46
| spl0_42
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f147,f266,f208,f360,f376]) ).
fof(f415,definition,
( spl0_54
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f419,definition,
( spl0_55
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f421,plain,
( spl0_47
| spl0_55
| ~ spl0_3
| spl0_43 ),
inference(avatar_split_clause,[],[f145,f363,f208,f419,f380]) ).
fof(f430,definition,
( spl0_58
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f432,plain,
( spl0_40
| spl0_58
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f143,f243,f208,f430,f351]) ).
fof(f438,definition,
( spl0_60
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f440,plain,
( spl0_60
| spl0_53
| ~ spl0_3
| spl0_26 ),
inference(avatar_split_clause,[],[f141,f294,f208,f409,f438]) ).
fof(f442,plain,
( spl0_32
| spl0_41
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f139,f259,f208,f356,f318]) ).
fof(f445,plain,
( spl0_54
| spl0_48
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f136,f282,f208,f384,f415]) ).
fof(f451,plain,
( spl0_30
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f133,f297,f208,f310]) ).
fof(f455,definition,
( spl0_62
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f457,plain,
( spl0_62
| spl0_48
| spl0_28
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f130,f208,f301,f384,f455]) ).
fof(f461,definition,
( spl0_63
<=> c2_1(a1) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f462,plain,
( ~ c2_1(a1)
| spl0_63 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f463,plain,
( ~ spl0_50
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f128,f461,f395]) ).
fof(f466,definition,
( spl0_64
<=> c2_1(a2) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f467,plain,
( ~ c2_1(a2)
| spl0_64 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f468,plain,
( ~ spl0_48
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f127,f466,f384]) ).
fof(f470,definition,
( spl0_65
<=> c1_1(a2) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f472,plain,
( ~ spl0_48
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f126,f470,f384]) ).
fof(f475,definition,
( spl0_66
<=> c2_1(a3) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f476,plain,
( ~ c2_1(a3)
| spl0_66 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f477,plain,
( ~ spl0_46
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f125,f475,f376]) ).
fof(f479,definition,
( spl0_67
<=> c1_1(a3) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f481,plain,
( ~ spl0_46
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f124,f479,f376]) ).
fof(f484,definition,
( spl0_68
<=> c1_1(a5) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f486,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f123,f484,f360]) ).
fof(f488,definition,
( spl0_69
<=> c0_1(a5) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f490,plain,
( ~ spl0_42
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f122,f488,f360]) ).
fof(f493,definition,
( spl0_70
<=> c3_1(a7) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f494,plain,
( ~ c3_1(a7)
| spl0_70 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f495,plain,
( ~ spl0_49
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f121,f493,f389]) ).
fof(f497,definition,
( spl0_71
<=> c1_1(a7) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f499,plain,
( ~ spl0_49
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f120,f497,f389]) ).
fof(f501,definition,
( spl0_72
<=> c0_1(a7) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f503,plain,
( ~ spl0_49
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f119,f501,f389]) ).
fof(f506,definition,
( spl0_73
<=> c3_1(a8) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f507,plain,
( ~ c3_1(a8)
| spl0_73 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f508,plain,
( ~ spl0_47
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f118,f506,f380]) ).
fof(f510,definition,
( spl0_74
<=> c2_1(a8) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f512,plain,
( ~ spl0_47
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f117,f510,f380]) ).
fof(f515,definition,
( spl0_75
<=> c2_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f516,plain,
( ~ c2_1(a10)
| spl0_75 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f517,plain,
( ~ spl0_52
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f116,f515,f403]) ).
fof(f533,definition,
( spl0_79
<=> c0_1(a14) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f535,plain,
( ~ spl0_33
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f112,f533,f322]) ).
fof(f538,definition,
( spl0_80
<=> c2_1(a15) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f539,plain,
( ~ c2_1(a15)
| spl0_80 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( ~ spl0_60
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f111,f538,f438]) ).
fof(f542,definition,
( spl0_81
<=> c1_1(a15) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f544,plain,
( ~ spl0_60
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f110,f542,f438]) ).
fof(f546,definition,
( spl0_82
<=> c0_1(a15) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f548,plain,
( ~ spl0_60
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f109,f546,f438]) ).
fof(f551,definition,
( spl0_83
<=> c3_1(a18) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f552,plain,
( ~ c3_1(a18)
| spl0_83 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f553,plain,
( ~ spl0_54
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f108,f551,f415]) ).
fof(f555,definition,
( spl0_84
<=> c2_1(a18) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f557,plain,
( ~ spl0_54
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f107,f555,f415]) ).
fof(f559,definition,
( spl0_85
<=> c1_1(a18) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f561,plain,
( ~ spl0_54
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f106,f559,f415]) ).
fof(f564,definition,
( spl0_86
<=> c0_1(a19) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f566,plain,
( ~ spl0_53
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f105,f564,f409]) ).
fof(f569,definition,
( spl0_87
<=> c3_1(a20) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f570,plain,
( ~ c3_1(a20)
| spl0_87 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f571,plain,
( ~ spl0_35
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f104,f569,f329]) ).
fof(f573,definition,
( spl0_88
<=> c2_1(a20) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f574,plain,
( ~ c2_1(a20)
| spl0_88 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f575,plain,
( ~ spl0_35
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f103,f573,f329]) ).
fof(f577,definition,
( spl0_89
<=> c0_1(a20) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f579,plain,
( ~ spl0_35
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f102,f577,f329]) ).
fof(f582,definition,
( spl0_90
<=> c1_1(a22) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f584,plain,
( ~ spl0_32
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f101,f582,f318]) ).
fof(f586,definition,
( spl0_91
<=> c0_1(a22) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f588,plain,
( ~ spl0_32
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f100,f586,f318]) ).
fof(f591,definition,
( spl0_92
<=> c2_1(a25) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f592,plain,
( ~ c2_1(a25)
| spl0_92 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( ~ spl0_44
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f99,f591,f367]) ).
fof(f596,definition,
( spl0_93
<=> c1_1(a28) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f598,plain,
( ~ spl0_41
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f98,f596,f356]) ).
fof(f606,definition,
( spl0_95
<=> c3_1(a33) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f607,plain,
( ~ c3_1(a33)
| spl0_95 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f608,plain,
( ~ spl0_55
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f96,f606,f419]) ).
fof(f610,definition,
( spl0_96
<=> c1_1(a33) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f612,plain,
( ~ spl0_55
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f95,f610,f419]) ).
fof(f615,definition,
( spl0_97
<=> c1_1(a39) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f617,plain,
( ~ spl0_37
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f94,f615,f337]) ).
fof(f620,definition,
( spl0_98
<=> c3_1(a40) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f621,plain,
( ~ c3_1(a40)
| spl0_98 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f622,plain,
( ~ spl0_30
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f93,f620,f310]) ).
fof(f624,definition,
( spl0_99
<=> c0_1(a40) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f626,plain,
( ~ spl0_30
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f92,f624,f310]) ).
fof(f629,definition,
( spl0_100
<=> c3_1(a43) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f630,plain,
( ~ c3_1(a43)
| spl0_100 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f631,plain,
( ~ spl0_39
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f91,f629,f347]) ).
fof(f634,definition,
( spl0_101
<=> c0_1(a47) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f636,plain,
( ~ spl0_36
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f90,f634,f333]) ).
fof(f639,definition,
( spl0_102
<=> c3_1(a48) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f640,plain,
( ~ c3_1(a48)
| spl0_102 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f641,plain,
( ~ spl0_40
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f89,f639,f351]) ).
fof(f643,definition,
( spl0_103
<=> c0_1(a48) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f645,plain,
( ~ spl0_40
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f88,f643,f351]) ).
fof(f657,definition,
( spl0_106
<=> c0_1(a64) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f659,plain,
( ~ spl0_58
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f85,f657,f430]) ).
fof(f662,definition,
( spl0_107
<=> c3_1(a73) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f663,plain,
( ~ c3_1(a73)
| spl0_107 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f664,plain,
( ~ spl0_51
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f84,f662,f399]) ).
fof(f666,definition,
( spl0_108
<=> c3_1(a1) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f667,plain,
( c3_1(a1)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f668,plain,
( spl0_108
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f83,f395,f666]) ).
fof(f670,definition,
( spl0_109
<=> c1_1(a1) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f672,plain,
( spl0_109
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f82,f395,f670]) ).
fof(f674,definition,
( spl0_110
<=> c0_1(a2) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f676,plain,
( spl0_110
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f81,f384,f674]) ).
fof(f678,definition,
( spl0_111
<=> c3_1(a3) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f679,plain,
( c3_1(a3)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f680,plain,
( spl0_111
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f80,f376,f678]) ).
fof(f682,definition,
( spl0_112
<=> c2_1(a5) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f683,plain,
( c2_1(a5)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f684,plain,
( spl0_112
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f79,f360,f682]) ).
fof(f686,definition,
( spl0_113
<=> c1_1(a8) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f688,plain,
( spl0_113
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f78,f380,f686]) ).
fof(f690,definition,
( spl0_114
<=> c3_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f691,plain,
( c3_1(a10)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f692,plain,
( spl0_114
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f77,f403,f690]) ).
fof(f694,definition,
( spl0_115
<=> c0_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f696,plain,
( spl0_115
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f76,f403,f694]) ).
fof(f702,definition,
( spl0_117
<=> c3_1(a14) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f703,plain,
( c3_1(a14)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f704,plain,
( spl0_117
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f74,f322,f702]) ).
fof(f706,definition,
( spl0_118
<=> c2_1(a19) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f707,plain,
( c2_1(a19)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f708,plain,
( spl0_118
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f73,f409,f706]) ).
fof(f710,definition,
( spl0_119
<=> c1_1(a19) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f712,plain,
( spl0_119
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f72,f409,f710]) ).
fof(f714,definition,
( spl0_120
<=> c3_1(a22) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f715,plain,
( c3_1(a22)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f716,plain,
( spl0_120
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f71,f318,f714]) ).
fof(f718,definition,
( spl0_121
<=> c1_1(a25) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f720,plain,
( spl0_121
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f70,f367,f718]) ).
fof(f722,definition,
( spl0_122
<=> c0_1(a25) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f724,plain,
( spl0_122
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f69,f367,f722]) ).
fof(f726,definition,
( spl0_123
<=> c3_1(a28) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f727,plain,
( c3_1(a28)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f728,plain,
( spl0_123
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f68,f356,f726]) ).
fof(f730,definition,
( spl0_124
<=> c2_1(a28) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f731,plain,
( c2_1(a28)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f732,plain,
( spl0_124
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f67,f356,f730]) ).
fof(f742,definition,
( spl0_127
<=> c0_1(a33) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f744,plain,
( spl0_127
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f64,f419,f742]) ).
fof(f746,definition,
( spl0_128
<=> c3_1(a39) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f747,plain,
( c3_1(a39)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f748,plain,
( spl0_128
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f63,f337,f746]) ).
fof(f750,definition,
( spl0_129
<=> c0_1(a39) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f752,plain,
( spl0_129
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f62,f337,f750]) ).
fof(f754,definition,
( spl0_130
<=> c2_1(a40) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f755,plain,
( c2_1(a40)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f756,plain,
( spl0_130
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f61,f310,f754]) ).
fof(f758,definition,
( spl0_131
<=> c1_1(a43) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f760,plain,
( spl0_131
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f60,f347,f758]) ).
fof(f762,definition,
( spl0_132
<=> c0_1(a43) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f764,plain,
( spl0_132
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f59,f347,f762]) ).
fof(f766,definition,
( spl0_133
<=> c3_1(a47) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f767,plain,
( c3_1(a47)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f768,plain,
( spl0_133
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f58,f333,f766]) ).
fof(f770,definition,
( spl0_134
<=> c2_1(a47) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f771,plain,
( c2_1(a47)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f772,plain,
( spl0_134
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f57,f333,f770]) ).
fof(f774,definition,
( spl0_135
<=> c1_1(a48) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f776,plain,
( spl0_135
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f56,f351,f774]) ).
fof(f782,definition,
( spl0_137
<=> c3_1(a64) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f783,plain,
( c3_1(a64)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f784,plain,
( spl0_137
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f54,f430,f782]) ).
fof(f786,definition,
( spl0_138
<=> c1_1(a64) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f788,plain,
( spl0_138
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f53,f430,f786]) ).
fof(f790,definition,
( spl0_139
<=> c2_1(a73) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f791,plain,
( c2_1(a73)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f792,plain,
( spl0_139
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f52,f399,f790]) ).
fof(f794,definition,
( spl0_140
<=> c0_1(a73) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f796,plain,
( spl0_140
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f51,f399,f794]) ).
fof(f811,definition,
( spl0_144
<=> c3_1(a13) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f812,plain,
( c3_1(a13)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f811]) ).
fof(f814,plain,
( spl0_144
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f47,f455,f811]) ).
fof(f816,definition,
( spl0_145
<=> c2_1(a13) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f817,plain,
( c2_1(a13)
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f818,plain,
( spl0_145
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f46,f455,f816]) ).
fof(f820,definition,
( spl0_146
<=> c1_1(a13) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f822,plain,
( spl0_146
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f45,f455,f820]) ).
fof(f824,definition,
( spl0_147
<=> c2_1(a23) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f825,plain,
( c2_1(a23)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f827,plain,
( spl0_147
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f44,f342,f824]) ).
fof(f829,definition,
( spl0_148
<=> c1_1(a23) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f831,plain,
( spl0_148
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f43,f342,f829]) ).
fof(f833,definition,
( spl0_149
<=> c0_1(a23) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f835,plain,
( spl0_149
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f42,f342,f833]) ).
fof(f840,definition,
( spl0_151
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f844,definition,
( spl0_152
<=> c2_1(a77) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f845,plain,
( c2_1(a77)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f846,plain,
( spl0_152
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f40,f840,f844]) ).
fof(f848,definition,
( spl0_153
<=> c0_1(a77) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f850,plain,
( spl0_153
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f39,f840,f848]) ).
fof(f851,plain,
( spl0_35
| spl0_36
| spl0_53 ),
inference(avatar_split_clause,[],[f38,f409,f333,f329]) ).
fof(f852,plain,
( spl0_40
| spl0_50
| spl0_53 ),
inference(avatar_split_clause,[],[f37,f409,f395,f351]) ).
fof(f853,plain,
( spl0_30
| spl0_40
| spl0_55 ),
inference(avatar_split_clause,[],[f36,f419,f351,f310]) ).
fof(f854,plain,
( spl0_49
| spl0_62
| spl0_48 ),
inference(avatar_split_clause,[],[f35,f384,f455,f389]) ).
fof(f857,plain,
( spl0_30
| spl0_58
| spl0_151 ),
inference(avatar_split_clause,[],[f33,f840,f430,f310]) ).
fof(f858,plain,
( spl0_35
| spl0_39
| spl0_44 ),
inference(avatar_split_clause,[],[f32,f367,f347,f329]) ).
fof(f869,plain,
( spl0_3
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f22,f438,f208]) ).
fof(f887,plain,
( spl0_3
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f4,f455,f208]) ).
fof(f890,plain,
( spl0_60
| spl0_62 ),
inference(avatar_split_clause,[],[f1,f455,f438]) ).
fof(f895,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_5 ),
inference(resolution,[],[f216,f212]) ).
fof(f896,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f895]) ).
fof(f904,definition,
( spl0_154
<=> c2_1(a7) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f908,definition,
( spl0_155
<=> c1_1(a40) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f916,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_11
| ~ spl0_12 ),
inference(resolution,[],[f240,f237]) ).
fof(f918,plain,
( ~ c1_1(a40)
| ~ c2_1(a40)
| ~ spl0_12
| spl0_98 ),
inference(resolution,[],[f240,f621]) ).
fof(f922,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_11
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f916]) ).
fof(f925,plain,
( spl0_43
| ~ spl0_11
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f922,f239,f236,f363]) ).
fof(f931,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_11
| ~ spl0_17 ),
inference(resolution,[],[f260,f237]) ).
fof(f932,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_2
| ~ spl0_17 ),
inference(resolution,[],[f260,f206]) ).
fof(f936,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c1_1(X0) )
| ~ spl0_2
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f932]) ).
fof(f937,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_11
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f931]) ).
fof(f942,plain,
( spl0_20
| ~ spl0_2
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f936,f259,f205,f270]) ).
fof(f943,plain,
( spl0_43
| ~ spl0_11
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f937,f259,f236,f363]) ).
fof(f947,definition,
( spl0_156
<=> c2_1(a22) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f948,plain,
( ~ c2_1(a22)
| spl0_156 ),
inference(avatar_component_clause,[],[f947]) ).
fof(f961,definition,
( spl0_157
<=> c1_1(a10) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f977,definition,
( spl0_158
<=> c0_1(a3) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f983,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_13
| ~ spl0_15 ),
inference(resolution,[],[f252,f244]) ).
fof(f985,plain,
( c2_1(a22)
| c1_1(a22)
| ~ spl0_15
| ~ spl0_120 ),
inference(resolution,[],[f252,f715]) ).
fof(f987,plain,
( c2_1(a3)
| c1_1(a3)
| ~ spl0_15
| ~ spl0_111 ),
inference(resolution,[],[f252,f679]) ).
fof(f988,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f983]) ).
fof(f990,plain,
( spl0_67
| spl0_66
| ~ spl0_15
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f987,f678,f251,f475,f479]) ).
fof(f994,plain,
( spl0_90
| spl0_156
| ~ spl0_15
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f985,f714,f251,f947,f582]) ).
fof(f1002,plain,
( c0_1(a22)
| ~ c2_1(a22)
| ~ spl0_19
| ~ spl0_120 ),
inference(resolution,[],[f267,f715]) ).
fof(f1008,plain,
( c0_1(a22)
| c1_1(a22)
| ~ spl0_21
| spl0_156 ),
inference(resolution,[],[f275,f948]) ).
fof(f1010,plain,
( c0_1(a3)
| c1_1(a3)
| ~ spl0_21
| spl0_66 ),
inference(resolution,[],[f275,f476]) ).
fof(f1011,plain,
( c0_1(a20)
| c1_1(a20)
| ~ spl0_21
| spl0_88 ),
inference(resolution,[],[f275,f574]) ).
fof(f1012,plain,
( c0_1(a15)
| c1_1(a15)
| ~ spl0_21
| spl0_80 ),
inference(resolution,[],[f275,f539]) ).
fof(f1017,definition,
( spl0_159
<=> c1_1(a20) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1033,plain,
( ~ c1_1(a20)
| c0_1(a20)
| ~ spl0_23
| spl0_88 ),
inference(resolution,[],[f283,f574]) ).
fof(f1037,plain,
( spl0_89
| ~ spl0_159
| ~ spl0_23
| spl0_88 ),
inference(avatar_split_clause,[],[f1033,f573,f282,f1017,f577]) ).
fof(f1053,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_13
| ~ spl0_24 ),
inference(resolution,[],[f287,f244]) ).
fof(f1058,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_13
| ~ spl0_24 ),
inference(duplicate_literal_removal,[],[f1053]) ).
fof(f1068,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_2
| ~ spl0_26 ),
inference(resolution,[],[f295,f206]) ).
fof(f1074,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_2
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f1068]) ).
fof(f1075,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1074,f294,f205,f202]) ).
fof(f1079,definition,
( spl0_161
<=> c2_1(a33) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1080,plain,
( c2_1(a33)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1090,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_11
| ~ spl0_27 ),
inference(resolution,[],[f298,f237]) ).
fof(f1093,plain,
( ~ c1_1(a20)
| c2_1(a20)
| ~ spl0_27
| spl0_87 ),
inference(resolution,[],[f298,f570]) ).
fof(f1096,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_11
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f1090]) ).
fof(f1101,plain,
( spl0_23
| ~ spl0_11
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1096,f297,f236,f282]) ).
fof(f1105,definition,
( spl0_162
<=> c0_1(a1) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1121,plain,
( c0_1(a1)
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1125,plain,
( spl0_88
| ~ spl0_159
| ~ spl0_27
| spl0_87 ),
inference(avatar_split_clause,[],[f1093,f569,f297,f1017,f573]) ).
fof(f1136,plain,
( ~ c2_1(a7)
| c1_1(a7)
| ~ spl0_6
| spl0_70 ),
inference(resolution,[],[f220,f494]) ).
fof(f1139,plain,
( spl0_71
| ~ spl0_154
| ~ spl0_6
| spl0_70 ),
inference(avatar_split_clause,[],[f1136,f493,f219,f904,f497]) ).
fof(f1147,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_13
| ~ spl0_14 ),
inference(resolution,[],[f248,f244]) ).
fof(f1151,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_13
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f1147]) ).
fof(f1154,plain,
( c1_1(a40)
| c0_1(a40)
| ~ spl0_20
| ~ spl0_130 ),
inference(resolution,[],[f271,f755]) ).
fof(f1161,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_19
| ~ spl0_25 ),
inference(resolution,[],[f292,f267]) ).
fof(f1163,plain,
( ~ c1_1(a40)
| c0_1(a40)
| ~ spl0_25
| spl0_98 ),
inference(resolution,[],[f292,f621]) ).
fof(f1168,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_19
| ~ spl0_25 ),
inference(duplicate_literal_removal,[],[f1161]) ).
fof(f1171,plain,
( spl0_43
| ~ spl0_19
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1168,f291,f266,f363]) ).
fof(f1187,plain,
( ~ c1_1(a1)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_162 ),
inference(resolution,[],[f1121,f896]) ).
fof(f1188,plain,
( ~ spl0_109
| ~ spl0_4
| ~ spl0_5
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f1187,f1105,f215,f211,f670]) ).
fof(f1191,plain,
( c0_1(a47)
| ~ c2_1(a47)
| ~ spl0_19
| ~ spl0_133 ),
inference(resolution,[],[f767,f267]) ).
fof(f1195,definition,
( spl0_163
<=> c1_1(a47) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1205,plain,
( spl0_5
| ~ spl0_13
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f1058,f286,f243,f215]) ).
fof(f1219,plain,
( ~ c0_1(a10)
| c1_1(a10)
| ~ spl0_9
| spl0_75 ),
inference(resolution,[],[f516,f230]) ).
fof(f1220,plain,
( spl0_157
| ~ spl0_115
| ~ spl0_9
| spl0_75 ),
inference(avatar_split_clause,[],[f1219,f515,f229,f694,f961]) ).
fof(f1221,plain,
( ~ c1_1(a43)
| c2_1(a43)
| ~ spl0_27
| spl0_100 ),
inference(resolution,[],[f630,f298]) ).
fof(f1223,definition,
( spl0_164
<=> c2_1(a43) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1226,plain,
( spl0_164
| ~ spl0_131
| ~ spl0_27
| spl0_100 ),
inference(avatar_split_clause,[],[f1221,f629,f297,f758,f1223]) ).
fof(f1230,plain,
( ~ c1_1(a48)
| c2_1(a48)
| ~ spl0_27
| spl0_102 ),
inference(resolution,[],[f640,f298]) ).
fof(f1232,definition,
( spl0_165
<=> c2_1(a48) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1235,plain,
( spl0_165
| ~ spl0_135
| ~ spl0_27
| spl0_102 ),
inference(avatar_split_clause,[],[f1230,f639,f297,f774,f1232]) ).
fof(f1236,plain,
( c2_1(a10)
| ~ c1_1(a10)
| ~ spl0_24
| ~ spl0_114 ),
inference(resolution,[],[f691,f287]) ).
fof(f1247,definition,
( spl0_166
<=> c0_1(a28) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1261,definition,
( spl0_167
<=> c0_1(a13) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1287,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_7
| ~ spl0_27 ),
inference(resolution,[],[f223,f298]) ).
fof(f1294,plain,
( c2_1(a10)
| ~ c0_1(a10)
| ~ spl0_7
| ~ spl0_114 ),
inference(resolution,[],[f223,f691]) ).
fof(f1297,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f1287]) ).
fof(f1299,plain,
( ~ spl0_115
| spl0_75
| ~ spl0_7
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f1294,f690,f222,f515,f694]) ).
fof(f1305,plain,
( spl0_5
| ~ spl0_7
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1297,f297,f222,f215]) ).
fof(f1307,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_8
| ~ spl0_27 ),
inference(resolution,[],[f226,f298]) ).
fof(f1316,plain,
( ~ c0_1(a1)
| ~ c1_1(a1)
| ~ spl0_8
| ~ spl0_108 ),
inference(resolution,[],[f226,f667]) ).
fof(f1317,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_8
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f1307]) ).
fof(f1324,plain,
( spl0_5
| ~ spl0_8
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1317,f297,f225,f215]) ).
fof(f1328,definition,
( spl0_169
<=> c1_1(a73) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1360,plain,
( ~ spl0_130
| ~ spl0_155
| ~ spl0_12
| spl0_98 ),
inference(avatar_split_clause,[],[f918,f620,f239,f908,f754]) ).
fof(f1364,plain,
( ~ c0_1(a25)
| ~ c1_1(a25)
| ~ spl0_5
| spl0_92 ),
inference(resolution,[],[f216,f592]) ).
fof(f1370,plain,
( ~ spl0_121
| ~ spl0_122
| ~ spl0_5
| spl0_92 ),
inference(avatar_split_clause,[],[f1364,f591,f215,f722,f718]) ).
fof(f1383,plain,
( c0_1(a13)
| ~ c1_1(a13)
| ~ spl0_11
| ~ spl0_144 ),
inference(resolution,[],[f237,f812]) ).
fof(f1384,plain,
( c0_1(a64)
| ~ c1_1(a64)
| ~ spl0_11
| ~ spl0_137 ),
inference(resolution,[],[f237,f783]) ).
fof(f1389,plain,
( c0_1(a1)
| ~ c1_1(a1)
| ~ spl0_11
| ~ spl0_108 ),
inference(resolution,[],[f237,f667]) ).
fof(f1396,plain,
( ~ spl0_146
| spl0_167
| ~ spl0_11
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1383,f811,f236,f1261,f820]) ).
fof(f1399,plain,
( ~ c1_1(a73)
| ~ c2_1(a73)
| ~ spl0_12
| spl0_107 ),
inference(resolution,[],[f240,f663]) ).
fof(f1400,plain,
( ~ c1_1(a48)
| ~ c2_1(a48)
| ~ spl0_12
| spl0_102 ),
inference(resolution,[],[f240,f640]) ).
fof(f1401,plain,
( ~ c1_1(a43)
| ~ c2_1(a43)
| ~ spl0_12
| spl0_100 ),
inference(resolution,[],[f240,f630]) ).
fof(f1410,plain,
( ~ spl0_139
| ~ spl0_169
| ~ spl0_12
| spl0_107 ),
inference(avatar_split_clause,[],[f1399,f662,f239,f1328,f790]) ).
fof(f1422,definition,
( spl0_170
<=> c1_1(a77) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1430,plain,
( ~ c2_1(a73)
| c1_1(a73)
| ~ spl0_6
| spl0_107 ),
inference(resolution,[],[f220,f663]) ).
fof(f1436,plain,
( spl0_169
| ~ spl0_139
| ~ spl0_6
| spl0_107 ),
inference(avatar_split_clause,[],[f1430,f662,f219,f790,f1328]) ).
fof(f1462,plain,
( ~ c0_1(a73)
| ~ c1_1(a73)
| ~ spl0_16
| spl0_107 ),
inference(resolution,[],[f255,f663]) ).
fof(f1474,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_6
| ~ spl0_18 ),
inference(resolution,[],[f264,f220]) ).
fof(f1479,plain,
( c1_1(a22)
| c0_1(a22)
| ~ spl0_18
| ~ spl0_120 ),
inference(resolution,[],[f264,f715]) ).
fof(f1482,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_6
| ~ spl0_18 ),
inference(duplicate_literal_removal,[],[f1474]) ).
fof(f1485,plain,
( spl0_20
| ~ spl0_6
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f1482,f263,f219,f270]) ).
fof(f1491,plain,
( ~ c2_1(a48)
| c0_1(a48)
| ~ spl0_17
| spl0_102 ),
inference(resolution,[],[f260,f640]) ).
fof(f1493,plain,
( ~ c2_1(a40)
| c0_1(a40)
| ~ spl0_17
| spl0_98 ),
inference(resolution,[],[f260,f621]) ).
fof(f1513,plain,
( ~ spl0_169
| ~ spl0_140
| ~ spl0_16
| spl0_107 ),
inference(avatar_split_clause,[],[f1462,f662,f254,f794,f1328]) ).
fof(f1538,plain,
( ~ c0_1(a3)
| c1_1(a3)
| ~ spl0_9
| spl0_66 ),
inference(resolution,[],[f476,f230]) ).
fof(f1546,plain,
( c1_1(a3)
| c0_1(a3)
| ~ spl0_18
| ~ spl0_111 ),
inference(resolution,[],[f679,f264]) ).
fof(f1548,plain,
( spl0_158
| spl0_67
| ~ spl0_18
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f1546,f678,f263,f479,f977]) ).
fof(f1558,plain,
( spl0_103
| ~ spl0_165
| ~ spl0_17
| spl0_102 ),
inference(avatar_split_clause,[],[f1491,f639,f259,f1232,f643]) ).
fof(f1560,plain,
( spl0_99
| ~ spl0_130
| ~ spl0_17
| spl0_98 ),
inference(avatar_split_clause,[],[f1493,f620,f259,f754,f624]) ).
fof(f1563,plain,
( spl0_159
| spl0_89
| ~ spl0_21
| spl0_88 ),
inference(avatar_split_clause,[],[f1011,f573,f274,f577,f1017]) ).
fof(f1578,plain,
( spl0_9
| ~ spl0_13
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1151,f247,f243,f229]) ).
fof(f1581,plain,
( spl0_91
| spl0_90
| ~ spl0_18
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1479,f714,f263,f582,f586]) ).
fof(f1588,plain,
( ~ spl0_156
| spl0_91
| ~ spl0_19
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1002,f714,f266,f586,f947]) ).
fof(f1590,plain,
( spl0_81
| spl0_82
| ~ spl0_21
| spl0_80 ),
inference(avatar_split_clause,[],[f1012,f538,f274,f546,f542]) ).
fof(f1591,plain,
( spl0_90
| spl0_91
| ~ spl0_21
| spl0_156 ),
inference(avatar_split_clause,[],[f1008,f947,f274,f586,f582]) ).
fof(f1592,plain,
( spl0_67
| spl0_158
| ~ spl0_21
| spl0_66 ),
inference(avatar_split_clause,[],[f1010,f475,f274,f977,f479]) ).
fof(f1594,plain,
( ~ spl0_109
| ~ spl0_162
| ~ spl0_8
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1316,f666,f225,f1105,f670]) ).
fof(f1599,plain,
( ~ c0_1(a33)
| c2_1(a33)
| ~ spl0_13
| spl0_95 ),
inference(resolution,[],[f607,f244]) ).
fof(f1601,plain,
( spl0_161
| ~ spl0_127
| ~ spl0_13
| spl0_95 ),
inference(avatar_split_clause,[],[f1599,f606,f243,f742,f1079]) ).
fof(f1608,plain,
( c1_1(a77)
| ~ c0_1(a77)
| ~ spl0_1
| ~ spl0_152 ),
inference(resolution,[],[f203,f845]) ).
fof(f1611,plain,
( c1_1(a73)
| ~ c0_1(a73)
| ~ spl0_1
| ~ spl0_139 ),
inference(resolution,[],[f203,f791]) ).
fof(f1616,plain,
( ~ spl0_140
| spl0_169
| ~ spl0_1
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1611,f790,f202,f1328,f794]) ).
fof(f1617,plain,
( ~ spl0_153
| spl0_170
| ~ spl0_1
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f1608,f844,f202,f1422,f848]) ).
fof(f1624,plain,
( c1_1(a28)
| ~ c2_1(a28)
| ~ spl0_2
| ~ spl0_123 ),
inference(resolution,[],[f206,f727]) ).
fof(f1625,plain,
( c1_1(a22)
| ~ c2_1(a22)
| ~ spl0_2
| ~ spl0_120 ),
inference(resolution,[],[f206,f715]) ).
fof(f1628,plain,
( ~ spl0_156
| spl0_90
| ~ spl0_2
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1625,f714,f205,f582,f947]) ).
fof(f1650,plain,
( ~ spl0_138
| spl0_106
| ~ spl0_11
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f1384,f782,f236,f657,f786]) ).
fof(f1653,plain,
( ~ spl0_109
| spl0_162
| ~ spl0_11
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1389,f666,f236,f1105,f670]) ).
fof(f1670,plain,
( c1_1(a14)
| c0_1(a14)
| ~ spl0_18
| ~ spl0_117 ),
inference(resolution,[],[f703,f264]) ).
fof(f1673,definition,
( spl0_173
<=> c1_1(a14) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1675,plain,
( spl0_79
| spl0_173
| ~ spl0_18
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1670,f702,f263,f1673,f533]) ).
fof(f1679,plain,
( ~ spl0_165
| ~ spl0_135
| ~ spl0_12
| spl0_102 ),
inference(avatar_split_clause,[],[f1400,f639,f239,f774,f1232]) ).
fof(f1680,plain,
( ~ spl0_164
| ~ spl0_131
| ~ spl0_12
| spl0_100 ),
inference(avatar_split_clause,[],[f1401,f629,f239,f758,f1223]) ).
fof(f1681,plain,
( spl0_9
| ~ spl0_13
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f988,f251,f243,f229]) ).
fof(f1688,plain,
( spl0_67
| ~ spl0_158
| ~ spl0_9
| spl0_66 ),
inference(avatar_split_clause,[],[f1538,f475,f229,f977,f479]) ).
fof(f1709,plain,
( ~ c0_1(a1)
| ~ c1_1(a1)
| ~ spl0_5
| spl0_63 ),
inference(resolution,[],[f216,f462]) ).
fof(f1715,plain,
( ~ spl0_109
| ~ spl0_162
| ~ spl0_5
| spl0_63 ),
inference(avatar_split_clause,[],[f1709,f461,f215,f1105,f670]) ).
fof(f1733,plain,
( ~ c0_1(a2)
| c1_1(a2)
| ~ spl0_9
| spl0_64 ),
inference(resolution,[],[f230,f467]) ).
fof(f1754,plain,
( ~ spl0_157
| spl0_75
| ~ spl0_24
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f1236,f690,f286,f515,f961]) ).
fof(f1759,plain,
( spl0_99
| spl0_155
| ~ spl0_20
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1154,f754,f270,f908,f624]) ).
fof(f1770,plain,
( c1_1(a28)
| ~ c0_1(a28)
| ~ spl0_1
| ~ spl0_124 ),
inference(resolution,[],[f731,f203]) ).
fof(f1771,plain,
( ~ spl0_166
| spl0_93
| ~ spl0_1
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1770,f730,f202,f596,f1247]) ).
fof(f1778,plain,
( ~ c2_1(a40)
| c1_1(a40)
| ~ spl0_6
| spl0_98 ),
inference(resolution,[],[f220,f621]) ).
fof(f1804,plain,
( c0_1(a47)
| ~ c1_1(a47)
| ~ spl0_11
| ~ spl0_133 ),
inference(resolution,[],[f237,f767]) ).
fof(f1807,plain,
( c0_1(a14)
| ~ c1_1(a14)
| ~ spl0_11
| ~ spl0_117 ),
inference(resolution,[],[f237,f703]) ).
fof(f1812,plain,
( ~ spl0_173
| spl0_79
| ~ spl0_11
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1807,f702,f236,f533,f1673]) ).
fof(f1813,plain,
( ~ spl0_163
| spl0_101
| ~ spl0_11
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f1804,f766,f236,f634,f1195]) ).
fof(f1816,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_10
| ~ spl0_16 ),
inference(resolution,[],[f255,f233]) ).
fof(f1819,plain,
( ~ c0_1(a43)
| ~ c1_1(a43)
| ~ spl0_16
| spl0_100 ),
inference(resolution,[],[f255,f630]) ).
fof(f1825,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_10
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f1816]) ).
fof(f1827,plain,
( ~ spl0_131
| ~ spl0_132
| ~ spl0_16
| spl0_100 ),
inference(avatar_split_clause,[],[f1819,f629,f254,f762,f758]) ).
fof(f1828,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1825,f254,f232,f211]) ).
fof(f1837,plain,
( c1_1(a28)
| c0_1(a28)
| ~ spl0_20
| ~ spl0_124 ),
inference(resolution,[],[f271,f731]) ).
fof(f1839,plain,
( c1_1(a5)
| c0_1(a5)
| ~ spl0_20
| ~ spl0_112 ),
inference(resolution,[],[f271,f683]) ).
fof(f1847,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_16
| ~ spl0_22 ),
inference(resolution,[],[f278,f255]) ).
fof(f1860,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_16
| ~ spl0_22 ),
inference(duplicate_literal_removal,[],[f1847]) ).
fof(f1862,plain,
( spl0_4
| ~ spl0_16
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1860,f277,f254,f211]) ).
fof(f1872,plain,
( ~ c0_1(a77)
| ~ c1_1(a77)
| ~ spl0_4
| ~ spl0_152 ),
inference(resolution,[],[f212,f845]) ).
fof(f1873,plain,
( ~ c0_1(a23)
| ~ c1_1(a23)
| ~ spl0_4
| ~ spl0_147 ),
inference(resolution,[],[f212,f825]) ).
fof(f1874,plain,
( ~ c0_1(a73)
| ~ c1_1(a73)
| ~ spl0_4
| ~ spl0_139 ),
inference(resolution,[],[f212,f791]) ).
fof(f1881,plain,
( ~ spl0_169
| ~ spl0_140
| ~ spl0_4
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1874,f790,f211,f794,f1328]) ).
fof(f1882,plain,
( ~ spl0_148
| ~ spl0_149
| ~ spl0_4
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1873,f824,f211,f833,f829]) ).
fof(f1883,plain,
( ~ spl0_170
| ~ spl0_153
| ~ spl0_4
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f1872,f844,f211,f848,f1422]) ).
fof(f1934,plain,
( c0_1(a20)
| c2_1(a20)
| ~ spl0_28
| spl0_87 ),
inference(resolution,[],[f302,f570]) ).
fof(f1936,plain,
( c0_1(a7)
| c2_1(a7)
| ~ spl0_28
| spl0_70 ),
inference(resolution,[],[f302,f494]) ).
fof(f1940,plain,
( spl0_154
| spl0_72
| ~ spl0_28
| spl0_70 ),
inference(avatar_split_clause,[],[f1936,f493,f301,f501,f904]) ).
fof(f1943,plain,
( spl0_88
| spl0_89
| ~ spl0_28
| spl0_87 ),
inference(avatar_split_clause,[],[f1934,f569,f301,f577,f573]) ).
fof(f1953,plain,
( c0_1(a20)
| c1_1(a20)
| ~ spl0_29
| spl0_87 ),
inference(resolution,[],[f307,f570]) ).
fof(f1955,plain,
( c0_1(a7)
| c1_1(a7)
| ~ spl0_29
| spl0_70 ),
inference(resolution,[],[f307,f494]) ).
fof(f1957,plain,
( spl0_71
| spl0_72
| ~ spl0_29
| spl0_70 ),
inference(avatar_split_clause,[],[f1955,f493,f306,f501,f497]) ).
fof(f1959,plain,
( spl0_159
| spl0_89
| ~ spl0_29
| spl0_87 ),
inference(avatar_split_clause,[],[f1953,f569,f306,f577,f1017]) ).
fof(f1969,plain,
( c1_1(a20)
| c2_1(a20)
| ~ spl0_31
| spl0_87 ),
inference(resolution,[],[f315,f570]) ).
fof(f1970,plain,
( c1_1(a18)
| c2_1(a18)
| ~ spl0_31
| spl0_83 ),
inference(resolution,[],[f315,f552]) ).
fof(f1974,plain,
( spl0_84
| spl0_85
| ~ spl0_31
| spl0_83 ),
inference(avatar_split_clause,[],[f1970,f551,f314,f559,f555]) ).
fof(f1975,plain,
( spl0_88
| spl0_159
| ~ spl0_31
| spl0_87 ),
inference(avatar_split_clause,[],[f1969,f569,f314,f1017,f573]) ).
fof(f1997,plain,
( c0_1(a47)
| ~ c1_1(a47)
| ~ spl0_43
| ~ spl0_134 ),
inference(resolution,[],[f364,f771]) ).
fof(f1998,plain,
( c0_1(a40)
| ~ c1_1(a40)
| ~ spl0_43
| ~ spl0_130 ),
inference(resolution,[],[f364,f755]) ).
fof(f2000,plain,
( c0_1(a19)
| ~ c1_1(a19)
| ~ spl0_43
| ~ spl0_118 ),
inference(resolution,[],[f364,f707]) ).
fof(f2015,plain,
( ~ c1_1(a8)
| c2_1(a8)
| ~ spl0_27
| spl0_73 ),
inference(resolution,[],[f507,f298]) ).
fof(f2018,plain,
( spl0_74
| ~ spl0_113
| ~ spl0_27
| spl0_73 ),
inference(avatar_split_clause,[],[f2015,f506,f297,f686,f510]) ).
fof(f2030,plain,
( ~ spl0_124
| spl0_93
| ~ spl0_2
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1624,f726,f205,f596,f730]) ).
fof(f2034,plain,
( spl0_65
| ~ spl0_110
| ~ spl0_9
| spl0_64 ),
inference(avatar_split_clause,[],[f1733,f466,f229,f674,f470]) ).
fof(f2040,plain,
( spl0_69
| spl0_68
| ~ spl0_20
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f1839,f682,f270,f484,f488]) ).
fof(f2042,plain,
( spl0_166
| spl0_93
| ~ spl0_20
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1837,f730,f270,f596,f1247]) ).
fof(f2045,plain,
( ~ spl0_163
| spl0_101
| ~ spl0_43
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f1997,f770,f363,f634,f1195]) ).
fof(f2046,plain,
( ~ spl0_155
| spl0_99
| ~ spl0_43
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1998,f754,f363,f624,f908]) ).
fof(f2048,plain,
( ~ spl0_119
| spl0_86
| ~ spl0_43
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f2000,f706,f363,f564,f710]) ).
fof(f2071,plain,
( spl0_155
| ~ spl0_130
| ~ spl0_6
| spl0_98 ),
inference(avatar_split_clause,[],[f1778,f620,f219,f754,f908]) ).
fof(f2083,plain,
( ~ c1_1(a13)
| ~ c2_1(a13)
| ~ spl0_22
| ~ spl0_144 ),
inference(resolution,[],[f812,f278]) ).
fof(f2084,plain,
( ~ spl0_145
| ~ spl0_146
| ~ spl0_22
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f2083,f811,f277,f820,f816]) ).
fof(f2085,plain,
( spl0_99
| ~ spl0_155
| ~ spl0_25
| spl0_98 ),
inference(avatar_split_clause,[],[f1163,f620,f291,f908,f624]) ).
fof(f2095,plain,
( c1_1(a47)
| ~ c2_1(a47)
| ~ spl0_2
| ~ spl0_133 ),
inference(resolution,[],[f206,f767]) ).
fof(f2105,plain,
( ~ spl0_134
| spl0_163
| ~ spl0_2
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f2095,f766,f205,f1195,f770]) ).
fof(f2109,plain,
( ~ c0_1(a13)
| ~ c1_1(a13)
| ~ spl0_4
| ~ spl0_145 ),
inference(resolution,[],[f212,f817]) ).
fof(f2114,plain,
( ~ spl0_146
| ~ spl0_167
| ~ spl0_4
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f2109,f816,f211,f1261,f820]) ).
fof(f2116,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_7
| ~ spl0_26 ),
inference(resolution,[],[f223,f295]) ).
fof(f2131,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_7
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f2116]) ).
fof(f2136,plain,
( spl0_9
| ~ spl0_7
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f2131,f294,f222,f229]) ).
fof(f2144,plain,
( ~ c0_1(a13)
| ~ c1_1(a13)
| ~ spl0_8
| ~ spl0_144 ),
inference(resolution,[],[f226,f812]) ).
fof(f2157,plain,
( ~ spl0_146
| ~ spl0_167
| ~ spl0_8
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f2144,f811,f225,f1261,f820]) ).
fof(f2199,plain,
( c1_1(a33)
| ~ c0_1(a33)
| ~ spl0_1
| ~ spl0_161 ),
inference(resolution,[],[f1080,f203]) ).
fof(f2200,plain,
( ~ spl0_127
| spl0_96
| ~ spl0_1
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f2199,f1079,f202,f610,f742]) ).
fof(f2211,plain,
( c1_1(a39)
| ~ c0_1(a39)
| ~ spl0_14
| ~ spl0_128 ),
inference(resolution,[],[f248,f747]) ).
fof(f2220,plain,
( ~ spl0_129
| spl0_97
| ~ spl0_14
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f2211,f746,f247,f615,f750]) ).
fof(f2242,plain,
( ~ c1_1(a48)
| c0_1(a48)
| ~ spl0_25
| spl0_102 ),
inference(resolution,[],[f292,f640]) ).
fof(f2249,plain,
( spl0_103
| ~ spl0_135
| ~ spl0_25
| spl0_102 ),
inference(avatar_split_clause,[],[f2242,f639,f291,f774,f643]) ).
fof(f2250,plain,
( ~ spl0_134
| spl0_101
| ~ spl0_19
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f1191,f766,f266,f634,f770]) ).
fof(f2276,plain,
( c0_1(a13)
| ~ c2_1(a13)
| ~ spl0_19
| ~ spl0_144 ),
inference(resolution,[],[f267,f812]) ).
fof(f2289,plain,
( ~ spl0_145
| spl0_167
| ~ spl0_19
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f2276,f811,f266,f1261,f816]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f213]) ).
cnf(s2,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_5 ),
inference(sat_conversion,[],[f217]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f227]) ).
cnf(s5,plain,
( spl0_2
| ~ spl0_3
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f241]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_14 ),
inference(sat_conversion,[],[f249]) ).
cnf(s8,plain,
( spl0_2
| ~ spl0_3
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f256]) ).
cnf(s9,plain,
( spl0_1
| ~ spl0_3
| spl0_7
| spl0_9 ),
inference(sat_conversion,[],[f257]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_4
| spl0_13
| spl0_17 ),
inference(sat_conversion,[],[f261]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_5
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f268]) ).
cnf(s12,plain,
( ~ spl0_3
| spl0_7
| spl0_11
| spl0_20 ),
inference(sat_conversion,[],[f272]) ).
cnf(s13,plain,
( spl0_2
| ~ spl0_3
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f279]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_6
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f280]) ).
cnf(s15,plain,
( spl0_2
| ~ spl0_3
| spl0_18
| spl0_23 ),
inference(sat_conversion,[],[f284]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_14
| spl0_21
| spl0_24 ),
inference(sat_conversion,[],[f288]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_11
| spl0_14
| spl0_21 ),
inference(sat_conversion,[],[f289]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_25
| spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f299]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_6
| spl0_12
| spl0_28 ),
inference(sat_conversion,[],[f303]) ).
cnf(s20,plain,
( ~ spl0_3
| spl0_6
| spl0_13
| spl0_18 ),
inference(sat_conversion,[],[f304]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_13
| spl0_20
| spl0_29 ),
inference(sat_conversion,[],[f308]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_10
| spl0_19
| spl0_30 ),
inference(sat_conversion,[],[f312]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_21
| spl0_27
| spl0_31 ),
inference(sat_conversion,[],[f316]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_8
| spl0_13
| spl0_32 ),
inference(sat_conversion,[],[f320]) ).
cnf(s26,plain,
( spl0_1
| ~ spl0_3
| spl0_16
| spl0_35 ),
inference(sat_conversion,[],[f331]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_4
| spl0_15
| spl0_36 ),
inference(sat_conversion,[],[f335]) ).
cnf(s28,plain,
( ~ spl0_3
| spl0_11
| spl0_16
| spl0_37 ),
inference(sat_conversion,[],[f339]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_11
| spl0_19
| spl0_35 ),
inference(sat_conversion,[],[f340]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_22
| spl0_25
| spl0_38 ),
inference(sat_conversion,[],[f344]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_8
| spl0_25
| spl0_32 ),
inference(sat_conversion,[],[f345]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_12
| spl0_13
| spl0_39 ),
inference(sat_conversion,[],[f349]) ).
cnf(s33,plain,
( spl0_2
| ~ spl0_3
| spl0_26
| spl0_40 ),
inference(sat_conversion,[],[f353]) ).
cnf(s34,plain,
( spl0_2
| ~ spl0_3
| spl0_9
| spl0_33 ),
inference(sat_conversion,[],[f354]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_11
| spl0_13
| spl0_41 ),
inference(sat_conversion,[],[f358]) ).
cnf(s40,plain,
( spl0_2
| ~ spl0_3
| spl0_18
| spl0_46 ),
inference(sat_conversion,[],[f378]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_18
| spl0_43
| spl0_47 ),
inference(sat_conversion,[],[f382]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_6
| spl0_27
| spl0_48 ),
inference(sat_conversion,[],[f386]) ).
cnf(s43,plain,
( spl0_1
| ~ spl0_3
| spl0_31
| spl0_39 ),
inference(sat_conversion,[],[f387]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_24
| spl0_29
| spl0_46 ),
inference(sat_conversion,[],[f392]) ).
cnf(s46,plain,
( ~ spl0_3
| spl0_29
| spl0_43
| spl0_48 ),
inference(sat_conversion,[],[f393]) ).
cnf(s47,plain,
( ~ spl0_3
| spl0_21
| spl0_27
| spl0_50 ),
inference(sat_conversion,[],[f397]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_8
| spl0_51 ),
inference(sat_conversion,[],[f401]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_12
| spl0_46
| spl0_52 ),
inference(sat_conversion,[],[f405]) ).
cnf(s52,plain,
( spl0_1
| ~ spl0_3
| spl0_36
| spl0_53 ),
inference(sat_conversion,[],[f411]) ).
cnf(s53,plain,
( spl0_1
| ~ spl0_3
| spl0_30
| spl0_37 ),
inference(sat_conversion,[],[f412]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_19
| spl0_42
| spl0_46 ),
inference(sat_conversion,[],[f413]) ).
cnf(s56,plain,
( ~ spl0_3
| spl0_43
| spl0_47
| spl0_55 ),
inference(sat_conversion,[],[f421]) ).
cnf(s58,plain,
( ~ spl0_3
| spl0_13
| spl0_40
| spl0_58 ),
inference(sat_conversion,[],[f432]) ).
cnf(s60,plain,
( ~ spl0_3
| spl0_26
| spl0_53
| spl0_60 ),
inference(sat_conversion,[],[f440]) ).
cnf(s62,plain,
( ~ spl0_3
| spl0_17
| spl0_32
| spl0_41 ),
inference(sat_conversion,[],[f442]) ).
cnf(s65,plain,
( ~ spl0_3
| spl0_23
| spl0_48
| spl0_54 ),
inference(sat_conversion,[],[f445]) ).
cnf(s68,plain,
( ~ spl0_3
| spl0_27
| spl0_30 ),
inference(sat_conversion,[],[f451]) ).
cnf(s71,plain,
( ~ spl0_3
| spl0_28
| spl0_48
| spl0_62 ),
inference(sat_conversion,[],[f457]) ).
cnf(s73,plain,
( ~ spl0_50
| ~ spl0_63 ),
inference(sat_conversion,[],[f463]) ).
cnf(s74,plain,
( ~ spl0_48
| ~ spl0_64 ),
inference(sat_conversion,[],[f468]) ).
cnf(s75,plain,
( ~ spl0_48
| ~ spl0_65 ),
inference(sat_conversion,[],[f472]) ).
cnf(s76,plain,
( ~ spl0_46
| ~ spl0_66 ),
inference(sat_conversion,[],[f477]) ).
cnf(s77,plain,
( ~ spl0_46
| ~ spl0_67 ),
inference(sat_conversion,[],[f481]) ).
cnf(s78,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(sat_conversion,[],[f486]) ).
cnf(s79,plain,
( ~ spl0_42
| ~ spl0_69 ),
inference(sat_conversion,[],[f490]) ).
cnf(s80,plain,
( ~ spl0_49
| ~ spl0_70 ),
inference(sat_conversion,[],[f495]) ).
cnf(s81,plain,
( ~ spl0_49
| ~ spl0_71 ),
inference(sat_conversion,[],[f499]) ).
cnf(s82,plain,
( ~ spl0_49
| ~ spl0_72 ),
inference(sat_conversion,[],[f503]) ).
cnf(s83,plain,
( ~ spl0_47
| ~ spl0_73 ),
inference(sat_conversion,[],[f508]) ).
cnf(s84,plain,
( ~ spl0_47
| ~ spl0_74 ),
inference(sat_conversion,[],[f512]) ).
cnf(s85,plain,
( ~ spl0_52
| ~ spl0_75 ),
inference(sat_conversion,[],[f517]) ).
cnf(s89,plain,
( ~ spl0_33
| ~ spl0_79 ),
inference(sat_conversion,[],[f535]) ).
cnf(s90,plain,
( ~ spl0_60
| ~ spl0_80 ),
inference(sat_conversion,[],[f540]) ).
cnf(s91,plain,
( ~ spl0_60
| ~ spl0_81 ),
inference(sat_conversion,[],[f544]) ).
cnf(s92,plain,
( ~ spl0_60
| ~ spl0_82 ),
inference(sat_conversion,[],[f548]) ).
cnf(s93,plain,
( ~ spl0_54
| ~ spl0_83 ),
inference(sat_conversion,[],[f553]) ).
cnf(s94,plain,
( ~ spl0_54
| ~ spl0_84 ),
inference(sat_conversion,[],[f557]) ).
cnf(s95,plain,
( ~ spl0_54
| ~ spl0_85 ),
inference(sat_conversion,[],[f561]) ).
cnf(s96,plain,
( ~ spl0_53
| ~ spl0_86 ),
inference(sat_conversion,[],[f566]) ).
cnf(s97,plain,
( ~ spl0_35
| ~ spl0_87 ),
inference(sat_conversion,[],[f571]) ).
cnf(s98,plain,
( ~ spl0_35
| ~ spl0_88 ),
inference(sat_conversion,[],[f575]) ).
cnf(s99,plain,
( ~ spl0_35
| ~ spl0_89 ),
inference(sat_conversion,[],[f579]) ).
cnf(s100,plain,
( ~ spl0_32
| ~ spl0_90 ),
inference(sat_conversion,[],[f584]) ).
cnf(s101,plain,
( ~ spl0_32
| ~ spl0_91 ),
inference(sat_conversion,[],[f588]) ).
cnf(s102,plain,
( ~ spl0_44
| ~ spl0_92 ),
inference(sat_conversion,[],[f593]) ).
cnf(s103,plain,
( ~ spl0_41
| ~ spl0_93 ),
inference(sat_conversion,[],[f598]) ).
cnf(s105,plain,
( ~ spl0_55
| ~ spl0_95 ),
inference(sat_conversion,[],[f608]) ).
cnf(s106,plain,
( ~ spl0_55
| ~ spl0_96 ),
inference(sat_conversion,[],[f612]) ).
cnf(s107,plain,
( ~ spl0_37
| ~ spl0_97 ),
inference(sat_conversion,[],[f617]) ).
cnf(s108,plain,
( ~ spl0_30
| ~ spl0_98 ),
inference(sat_conversion,[],[f622]) ).
cnf(s109,plain,
( ~ spl0_30
| ~ spl0_99 ),
inference(sat_conversion,[],[f626]) ).
cnf(s110,plain,
( ~ spl0_39
| ~ spl0_100 ),
inference(sat_conversion,[],[f631]) ).
cnf(s111,plain,
( ~ spl0_36
| ~ spl0_101 ),
inference(sat_conversion,[],[f636]) ).
cnf(s112,plain,
( ~ spl0_40
| ~ spl0_102 ),
inference(sat_conversion,[],[f641]) ).
cnf(s113,plain,
( ~ spl0_40
| ~ spl0_103 ),
inference(sat_conversion,[],[f645]) ).
cnf(s116,plain,
( ~ spl0_58
| ~ spl0_106 ),
inference(sat_conversion,[],[f659]) ).
cnf(s117,plain,
( ~ spl0_51
| ~ spl0_107 ),
inference(sat_conversion,[],[f664]) ).
cnf(s118,plain,
( ~ spl0_50
| spl0_108 ),
inference(sat_conversion,[],[f668]) ).
cnf(s119,plain,
( ~ spl0_50
| spl0_109 ),
inference(sat_conversion,[],[f672]) ).
cnf(s120,plain,
( ~ spl0_48
| spl0_110 ),
inference(sat_conversion,[],[f676]) ).
cnf(s121,plain,
( ~ spl0_46
| spl0_111 ),
inference(sat_conversion,[],[f680]) ).
cnf(s122,plain,
( ~ spl0_42
| spl0_112 ),
inference(sat_conversion,[],[f684]) ).
cnf(s123,plain,
( ~ spl0_47
| spl0_113 ),
inference(sat_conversion,[],[f688]) ).
cnf(s124,plain,
( ~ spl0_52
| spl0_114 ),
inference(sat_conversion,[],[f692]) ).
cnf(s125,plain,
( ~ spl0_52
| spl0_115 ),
inference(sat_conversion,[],[f696]) ).
cnf(s127,plain,
( ~ spl0_33
| spl0_117 ),
inference(sat_conversion,[],[f704]) ).
cnf(s128,plain,
( ~ spl0_53
| spl0_118 ),
inference(sat_conversion,[],[f708]) ).
cnf(s129,plain,
( ~ spl0_53
| spl0_119 ),
inference(sat_conversion,[],[f712]) ).
cnf(s130,plain,
( ~ spl0_32
| spl0_120 ),
inference(sat_conversion,[],[f716]) ).
cnf(s131,plain,
( ~ spl0_44
| spl0_121 ),
inference(sat_conversion,[],[f720]) ).
cnf(s132,plain,
( ~ spl0_44
| spl0_122 ),
inference(sat_conversion,[],[f724]) ).
cnf(s133,plain,
( ~ spl0_41
| spl0_123 ),
inference(sat_conversion,[],[f728]) ).
cnf(s134,plain,
( ~ spl0_41
| spl0_124 ),
inference(sat_conversion,[],[f732]) ).
cnf(s137,plain,
( ~ spl0_55
| spl0_127 ),
inference(sat_conversion,[],[f744]) ).
cnf(s138,plain,
( ~ spl0_37
| spl0_128 ),
inference(sat_conversion,[],[f748]) ).
cnf(s139,plain,
( ~ spl0_37
| spl0_129 ),
inference(sat_conversion,[],[f752]) ).
cnf(s140,plain,
( ~ spl0_30
| spl0_130 ),
inference(sat_conversion,[],[f756]) ).
cnf(s141,plain,
( ~ spl0_39
| spl0_131 ),
inference(sat_conversion,[],[f760]) ).
cnf(s142,plain,
( ~ spl0_39
| spl0_132 ),
inference(sat_conversion,[],[f764]) ).
cnf(s143,plain,
( ~ spl0_36
| spl0_133 ),
inference(sat_conversion,[],[f768]) ).
cnf(s144,plain,
( ~ spl0_36
| spl0_134 ),
inference(sat_conversion,[],[f772]) ).
cnf(s145,plain,
( ~ spl0_40
| spl0_135 ),
inference(sat_conversion,[],[f776]) ).
cnf(s147,plain,
( ~ spl0_58
| spl0_137 ),
inference(sat_conversion,[],[f784]) ).
cnf(s148,plain,
( ~ spl0_58
| spl0_138 ),
inference(sat_conversion,[],[f788]) ).
cnf(s149,plain,
( ~ spl0_51
| spl0_139 ),
inference(sat_conversion,[],[f792]) ).
cnf(s150,plain,
( ~ spl0_51
| spl0_140 ),
inference(sat_conversion,[],[f796]) ).
cnf(s154,plain,
( ~ spl0_62
| spl0_144 ),
inference(sat_conversion,[],[f814]) ).
cnf(s155,plain,
( ~ spl0_62
| spl0_145 ),
inference(sat_conversion,[],[f818]) ).
cnf(s156,plain,
( ~ spl0_62
| spl0_146 ),
inference(sat_conversion,[],[f822]) ).
cnf(s157,plain,
( ~ spl0_38
| spl0_147 ),
inference(sat_conversion,[],[f827]) ).
cnf(s158,plain,
( ~ spl0_38
| spl0_148 ),
inference(sat_conversion,[],[f831]) ).
cnf(s159,plain,
( ~ spl0_38
| spl0_149 ),
inference(sat_conversion,[],[f835]) ).
cnf(s161,plain,
( ~ spl0_151
| spl0_152 ),
inference(sat_conversion,[],[f846]) ).
cnf(s162,plain,
( ~ spl0_151
| spl0_153 ),
inference(sat_conversion,[],[f850]) ).
cnf(s163,plain,
( spl0_35
| spl0_36
| spl0_53 ),
inference(sat_conversion,[],[f851]) ).
cnf(s164,plain,
( spl0_40
| spl0_50
| spl0_53 ),
inference(sat_conversion,[],[f852]) ).
cnf(s165,plain,
( spl0_30
| spl0_40
| spl0_55 ),
inference(sat_conversion,[],[f853]) ).
cnf(s166,plain,
( spl0_48
| spl0_49
| spl0_62 ),
inference(sat_conversion,[],[f854]) ).
cnf(s168,plain,
( spl0_30
| spl0_58
| spl0_151 ),
inference(sat_conversion,[],[f857]) ).
cnf(s169,plain,
( spl0_35
| spl0_39
| spl0_44 ),
inference(sat_conversion,[],[f858]) ).
cnf(s179,plain,
( spl0_3
| ~ spl0_60 ),
inference(sat_conversion,[],[f869]) ).
cnf(s197,plain,
( spl0_3
| ~ spl0_62 ),
inference(sat_conversion,[],[f887]) ).
cnf(s200,plain,
( spl0_60
| spl0_62 ),
inference(sat_conversion,[],[f890]) ).
cnf(s204,plain,
( ~ spl0_11
| ~ spl0_12
| spl0_43 ),
inference(sat_conversion,[],[f925]) ).
cnf(s207,plain,
( ~ spl0_2
| ~ spl0_17
| spl0_20 ),
inference(sat_conversion,[],[f942]) ).
cnf(s208,plain,
( ~ spl0_11
| ~ spl0_17
| spl0_43 ),
inference(sat_conversion,[],[f943]) ).
cnf(s217,plain,
( ~ spl0_15
| spl0_66
| spl0_67
| ~ spl0_111 ),
inference(sat_conversion,[],[f990]) ).
cnf(s219,plain,
( ~ spl0_15
| spl0_90
| ~ spl0_120
| spl0_156 ),
inference(sat_conversion,[],[f994]) ).
cnf(s225,plain,
( ~ spl0_23
| spl0_88
| spl0_89
| ~ spl0_159 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s230,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_26 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s233,plain,
( ~ spl0_11
| spl0_23
| ~ spl0_27 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s240,plain,
( ~ spl0_27
| spl0_87
| spl0_88
| ~ spl0_159 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s244,plain,
( ~ spl0_6
| spl0_70
| spl0_71
| ~ spl0_154 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s249,plain,
( ~ spl0_19
| ~ spl0_25
| spl0_43 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s252,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_109
| ~ spl0_162 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s257,plain,
( spl0_5
| ~ spl0_13
| ~ spl0_24 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s274,plain,
( ~ spl0_9
| spl0_75
| ~ spl0_115
| spl0_157 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s275,plain,
( ~ spl0_27
| spl0_100
| ~ spl0_131
| spl0_164 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s278,plain,
( ~ spl0_27
| spl0_102
| ~ spl0_135
| spl0_165 ),
inference(sat_conversion,[],[f1235]) ).
cnf(s300,plain,
( ~ spl0_7
| spl0_75
| ~ spl0_114
| ~ spl0_115 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s302,plain,
( spl0_5
| ~ spl0_7
| ~ spl0_27 ),
inference(sat_conversion,[],[f1305]) ).
cnf(s308,plain,
( spl0_5
| ~ spl0_8
| ~ spl0_27 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s321,plain,
( ~ spl0_12
| spl0_98
| ~ spl0_130
| ~ spl0_155 ),
inference(sat_conversion,[],[f1360]) ).
cnf(s323,plain,
( ~ spl0_5
| spl0_92
| ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f1370]) ).
cnf(s327,plain,
( ~ spl0_11
| ~ spl0_144
| ~ spl0_146
| spl0_167 ),
inference(sat_conversion,[],[f1396]) ).
cnf(s331,plain,
( ~ spl0_12
| spl0_107
| ~ spl0_139
| ~ spl0_169 ),
inference(sat_conversion,[],[f1410]) ).
cnf(s344,plain,
( ~ spl0_6
| spl0_107
| ~ spl0_139
| spl0_169 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s351,plain,
( ~ spl0_6
| ~ spl0_18
| spl0_20 ),
inference(sat_conversion,[],[f1485]) ).
cnf(s371,plain,
( ~ spl0_16
| spl0_107
| ~ spl0_140
| ~ spl0_169 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s399,plain,
( ~ spl0_18
| spl0_67
| ~ spl0_111
| spl0_158 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s412,plain,
( ~ spl0_17
| spl0_102
| spl0_103
| ~ spl0_165 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s414,plain,
( ~ spl0_17
| spl0_98
| spl0_99
| ~ spl0_130 ),
inference(sat_conversion,[],[f1560]) ).
cnf(s417,plain,
( ~ spl0_21
| spl0_88
| spl0_89
| spl0_159 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s432,plain,
( spl0_9
| ~ spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s435,plain,
( ~ spl0_18
| spl0_90
| spl0_91
| ~ spl0_120 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s443,plain,
( ~ spl0_19
| spl0_91
| ~ spl0_120
| ~ spl0_156 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s445,plain,
( ~ spl0_21
| spl0_80
| spl0_81
| spl0_82 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s446,plain,
( ~ spl0_21
| spl0_90
| spl0_91
| spl0_156 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s447,plain,
( ~ spl0_21
| spl0_66
| spl0_67
| spl0_158 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s449,plain,
( ~ spl0_8
| ~ spl0_108
| ~ spl0_109
| ~ spl0_162 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s454,plain,
( ~ spl0_13
| spl0_95
| ~ spl0_127
| spl0_161 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s458,plain,
( ~ spl0_1
| ~ spl0_139
| ~ spl0_140
| spl0_169 ),
inference(sat_conversion,[],[f1616]) ).
cnf(s459,plain,
( ~ spl0_1
| ~ spl0_152
| ~ spl0_153
| spl0_170 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s460,plain,
( ~ spl0_2
| spl0_90
| ~ spl0_120
| ~ spl0_156 ),
inference(sat_conversion,[],[f1628]) ).
cnf(s473,plain,
( ~ spl0_11
| spl0_106
| ~ spl0_137
| ~ spl0_138 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s476,plain,
( ~ spl0_11
| ~ spl0_108
| ~ spl0_109
| spl0_162 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s491,plain,
( ~ spl0_18
| spl0_79
| ~ spl0_117
| spl0_173 ),
inference(sat_conversion,[],[f1675]) ).
cnf(s495,plain,
( ~ spl0_12
| spl0_102
| ~ spl0_135
| ~ spl0_165 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s496,plain,
( ~ spl0_12
| spl0_100
| ~ spl0_131
| ~ spl0_164 ),
inference(sat_conversion,[],[f1680]) ).
cnf(s497,plain,
( spl0_9
| ~ spl0_13
| ~ spl0_15 ),
inference(sat_conversion,[],[f1681]) ).
cnf(s505,plain,
( ~ spl0_9
| spl0_66
| spl0_67
| ~ spl0_158 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s515,plain,
( ~ spl0_5
| spl0_63
| ~ spl0_109
| ~ spl0_162 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s536,plain,
( ~ spl0_24
| spl0_75
| ~ spl0_114
| ~ spl0_157 ),
inference(sat_conversion,[],[f1754]) ).
cnf(s541,plain,
( ~ spl0_20
| spl0_99
| ~ spl0_130
| spl0_155 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s548,plain,
( ~ spl0_1
| spl0_93
| ~ spl0_124
| ~ spl0_166 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s554,plain,
( ~ spl0_11
| spl0_79
| ~ spl0_117
| ~ spl0_173 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s555,plain,
( ~ spl0_11
| spl0_101
| ~ spl0_133
| ~ spl0_163 ),
inference(sat_conversion,[],[f1813]) ).
cnf(s558,plain,
( ~ spl0_16
| spl0_100
| ~ spl0_131
| ~ spl0_132 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s559,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s566,plain,
( spl0_4
| ~ spl0_16
| ~ spl0_22 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s575,plain,
( ~ spl0_4
| ~ spl0_139
| ~ spl0_140
| ~ spl0_169 ),
inference(sat_conversion,[],[f1881]) ).
cnf(s576,plain,
( ~ spl0_4
| ~ spl0_147
| ~ spl0_148
| ~ spl0_149 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s577,plain,
( ~ spl0_4
| ~ spl0_152
| ~ spl0_153
| ~ spl0_170 ),
inference(sat_conversion,[],[f1883]) ).
cnf(s581,plain,
( ~ spl0_28
| spl0_70
| spl0_72
| spl0_154 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s583,plain,
( ~ spl0_28
| spl0_87
| spl0_88
| spl0_89 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s586,plain,
( ~ spl0_29
| spl0_70
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s588,plain,
( ~ spl0_29
| spl0_87
| spl0_89
| spl0_159 ),
inference(sat_conversion,[],[f1959]) ).
cnf(s592,plain,
( ~ spl0_31
| spl0_83
| spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f1974]) ).
cnf(s593,plain,
( ~ spl0_31
| spl0_87
| spl0_88
| spl0_159 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s600,plain,
( ~ spl0_27
| spl0_73
| spl0_74
| ~ spl0_113 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s609,plain,
( ~ spl0_2
| spl0_93
| ~ spl0_123
| ~ spl0_124 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s613,plain,
( ~ spl0_9
| spl0_64
| spl0_65
| ~ spl0_110 ),
inference(sat_conversion,[],[f2034]) ).
cnf(s620,plain,
( ~ spl0_20
| spl0_68
| spl0_69
| ~ spl0_112 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s622,plain,
( ~ spl0_20
| spl0_93
| ~ spl0_124
| spl0_166 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s625,plain,
( ~ spl0_43
| spl0_101
| ~ spl0_134
| ~ spl0_163 ),
inference(sat_conversion,[],[f2045]) ).
cnf(s626,plain,
( ~ spl0_43
| spl0_99
| ~ spl0_130
| ~ spl0_155 ),
inference(sat_conversion,[],[f2046]) ).
cnf(s628,plain,
( ~ spl0_43
| spl0_86
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f2048]) ).
cnf(s651,plain,
( ~ spl0_6
| spl0_98
| ~ spl0_130
| spl0_155 ),
inference(sat_conversion,[],[f2071]) ).
cnf(s656,plain,
( ~ spl0_22
| ~ spl0_144
| ~ spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f2084]) ).
cnf(s657,plain,
( ~ spl0_25
| spl0_98
| spl0_99
| ~ spl0_155 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s659,plain,
( ~ spl0_2
| ~ spl0_133
| ~ spl0_134
| spl0_163 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s661,plain,
( ~ spl0_4
| ~ spl0_145
| ~ spl0_146
| ~ spl0_167 ),
inference(sat_conversion,[],[f2114]) ).
cnf(s664,plain,
( ~ spl0_7
| spl0_9
| ~ spl0_26 ),
inference(sat_conversion,[],[f2136]) ).
cnf(s667,plain,
( ~ spl0_8
| ~ spl0_144
| ~ spl0_146
| ~ spl0_167 ),
inference(sat_conversion,[],[f2157]) ).
cnf(s673,plain,
( ~ spl0_1
| spl0_96
| ~ spl0_127
| ~ spl0_161 ),
inference(sat_conversion,[],[f2200]) ).
cnf(s675,plain,
( ~ spl0_14
| spl0_97
| ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s677,plain,
( ~ spl0_25
| spl0_102
| spl0_103
| ~ spl0_135 ),
inference(sat_conversion,[],[f2249]) ).
cnf(s680,plain,
( ~ spl0_19
| spl0_101
| ~ spl0_133
| ~ spl0_134 ),
inference(sat_conversion,[],[f2250]) ).
cnf(s683,plain,
( ~ spl0_19
| ~ spl0_144
| ~ spl0_145
| spl0_167 ),
inference(sat_conversion,[],[f2289]) ).
cnf(s687,plain,
spl0_3,
inference(rat,[],[s200,s179,s197]) ).
cnf(s688,plain,
( ~ spl0_30
| ~ spl0_12
| ~ spl0_20 ),
inference(rat,[],[s321,s541,s108,s109,s140]) ).
cnf(s691,plain,
( ~ spl0_40
| ~ spl0_25 ),
inference(rat,[],[s677,s112,s113,s145]) ).
cnf(s692,plain,
( ~ spl0_46
| ~ spl0_18
| ~ spl0_9 ),
inference(rat,[],[s505,s399,s76,s77,s121]) ).
cnf(s695,plain,
( ~ spl0_39
| ~ spl0_16 ),
inference(rat,[],[s558,s110,s141,s142]) ).
cnf(s698,plain,
( ~ spl0_60
| ~ spl0_21 ),
inference(rat,[],[s445,s90,s91,s92]) ).
cnf(s699,plain,
( spl0_11
| spl0_7
| spl0_2
| spl0_1 ),
inference(rat,[],[s240,s417,s97,s98,s99,s29,s683,s661,s154,s155,s156,s200,s698,s17,s675,s107,s138,s139,s53,s68,s688,s5,s12,s1,s687]) ).
cnf(s700,plain,
( ~ spl0_62
| ~ spl0_11
| ~ spl0_4 ),
inference(rat,[],[s327,s661,s154,s155,s156]) ).
cnf(s701,plain,
( ~ spl0_35
| ~ spl0_31
| ~ spl0_23 ),
inference(rat,[],[s593,s225,s97,s98,s99]) ).
cnf(s702,plain,
( ~ spl0_44
| ~ spl0_5 ),
inference(rat,[],[s323,s102,s131,s132]) ).
cnf(s703,plain,
( ~ spl0_48
| ~ spl0_9 ),
inference(rat,[],[s613,s74,s75,s120]) ).
cnf(s704,plain,
( spl0_39
| ~ spl0_23
| spl0_44
| spl0_1 ),
inference(rat,[],[s701,s169,s43,s687]) ).
cnf(s705,plain,
( spl0_7
| spl0_6
| spl0_2
| spl0_1 ),
inference(rat,[],[s583,s97,s98,s99,s26,s695,s704,s233,s42,s71,s703,s700,s699,s9,s1,s702,s2,s687]) ).
cnf(s706,plain,
( spl0_39
| ~ spl0_27
| spl0_44
| spl0_1 ),
inference(rat,[],[s240,s593,s97,s98,s169,s43,s687]) ).
cnf(s707,plain,
( ~ spl0_27
| ~ spl0_12
| spl0_44
| spl0_1 ),
inference(rat,[],[s496,s275,s110,s141,s706]) ).
cnf(s708,plain,
( spl0_27
| ~ spl0_7
| spl0_6
| spl0_2 ),
inference(rat,[],[s691,s33,s18,s664,s703,s42,s687]) ).
cnf(s709,plain,
( spl0_6
| spl0_2
| spl0_1 ),
inference(rat,[],[s583,s97,s98,s99,s26,s19,s695,s707,s706,s708,s705,s702,s2,s687]) ).
cnf(s710,plain,
( ~ spl0_12
| spl0_2
| spl0_1 ),
inference(rat,[],[s651,s321,s108,s140,s68,s707,s702,s2,s709,s687]) ).
cnf(s711,plain,
( spl0_16
| spl0_2
| spl0_1 ),
inference(rat,[],[s217,s76,s77,s121,s40,s491,s554,s89,s127,s34,s703,s71,s583,s97,s98,s99,s8,s26,s700,s5,s710,s1,s687]) ).
cnf(s712,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s476,s252,s118,s119,s47,s706,s695,s711,s698,s200,s700,s5,s710,s702,s1,s2,s687]) ).
cnf(s713,plain,
( spl0_16
| ~ spl0_27
| spl0_11
| spl0_1 ),
inference(rat,[],[s417,s17,s240,s675,s97,s98,s99,s107,s138,s139,s26,s28,s687]) ).
cnf(s714,plain,
( ~ spl0_27
| spl0_11
| spl0_1 ),
inference(rat,[],[s344,s371,s117,s149,s150,s3,s48,s302,s308,s702,s706,s695,s713,s687]) ).
cnf(s715,plain,
( ~ spl0_41
| ~ spl0_2 ),
inference(rat,[],[s609,s103,s133,s134]) ).
cnf(s716,plain,
( spl0_11
| spl0_1 ),
inference(rat,[],[s17,s446,s460,s432,s100,s101,s130,s35,s62,s703,s42,s651,s414,s657,s108,s109,s140,s18,s68,s714,s230,s715,s712,s687]) ).
cnf(s717,plain,
( ~ spl0_36
| spl0_1 ),
inference(rat,[],[s555,s659,s111,s143,s144,s712,s716]) ).
cnf(s718,plain,
( ~ spl0_2
| spl0_1 ),
inference(rat,[],[s14,s651,s249,s657,s108,s109,s140,s18,s68,s600,s83,s84,s123,s41,s435,s100,s101,s130,s62,s208,s628,s96,s128,s129,s52,s717,s716,s715,s230,s687]) ).
cnf(s719,plain,
spl0_1,
inference(rat,[],[s718,s712]) ).
cnf(s720,plain,
( ~ spl0_62
| ~ spl0_22 ),
inference(rat,[],[s656,s154,s155,s156]) ).
cnf(s721,plain,
( ~ spl0_35
| ~ spl0_27
| spl0_2
| spl0_11 ),
inference(rat,[],[s622,s21,s548,s103,s134,s35,s432,s703,s71,s720,s17,s13,s588,s417,s240,s583,s97,s98,s99,s687,s719]) ).
cnf(s722,plain,
( ~ spl0_39
| ~ spl0_27
| ~ spl0_12 ),
inference(rat,[],[s496,s275,s110,s141]) ).
cnf(s723,plain,
( ~ spl0_51
| ~ spl0_12 ),
inference(rat,[],[s331,s458,s117,s149,s150,s719]) ).
cnf(s724,plain,
( ~ spl0_27
| spl0_2
| spl0_11 ),
inference(rat,[],[s702,s169,s308,s722,s721,s48,s723,s5,s687]) ).
cnf(s725,plain,
( spl0_2
| spl0_11 ),
inference(rat,[],[s708,s651,s12,s321,s688,s108,s140,s68,s724,s5,s687]) ).
cnf(s726,plain,
( ~ spl0_18
| spl0_19
| ~ spl0_9
| ~ spl0_2 ),
inference(rat,[],[s435,s100,s101,s130,s62,s207,s620,s78,s79,s122,s54,s692,s715,s687]) ).
cnf(s727,plain,
( ~ spl0_55
| ~ spl0_13 ),
inference(rat,[],[s454,s673,s105,s106,s137,s719]) ).
cnf(s728,plain,
( ~ spl0_40
| ~ spl0_12
| ~ spl0_27 ),
inference(rat,[],[s278,s495,s112,s145]) ).
cnf(s729,plain,
( ~ spl0_12
| ~ spl0_27
| spl0_11 ),
inference(rat,[],[s651,s321,s108,s140,s165,s728,s14,s726,s683,s667,s154,s155,s156,s71,s703,s432,s17,s417,s240,s583,s97,s98,s99,s169,s702,s308,s48,s722,s723,s727,s35,s715,s725,s687]) ).
cnf(s730,plain,
( ~ spl0_36
| ~ spl0_43
| ~ spl0_2 ),
inference(rat,[],[s625,s659,s111,s143,s144]) ).
cnf(s731,plain,
( ~ spl0_40
| spl0_36
| spl0_22
| ~ spl0_27
| ~ spl0_2 ),
inference(rat,[],[s219,s27,s460,s576,s100,s130,s157,s158,s159,s62,s30,s412,s278,s691,s112,s113,s145,s715,s687]) ).
cnf(s732,plain,
( ~ spl0_35
| ~ spl0_27
| spl0_11 ),
inference(rat,[],[s651,s626,s108,s109,s140,s165,s731,s730,s720,s46,s71,s703,s432,s17,s588,s417,s19,s240,s583,s97,s98,s99,s727,s35,s715,s725,s729,s687]) ).
cnf(s733,plain,
( ~ spl0_36
| ~ spl0_19 ),
inference(rat,[],[s680,s111,s143,s144]) ).
cnf(s734,plain,
( ~ spl0_27
| spl0_11 ),
inference(rat,[],[s600,s83,s84,s123,s56,s628,s96,s128,s129,s163,s733,s29,s732,s727,s35,s715,s725,s687]) ).
cnf(s735,plain,
( ~ spl0_54
| ~ spl0_31 ),
inference(rat,[],[s592,s93,s94,s95]) ).
cnf(s736,plain,
( ~ spl0_49
| ~ spl0_29 ),
inference(rat,[],[s586,s80,s81,s82]) ).
cnf(s737,plain,
spl0_11,
inference(rat,[],[s683,s661,s154,s155,s156,s166,s736,s27,s733,s29,s701,s65,s735,s46,s626,s651,s42,s703,s432,s23,s17,s219,s446,s460,s100,s101,s130,s62,s414,s108,s109,s140,s68,s734,s35,s715,s725,s687]) ).
cnf(s738,plain,
( ~ spl0_35
| spl0_48
| ~ spl0_23
| spl0_2 ),
inference(rat,[],[s720,s13,s71,s417,s583,s225,s97,s98,s99,s687]) ).
cnf(s739,plain,
( ~ spl0_12
| spl0_35
| ~ spl0_27 ),
inference(rat,[],[s702,s308,s169,s48,s722,s723,s687]) ).
cnf(s740,plain,
( spl0_46
| spl0_29
| spl0_12
| ~ spl0_9 ),
inference(rat,[],[s536,s274,s85,s124,s125,s45,s49,s687]) ).
cnf(s741,plain,
( spl0_62
| spl0_12
| spl0_35
| ~ spl0_9 ),
inference(rat,[],[s628,s96,s128,s129,s163,s733,s14,s692,s740,s244,s46,s581,s736,s80,s81,s82,s166,s71,s703,s687]) ).
cnf(s742,plain,
( spl0_30
| spl0_55
| spl0_10
| spl0_8
| ~ spl0_21 ),
inference(rat,[],[s446,s443,s100,s101,s130,s31,s691,s22,s165,s687]) ).
cnf(s743,plain,
( ~ spl0_47
| ~ spl0_27 ),
inference(rat,[],[s600,s83,s84,s123]) ).
cnf(s744,plain,
( ~ spl0_46
| ~ spl0_21
| ~ spl0_9 ),
inference(rat,[],[s447,s505,s76,s77]) ).
cnf(s745,plain,
( ~ spl0_32
| ~ spl0_18 ),
inference(rat,[],[s435,s100,s101,s130]) ).
cnf(s746,plain,
( ~ spl0_9
| ~ spl0_27
| spl0_2 ),
inference(rat,[],[s541,s626,s109,s140,s56,s165,s727,s691,s24,s31,s745,s351,s3,s300,s85,s124,s125,s40,s49,s744,s667,s13,s327,s720,s154,s156,s741,s739,s738,s703,s233,s743,s687,s737]) ).
cnf(s747,plain,
~ spl0_58,
inference(rat,[],[s473,s116,s147,s148,s737]) ).
cnf(s748,plain,
( spl0_13
| spl0_39
| ~ spl0_27 ),
inference(rat,[],[s728,s58,s32,s687,s747]) ).
cnf(s749,plain,
( ~ spl0_50
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s476,s252,s118,s119,s737]) ).
cnf(s750,plain,
( ~ spl0_53
| ~ spl0_43 ),
inference(rat,[],[s628,s96,s128,s129]) ).
cnf(s751,plain,
( ~ spl0_30
| ~ spl0_6
| ~ spl0_43 ),
inference(rat,[],[s651,s626,s108,s109,s140]) ).
cnf(s752,plain,
( ~ spl0_152
| ~ spl0_153
| ~ spl0_4 ),
inference(rat,[],[s459,s577,s719]) ).
cnf(s753,plain,
( spl0_21
| ~ spl0_27
| spl0_2 ),
inference(rat,[],[s752,s161,s162,s168,s751,s19,s728,s164,s749,s583,s97,s98,s99,s169,s702,s257,s16,s566,s13,s432,s748,s695,s8,s217,s76,s77,s121,s40,s750,s41,s491,s554,s89,s127,s34,s746,s743,s747,s687,s737]) ).
cnf(s754,plain,
( ~ spl0_27
| spl0_2 ),
inference(rat,[],[s751,s3,s742,s667,s559,s327,s664,s700,s154,s156,s60,s200,s698,s753,s750,s727,s748,s695,s8,s217,s76,s77,s121,s41,s40,s491,s554,s89,s127,s34,s746,s743,s687,s737]) ).
cnf(s755,plain,
( ~ spl0_43
| spl0_2 ),
inference(rat,[],[s417,s225,s47,s98,s99,s749,s27,s163,s7,s733,s497,s432,s14,s20,s15,s491,s554,s89,s127,s34,s703,s42,s751,s750,s68,s754,s687,s737]) ).
cnf(s756,plain,
( spl0_21
| spl0_9
| ~ spl0_13
| spl0_2 ),
inference(rat,[],[s257,s749,s566,s16,s47,s13,s754,s432,s8,s497,s687]) ).
cnf(s757,plain,
( spl0_9
| ~ spl0_13
| spl0_2 ),
inference(rat,[],[s371,s458,s117,s149,s150,s48,s667,s327,s154,s156,s200,s698,s756,s8,s497,s719,s687,s737]) ).
cnf(s758,plain,
( ~ spl0_9
| spl0_2 ),
inference(rat,[],[s745,s40,s31,s744,s667,s13,s327,s720,s154,s156,s166,s657,s736,s651,s46,s42,s703,s140,s109,s108,s68,s754,s755,s687,s737]) ).
cnf(s759,plain,
spl0_2,
inference(rat,[],[s217,s76,s77,s121,s40,s8,s491,s695,s554,s32,s89,s127,s757,s34,s758,s204,s755,s687,s737]) ).
cnf(s760,plain,
~ spl0_41,
inference(rat,[],[s715,s759]) ).
cnf(s761,plain,
( spl0_9
| ~ spl0_13
| ~ spl0_27 ),
inference(rat,[],[s752,s161,s162,s168,s751,s19,s728,s164,s749,s257,s27,s16,s497,s432,s583,s97,s417,s225,s233,s98,s99,s163,s750,s730,s56,s727,s743,s747,s687,s759,s737]) ).
cnf(s762,plain,
( ~ spl0_13
| ~ spl0_27 ),
inference(rat,[],[s19,s723,s751,s48,s165,s667,s731,s327,s720,s154,s156,s71,s703,s761,s583,s97,s98,s99,s163,s750,s730,s56,s727,s743,s687,s759,s737]) ).
cnf(s763,plain,
~ spl0_27,
inference(rat,[],[s752,s161,s162,s168,s751,s20,s41,s745,s10,s62,s412,s278,s112,s113,s145,s58,s762,s743,s747,s687,s760]) ).
cnf(s764,plain,
spl0_30,
inference(rat,[],[s68,s687,s763]) ).
cnf(s765,plain,
spl0_130,
inference(rat,[],[s140,s764]) ).
cnf(s766,plain,
~ spl0_99,
inference(rat,[],[s109,s764]) ).
cnf(s767,plain,
~ spl0_98,
inference(rat,[],[s108,s764]) ).
cnf(s768,plain,
~ spl0_17,
inference(rat,[],[s414,s765,s767,s766]) ).
cnf(s769,plain,
spl0_32,
inference(rat,[],[s62,s760,s687,s768]) ).
cnf(s770,plain,
spl0_120,
inference(rat,[],[s130,s769]) ).
cnf(s771,plain,
~ spl0_91,
inference(rat,[],[s101,s769]) ).
cnf(s772,plain,
~ spl0_90,
inference(rat,[],[s100,s769]) ).
cnf(s773,plain,
~ spl0_18,
inference(rat,[],[s745,s769]) ).
cnf(s774,plain,
~ spl0_156,
inference(rat,[],[s460,s759,s770,s772]) ).
cnf(s775,plain,
~ spl0_15,
inference(rat,[],[s219,s772,s770,s774]) ).
cnf(s776,plain,
~ spl0_21,
inference(rat,[],[s446,s771,s772,s774]) ).
cnf(s777,plain,
spl0_50,
inference(rat,[],[s47,s763,s687,s776]) ).
cnf(s779,plain,
spl0_109,
inference(rat,[],[s119,s777]) ).
cnf(s780,plain,
spl0_108,
inference(rat,[],[s118,s777]) ).
cnf(s781,plain,
~ spl0_63,
inference(rat,[],[s73,s777]) ).
cnf(s783,plain,
spl0_162,
inference(rat,[],[s476,s737,s779,s780]) ).
cnf(s785,plain,
~ spl0_8,
inference(rat,[],[s449,s779,s780,s783]) ).
cnf(s786,plain,
~ spl0_5,
inference(rat,[],[s515,s779,s781,s783]) ).
cnf(s789,plain,
spl0_51,
inference(rat,[],[s48,s687,s785]) ).
cnf(s790,plain,
spl0_19,
inference(rat,[],[s11,s773,s687,s786]) ).
cnf(s792,plain,
spl0_140,
inference(rat,[],[s150,s789]) ).
cnf(s793,plain,
spl0_139,
inference(rat,[],[s149,s789]) ).
cnf(s796,plain,
~ spl0_36,
inference(rat,[],[s733,s790]) ).
cnf(s800,plain,
spl0_169,
inference(rat,[],[s458,s719,s792,s793]) ).
cnf(s801,plain,
spl0_4,
inference(rat,[],[s27,s687,s775,s796]) ).
cnf(s804,plain,
$false,
inference(rat,[],[s575,s792,s793,s801,s800]) ).
fof(f2291,plain,
$false,
inference(avatar_sat_refutation,[],[s804]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN500-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n020.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:18:19 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.10/1.14 % (280631)Input is clausal, will run a generic CNF schedule.
% 1.10/1.14 % (280636)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4206522100:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 1.10/1.14 % (280637)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2735957384:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 1.10/1.14 % (280642)dis-21_1_sil=8000:lcm=predicate:random_seed=1163843075:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 1.10/1.14 % (280640)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2206396759:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 1.10/1.14 % (280638)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2876862865:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 1.10/1.14 % (280639)lrs+10_1_sil=8000:sp=occurrence:random_seed=4224627883:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 1.10/1.14 % (280641)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3989485591:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 1.10/1.14 % (280642)First to succeed.
% 1.10/1.14 % (280642)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-280631"
% 1.10/1.14 % (280640)Also succeeded, but the first one will report.
% 1.10/1.14 % (280639)Also succeeded, but the first one will report.
% 1.10/1.14 % (280641)Also succeeded, but the first one will report.
% 1.10/1.14 % (280642)Refutation found. Thanks to Tanya!
% 1.10/1.14 % SZS status Unsatisfiable for theBenchmark
% 1.10/1.14 % SZS output start Proof for theBenchmark
% See solution above
% 3.97/1.34 % (280642)------------------------------
% 3.97/1.34 % (280642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.97/1.34 % (280642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.34 % (280642)CaDiCaL version: 2.1.3
% 3.97/1.34 % (280642)Termination reason: Refutation
% 3.97/1.34 % (280642)Time elapsed: 0.036 s
% 3.97/1.34 % (280642)Peak memory usage: 90 MB
% 3.97/1.34 % (280642)Instructions burned: 57 (million)
% 3.97/1.34 % (280642)------------------------------
% 3.97/1.34 % (280642)------------------------------
% 3.97/1.34 % (280631)Success in time 0.475 s
% 3.97/1.34 % Vampire exiting
%------------------------------------------------------------------------------