%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN461+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:09:25 PM UTC 2026
% Result : Theorem 0.08s 0.18s
% Output : Refutation 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a1168)
& c1_1(a1168)
& ~ c2_1(a1168) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a1169)
& ~ c2_1(a1169)
& ~ c3_1(a1169) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1172)
& c3_1(a1172)
& ~ c0_1(a1172) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a1174)
& c1_1(a1174)
& ~ c3_1(a1174) ) )
& ( ~ hskp4
| ( ndr1_0
& c1_1(a1175)
& c2_1(a1175)
& ~ c0_1(a1175) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a1176)
& c2_1(a1176)
& ~ c3_1(a1176) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a1178)
& c2_1(a1178)
& ~ c3_1(a1178) ) )
& ( ~ hskp7
| ( ndr1_0
& ~ c1_1(a1179)
& ~ c2_1(a1179)
& ~ c3_1(a1179) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a1180)
& ~ c0_1(a1180)
& ~ c3_1(a1180) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a1181)
& c3_1(a1181)
& ~ c2_1(a1181) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a1184)
& ~ c1_1(a1184)
& ~ c2_1(a1184) ) )
& ( ~ hskp11
| ( ndr1_0
& c0_1(a1186)
& ~ c2_1(a1186)
& ~ c3_1(a1186) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c0_1(a1187)
& ~ c2_1(a1187)
& ~ c3_1(a1187) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a1192)
& ~ c0_1(a1192)
& ~ c2_1(a1192) ) )
& ( ~ hskp14
| ( ndr1_0
& c2_1(a1194)
& ~ c0_1(a1194)
& ~ c1_1(a1194) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a1195)
& ~ c1_1(a1195)
& ~ c3_1(a1195) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1199)
& ~ c0_1(a1199)
& ~ c3_1(a1199) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a1200)
& ~ c1_1(a1200)
& ~ c2_1(a1200) ) )
& ( ~ hskp18
| ( ndr1_0
& c1_1(a1202)
& c3_1(a1202)
& ~ c0_1(a1202) ) )
& ( ~ hskp19
| ( ndr1_0
& c3_1(a1204)
& ~ c1_1(a1204)
& ~ c2_1(a1204) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a1205)
& c3_1(a1205)
& ~ c2_1(a1205) ) )
& ( ~ hskp21
| ( ndr1_0
& c2_1(a1207)
& c3_1(a1207)
& ~ c1_1(a1207) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a1211)
& c3_1(a1211)
& ~ c1_1(a1211) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a1218)
& ~ c1_1(a1218)
& ~ c3_1(a1218) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a1232)
& ~ c0_1(a1232)
& ~ c1_1(a1232) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a1182)
& c2_1(a1182)
& c3_1(a1182) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a1190)
& c1_1(a1190)
& c3_1(a1190) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a1201)
& c1_1(a1201)
& c2_1(a1201) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a1236)
& c2_1(a1236)
& c3_1(a1236) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c1_1(X4)
| c2_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| ! [X6] :
( ndr1_0
=> ( c2_1(X6)
| ~ c0_1(X6)
| ~ c3_1(X6) ) )
| hskp1 )
& ( ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c3_1(X8)
| ~ c0_1(X8)
| ~ c2_1(X8) ) )
| hskp0 )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| ~ c2_1(X10) ) )
| hskp0 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| ! [X15] :
( ndr1_0
=> ( c1_1(X15)
| c3_1(X15)
| ~ c0_1(X15) ) )
| hskp2 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| c3_1(X16) ) )
| hskp0
| hskp3 )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21) ) )
| hskp4 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c1_1(X23)
| c2_1(X23)
| c3_1(X23) ) )
| hskp5 )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c2_1(X24)
| c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c1_1(X25)
| ~ c0_1(X25)
| ~ c2_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( c1_1(X26)
| ~ c0_1(X26)
| ~ c3_1(X26) ) ) )
& ( ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c2_1(X27)
| c3_1(X27) ) )
| hskp3
| hskp6 )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c1_1(X29)
| c2_1(X29)
| ~ c0_1(X29) ) )
| hskp7 )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c2_1(X30)
| ~ c1_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c3_1(X31)
| ~ c0_1(X31)
| ~ c2_1(X31) ) )
| hskp8 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| ~ c1_1(X32) ) )
| hskp9
| hskp25 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c3_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c2_1(X34)
| ~ c3_1(X34) ) )
| hskp1 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c3_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36) ) )
| hskp10 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c3_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c2_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38) ) )
| hskp3 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c3_1(X39)
| ~ c2_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c2_1(X40)
| c3_1(X40)
| ~ c0_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c0_1(X41)
| ~ c1_1(X41)
| ~ c2_1(X41) ) ) )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| ~ c1_1(X42)
| ~ c2_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| ~ c0_1(X43)
| ~ c2_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( ~ c0_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46) ) )
| hskp11 )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| ~ c1_1(X47)
| ~ c3_1(X47) ) )
| ! [X48] :
( ndr1_0
=> ( c1_1(X48)
| ~ c0_1(X48)
| ~ c2_1(X48) ) )
| hskp12 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c1_1(X49)
| ~ c3_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c3_1(X50)
| ~ c0_1(X50)
| ~ c2_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51) ) ) )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52) ) )
| hskp5
| hskp4 )
& ( ! [X53] :
( ndr1_0
=> ( c1_1(X53)
| c2_1(X53)
| c3_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c1_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| hskp26 )
& ( ! [X55] :
( ndr1_0
=> ( c1_1(X55)
| c2_1(X55)
| c3_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c2_1(X56)
| ~ c0_1(X56)
| ~ c1_1(X56) ) )
| hskp6 )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c2_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58) ) )
| hskp13 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| c3_1(X59) ) )
| ! [X60] :
( ndr1_0
=> ( ~ c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60) ) )
| hskp3 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| c3_1(X61) ) )
| hskp14
| hskp15 )
& ( ! [X62] :
( ndr1_0
=> ( c1_1(X62)
| c2_1(X62)
| ~ c0_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| ~ c0_1(X63)
| ~ c3_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c2_1(X65)
| ~ c0_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66) ) ) )
& ( ! [X67] :
( ndr1_0
=> ( c1_1(X67)
| c2_1(X67)
| ~ c0_1(X67) ) )
| hskp0 )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c2_1(X68)
| ~ c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c0_1(X69)
| ~ c1_1(X69) ) )
| hskp11 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70) ) )
| hskp0
| hskp16 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c2_1(X72)
| c3_1(X72)
| ~ c0_1(X72) ) )
| hskp17 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c0_1(X73)
| ~ c2_1(X73) ) )
| hskp27
| hskp18 )
& ( ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c3_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( ~ c0_1(X76)
| ~ c1_1(X76)
| ~ c2_1(X76) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77) ) )
| hskp13
| hskp19 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| ~ c2_1(X78)
| ~ c3_1(X78) ) )
| hskp20
| hskp12 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79) ) )
| hskp21
| hskp12 )
& ( ! [X80] :
( ndr1_0
=> ( c2_1(X80)
| c3_1(X80)
| ~ c0_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) )
| hskp11 )
& ( ! [X82] :
( ndr1_0
=> ( c2_1(X82)
| c3_1(X82)
| ~ c0_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83) ) )
| hskp13 )
& ( ! [X84] :
( ndr1_0
=> ( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84) ) )
| hskp22
| hskp17 )
& ( ! [X85] :
( ndr1_0
=> ( c2_1(X85)
| c3_1(X85)
| ~ c0_1(X85) ) )
| hskp22
| hskp14 )
& ( ! [X86] :
( ndr1_0
=> ( c2_1(X86)
| c3_1(X86)
| ~ c0_1(X86) ) )
| hskp9
| hskp18 )
& ( ! [X87] :
( ndr1_0
=> ( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87) ) )
| hskp19
| hskp23 )
& ( ! [X88] :
( ndr1_0
=> ( c2_1(X88)
| ~ c0_1(X88)
| ~ c1_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c0_1(X89)
| ~ c1_1(X89) ) )
| hskp25 )
& ( ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| ~ c1_1(X90)
| ~ c3_1(X90) ) )
| hskp26
| hskp8 )
& ( ! [X91] :
( ndr1_0
=> ( c3_1(X91)
| ~ c0_1(X91)
| ~ c2_1(X91) ) )
| hskp22
| hskp14 )
& ( ! [X92] :
( ndr1_0
=> ( c3_1(X92)
| ~ c0_1(X92)
| ~ c2_1(X92) ) )
| hskp11
| hskp15 )
& ( ! [X93] :
( ndr1_0
=> ( ~ c0_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93) ) )
| hskp22
| hskp2 )
& ( ! [X94] :
( ndr1_0
=> ( ~ c0_1(X94)
| ~ c2_1(X94)
| ~ c3_1(X94) ) )
| hskp13
| hskp10 )
& ( hskp26
| hskp17
| hskp24 )
& ( hskp0
| hskp1
| hskp14 )
& ( hskp28
| hskp8 )
& ( hskp17
| hskp13
| hskp2 )
& ( hskp17
| hskp1
| hskp16 )
& ( hskp6
| hskp21
| hskp14 )
& ( hskp8
| hskp21
| hskp19 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a1168)
& c1_1(a1168)
& ~ c2_1(a1168) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a1169)
& ~ c2_1(a1169)
& ~ c3_1(a1169) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1172)
& c3_1(a1172)
& ~ c0_1(a1172) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a1174)
& c1_1(a1174)
& ~ c3_1(a1174) ) )
& ( ~ hskp4
| ( ndr1_0
& c1_1(a1175)
& c2_1(a1175)
& ~ c0_1(a1175) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a1176)
& c2_1(a1176)
& ~ c3_1(a1176) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a1178)
& c2_1(a1178)
& ~ c3_1(a1178) ) )
& ( ~ hskp7
| ( ndr1_0
& ~ c1_1(a1179)
& ~ c2_1(a1179)
& ~ c3_1(a1179) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a1180)
& ~ c0_1(a1180)
& ~ c3_1(a1180) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a1181)
& c3_1(a1181)
& ~ c2_1(a1181) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a1184)
& ~ c1_1(a1184)
& ~ c2_1(a1184) ) )
& ( ~ hskp11
| ( ndr1_0
& c0_1(a1186)
& ~ c2_1(a1186)
& ~ c3_1(a1186) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c0_1(a1187)
& ~ c2_1(a1187)
& ~ c3_1(a1187) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a1192)
& ~ c0_1(a1192)
& ~ c2_1(a1192) ) )
& ( ~ hskp14
| ( ndr1_0
& c2_1(a1194)
& ~ c0_1(a1194)
& ~ c1_1(a1194) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a1195)
& ~ c1_1(a1195)
& ~ c3_1(a1195) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1199)
& ~ c0_1(a1199)
& ~ c3_1(a1199) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a1200)
& ~ c1_1(a1200)
& ~ c2_1(a1200) ) )
& ( ~ hskp18
| ( ndr1_0
& c1_1(a1202)
& c3_1(a1202)
& ~ c0_1(a1202) ) )
& ( ~ hskp19
| ( ndr1_0
& c3_1(a1204)
& ~ c1_1(a1204)
& ~ c2_1(a1204) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a1205)
& c3_1(a1205)
& ~ c2_1(a1205) ) )
& ( ~ hskp21
| ( ndr1_0
& c2_1(a1207)
& c3_1(a1207)
& ~ c1_1(a1207) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a1211)
& c3_1(a1211)
& ~ c1_1(a1211) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a1218)
& ~ c1_1(a1218)
& ~ c3_1(a1218) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a1232)
& ~ c0_1(a1232)
& ~ c1_1(a1232) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a1182)
& c2_1(a1182)
& c3_1(a1182) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a1190)
& c1_1(a1190)
& c3_1(a1190) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a1201)
& c1_1(a1201)
& c2_1(a1201) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a1236)
& c2_1(a1236)
& c3_1(a1236) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c1_1(X4)
| c2_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| ! [X6] :
( ndr1_0
=> ( c2_1(X6)
| ~ c0_1(X6)
| ~ c3_1(X6) ) )
| hskp1 )
& ( ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c3_1(X8)
| ~ c0_1(X8)
| ~ c2_1(X8) ) )
| hskp0 )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| ~ c2_1(X10) ) )
| hskp0 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| ! [X15] :
( ndr1_0
=> ( c1_1(X15)
| c3_1(X15)
| ~ c0_1(X15) ) )
| hskp2 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| c3_1(X16) ) )
| hskp0
| hskp3 )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21) ) )
| hskp4 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c1_1(X23)
| c2_1(X23)
| c3_1(X23) ) )
| hskp5 )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c2_1(X24)
| c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c1_1(X25)
| ~ c0_1(X25)
| ~ c2_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( c1_1(X26)
| ~ c0_1(X26)
| ~ c3_1(X26) ) ) )
& ( ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c2_1(X27)
| c3_1(X27) ) )
| hskp3
| hskp6 )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c1_1(X29)
| c2_1(X29)
| ~ c0_1(X29) ) )
| hskp7 )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c2_1(X30)
| ~ c1_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c3_1(X31)
| ~ c0_1(X31)
| ~ c2_1(X31) ) )
| hskp8 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| ~ c1_1(X32) ) )
| hskp9
| hskp25 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c3_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c2_1(X34)
| ~ c3_1(X34) ) )
| hskp1 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c3_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36) ) )
| hskp10 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c3_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c2_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38) ) )
| hskp3 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c3_1(X39)
| ~ c2_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c2_1(X40)
| c3_1(X40)
| ~ c0_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c0_1(X41)
| ~ c1_1(X41)
| ~ c2_1(X41) ) ) )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| ~ c1_1(X42)
| ~ c2_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| ~ c0_1(X43)
| ~ c2_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( ~ c0_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46) ) )
| hskp11 )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| ~ c1_1(X47)
| ~ c3_1(X47) ) )
| ! [X48] :
( ndr1_0
=> ( c1_1(X48)
| ~ c0_1(X48)
| ~ c2_1(X48) ) )
| hskp12 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c1_1(X49)
| ~ c3_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c3_1(X50)
| ~ c0_1(X50)
| ~ c2_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51) ) ) )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52) ) )
| hskp5
| hskp4 )
& ( ! [X53] :
( ndr1_0
=> ( c1_1(X53)
| c2_1(X53)
| c3_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c1_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| hskp26 )
& ( ! [X55] :
( ndr1_0
=> ( c1_1(X55)
| c2_1(X55)
| c3_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c2_1(X56)
| ~ c0_1(X56)
| ~ c1_1(X56) ) )
| hskp6 )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c2_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58) ) )
| hskp13 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| c3_1(X59) ) )
| ! [X60] :
( ndr1_0
=> ( ~ c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60) ) )
| hskp3 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| c3_1(X61) ) )
| hskp14
| hskp15 )
& ( ! [X62] :
( ndr1_0
=> ( c1_1(X62)
| c2_1(X62)
| ~ c0_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| ~ c0_1(X63)
| ~ c3_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c2_1(X65)
| ~ c0_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66) ) ) )
& ( ! [X67] :
( ndr1_0
=> ( c1_1(X67)
| c2_1(X67)
| ~ c0_1(X67) ) )
| hskp0 )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c2_1(X68)
| ~ c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c0_1(X69)
| ~ c1_1(X69) ) )
| hskp11 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70) ) )
| hskp0
| hskp16 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c2_1(X72)
| c3_1(X72)
| ~ c0_1(X72) ) )
| hskp17 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c0_1(X73)
| ~ c2_1(X73) ) )
| hskp27
| hskp18 )
& ( ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c3_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( ~ c0_1(X76)
| ~ c1_1(X76)
| ~ c2_1(X76) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77) ) )
| hskp13
| hskp19 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| ~ c2_1(X78)
| ~ c3_1(X78) ) )
| hskp20
| hskp12 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79) ) )
| hskp21
| hskp12 )
& ( ! [X80] :
( ndr1_0
=> ( c2_1(X80)
| c3_1(X80)
| ~ c0_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) )
| hskp11 )
& ( ! [X82] :
( ndr1_0
=> ( c2_1(X82)
| c3_1(X82)
| ~ c0_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83) ) )
| hskp13 )
& ( ! [X84] :
( ndr1_0
=> ( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84) ) )
| hskp22
| hskp17 )
& ( ! [X85] :
( ndr1_0
=> ( c2_1(X85)
| c3_1(X85)
| ~ c0_1(X85) ) )
| hskp22
| hskp14 )
& ( ! [X86] :
( ndr1_0
=> ( c2_1(X86)
| c3_1(X86)
| ~ c0_1(X86) ) )
| hskp9
| hskp18 )
& ( ! [X87] :
( ndr1_0
=> ( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87) ) )
| hskp19
| hskp23 )
& ( ! [X88] :
( ndr1_0
=> ( c2_1(X88)
| ~ c0_1(X88)
| ~ c1_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c0_1(X89)
| ~ c1_1(X89) ) )
| hskp25 )
& ( ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| ~ c1_1(X90)
| ~ c3_1(X90) ) )
| hskp26
| hskp8 )
& ( ! [X91] :
( ndr1_0
=> ( c3_1(X91)
| ~ c0_1(X91)
| ~ c2_1(X91) ) )
| hskp22
| hskp14 )
& ( ! [X92] :
( ndr1_0
=> ( c3_1(X92)
| ~ c0_1(X92)
| ~ c2_1(X92) ) )
| hskp11
| hskp15 )
& ( ! [X93] :
( ndr1_0
=> ( ~ c0_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93) ) )
| hskp22
| hskp2 )
& ( ! [X94] :
( ndr1_0
=> ( ~ c0_1(X94)
| ~ c2_1(X94)
| ~ c3_1(X94) ) )
| hskp13
| hskp10 )
& ( hskp26
| hskp17
| hskp24 )
& ( hskp0
| hskp1
| hskp14 )
& ( hskp28
| hskp8 )
& ( hskp17
| hskp13
| hskp2 )
& ( hskp17
| hskp1
| hskp16 )
& ( hskp6
| hskp21
| hskp14 )
& ( hskp8
| hskp21
| hskp19 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a1168)
& c1_1(a1168)
& ~ c2_1(a1168) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a1169)
& ~ c2_1(a1169)
& ~ c3_1(a1169) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1172)
& c3_1(a1172)
& ~ c0_1(a1172) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a1174)
& c1_1(a1174)
& ~ c3_1(a1174) ) )
& ( ~ hskp4
| ( ndr1_0
& c1_1(a1175)
& c2_1(a1175)
& ~ c0_1(a1175) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a1176)
& c2_1(a1176)
& ~ c3_1(a1176) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a1178)
& c2_1(a1178)
& ~ c3_1(a1178) ) )
& ( ~ hskp7
| ( ndr1_0
& ~ c1_1(a1179)
& ~ c2_1(a1179)
& ~ c3_1(a1179) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a1180)
& ~ c0_1(a1180)
& ~ c3_1(a1180) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a1181)
& c3_1(a1181)
& ~ c2_1(a1181) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a1184)
& ~ c1_1(a1184)
& ~ c2_1(a1184) ) )
& ( ~ hskp11
| ( ndr1_0
& c0_1(a1186)
& ~ c2_1(a1186)
& ~ c3_1(a1186) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c0_1(a1187)
& ~ c2_1(a1187)
& ~ c3_1(a1187) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a1192)
& ~ c0_1(a1192)
& ~ c2_1(a1192) ) )
& ( ~ hskp14
| ( ndr1_0
& c2_1(a1194)
& ~ c0_1(a1194)
& ~ c1_1(a1194) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a1195)
& ~ c1_1(a1195)
& ~ c3_1(a1195) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1199)
& ~ c0_1(a1199)
& ~ c3_1(a1199) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a1200)
& ~ c1_1(a1200)
& ~ c2_1(a1200) ) )
& ( ~ hskp18
| ( ndr1_0
& c1_1(a1202)
& c3_1(a1202)
& ~ c0_1(a1202) ) )
& ( ~ hskp19
| ( ndr1_0
& c3_1(a1204)
& ~ c1_1(a1204)
& ~ c2_1(a1204) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a1205)
& c3_1(a1205)
& ~ c2_1(a1205) ) )
& ( ~ hskp21
| ( ndr1_0
& c2_1(a1207)
& c3_1(a1207)
& ~ c1_1(a1207) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a1211)
& c3_1(a1211)
& ~ c1_1(a1211) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a1218)
& ~ c1_1(a1218)
& ~ c3_1(a1218) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a1232)
& ~ c0_1(a1232)
& ~ c1_1(a1232) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a1182)
& c2_1(a1182)
& c3_1(a1182) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a1190)
& c1_1(a1190)
& c3_1(a1190) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a1201)
& c1_1(a1201)
& c2_1(a1201) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a1236)
& c2_1(a1236)
& c3_1(a1236) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c1_1(X4)
| c2_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| ! [X6] :
( ndr1_0
=> ( c2_1(X6)
| ~ c0_1(X6)
| ~ c3_1(X6) ) )
| hskp1 )
& ( ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c3_1(X8)
| ~ c0_1(X8)
| ~ c2_1(X8) ) )
| hskp0 )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| ~ c2_1(X10) ) )
| hskp0 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| ! [X15] :
( ndr1_0
=> ( c1_1(X15)
| c3_1(X15)
| ~ c0_1(X15) ) )
| hskp2 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| c3_1(X16) ) )
| hskp0
| hskp3 )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21) ) )
| hskp4 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c1_1(X23)
| c2_1(X23)
| c3_1(X23) ) )
| hskp5 )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c2_1(X24)
| c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c1_1(X25)
| ~ c0_1(X25)
| ~ c2_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( c1_1(X26)
| ~ c0_1(X26)
| ~ c3_1(X26) ) ) )
& ( ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c2_1(X27)
| c3_1(X27) ) )
| hskp3
| hskp6 )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c1_1(X29)
| c2_1(X29)
| ~ c0_1(X29) ) )
| hskp7 )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c2_1(X30)
| ~ c1_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c3_1(X31)
| ~ c0_1(X31)
| ~ c2_1(X31) ) )
| hskp8 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| ~ c1_1(X32) ) )
| hskp9
| hskp25 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c3_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c2_1(X34)
| ~ c3_1(X34) ) )
| hskp1 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c3_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36) ) )
| hskp10 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c3_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c2_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38) ) )
| hskp3 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c3_1(X39)
| ~ c2_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c2_1(X40)
| c3_1(X40)
| ~ c0_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c0_1(X41)
| ~ c1_1(X41)
| ~ c2_1(X41) ) ) )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| ~ c1_1(X42)
| ~ c2_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| ~ c0_1(X43)
| ~ c2_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( ~ c0_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46) ) )
| hskp11 )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| ~ c1_1(X47)
| ~ c3_1(X47) ) )
| ! [X48] :
( ndr1_0
=> ( c1_1(X48)
| ~ c0_1(X48)
| ~ c2_1(X48) ) )
| hskp12 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c1_1(X49)
| ~ c3_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c3_1(X50)
| ~ c0_1(X50)
| ~ c2_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51) ) ) )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52) ) )
| hskp5
| hskp4 )
& ( ! [X53] :
( ndr1_0
=> ( c1_1(X53)
| c2_1(X53)
| c3_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c1_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| hskp26 )
& ( ! [X55] :
( ndr1_0
=> ( c1_1(X55)
| c2_1(X55)
| c3_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c2_1(X56)
| ~ c0_1(X56)
| ~ c1_1(X56) ) )
| hskp6 )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c2_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58) ) )
| hskp13 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| c3_1(X59) ) )
| ! [X60] :
( ndr1_0
=> ( ~ c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60) ) )
| hskp3 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| c3_1(X61) ) )
| hskp14
| hskp15 )
& ( ! [X62] :
( ndr1_0
=> ( c1_1(X62)
| c2_1(X62)
| ~ c0_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| ~ c0_1(X63)
| ~ c3_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c2_1(X65)
| ~ c0_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66) ) ) )
& ( ! [X67] :
( ndr1_0
=> ( c1_1(X67)
| c2_1(X67)
| ~ c0_1(X67) ) )
| hskp0 )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c2_1(X68)
| ~ c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c0_1(X69)
| ~ c1_1(X69) ) )
| hskp11 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70) ) )
| hskp0
| hskp16 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c2_1(X72)
| c3_1(X72)
| ~ c0_1(X72) ) )
| hskp17 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c0_1(X73)
| ~ c2_1(X73) ) )
| hskp27
| hskp18 )
& ( ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c3_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( ~ c0_1(X76)
| ~ c1_1(X76)
| ~ c2_1(X76) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77) ) )
| hskp13
| hskp19 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| ~ c2_1(X78)
| ~ c3_1(X78) ) )
| hskp20
| hskp12 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79) ) )
| hskp21
| hskp12 )
& ( ! [X80] :
( ndr1_0
=> ( c2_1(X80)
| c3_1(X80)
| ~ c0_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) )
| hskp11 )
& ( ! [X82] :
( ndr1_0
=> ( c2_1(X82)
| c3_1(X82)
| ~ c0_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83) ) )
| hskp13 )
& ( ! [X84] :
( ndr1_0
=> ( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84) ) )
| hskp22
| hskp17 )
& ( ! [X85] :
( ndr1_0
=> ( c2_1(X85)
| c3_1(X85)
| ~ c0_1(X85) ) )
| hskp22
| hskp14 )
& ( ! [X86] :
( ndr1_0
=> ( c2_1(X86)
| c3_1(X86)
| ~ c0_1(X86) ) )
| hskp9
| hskp18 )
& ( ! [X87] :
( ndr1_0
=> ( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87) ) )
| hskp19
| hskp23 )
& ( ! [X88] :
( ndr1_0
=> ( c2_1(X88)
| ~ c0_1(X88)
| ~ c1_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c0_1(X89)
| ~ c1_1(X89) ) )
| hskp25 )
& ( ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| ~ c1_1(X90)
| ~ c3_1(X90) ) )
| hskp26
| hskp8 )
& ( ! [X91] :
( ndr1_0
=> ( c3_1(X91)
| ~ c0_1(X91)
| ~ c2_1(X91) ) )
| hskp22
| hskp14 )
& ( ! [X92] :
( ndr1_0
=> ( c3_1(X92)
| ~ c0_1(X92)
| ~ c2_1(X92) ) )
| hskp11
| hskp15 )
& ( ! [X93] :
( ndr1_0
=> ( ~ c0_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93) ) )
| hskp22
| hskp2 )
& ( ! [X94] :
( ndr1_0
=> ( ~ c0_1(X94)
| ~ c2_1(X94)
| ~ c3_1(X94) ) )
| hskp13
| hskp10 )
& ( hskp26
| hskp17
| hskp24 )
& ( hskp0
| hskp1
| hskp14 )
& ( hskp28
| hskp8 )
& ( hskp17
| hskp13
| hskp2 )
& ( hskp17
| hskp1
| hskp16 )
& ( hskp6
| hskp21
| hskp14 )
& ( hskp8
| hskp21
| hskp19 ) ),
inference(flattening,[],[f2]) ).
fof(f4,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a1168)
& c1_1(a1168)
& ~ c2_1(a1168) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a1169)
& ~ c2_1(a1169)
& ~ c3_1(a1169) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1172)
& c3_1(a1172)
& ~ c0_1(a1172) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a1174)
& c1_1(a1174)
& ~ c3_1(a1174) ) )
& ( ~ hskp4
| ( ndr1_0
& c1_1(a1175)
& c2_1(a1175)
& ~ c0_1(a1175) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a1176)
& c2_1(a1176)
& ~ c3_1(a1176) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a1178)
& c2_1(a1178)
& ~ c3_1(a1178) ) )
& ( ~ hskp7
| ( ndr1_0
& ~ c1_1(a1179)
& ~ c2_1(a1179)
& ~ c3_1(a1179) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a1180)
& ~ c0_1(a1180)
& ~ c3_1(a1180) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a1181)
& c3_1(a1181)
& ~ c2_1(a1181) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a1184)
& ~ c1_1(a1184)
& ~ c2_1(a1184) ) )
& ( ~ hskp11
| ( ndr1_0
& c0_1(a1186)
& ~ c2_1(a1186)
& ~ c3_1(a1186) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c0_1(a1187)
& ~ c2_1(a1187)
& ~ c3_1(a1187) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a1192)
& ~ c0_1(a1192)
& ~ c2_1(a1192) ) )
& ( ~ hskp14
| ( ndr1_0
& c2_1(a1194)
& ~ c0_1(a1194)
& ~ c1_1(a1194) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a1195)
& ~ c1_1(a1195)
& ~ c3_1(a1195) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1199)
& ~ c0_1(a1199)
& ~ c3_1(a1199) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a1200)
& ~ c1_1(a1200)
& ~ c2_1(a1200) ) )
& ( ~ hskp18
| ( ndr1_0
& c1_1(a1202)
& c3_1(a1202)
& ~ c0_1(a1202) ) )
& ( ~ hskp19
| ( ndr1_0
& c3_1(a1204)
& ~ c1_1(a1204)
& ~ c2_1(a1204) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a1205)
& c3_1(a1205)
& ~ c2_1(a1205) ) )
& ( ~ hskp21
| ( ndr1_0
& c2_1(a1207)
& c3_1(a1207)
& ~ c1_1(a1207) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a1211)
& c3_1(a1211)
& ~ c1_1(a1211) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a1218)
& ~ c1_1(a1218)
& ~ c3_1(a1218) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a1232)
& ~ c0_1(a1232)
& ~ c1_1(a1232) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a1182)
& c2_1(a1182)
& c3_1(a1182) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a1190)
& c1_1(a1190)
& c3_1(a1190) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a1201)
& c1_1(a1201)
& c2_1(a1201) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a1236)
& c2_1(a1236)
& c3_1(a1236) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c1_1(X4)
| c2_1(X4)
| ~ c3_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| ! [X6] :
( c2_1(X6)
| ~ c0_1(X6)
| ~ c3_1(X6)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X7] :
( c0_1(X7)
| c1_1(X7)
| c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c3_1(X8)
| ~ c0_1(X8)
| ~ c2_1(X8)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c0_1(X10)
| c1_1(X10)
| ~ c2_1(X10)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| c3_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0 ) )
& ( ! [X14] :
( c0_1(X14)
| c1_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| ! [X15] :
( c1_1(X15)
| c3_1(X15)
| ~ c0_1(X15)
| ~ ndr1_0 )
| hskp2 )
& ( ! [X16] :
( c0_1(X16)
| c1_1(X16)
| c3_1(X16)
| ~ ndr1_0 )
| hskp0
| hskp3 )
& ( ! [X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0 )
| ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 ) )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22)
| ~ ndr1_0 )
| ! [X23] :
( c1_1(X23)
| c2_1(X23)
| c3_1(X23)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X24] :
( c0_1(X24)
| c2_1(X24)
| c3_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( c1_1(X25)
| ~ c0_1(X25)
| ~ c2_1(X25)
| ~ ndr1_0 )
| ! [X26] :
( c1_1(X26)
| ~ c0_1(X26)
| ~ c3_1(X26)
| ~ ndr1_0 ) )
& ( ! [X27] :
( c0_1(X27)
| c2_1(X27)
| c3_1(X27)
| ~ ndr1_0 )
| hskp3
| hskp6 )
& ( ! [X28] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( c1_1(X29)
| c2_1(X29)
| ~ c0_1(X29)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X30] :
( c0_1(X30)
| c2_1(X30)
| ~ c1_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c3_1(X31)
| ~ c0_1(X31)
| ~ c2_1(X31)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X32] :
( c0_1(X32)
| c2_1(X32)
| ~ c1_1(X32)
| ~ ndr1_0 )
| hskp9
| hskp25 )
& ( ! [X33] :
( c0_1(X33)
| c2_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| ~ c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c3_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X37] :
( c0_1(X37)
| c3_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c2_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X39] :
( c0_1(X39)
| c3_1(X39)
| ~ c2_1(X39)
| ~ ndr1_0 )
| ! [X40] :
( c2_1(X40)
| c3_1(X40)
| ~ c0_1(X40)
| ~ ndr1_0 )
| ! [X41] :
( ~ c0_1(X41)
| ~ c1_1(X41)
| ~ c2_1(X41)
| ~ ndr1_0 ) )
& ( ! [X42] :
( c0_1(X42)
| ~ c1_1(X42)
| ~ c2_1(X42)
| ~ ndr1_0 )
| ! [X43] :
( c3_1(X43)
| ~ c0_1(X43)
| ~ c2_1(X43)
| ~ ndr1_0 )
| ! [X44] :
( ~ c0_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 ) )
& ( ! [X45] :
( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| ! [X46] :
( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X47] :
( c0_1(X47)
| ~ c1_1(X47)
| ~ c3_1(X47)
| ~ ndr1_0 )
| ! [X48] :
( c1_1(X48)
| ~ c0_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X49] :
( c0_1(X49)
| ~ c1_1(X49)
| ~ c3_1(X49)
| ~ ndr1_0 )
| ! [X50] :
( c3_1(X50)
| ~ c0_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( c3_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0 ) )
& ( ! [X52] :
( c0_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| hskp5
| hskp4 )
& ( ! [X53] :
( c1_1(X53)
| c2_1(X53)
| c3_1(X53)
| ~ ndr1_0 )
| ! [X54] :
( c1_1(X54)
| c3_1(X54)
| ~ c2_1(X54)
| ~ ndr1_0 )
| hskp26 )
& ( ! [X55] :
( c1_1(X55)
| c2_1(X55)
| c3_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( c2_1(X56)
| ~ c0_1(X56)
| ~ c1_1(X56)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X57] :
( c1_1(X57)
| c2_1(X57)
| c3_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c2_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X59] :
( c1_1(X59)
| c2_1(X59)
| c3_1(X59)
| ~ ndr1_0 )
| ! [X60] :
( ~ c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X61] :
( c1_1(X61)
| c2_1(X61)
| c3_1(X61)
| ~ ndr1_0 )
| hskp14
| hskp15 )
& ( ! [X62] :
( c1_1(X62)
| c2_1(X62)
| ~ c0_1(X62)
| ~ ndr1_0 )
| ! [X63] :
( c1_1(X63)
| ~ c0_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 ) )
& ( ! [X65] :
( c1_1(X65)
| c2_1(X65)
| ~ c0_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( ~ c0_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 ) )
& ( ! [X67] :
( c1_1(X67)
| c2_1(X67)
| ~ c0_1(X67)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X68] :
( c1_1(X68)
| c2_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c3_1(X69)
| ~ c0_1(X69)
| ~ c1_1(X69)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X70] :
( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0 )
| hskp0
| hskp16 )
& ( ! [X71] :
( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 )
| ! [X72] :
( c2_1(X72)
| c3_1(X72)
| ~ c0_1(X72)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X73] :
( c1_1(X73)
| ~ c0_1(X73)
| ~ c2_1(X73)
| ~ ndr1_0 )
| hskp27
| hskp18 )
& ( ! [X74] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0 )
| ! [X75] :
( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( ~ c0_1(X76)
| ~ c1_1(X76)
| ~ c2_1(X76)
| ~ ndr1_0 ) )
& ( ! [X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0 )
| hskp13
| hskp19 )
& ( ! [X78] :
( c1_1(X78)
| ~ c2_1(X78)
| ~ c3_1(X78)
| ~ ndr1_0 )
| hskp20
| hskp12 )
& ( ! [X79] :
( c1_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0 )
| hskp21
| hskp12 )
& ( ! [X80] :
( c2_1(X80)
| c3_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X82] :
( c2_1(X82)
| c3_1(X82)
| ~ c0_1(X82)
| ~ ndr1_0 )
| ! [X83] :
( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X84] :
( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ~ ndr1_0 )
| hskp22
| hskp17 )
& ( ! [X85] :
( c2_1(X85)
| c3_1(X85)
| ~ c0_1(X85)
| ~ ndr1_0 )
| hskp22
| hskp14 )
& ( ! [X86] :
( c2_1(X86)
| c3_1(X86)
| ~ c0_1(X86)
| ~ ndr1_0 )
| hskp9
| hskp18 )
& ( ! [X87] :
( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0 )
| hskp19
| hskp23 )
& ( ! [X88] :
( c2_1(X88)
| ~ c0_1(X88)
| ~ c1_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c3_1(X89)
| ~ c0_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0 )
| hskp25 )
& ( ! [X90] :
( c2_1(X90)
| ~ c1_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 )
| hskp26
| hskp8 )
& ( ! [X91] :
( c3_1(X91)
| ~ c0_1(X91)
| ~ c2_1(X91)
| ~ ndr1_0 )
| hskp22
| hskp14 )
& ( ! [X92] :
( c3_1(X92)
| ~ c0_1(X92)
| ~ c2_1(X92)
| ~ ndr1_0 )
| hskp11
| hskp15 )
& ( ! [X93] :
( ~ c0_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93)
| ~ ndr1_0 )
| hskp22
| hskp2 )
& ( ! [X94] :
( ~ c0_1(X94)
| ~ c2_1(X94)
| ~ c3_1(X94)
| ~ ndr1_0 )
| hskp13
| hskp10 )
& ( hskp26
| hskp17
| hskp24 )
& ( hskp0
| hskp1
| hskp14 )
& ( hskp28
| hskp8 )
& ( hskp17
| hskp13
| hskp2 )
& ( hskp17
| hskp1
| hskp16 )
& ( hskp6
| hskp21
| hskp14 )
& ( hskp8
| hskp21
| hskp19 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a1168)
& c1_1(a1168)
& ~ c2_1(a1168) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a1169)
& ~ c2_1(a1169)
& ~ c3_1(a1169) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1172)
& c3_1(a1172)
& ~ c0_1(a1172) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a1174)
& c1_1(a1174)
& ~ c3_1(a1174) ) )
& ( ~ hskp4
| ( ndr1_0
& c1_1(a1175)
& c2_1(a1175)
& ~ c0_1(a1175) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a1176)
& c2_1(a1176)
& ~ c3_1(a1176) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a1178)
& c2_1(a1178)
& ~ c3_1(a1178) ) )
& ( ~ hskp7
| ( ndr1_0
& ~ c1_1(a1179)
& ~ c2_1(a1179)
& ~ c3_1(a1179) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a1180)
& ~ c0_1(a1180)
& ~ c3_1(a1180) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a1181)
& c3_1(a1181)
& ~ c2_1(a1181) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a1184)
& ~ c1_1(a1184)
& ~ c2_1(a1184) ) )
& ( ~ hskp11
| ( ndr1_0
& c0_1(a1186)
& ~ c2_1(a1186)
& ~ c3_1(a1186) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c0_1(a1187)
& ~ c2_1(a1187)
& ~ c3_1(a1187) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a1192)
& ~ c0_1(a1192)
& ~ c2_1(a1192) ) )
& ( ~ hskp14
| ( ndr1_0
& c2_1(a1194)
& ~ c0_1(a1194)
& ~ c1_1(a1194) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a1195)
& ~ c1_1(a1195)
& ~ c3_1(a1195) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1199)
& ~ c0_1(a1199)
& ~ c3_1(a1199) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a1200)
& ~ c1_1(a1200)
& ~ c2_1(a1200) ) )
& ( ~ hskp18
| ( ndr1_0
& c1_1(a1202)
& c3_1(a1202)
& ~ c0_1(a1202) ) )
& ( ~ hskp19
| ( ndr1_0
& c3_1(a1204)
& ~ c1_1(a1204)
& ~ c2_1(a1204) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a1205)
& c3_1(a1205)
& ~ c2_1(a1205) ) )
& ( ~ hskp21
| ( ndr1_0
& c2_1(a1207)
& c3_1(a1207)
& ~ c1_1(a1207) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a1211)
& c3_1(a1211)
& ~ c1_1(a1211) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a1218)
& ~ c1_1(a1218)
& ~ c3_1(a1218) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a1232)
& ~ c0_1(a1232)
& ~ c1_1(a1232) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a1182)
& c2_1(a1182)
& c3_1(a1182) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a1190)
& c1_1(a1190)
& c3_1(a1190) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a1201)
& c1_1(a1201)
& c2_1(a1201) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a1236)
& c2_1(a1236)
& c3_1(a1236) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c1_1(X4)
| c2_1(X4)
| ~ c3_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| ! [X6] :
( c2_1(X6)
| ~ c0_1(X6)
| ~ c3_1(X6)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X7] :
( c0_1(X7)
| c1_1(X7)
| c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c3_1(X8)
| ~ c0_1(X8)
| ~ c2_1(X8)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c0_1(X10)
| c1_1(X10)
| ~ c2_1(X10)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| c3_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0 ) )
& ( ! [X14] :
( c0_1(X14)
| c1_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| ! [X15] :
( c1_1(X15)
| c3_1(X15)
| ~ c0_1(X15)
| ~ ndr1_0 )
| hskp2 )
& ( ! [X16] :
( c0_1(X16)
| c1_1(X16)
| c3_1(X16)
| ~ ndr1_0 )
| hskp0
| hskp3 )
& ( ! [X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0 )
| ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 ) )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22)
| ~ ndr1_0 )
| ! [X23] :
( c1_1(X23)
| c2_1(X23)
| c3_1(X23)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X24] :
( c0_1(X24)
| c2_1(X24)
| c3_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( c1_1(X25)
| ~ c0_1(X25)
| ~ c2_1(X25)
| ~ ndr1_0 )
| ! [X26] :
( c1_1(X26)
| ~ c0_1(X26)
| ~ c3_1(X26)
| ~ ndr1_0 ) )
& ( ! [X27] :
( c0_1(X27)
| c2_1(X27)
| c3_1(X27)
| ~ ndr1_0 )
| hskp3
| hskp6 )
& ( ! [X28] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( c1_1(X29)
| c2_1(X29)
| ~ c0_1(X29)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X30] :
( c0_1(X30)
| c2_1(X30)
| ~ c1_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c3_1(X31)
| ~ c0_1(X31)
| ~ c2_1(X31)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X32] :
( c0_1(X32)
| c2_1(X32)
| ~ c1_1(X32)
| ~ ndr1_0 )
| hskp9
| hskp25 )
& ( ! [X33] :
( c0_1(X33)
| c2_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| ~ c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c3_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X37] :
( c0_1(X37)
| c3_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c2_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X39] :
( c0_1(X39)
| c3_1(X39)
| ~ c2_1(X39)
| ~ ndr1_0 )
| ! [X40] :
( c2_1(X40)
| c3_1(X40)
| ~ c0_1(X40)
| ~ ndr1_0 )
| ! [X41] :
( ~ c0_1(X41)
| ~ c1_1(X41)
| ~ c2_1(X41)
| ~ ndr1_0 ) )
& ( ! [X42] :
( c0_1(X42)
| ~ c1_1(X42)
| ~ c2_1(X42)
| ~ ndr1_0 )
| ! [X43] :
( c3_1(X43)
| ~ c0_1(X43)
| ~ c2_1(X43)
| ~ ndr1_0 )
| ! [X44] :
( ~ c0_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 ) )
& ( ! [X45] :
( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| ! [X46] :
( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X47] :
( c0_1(X47)
| ~ c1_1(X47)
| ~ c3_1(X47)
| ~ ndr1_0 )
| ! [X48] :
( c1_1(X48)
| ~ c0_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X49] :
( c0_1(X49)
| ~ c1_1(X49)
| ~ c3_1(X49)
| ~ ndr1_0 )
| ! [X50] :
( c3_1(X50)
| ~ c0_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( c3_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0 ) )
& ( ! [X52] :
( c0_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| hskp5
| hskp4 )
& ( ! [X53] :
( c1_1(X53)
| c2_1(X53)
| c3_1(X53)
| ~ ndr1_0 )
| ! [X54] :
( c1_1(X54)
| c3_1(X54)
| ~ c2_1(X54)
| ~ ndr1_0 )
| hskp26 )
& ( ! [X55] :
( c1_1(X55)
| c2_1(X55)
| c3_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( c2_1(X56)
| ~ c0_1(X56)
| ~ c1_1(X56)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X57] :
( c1_1(X57)
| c2_1(X57)
| c3_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c2_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X59] :
( c1_1(X59)
| c2_1(X59)
| c3_1(X59)
| ~ ndr1_0 )
| ! [X60] :
( ~ c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X61] :
( c1_1(X61)
| c2_1(X61)
| c3_1(X61)
| ~ ndr1_0 )
| hskp14
| hskp15 )
& ( ! [X62] :
( c1_1(X62)
| c2_1(X62)
| ~ c0_1(X62)
| ~ ndr1_0 )
| ! [X63] :
( c1_1(X63)
| ~ c0_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 ) )
& ( ! [X65] :
( c1_1(X65)
| c2_1(X65)
| ~ c0_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( ~ c0_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 ) )
& ( ! [X67] :
( c1_1(X67)
| c2_1(X67)
| ~ c0_1(X67)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X68] :
( c1_1(X68)
| c2_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c3_1(X69)
| ~ c0_1(X69)
| ~ c1_1(X69)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X70] :
( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0 )
| hskp0
| hskp16 )
& ( ! [X71] :
( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 )
| ! [X72] :
( c2_1(X72)
| c3_1(X72)
| ~ c0_1(X72)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X73] :
( c1_1(X73)
| ~ c0_1(X73)
| ~ c2_1(X73)
| ~ ndr1_0 )
| hskp27
| hskp18 )
& ( ! [X74] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0 )
| ! [X75] :
( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( ~ c0_1(X76)
| ~ c1_1(X76)
| ~ c2_1(X76)
| ~ ndr1_0 ) )
& ( ! [X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0 )
| hskp13
| hskp19 )
& ( ! [X78] :
( c1_1(X78)
| ~ c2_1(X78)
| ~ c3_1(X78)
| ~ ndr1_0 )
| hskp20
| hskp12 )
& ( ! [X79] :
( c1_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0 )
| hskp21
| hskp12 )
& ( ! [X80] :
( c2_1(X80)
| c3_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X82] :
( c2_1(X82)
| c3_1(X82)
| ~ c0_1(X82)
| ~ ndr1_0 )
| ! [X83] :
( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X84] :
( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ~ ndr1_0 )
| hskp22
| hskp17 )
& ( ! [X85] :
( c2_1(X85)
| c3_1(X85)
| ~ c0_1(X85)
| ~ ndr1_0 )
| hskp22
| hskp14 )
& ( ! [X86] :
( c2_1(X86)
| c3_1(X86)
| ~ c0_1(X86)
| ~ ndr1_0 )
| hskp9
| hskp18 )
& ( ! [X87] :
( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0 )
| hskp19
| hskp23 )
& ( ! [X88] :
( c2_1(X88)
| ~ c0_1(X88)
| ~ c1_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c3_1(X89)
| ~ c0_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0 )
| hskp25 )
& ( ! [X90] :
( c2_1(X90)
| ~ c1_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 )
| hskp26
| hskp8 )
& ( ! [X91] :
( c3_1(X91)
| ~ c0_1(X91)
| ~ c2_1(X91)
| ~ ndr1_0 )
| hskp22
| hskp14 )
& ( ! [X92] :
( c3_1(X92)
| ~ c0_1(X92)
| ~ c2_1(X92)
| ~ ndr1_0 )
| hskp11
| hskp15 )
& ( ! [X93] :
( ~ c0_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93)
| ~ ndr1_0 )
| hskp22
| hskp2 )
& ( ! [X94] :
( ~ c0_1(X94)
| ~ c2_1(X94)
| ~ c3_1(X94)
| ~ ndr1_0 )
| hskp13
| hskp10 )
& ( hskp26
| hskp17
| hskp24 )
& ( hskp0
| hskp1
| hskp14 )
& ( hskp28
| hskp8 )
& ( hskp17
| hskp13
| hskp2 )
& ( hskp17
| hskp1
| hskp16 )
& ( hskp6
| hskp21
| hskp14 )
& ( hskp8
| hskp21
| hskp19 ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
( hskp8
| hskp21
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f9,plain,
( hskp17
| hskp13
| hskp2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f10,plain,
( hskp28
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f11,plain,
( hskp0
| hskp1
| hskp14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f13,plain,
! [X94] :
( ~ c0_1(X94)
| ~ c2_1(X94)
| ~ c3_1(X94)
| ~ ndr1_0
| hskp13
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f14,plain,
! [X93] :
( ~ c0_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93)
| ~ ndr1_0
| hskp22
| hskp2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f16,plain,
! [X91] :
( c3_1(X91)
| ~ c0_1(X91)
| ~ c2_1(X91)
| ~ ndr1_0
| hskp22
| hskp14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f18,plain,
! [X88,X89] :
( c2_1(X88)
| ~ c0_1(X88)
| ~ c1_1(X88)
| ~ ndr1_0
| c3_1(X89)
| ~ c0_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0
| hskp25 ),
inference(cnf_transformation,[],[f5]) ).
fof(f19,plain,
! [X87] :
( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0
| hskp19
| hskp23 ),
inference(cnf_transformation,[],[f5]) ).
fof(f21,plain,
! [X85] :
( c2_1(X85)
| c3_1(X85)
| ~ c0_1(X85)
| ~ ndr1_0
| hskp22
| hskp14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f22,plain,
! [X84] :
( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ~ ndr1_0
| hskp22
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f25,plain,
! [X79] :
( c1_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0
| hskp21
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0
| hskp13
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f28,plain,
! [X76,X74,X75] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0
| c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0
| ~ c0_1(X76)
| ~ c1_1(X76)
| ~ c2_1(X76)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f30,plain,
! [X72,X71] :
( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0
| c2_1(X72)
| c3_1(X72)
| ~ c0_1(X72)
| ~ ndr1_0
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f31,plain,
! [X70] :
( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0
| hskp0
| hskp16 ),
inference(cnf_transformation,[],[f5]) ).
fof(f32,plain,
! [X68,X69] :
( c1_1(X68)
| c2_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0
| c3_1(X69)
| ~ c0_1(X69)
| ~ c1_1(X69)
| ~ ndr1_0
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f33,plain,
! [X67] :
( c1_1(X67)
| c2_1(X67)
| ~ c0_1(X67)
| ~ ndr1_0
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f34,plain,
! [X65,X66] :
( c1_1(X65)
| c2_1(X65)
| ~ c0_1(X65)
| ~ ndr1_0
| ~ c0_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f35,plain,
! [X62,X63,X64] :
( c1_1(X62)
| c2_1(X62)
| ~ c0_1(X62)
| ~ ndr1_0
| c1_1(X63)
| ~ c0_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0
| c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f38,plain,
! [X58,X57] :
( c1_1(X57)
| c2_1(X57)
| c3_1(X57)
| ~ ndr1_0
| c2_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f39,plain,
! [X56,X55] :
( c1_1(X55)
| c2_1(X55)
| c3_1(X55)
| ~ ndr1_0
| c2_1(X56)
| ~ c0_1(X56)
| ~ c1_1(X56)
| ~ ndr1_0
| hskp6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f42,plain,
! [X50,X51,X49] :
( c0_1(X49)
| ~ c1_1(X49)
| ~ c3_1(X49)
| ~ ndr1_0
| c3_1(X50)
| ~ c0_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0
| c3_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f44,plain,
! [X46,X45] :
( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0
| c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46)
| ~ ndr1_0
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f45,plain,
! [X44,X42,X43] :
( c0_1(X42)
| ~ c1_1(X42)
| ~ c2_1(X42)
| ~ ndr1_0
| c3_1(X43)
| ~ c0_1(X43)
| ~ c2_1(X43)
| ~ ndr1_0
| ~ c0_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f47,plain,
! [X38,X37] :
( c0_1(X37)
| c3_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0
| c2_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38)
| ~ ndr1_0
| hskp3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f49,plain,
! [X34,X33] :
( c0_1(X33)
| c2_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0
| c1_1(X34)
| ~ c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0
| hskp1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f50,plain,
! [X32] :
( c0_1(X32)
| c2_1(X32)
| ~ c1_1(X32)
| ~ ndr1_0
| hskp9
| hskp25 ),
inference(cnf_transformation,[],[f5]) ).
fof(f53,plain,
! [X27] :
( c0_1(X27)
| c2_1(X27)
| c3_1(X27)
| ~ ndr1_0
| hskp3
| hskp6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f54,plain,
! [X26,X24,X25] :
( c0_1(X24)
| c2_1(X24)
| c3_1(X24)
| ~ ndr1_0
| c1_1(X25)
| ~ c0_1(X25)
| ~ c2_1(X25)
| ~ ndr1_0
| c1_1(X26)
| ~ c0_1(X26)
| ~ c3_1(X26)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f55,plain,
! [X22,X23] :
( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22)
| ~ ndr1_0
| c1_1(X23)
| c2_1(X23)
| c3_1(X23)
| ~ ndr1_0
| hskp5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f56,plain,
! [X21,X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0
| c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0
| hskp4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f57,plain,
! [X18,X19,X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0
| c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0
| c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f58,plain,
! [X16] :
( c0_1(X16)
| c1_1(X16)
| c3_1(X16)
| ~ ndr1_0
| hskp0
| hskp3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f61,plain,
! [X10,X9] :
( c0_1(X9)
| c1_1(X9)
| c3_1(X9)
| ~ ndr1_0
| c0_1(X10)
| c1_1(X10)
| ~ c2_1(X10)
| ~ ndr1_0
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f66,plain,
( ~ hskp28
| c3_1(a1236) ),
inference(cnf_transformation,[],[f5]) ).
fof(f67,plain,
( ~ hskp28
| c2_1(a1236) ),
inference(cnf_transformation,[],[f5]) ).
fof(f68,plain,
( ~ hskp28
| c0_1(a1236) ),
inference(cnf_transformation,[],[f5]) ).
fof(f78,plain,
( ~ hskp25
| c3_1(a1182) ),
inference(cnf_transformation,[],[f5]) ).
fof(f79,plain,
( ~ hskp25
| c2_1(a1182) ),
inference(cnf_transformation,[],[f5]) ).
fof(f80,plain,
( ~ hskp25
| c1_1(a1182) ),
inference(cnf_transformation,[],[f5]) ).
fof(f86,plain,
( ~ hskp23
| ~ c3_1(a1218) ),
inference(cnf_transformation,[],[f5]) ).
fof(f87,plain,
( ~ hskp23
| ~ c1_1(a1218) ),
inference(cnf_transformation,[],[f5]) ).
fof(f88,plain,
( ~ hskp23
| ~ c0_1(a1218) ),
inference(cnf_transformation,[],[f5]) ).
fof(f90,plain,
( ~ hskp22
| ~ c1_1(a1211) ),
inference(cnf_transformation,[],[f5]) ).
fof(f91,plain,
( ~ hskp22
| c3_1(a1211) ),
inference(cnf_transformation,[],[f5]) ).
fof(f92,plain,
( ~ hskp22
| c0_1(a1211) ),
inference(cnf_transformation,[],[f5]) ).
fof(f94,plain,
( ~ hskp21
| ~ c1_1(a1207) ),
inference(cnf_transformation,[],[f5]) ).
fof(f95,plain,
( ~ hskp21
| c3_1(a1207) ),
inference(cnf_transformation,[],[f5]) ).
fof(f96,plain,
( ~ hskp21
| c2_1(a1207) ),
inference(cnf_transformation,[],[f5]) ).
fof(f97,plain,
( ~ hskp21
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f102,plain,
( ~ hskp19
| ~ c2_1(a1204) ),
inference(cnf_transformation,[],[f5]) ).
fof(f103,plain,
( ~ hskp19
| ~ c1_1(a1204) ),
inference(cnf_transformation,[],[f5]) ).
fof(f104,plain,
( ~ hskp19
| c3_1(a1204) ),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
( ~ hskp19
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f110,plain,
( ~ hskp17
| ~ c2_1(a1200) ),
inference(cnf_transformation,[],[f5]) ).
fof(f111,plain,
( ~ hskp17
| ~ c1_1(a1200) ),
inference(cnf_transformation,[],[f5]) ).
fof(f112,plain,
( ~ hskp17
| c0_1(a1200) ),
inference(cnf_transformation,[],[f5]) ).
fof(f114,plain,
( ~ hskp16
| ~ c3_1(a1199) ),
inference(cnf_transformation,[],[f5]) ).
fof(f115,plain,
( ~ hskp16
| ~ c0_1(a1199) ),
inference(cnf_transformation,[],[f5]) ).
fof(f116,plain,
( ~ hskp16
| c2_1(a1199) ),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
( ~ hskp14
| ~ c1_1(a1194) ),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
( ~ hskp14
| ~ c0_1(a1194) ),
inference(cnf_transformation,[],[f5]) ).
fof(f124,plain,
( ~ hskp14
| c2_1(a1194) ),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
( ~ hskp13
| ~ c2_1(a1192) ),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
( ~ hskp13
| ~ c0_1(a1192) ),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
( ~ hskp13
| c1_1(a1192) ),
inference(cnf_transformation,[],[f5]) ).
fof(f130,plain,
( ~ hskp12
| ~ c3_1(a1187) ),
inference(cnf_transformation,[],[f5]) ).
fof(f131,plain,
( ~ hskp12
| ~ c2_1(a1187) ),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
( ~ hskp12
| ~ c0_1(a1187) ),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
( ~ hskp11
| ~ c3_1(a1186) ),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
( ~ hskp11
| ~ c2_1(a1186) ),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
( ~ hskp11
| c0_1(a1186) ),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
( ~ hskp10
| ~ c2_1(a1184) ),
inference(cnf_transformation,[],[f5]) ).
fof(f140,plain,
( ~ hskp10
| ~ c0_1(a1184) ),
inference(cnf_transformation,[],[f5]) ).
fof(f142,plain,
( ~ hskp9
| ~ c2_1(a1181) ),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
( ~ hskp9
| c3_1(a1181) ),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
( ~ hskp9
| c0_1(a1181) ),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
( ~ hskp8
| ~ c3_1(a1180) ),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
( ~ hskp8
| ~ c0_1(a1180) ),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
( ~ hskp8
| c1_1(a1180) ),
inference(cnf_transformation,[],[f5]) ).
fof(f149,plain,
( ~ hskp8
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
( ~ hskp6
| ~ c3_1(a1178) ),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
( ~ hskp6
| c2_1(a1178) ),
inference(cnf_transformation,[],[f5]) ).
fof(f156,plain,
( ~ hskp6
| c1_1(a1178) ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( ~ hskp5
| ~ c3_1(a1176) ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( ~ hskp5
| c2_1(a1176) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( ~ hskp5
| c0_1(a1176) ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( ~ hskp4
| ~ c0_1(a1175) ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( ~ hskp4
| c2_1(a1175) ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( ~ hskp4
| c1_1(a1175) ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( ~ hskp3
| ~ c3_1(a1174) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( ~ hskp3
| c1_1(a1174) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( ~ hskp3
| c0_1(a1174) ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( ~ hskp2
| ~ c0_1(a1172) ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( ~ hskp2
| c3_1(a1172) ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( ~ hskp2
| c2_1(a1172) ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( ~ hskp1
| ~ c3_1(a1169) ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( ~ hskp1
| ~ c2_1(a1169) ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( ~ hskp1
| c1_1(a1169) ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( ~ hskp0
| ~ c2_1(a1168) ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( ~ hskp0
| c1_1(a1168) ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( ~ hskp0
| c0_1(a1168) ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( ~ hskp0
| ~ c0_1(a1168) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f183,plain,
( ~ hskp0
| c2_1(a1168) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f184,plain,
( ~ hskp1
| c2_1(a1169) ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f185,plain,
( ~ hskp1
| c3_1(a1169) ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f187,plain,
( hskp2
| ~ c2_1(a1172) ),
inference(consistent_polarity_flipping,[],[f172]) ).
fof(f188,plain,
( hskp2
| ~ c3_1(a1172) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f189,plain,
( hskp2
| c0_1(a1172) ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f190,plain,
( ~ hskp3
| ~ c0_1(a1174) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f191,plain,
( ~ hskp3
| c3_1(a1174) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f192,plain,
( ~ hskp4
| ~ c2_1(a1175) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f193,plain,
( ~ hskp4
| c0_1(a1175) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f194,plain,
( ~ hskp5
| ~ c0_1(a1176) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f195,plain,
( ~ hskp5
| ~ c2_1(a1176) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f196,plain,
( ~ hskp5
| c3_1(a1176) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f197,plain,
( ~ hskp6
| ~ c2_1(a1178) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f198,plain,
( ~ hskp6
| c3_1(a1178) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f201,plain,
( hskp8
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f202,plain,
( hskp8
| c1_1(a1180) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f203,plain,
( hskp8
| c0_1(a1180) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f204,plain,
( hskp8
| c3_1(a1180) ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f205,plain,
( ~ hskp9
| ~ c0_1(a1181) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f206,plain,
( ~ hskp9
| ~ c3_1(a1181) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f207,plain,
( ~ hskp9
| c2_1(a1181) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f208,plain,
( ~ hskp10
| c0_1(a1184) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f209,plain,
( ~ hskp10
| c2_1(a1184) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f210,plain,
( ~ hskp11
| ~ c0_1(a1186) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f211,plain,
( ~ hskp11
| c2_1(a1186) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f212,plain,
( ~ hskp11
| c3_1(a1186) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f214,plain,
( hskp12
| c0_1(a1187) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f215,plain,
( hskp12
| c2_1(a1187) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f216,plain,
( hskp12
| c3_1(a1187) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f217,plain,
( ~ hskp13
| c0_1(a1192) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f218,plain,
( ~ hskp13
| c2_1(a1192) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f219,plain,
( ~ hskp14
| ~ c2_1(a1194) ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f220,plain,
( ~ hskp14
| c0_1(a1194) ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f226,plain,
( hskp16
| ~ c2_1(a1199) ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f227,plain,
( hskp16
| c0_1(a1199) ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f228,plain,
( hskp16
| c3_1(a1199) ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f229,plain,
( ~ hskp17
| ~ c0_1(a1200) ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f230,plain,
( ~ hskp17
| c2_1(a1200) ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f233,plain,
( ~ hskp19
| ~ c3_1(a1204) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f234,plain,
( ~ hskp19
| c2_1(a1204) ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f237,plain,
( hskp21
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f238,plain,
( hskp21
| ~ c2_1(a1207) ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f239,plain,
( hskp21
| ~ c3_1(a1207) ),
inference(consistent_polarity_flipping,[],[f95]) ).
fof(f240,plain,
( hskp21
| ~ c1_1(a1207) ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f241,plain,
( ~ hskp22
| ~ c0_1(a1211) ),
inference(consistent_polarity_flipping,[],[f92]) ).
fof(f242,plain,
( ~ hskp22
| ~ c3_1(a1211) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f244,plain,
( hskp23
| c0_1(a1218) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f245,plain,
( hskp23
| ~ c1_1(a1218) ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f246,plain,
( hskp23
| c3_1(a1218) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f252,plain,
( hskp25
| c1_1(a1182) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f253,plain,
( hskp25
| ~ c2_1(a1182) ),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f254,plain,
( hskp25
| ~ c3_1(a1182) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f264,plain,
( hskp28
| ~ c0_1(a1236) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f265,plain,
( hskp28
| ~ c2_1(a1236) ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f266,plain,
( hskp28
| ~ c3_1(a1236) ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f271,plain,
! [X10,X9] :
( ~ c0_1(X9)
| c1_1(X9)
| ~ c3_1(X9)
| ~ ndr1_0
| ~ c0_1(X10)
| c1_1(X10)
| c2_1(X10)
| ~ ndr1_0
| hskp0 ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f274,plain,
! [X16] :
( ~ c0_1(X16)
| c1_1(X16)
| ~ c3_1(X16)
| ~ ndr1_0
| hskp0
| hskp3 ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f275,plain,
! [X18,X19,X17] :
( ~ c0_1(X17)
| c1_1(X17)
| c2_1(X17)
| ~ ndr1_0
| ~ c0_1(X18)
| c1_1(X18)
| c3_1(X18)
| ~ ndr1_0
| ~ c3_1(X19)
| ~ c1_1(X19)
| c2_1(X19)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f276,plain,
! [X21,X20] :
( ~ c0_1(X20)
| c1_1(X20)
| c2_1(X20)
| ~ ndr1_0
| ~ c0_1(X21)
| c1_1(X21)
| c3_1(X21)
| ~ ndr1_0
| hskp4 ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f277,plain,
! [X22,X23] :
( ~ c0_1(X22)
| c1_1(X22)
| c2_1(X22)
| ~ ndr1_0
| c1_1(X23)
| ~ c2_1(X23)
| ~ c3_1(X23)
| ~ ndr1_0
| hskp5 ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f278,plain,
! [X26,X24,X25] :
( ~ c0_1(X24)
| ~ c2_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0
| c1_1(X25)
| c0_1(X25)
| c2_1(X25)
| ~ ndr1_0
| c1_1(X26)
| c0_1(X26)
| c3_1(X26)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f279,plain,
! [X27] :
( ~ c0_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0
| hskp3
| hskp6 ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f282,plain,
! [X32] :
( ~ c0_1(X32)
| ~ c2_1(X32)
| ~ c1_1(X32)
| ~ ndr1_0
| hskp9
| ~ hskp25 ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f283,plain,
! [X34,X33] :
( ~ c0_1(X33)
| ~ c2_1(X33)
| c3_1(X33)
| ~ ndr1_0
| c1_1(X34)
| c2_1(X34)
| c3_1(X34)
| ~ ndr1_0
| hskp1 ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f285,plain,
! [X38,X37] :
( ~ c0_1(X37)
| ~ c3_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0
| ~ c2_1(X38)
| ~ c1_1(X38)
| c3_1(X38)
| ~ ndr1_0
| hskp3 ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f287,plain,
! [X44,X42,X43] :
( ~ c0_1(X42)
| ~ c1_1(X42)
| c2_1(X42)
| ~ ndr1_0
| ~ c3_1(X43)
| c0_1(X43)
| c2_1(X43)
| ~ ndr1_0
| c0_1(X44)
| c2_1(X44)
| c3_1(X44)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f288,plain,
! [X46,X45] :
( ~ c0_1(X45)
| ~ c1_1(X45)
| c3_1(X45)
| ~ ndr1_0
| c1_1(X46)
| ~ c2_1(X46)
| c3_1(X46)
| ~ ndr1_0
| hskp11 ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f290,plain,
! [X50,X51,X49] :
( ~ c0_1(X49)
| ~ c1_1(X49)
| c3_1(X49)
| ~ ndr1_0
| ~ c3_1(X50)
| c0_1(X50)
| c2_1(X50)
| ~ ndr1_0
| ~ c3_1(X51)
| ~ c1_1(X51)
| c2_1(X51)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f293,plain,
! [X56,X55] :
( c1_1(X55)
| ~ c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0
| ~ c2_1(X56)
| c0_1(X56)
| ~ c1_1(X56)
| ~ ndr1_0
| hskp6 ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f294,plain,
! [X58,X57] :
( c1_1(X57)
| ~ c2_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0
| ~ c2_1(X58)
| ~ c1_1(X58)
| c3_1(X58)
| ~ ndr1_0
| hskp13 ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f297,plain,
! [X62,X63,X64] :
( c1_1(X62)
| ~ c2_1(X62)
| c0_1(X62)
| ~ ndr1_0
| c1_1(X63)
| c0_1(X63)
| c3_1(X63)
| ~ ndr1_0
| ~ c2_1(X64)
| c0_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f298,plain,
! [X65,X66] :
( c1_1(X65)
| ~ c2_1(X65)
| c0_1(X65)
| ~ ndr1_0
| c0_1(X66)
| ~ c1_1(X66)
| c3_1(X66)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f299,plain,
! [X67] :
( c1_1(X67)
| ~ c2_1(X67)
| c0_1(X67)
| ~ ndr1_0
| hskp0 ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f300,plain,
! [X68,X69] :
( c1_1(X68)
| ~ c2_1(X68)
| c3_1(X68)
| ~ ndr1_0
| ~ c3_1(X69)
| c0_1(X69)
| ~ c1_1(X69)
| ~ ndr1_0
| hskp11 ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f301,plain,
! [X70] :
( c1_1(X70)
| ~ c2_1(X70)
| c3_1(X70)
| ~ ndr1_0
| hskp0
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f302,plain,
! [X72,X71] :
( c1_1(X71)
| c0_1(X71)
| c2_1(X71)
| ~ ndr1_0
| ~ c2_1(X72)
| ~ c3_1(X72)
| c0_1(X72)
| ~ ndr1_0
| hskp17 ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f304,plain,
! [X76,X74,X75] :
( c1_1(X74)
| c0_1(X74)
| c3_1(X74)
| ~ ndr1_0
| ~ c2_1(X75)
| ~ c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0
| c0_1(X76)
| ~ c1_1(X76)
| c2_1(X76)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f305,plain,
! [X77] :
( c1_1(X77)
| c0_1(X77)
| c3_1(X77)
| ~ ndr1_0
| hskp13
| hskp19 ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f307,plain,
! [X79] :
( c1_1(X79)
| c2_1(X79)
| c3_1(X79)
| ~ ndr1_0
| ~ hskp21
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f310,plain,
! [X84] :
( ~ c2_1(X84)
| ~ c3_1(X84)
| c0_1(X84)
| ~ ndr1_0
| hskp22
| hskp17 ),
inference(consistent_polarity_flipping,[],[f22]) ).
fof(f311,plain,
! [X85] :
( ~ c2_1(X85)
| ~ c3_1(X85)
| c0_1(X85)
| ~ ndr1_0
| hskp22
| hskp14 ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f313,plain,
! [X87] :
( ~ c2_1(X87)
| ~ c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0
| hskp19
| ~ hskp23 ),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f314,plain,
! [X88,X89] :
( ~ c2_1(X88)
| c0_1(X88)
| ~ c1_1(X88)
| ~ ndr1_0
| ~ c3_1(X89)
| c0_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0
| ~ hskp25 ),
inference(consistent_polarity_flipping,[],[f18]) ).
fof(f316,plain,
! [X91] :
( ~ c3_1(X91)
| c0_1(X91)
| c2_1(X91)
| ~ ndr1_0
| hskp22
| hskp14 ),
inference(consistent_polarity_flipping,[],[f16]) ).
fof(f318,plain,
! [X93] :
( c0_1(X93)
| c2_1(X93)
| c3_1(X93)
| ~ ndr1_0
| hskp22
| ~ hskp2 ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f319,plain,
! [X94] :
( c0_1(X94)
| c2_1(X94)
| c3_1(X94)
| ~ ndr1_0
| hskp13
| hskp10 ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f321,plain,
( ~ hskp28
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f322,plain,
( hskp17
| hskp13
| ~ hskp2 ),
inference(consistent_polarity_flipping,[],[f9]) ).
fof(f325,plain,
( ~ hskp8
| ~ hskp21
| hskp19 ),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f326,plain,
! [X88,X89] :
( ~ c2_1(X88)
| c0_1(X88)
| ~ c1_1(X88)
| ~ ndr1_0
| ~ c3_1(X89)
| c0_1(X89)
| ~ c1_1(X89)
| ~ hskp25 ),
inference(duplicate_literal_removal,[],[f314]) ).
fof(f329,plain,
! [X76,X74,X75] :
( c1_1(X74)
| c0_1(X74)
| c3_1(X74)
| ~ ndr1_0
| ~ c2_1(X75)
| ~ c3_1(X75)
| ~ c1_1(X75)
| c0_1(X76)
| ~ c1_1(X76)
| c2_1(X76) ),
inference(duplicate_literal_removal,[],[f304]) ).
fof(f330,plain,
! [X72,X71] :
( c1_1(X71)
| c0_1(X71)
| c2_1(X71)
| ~ ndr1_0
| ~ c2_1(X72)
| ~ c3_1(X72)
| c0_1(X72)
| hskp17 ),
inference(duplicate_literal_removal,[],[f302]) ).
fof(f331,plain,
! [X68,X69] :
( c1_1(X68)
| ~ c2_1(X68)
| c3_1(X68)
| ~ ndr1_0
| ~ c3_1(X69)
| c0_1(X69)
| ~ c1_1(X69)
| hskp11 ),
inference(duplicate_literal_removal,[],[f300]) ).
fof(f332,plain,
! [X65,X66] :
( c1_1(X65)
| ~ c2_1(X65)
| c0_1(X65)
| ~ ndr1_0
| c0_1(X66)
| ~ c1_1(X66)
| c3_1(X66) ),
inference(duplicate_literal_removal,[],[f298]) ).
fof(f333,plain,
! [X62,X63,X64] :
( c1_1(X62)
| ~ c2_1(X62)
| c0_1(X62)
| ~ ndr1_0
| c1_1(X63)
| c0_1(X63)
| c3_1(X63)
| ~ c2_1(X64)
| c0_1(X64)
| ~ c1_1(X64) ),
inference(duplicate_literal_removal,[],[f297]) ).
fof(f335,plain,
! [X58,X57] :
( c1_1(X57)
| ~ c2_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0
| ~ c2_1(X58)
| ~ c1_1(X58)
| c3_1(X58)
| hskp13 ),
inference(duplicate_literal_removal,[],[f294]) ).
fof(f336,plain,
! [X56,X55] :
( c1_1(X55)
| ~ c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0
| ~ c2_1(X56)
| c0_1(X56)
| ~ c1_1(X56)
| hskp6 ),
inference(duplicate_literal_removal,[],[f293]) ).
fof(f338,plain,
! [X50,X51,X49] :
( ~ c0_1(X49)
| ~ c1_1(X49)
| c3_1(X49)
| ~ ndr1_0
| ~ c3_1(X50)
| c0_1(X50)
| c2_1(X50)
| ~ c3_1(X51)
| ~ c1_1(X51)
| c2_1(X51) ),
inference(duplicate_literal_removal,[],[f290]) ).
fof(f340,plain,
! [X46,X45] :
( ~ c0_1(X45)
| ~ c1_1(X45)
| c3_1(X45)
| ~ ndr1_0
| c1_1(X46)
| ~ c2_1(X46)
| c3_1(X46)
| hskp11 ),
inference(duplicate_literal_removal,[],[f288]) ).
fof(f341,plain,
! [X44,X42,X43] :
( ~ c0_1(X42)
| ~ c1_1(X42)
| c2_1(X42)
| ~ ndr1_0
| ~ c3_1(X43)
| c0_1(X43)
| c2_1(X43)
| c0_1(X44)
| c2_1(X44)
| c3_1(X44) ),
inference(duplicate_literal_removal,[],[f287]) ).
fof(f343,plain,
! [X38,X37] :
( ~ c0_1(X37)
| ~ c3_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0
| ~ c2_1(X38)
| ~ c1_1(X38)
| c3_1(X38)
| hskp3 ),
inference(duplicate_literal_removal,[],[f285]) ).
fof(f345,plain,
! [X34,X33] :
( ~ c0_1(X33)
| ~ c2_1(X33)
| c3_1(X33)
| ~ ndr1_0
| c1_1(X34)
| c2_1(X34)
| c3_1(X34)
| hskp1 ),
inference(duplicate_literal_removal,[],[f283]) ).
fof(f348,plain,
! [X26,X24,X25] :
( ~ c0_1(X24)
| ~ c2_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0
| c1_1(X25)
| c0_1(X25)
| c2_1(X25)
| c1_1(X26)
| c0_1(X26)
| c3_1(X26) ),
inference(duplicate_literal_removal,[],[f278]) ).
fof(f349,plain,
! [X22,X23] :
( ~ c0_1(X22)
| c1_1(X22)
| c2_1(X22)
| ~ ndr1_0
| c1_1(X23)
| ~ c2_1(X23)
| ~ c3_1(X23)
| hskp5 ),
inference(duplicate_literal_removal,[],[f277]) ).
fof(f350,plain,
! [X21,X20] :
( ~ c0_1(X20)
| c1_1(X20)
| c2_1(X20)
| ~ ndr1_0
| ~ c0_1(X21)
| c1_1(X21)
| c3_1(X21)
| hskp4 ),
inference(duplicate_literal_removal,[],[f276]) ).
fof(f351,plain,
! [X18,X19,X17] :
( ~ c0_1(X17)
| c1_1(X17)
| c2_1(X17)
| ~ ndr1_0
| ~ c0_1(X18)
| c1_1(X18)
| c3_1(X18)
| ~ c3_1(X19)
| ~ c1_1(X19)
| c2_1(X19) ),
inference(duplicate_literal_removal,[],[f275]) ).
fof(f354,plain,
! [X10,X9] :
( ~ c0_1(X9)
| c1_1(X9)
| ~ c3_1(X9)
| ~ ndr1_0
| ~ c0_1(X10)
| c1_1(X10)
| c2_1(X10)
| hskp0 ),
inference(duplicate_literal_removal,[],[f271]) ).
fof(f360,definition,
( spl0_1
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f364,definition,
( spl0_2
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f368,definition,
( spl0_3
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f371,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f325,f368,f364,f360]) ).
fof(f373,definition,
( spl0_4
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f377,definition,
( spl0_5
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f382,definition,
( spl0_6
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f386,definition,
( spl0_7
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f390,definition,
( spl0_8
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f395,definition,
( spl0_9
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f399,definition,
( spl0_10
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f402,plain,
( ~ spl0_9
| spl0_10
| spl0_8 ),
inference(avatar_split_clause,[],[f322,f390,f399,f395]) ).
fof(f404,definition,
( spl0_11
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f407,plain,
( ~ spl0_3
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f321,f404,f368]) ).
fof(f409,definition,
( spl0_12
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f412,plain,
( spl0_4
| spl0_7
| spl0_12 ),
inference(avatar_split_clause,[],[f11,f409,f386,f373]) ).
fof(f423,definition,
( spl0_15
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f427,definition,
( spl0_16
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f431,definition,
( spl0_17
<=> ! [X94] :
( c0_1(X94)
| c3_1(X94)
| c2_1(X94) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f432,plain,
( ! [X94] :
( c3_1(X94)
| c0_1(X94)
| c2_1(X94) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f433,plain,
( spl0_15
| spl0_10
| ~ spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f319,f431,f427,f399,f423]) ).
fof(f435,definition,
( spl0_18
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f438,plain,
( ~ spl0_9
| spl0_18
| ~ spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f318,f431,f427,f435,f395]) ).
fof(f444,definition,
( spl0_20
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f448,definition,
( spl0_21
<=> ! [X92] :
( ~ c3_1(X92)
| c2_1(X92)
| c0_1(X92) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f449,plain,
( ! [X92] :
( ~ c3_1(X92)
| c2_1(X92)
| c0_1(X92) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f451,plain,
( spl0_4
| spl0_18
| ~ spl0_16
| spl0_21 ),
inference(avatar_split_clause,[],[f316,f448,f427,f435,f373]) ).
fof(f453,definition,
( spl0_22
<=> ! [X90] :
( ~ c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f454,plain,
( ! [X90] :
( c3_1(X90)
| ~ c2_1(X90)
| ~ c1_1(X90) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f457,definition,
( spl0_23
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f461,definition,
( spl0_24
<=> ! [X89] :
( ~ c3_1(X89)
| ~ c1_1(X89)
| c0_1(X89) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f462,plain,
( ! [X89] :
( ~ c3_1(X89)
| ~ c1_1(X89)
| c0_1(X89) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f464,definition,
( spl0_25
<=> ! [X88] :
( ~ c2_1(X88)
| ~ c1_1(X88)
| c0_1(X88) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f465,plain,
( ! [X88] :
( ~ c2_1(X88)
| ~ c1_1(X88)
| c0_1(X88) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f466,plain,
( ~ spl0_23
| spl0_24
| ~ spl0_16
| spl0_25 ),
inference(avatar_split_clause,[],[f326,f464,f427,f461,f457]) ).
fof(f468,definition,
( spl0_26
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f472,definition,
( spl0_27
<=> ! [X87] :
( ~ c2_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f473,plain,
( ! [X87] :
( ~ c3_1(X87)
| ~ c1_1(X87)
| ~ c2_1(X87) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f474,plain,
( ~ spl0_26
| spl0_1
| ~ spl0_16
| spl0_27 ),
inference(avatar_split_clause,[],[f313,f472,f427,f360,f468]) ).
fof(f480,definition,
( spl0_29
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f484,definition,
( spl0_30
<=> ! [X86] :
( ~ c2_1(X86)
| c0_1(X86)
| ~ c3_1(X86) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f485,plain,
( ! [X86] :
( ~ c3_1(X86)
| c0_1(X86)
| ~ c2_1(X86) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f487,plain,
( spl0_4
| spl0_18
| ~ spl0_16
| spl0_30 ),
inference(avatar_split_clause,[],[f311,f484,f427,f435,f373]) ).
fof(f488,plain,
( spl0_8
| spl0_18
| ~ spl0_16
| spl0_30 ),
inference(avatar_split_clause,[],[f310,f484,f427,f435,f390]) ).
fof(f490,definition,
( spl0_31
<=> ! [X83] :
( c0_1(X83)
| c3_1(X83)
| ~ c1_1(X83) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f491,plain,
( ! [X83] :
( c3_1(X83)
| c0_1(X83)
| ~ c1_1(X83) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f490]) ).
fof(f495,definition,
( spl0_32
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f499,definition,
( spl0_33
<=> ! [X79] :
( c1_1(X79)
| c3_1(X79)
| c2_1(X79) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f500,plain,
( ! [X79] :
( c3_1(X79)
| c1_1(X79)
| c2_1(X79) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f501,plain,
( ~ spl0_32
| ~ spl0_2
| ~ spl0_16
| spl0_33 ),
inference(avatar_split_clause,[],[f307,f499,f427,f364,f495]) ).
fof(f508,definition,
( spl0_35
<=> ! [X77] :
( c1_1(X77)
| c3_1(X77)
| c0_1(X77) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f509,plain,
( ! [X77] :
( c3_1(X77)
| c1_1(X77)
| c0_1(X77) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f510,plain,
( spl0_1
| spl0_10
| ~ spl0_16
| spl0_35 ),
inference(avatar_split_clause,[],[f305,f508,f427,f399,f360]) ).
fof(f512,definition,
( spl0_36
<=> ! [X76] :
( c0_1(X76)
| c2_1(X76)
| ~ c1_1(X76) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f513,plain,
( ! [X76] :
( c2_1(X76)
| c0_1(X76)
| ~ c1_1(X76) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( spl0_36
| spl0_27
| ~ spl0_16
| spl0_35 ),
inference(avatar_split_clause,[],[f329,f508,f427,f472,f512]) ).
fof(f520,definition,
( spl0_38
<=> ! [X73] :
( c1_1(X73)
| c2_1(X73)
| c0_1(X73) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f521,plain,
( ! [X73] :
( c2_1(X73)
| c1_1(X73)
| c0_1(X73) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f523,plain,
( spl0_8
| spl0_30
| ~ spl0_16
| spl0_38 ),
inference(avatar_split_clause,[],[f330,f520,f427,f484,f390]) ).
fof(f525,definition,
( spl0_39
<=> ! [X70] :
( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70) ) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f526,plain,
( ! [X70] :
( c3_1(X70)
| c1_1(X70)
| ~ c2_1(X70) )
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f527,plain,
( ~ spl0_6
| spl0_12
| ~ spl0_16
| spl0_39 ),
inference(avatar_split_clause,[],[f301,f525,f427,f409,f382]) ).
fof(f528,plain,
( spl0_20
| spl0_24
| ~ spl0_16
| spl0_39 ),
inference(avatar_split_clause,[],[f331,f525,f427,f461,f444]) ).
fof(f530,definition,
( spl0_40
<=> ! [X67] :
( c1_1(X67)
| c0_1(X67)
| ~ c2_1(X67) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f531,plain,
( ! [X67] :
( ~ c2_1(X67)
| c0_1(X67)
| c1_1(X67) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f532,plain,
( spl0_12
| ~ spl0_16
| spl0_40 ),
inference(avatar_split_clause,[],[f299,f530,f427,f409]) ).
fof(f533,plain,
( spl0_31
| ~ spl0_16
| spl0_40 ),
inference(avatar_split_clause,[],[f332,f530,f427,f490]) ).
fof(f534,plain,
( spl0_25
| spl0_35
| ~ spl0_16
| spl0_40 ),
inference(avatar_split_clause,[],[f333,f530,f427,f508,f464]) ).
fof(f536,definition,
( spl0_41
<=> ! [X61] :
( c1_1(X61)
| ~ c3_1(X61)
| ~ c2_1(X61) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f537,plain,
( ! [X61] :
( ~ c3_1(X61)
| c1_1(X61)
| ~ c2_1(X61) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f540,definition,
( spl0_42
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f544,plain,
( spl0_10
| spl0_22
| ~ spl0_16
| spl0_41 ),
inference(avatar_split_clause,[],[f335,f536,f427,f453,f399]) ).
fof(f545,plain,
( spl0_5
| spl0_25
| ~ spl0_16
| spl0_41 ),
inference(avatar_split_clause,[],[f336,f536,f427,f464,f377]) ).
fof(f551,definition,
( spl0_44
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f555,definition,
( spl0_45
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f559,definition,
( spl0_46
<=> ! [X52] :
( ~ c0_1(X52)
| c3_1(X52)
| ~ c1_1(X52) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f560,plain,
( ! [X52] :
( c3_1(X52)
| ~ c0_1(X52)
| ~ c1_1(X52) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f563,definition,
( spl0_47
<=> ! [X51] :
( ~ c3_1(X51)
| c2_1(X51)
| ~ c1_1(X51) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f564,plain,
( ! [X51] :
( ~ c3_1(X51)
| c2_1(X51)
| ~ c1_1(X51) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f565,plain,
( spl0_47
| spl0_21
| ~ spl0_16
| spl0_46 ),
inference(avatar_split_clause,[],[f338,f559,f427,f448,f563]) ).
fof(f567,plain,
( spl0_20
| spl0_39
| ~ spl0_16
| spl0_46 ),
inference(avatar_split_clause,[],[f340,f559,f427,f525,f444]) ).
fof(f569,definition,
( spl0_48
<=> ! [X42] :
( ~ c0_1(X42)
| c2_1(X42)
| ~ c1_1(X42) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f570,plain,
( ! [X42] :
( c2_1(X42)
| ~ c0_1(X42)
| ~ c1_1(X42) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f571,plain,
( spl0_17
| spl0_21
| ~ spl0_16
| spl0_48 ),
inference(avatar_split_clause,[],[f341,f569,f427,f448,f431]) ).
fof(f577,definition,
( spl0_50
<=> ! [X37] :
( ~ c0_1(X37)
| ~ c1_1(X37)
| ~ c3_1(X37) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f578,plain,
( ! [X37] :
( ~ c3_1(X37)
| ~ c1_1(X37)
| ~ c0_1(X37) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f579,plain,
( spl0_42
| spl0_22
| ~ spl0_16
| spl0_50 ),
inference(avatar_split_clause,[],[f343,f577,f427,f453,f540]) ).
fof(f581,definition,
( spl0_51
<=> ! [X35] :
( ~ c0_1(X35)
| c3_1(X35)
| ~ c2_1(X35) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f582,plain,
( ! [X35] :
( c3_1(X35)
| ~ c0_1(X35)
| ~ c2_1(X35) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f584,plain,
( spl0_7
| spl0_33
| ~ spl0_16
| spl0_51 ),
inference(avatar_split_clause,[],[f345,f581,f427,f499,f386]) ).
fof(f586,definition,
( spl0_52
<=> ! [X32] :
( ~ c0_1(X32)
| ~ c1_1(X32)
| ~ c2_1(X32) ) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f587,plain,
( ! [X32] :
( ~ c2_1(X32)
| ~ c1_1(X32)
| ~ c0_1(X32) )
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f588,plain,
( ~ spl0_23
| spl0_29
| ~ spl0_16
| spl0_52 ),
inference(avatar_split_clause,[],[f282,f586,f427,f480,f457]) ).
fof(f596,definition,
( spl0_54
<=> ! [X27] :
( ~ c0_1(X27)
| ~ c3_1(X27)
| ~ c2_1(X27) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f597,plain,
( ! [X27] :
( ~ c3_1(X27)
| ~ c0_1(X27)
| ~ c2_1(X27) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f598,plain,
( spl0_5
| spl0_42
| ~ spl0_16
| spl0_54 ),
inference(avatar_split_clause,[],[f279,f596,f427,f540,f377]) ).
fof(f599,plain,
( spl0_35
| spl0_38
| ~ spl0_16
| spl0_54 ),
inference(avatar_split_clause,[],[f348,f596,f427,f520,f508]) ).
fof(f601,definition,
( spl0_55
<=> ! [X22] :
( ~ c0_1(X22)
| c2_1(X22)
| c1_1(X22) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f602,plain,
( ! [X22] :
( c2_1(X22)
| ~ c0_1(X22)
| c1_1(X22) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f603,plain,
( spl0_45
| spl0_41
| ~ spl0_16
| spl0_55 ),
inference(avatar_split_clause,[],[f349,f601,f427,f536,f555]) ).
fof(f605,definition,
( spl0_56
<=> ! [X21] :
( ~ c0_1(X21)
| c3_1(X21)
| c1_1(X21) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f606,plain,
( ! [X21] :
( c3_1(X21)
| ~ c0_1(X21)
| c1_1(X21) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f607,plain,
( spl0_44
| spl0_56
| ~ spl0_16
| spl0_55 ),
inference(avatar_split_clause,[],[f350,f601,f427,f605,f551]) ).
fof(f608,plain,
( spl0_47
| spl0_56
| ~ spl0_16
| spl0_55 ),
inference(avatar_split_clause,[],[f351,f601,f427,f605,f563]) ).
fof(f610,definition,
( spl0_57
<=> ! [X16] :
( ~ c0_1(X16)
| ~ c3_1(X16)
| c1_1(X16) ) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f611,plain,
( ! [X16] :
( ~ c3_1(X16)
| ~ c0_1(X16)
| c1_1(X16) )
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f612,plain,
( spl0_42
| spl0_12
| ~ spl0_16
| spl0_57 ),
inference(avatar_split_clause,[],[f274,f610,f427,f409,f540]) ).
fof(f621,plain,
( spl0_12
| spl0_55
| ~ spl0_16
| spl0_57 ),
inference(avatar_split_clause,[],[f354,f610,f427,f601,f409]) ).
fof(f633,definition,
( spl0_62
<=> c3_1(a1236) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f635,plain,
( ~ c3_1(a1236)
| spl0_62 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,plain,
( ~ spl0_62
| spl0_11 ),
inference(avatar_split_clause,[],[f266,f404,f633]) ).
fof(f638,definition,
( spl0_63
<=> c2_1(a1236) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f640,plain,
( ~ c2_1(a1236)
| spl0_63 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f641,plain,
( ~ spl0_63
| spl0_11 ),
inference(avatar_split_clause,[],[f265,f404,f638]) ).
fof(f643,definition,
( spl0_64
<=> c0_1(a1236) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f646,plain,
( ~ spl0_64
| spl0_11 ),
inference(avatar_split_clause,[],[f264,f404,f643]) ).
fof(f681,definition,
( spl0_71
<=> c3_1(a1182) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f683,plain,
( ~ c3_1(a1182)
| spl0_71 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f684,plain,
( ~ spl0_71
| spl0_23 ),
inference(avatar_split_clause,[],[f254,f457,f681]) ).
fof(f686,definition,
( spl0_72
<=> c2_1(a1182) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f689,plain,
( ~ spl0_72
| spl0_23 ),
inference(avatar_split_clause,[],[f253,f457,f686]) ).
fof(f691,definition,
( spl0_73
<=> c1_1(a1182) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f694,plain,
( spl0_73
| spl0_23 ),
inference(avatar_split_clause,[],[f252,f457,f691]) ).
fof(f713,definition,
( spl0_77
<=> c3_1(a1218) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f715,plain,
( c3_1(a1218)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f716,plain,
( spl0_77
| spl0_26 ),
inference(avatar_split_clause,[],[f246,f468,f713]) ).
fof(f718,definition,
( spl0_78
<=> c1_1(a1218) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f721,plain,
( ~ spl0_78
| spl0_26 ),
inference(avatar_split_clause,[],[f245,f468,f718]) ).
fof(f723,definition,
( spl0_79
<=> c0_1(a1218) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f726,plain,
( spl0_79
| spl0_26 ),
inference(avatar_split_clause,[],[f244,f468,f723]) ).
fof(f729,definition,
( spl0_80
<=> c1_1(a1211) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f731,plain,
( ~ c1_1(a1211)
| spl0_80 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f732,plain,
( ~ spl0_80
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f90,f435,f729]) ).
fof(f734,definition,
( spl0_81
<=> c3_1(a1211) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f736,plain,
( ~ c3_1(a1211)
| spl0_81 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f737,plain,
( ~ spl0_81
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f242,f435,f734]) ).
fof(f739,definition,
( spl0_82
<=> c0_1(a1211) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f742,plain,
( ~ spl0_82
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f241,f435,f739]) ).
fof(f745,definition,
( spl0_83
<=> c1_1(a1207) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f748,plain,
( ~ spl0_83
| spl0_2 ),
inference(avatar_split_clause,[],[f240,f364,f745]) ).
fof(f750,definition,
( spl0_84
<=> c3_1(a1207) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f752,plain,
( ~ c3_1(a1207)
| spl0_84 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f753,plain,
( ~ spl0_84
| spl0_2 ),
inference(avatar_split_clause,[],[f239,f364,f750]) ).
fof(f755,definition,
( spl0_85
<=> c2_1(a1207) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f757,plain,
( ~ c2_1(a1207)
| spl0_85 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f758,plain,
( ~ spl0_85
| spl0_2 ),
inference(avatar_split_clause,[],[f238,f364,f755]) ).
fof(f759,plain,
( spl0_16
| spl0_2 ),
inference(avatar_split_clause,[],[f237,f364,f427]) ).
fof(f777,definition,
( spl0_89
<=> c2_1(a1204) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f780,plain,
( spl0_89
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f234,f360,f777]) ).
fof(f782,definition,
( spl0_90
<=> c1_1(a1204) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f785,plain,
( ~ spl0_90
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f103,f360,f782]) ).
fof(f787,definition,
( spl0_91
<=> c3_1(a1204) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f789,plain,
( ~ c3_1(a1204)
| spl0_91 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f790,plain,
( ~ spl0_91
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f233,f360,f787]) ).
fof(f791,plain,
( spl0_16
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f105,f360,f427]) ).
fof(f809,definition,
( spl0_95
<=> c2_1(a1200) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f811,plain,
( c2_1(a1200)
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f812,plain,
( spl0_95
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f230,f390,f809]) ).
fof(f814,definition,
( spl0_96
<=> c1_1(a1200) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f817,plain,
( ~ spl0_96
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f111,f390,f814]) ).
fof(f819,definition,
( spl0_97
<=> c0_1(a1200) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f822,plain,
( ~ spl0_97
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f229,f390,f819]) ).
fof(f825,definition,
( spl0_98
<=> c3_1(a1199) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f827,plain,
( c3_1(a1199)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f828,plain,
( spl0_98
| spl0_6 ),
inference(avatar_split_clause,[],[f228,f382,f825]) ).
fof(f830,definition,
( spl0_99
<=> c0_1(a1199) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f833,plain,
( spl0_99
| spl0_6 ),
inference(avatar_split_clause,[],[f227,f382,f830]) ).
fof(f835,definition,
( spl0_100
<=> c2_1(a1199) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f838,plain,
( ~ spl0_100
| spl0_6 ),
inference(avatar_split_clause,[],[f226,f382,f835]) ).
fof(f857,definition,
( spl0_104
<=> c1_1(a1194) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f859,plain,
( ~ c1_1(a1194)
| spl0_104 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f860,plain,
( ~ spl0_104
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f122,f373,f857]) ).
fof(f862,definition,
( spl0_105
<=> c0_1(a1194) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f865,plain,
( spl0_105
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f220,f373,f862]) ).
fof(f867,definition,
( spl0_106
<=> c2_1(a1194) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f869,plain,
( ~ c2_1(a1194)
| spl0_106 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f870,plain,
( ~ spl0_106
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f219,f373,f867]) ).
fof(f873,definition,
( spl0_107
<=> c2_1(a1192) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f875,plain,
( c2_1(a1192)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f876,plain,
( spl0_107
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f218,f399,f873]) ).
fof(f878,definition,
( spl0_108
<=> c0_1(a1192) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f881,plain,
( spl0_108
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f217,f399,f878]) ).
fof(f883,definition,
( spl0_109
<=> c1_1(a1192) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f885,plain,
( c1_1(a1192)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f886,plain,
( spl0_109
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f128,f399,f883]) ).
fof(f889,definition,
( spl0_110
<=> c3_1(a1187) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f891,plain,
( c3_1(a1187)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f889]) ).
fof(f892,plain,
( spl0_110
| spl0_32 ),
inference(avatar_split_clause,[],[f216,f495,f889]) ).
fof(f894,definition,
( spl0_111
<=> c2_1(a1187) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f897,plain,
( spl0_111
| spl0_32 ),
inference(avatar_split_clause,[],[f215,f495,f894]) ).
fof(f899,definition,
( spl0_112
<=> c0_1(a1187) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f902,plain,
( spl0_112
| spl0_32 ),
inference(avatar_split_clause,[],[f214,f495,f899]) ).
fof(f905,definition,
( spl0_113
<=> c3_1(a1186) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f907,plain,
( c3_1(a1186)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f908,plain,
( spl0_113
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f212,f444,f905]) ).
fof(f910,definition,
( spl0_114
<=> c2_1(a1186) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f913,plain,
( spl0_114
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f211,f444,f910]) ).
fof(f915,definition,
( spl0_115
<=> c0_1(a1186) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f918,plain,
( ~ spl0_115
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f210,f444,f915]) ).
fof(f921,definition,
( spl0_116
<=> c2_1(a1184) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f923,plain,
( c2_1(a1184)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f924,plain,
( spl0_116
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f209,f423,f921]) ).
fof(f931,definition,
( spl0_118
<=> c0_1(a1184) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f934,plain,
( spl0_118
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f208,f423,f931]) ).
fof(f937,definition,
( spl0_119
<=> c2_1(a1181) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f939,plain,
( c2_1(a1181)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f940,plain,
( spl0_119
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f207,f480,f937]) ).
fof(f942,definition,
( spl0_120
<=> c3_1(a1181) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f944,plain,
( ~ c3_1(a1181)
| spl0_120 ),
inference(avatar_component_clause,[],[f942]) ).
fof(f945,plain,
( ~ spl0_120
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f206,f480,f942]) ).
fof(f947,definition,
( spl0_121
<=> c0_1(a1181) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f950,plain,
( ~ spl0_121
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f205,f480,f947]) ).
fof(f953,definition,
( spl0_122
<=> c3_1(a1180) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f955,plain,
( c3_1(a1180)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f956,plain,
( spl0_122
| spl0_3 ),
inference(avatar_split_clause,[],[f204,f368,f953]) ).
fof(f958,definition,
( spl0_123
<=> c0_1(a1180) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f961,plain,
( spl0_123
| spl0_3 ),
inference(avatar_split_clause,[],[f203,f368,f958]) ).
fof(f963,definition,
( spl0_124
<=> c1_1(a1180) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f966,plain,
( spl0_124
| spl0_3 ),
inference(avatar_split_clause,[],[f202,f368,f963]) ).
fof(f967,plain,
( spl0_16
| spl0_3 ),
inference(avatar_split_clause,[],[f201,f368,f427]) ).
fof(f985,definition,
( spl0_128
<=> c3_1(a1178) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f987,plain,
( c3_1(a1178)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f988,plain,
( spl0_128
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f198,f377,f985]) ).
fof(f990,definition,
( spl0_129
<=> c2_1(a1178) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f993,plain,
( ~ spl0_129
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f197,f377,f990]) ).
fof(f995,definition,
( spl0_130
<=> c1_1(a1178) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f998,plain,
( spl0_130
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f156,f377,f995]) ).
fof(f1001,definition,
( spl0_131
<=> c3_1(a1176) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1003,plain,
( c3_1(a1176)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f1001]) ).
fof(f1004,plain,
( spl0_131
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f196,f555,f1001]) ).
fof(f1006,definition,
( spl0_132
<=> c2_1(a1176) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1009,plain,
( ~ spl0_132
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f195,f555,f1006]) ).
fof(f1011,definition,
( spl0_133
<=> c0_1(a1176) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1014,plain,
( ~ spl0_133
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f194,f555,f1011]) ).
fof(f1017,definition,
( spl0_134
<=> c0_1(a1175) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f1020,plain,
( spl0_134
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f193,f551,f1017]) ).
fof(f1022,definition,
( spl0_135
<=> c2_1(a1175) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f1024,plain,
( ~ c2_1(a1175)
| spl0_135 ),
inference(avatar_component_clause,[],[f1022]) ).
fof(f1025,plain,
( ~ spl0_135
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f192,f551,f1022]) ).
fof(f1027,definition,
( spl0_136
<=> c1_1(a1175) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f1030,plain,
( spl0_136
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f164,f551,f1027]) ).
fof(f1033,definition,
( spl0_137
<=> c3_1(a1174) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1035,plain,
( c3_1(a1174)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1036,plain,
( spl0_137
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f191,f540,f1033]) ).
fof(f1038,definition,
( spl0_138
<=> c1_1(a1174) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1040,plain,
( c1_1(a1174)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f1038]) ).
fof(f1041,plain,
( spl0_138
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f167,f540,f1038]) ).
fof(f1043,definition,
( spl0_139
<=> c0_1(a1174) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1046,plain,
( ~ spl0_139
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f190,f540,f1043]) ).
fof(f1049,definition,
( spl0_140
<=> c0_1(a1172) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1052,plain,
( spl0_140
| spl0_9 ),
inference(avatar_split_clause,[],[f189,f395,f1049]) ).
fof(f1054,definition,
( spl0_141
<=> c3_1(a1172) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1056,plain,
( ~ c3_1(a1172)
| spl0_141 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1057,plain,
( ~ spl0_141
| spl0_9 ),
inference(avatar_split_clause,[],[f188,f395,f1054]) ).
fof(f1059,definition,
( spl0_142
<=> c2_1(a1172) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1061,plain,
( ~ c2_1(a1172)
| spl0_142 ),
inference(avatar_component_clause,[],[f1059]) ).
fof(f1062,plain,
( ~ spl0_142
| spl0_9 ),
inference(avatar_split_clause,[],[f187,f395,f1059]) ).
fof(f1065,definition,
( spl0_143
<=> c3_1(a1169) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1067,plain,
( c3_1(a1169)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f1065]) ).
fof(f1068,plain,
( spl0_143
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f185,f386,f1065]) ).
fof(f1070,definition,
( spl0_144
<=> c2_1(a1169) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1072,plain,
( c2_1(a1169)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f1070]) ).
fof(f1073,plain,
( spl0_144
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f184,f386,f1070]) ).
fof(f1075,definition,
( spl0_145
<=> c1_1(a1169) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1078,plain,
( spl0_145
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f176,f386,f1075]) ).
fof(f1081,definition,
( spl0_146
<=> c2_1(a1168) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1083,plain,
( c2_1(a1168)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1084,plain,
( spl0_146
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f183,f409,f1081]) ).
fof(f1086,definition,
( spl0_147
<=> c1_1(a1168) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1089,plain,
( spl0_147
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f179,f409,f1086]) ).
fof(f1091,definition,
( spl0_148
<=> c0_1(a1168) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1094,plain,
( ~ spl0_148
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f182,f409,f1091]) ).
fof(f1115,plain,
( c0_1(a1182)
| c2_1(a1182)
| ~ spl0_17
| spl0_71 ),
inference(resolution,[],[f432,f683]) ).
fof(f1125,definition,
( spl0_150
<=> c0_1(a1182) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1140,definition,
( spl0_153
<=> c2_1(a1211) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1142,plain,
( c2_1(a1211)
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1145,definition,
( spl0_154
<=> c0_1(a1207) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f1174,definition,
( spl0_159
<=> c2_1(a1180) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1184,definition,
( spl0_161
<=> c0_1(a1178) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1190,definition,
( spl0_162
<=> c2_1(a1174) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1196,definition,
( spl0_163
<=> c0_1(a1169) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1223,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22
| ~ spl0_24 ),
inference(resolution,[],[f462,f454]) ).
fof(f1224,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_22
| ~ spl0_24 ),
inference(duplicate_literal_removal,[],[f1223]) ).
fof(f1225,plain,
( spl0_25
| ~ spl0_22
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f1224,f461,f453,f464]) ).
fof(f1245,plain,
( c1_1(a1207)
| c2_1(a1207)
| ~ spl0_33
| spl0_84 ),
inference(resolution,[],[f500,f752]) ).
fof(f1246,plain,
( c1_1(a1211)
| c2_1(a1211)
| ~ spl0_33
| spl0_81 ),
inference(resolution,[],[f500,f736]) ).
fof(f1254,definition,
( spl0_164
<=> c1_1(a1236) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1261,plain,
( spl0_153
| spl0_80
| ~ spl0_33
| spl0_81 ),
inference(avatar_split_clause,[],[f1246,f734,f499,f729,f1140]) ).
fof(f1267,definition,
( spl0_165
<=> c1_1(a1199) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1273,definition,
( spl0_166
<=> c1_1(a1187) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1275,plain,
( c1_1(a1187)
| ~ spl0_166 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1283,definition,
( spl0_168
<=> c1_1(a1181) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1297,definition,
( spl0_170
<=> c1_1(a1172) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1302,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_30
| ~ spl0_35 ),
inference(resolution,[],[f509,f485]) ).
fof(f1305,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_21
| ~ spl0_35 ),
inference(resolution,[],[f509,f449]) ).
fof(f1321,plain,
( c1_1(a1207)
| c0_1(a1207)
| ~ spl0_35
| spl0_84 ),
inference(resolution,[],[f509,f752]) ).
fof(f1327,plain,
( c1_1(a1236)
| c0_1(a1236)
| ~ spl0_35
| spl0_62 ),
inference(resolution,[],[f509,f635]) ).
fof(f1328,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_21
| ~ spl0_35 ),
inference(duplicate_literal_removal,[],[f1305]) ).
fof(f1330,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_30
| ~ spl0_35 ),
inference(duplicate_literal_removal,[],[f1302]) ).
fof(f1336,plain,
( spl0_154
| spl0_83
| ~ spl0_35
| spl0_84 ),
inference(avatar_split_clause,[],[f1321,f750,f508,f745,f1145]) ).
fof(f1375,plain,
( c1_1(a1236)
| c0_1(a1236)
| ~ spl0_38
| spl0_63 ),
inference(resolution,[],[f521,f640]) ).
fof(f1376,plain,
( spl0_64
| spl0_164
| ~ spl0_38
| spl0_63 ),
inference(avatar_split_clause,[],[f1375,f638,f520,f1254,f643]) ).
fof(f1416,plain,
( c1_1(a1204)
| ~ c2_1(a1204)
| ~ spl0_39
| spl0_91 ),
inference(resolution,[],[f526,f789]) ).
fof(f1428,plain,
( c0_1(a1200)
| c1_1(a1200)
| ~ spl0_40
| ~ spl0_95 ),
inference(resolution,[],[f531,f811]) ).
fof(f1430,plain,
( spl0_96
| spl0_97
| ~ spl0_40
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f1428,f809,f530,f819,f814]) ).
fof(f1465,plain,
( ~ c0_1(a1182)
| ~ c1_1(a1182)
| ~ spl0_46
| spl0_71 ),
inference(resolution,[],[f560,f683]) ).
fof(f1471,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_46
| ~ spl0_50 ),
inference(resolution,[],[f578,f560]) ).
fof(f1472,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_46
| ~ spl0_50 ),
inference(duplicate_literal_removal,[],[f1471]) ).
fof(f1473,plain,
( ~ c0_1(a1192)
| ~ spl0_46
| ~ spl0_50
| ~ spl0_109 ),
inference(resolution,[],[f1472,f885]) ).
fof(f1477,plain,
( ~ spl0_108
| ~ spl0_46
| ~ spl0_50
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f1473,f883,f577,f559,f878]) ).
fof(f1479,plain,
( c0_1(a1174)
| ~ c2_1(a1174)
| ~ spl0_30
| ~ spl0_137 ),
inference(resolution,[],[f1035,f485]) ).
fof(f1481,plain,
( ~ c1_1(a1174)
| c0_1(a1174)
| ~ spl0_24
| ~ spl0_137 ),
inference(resolution,[],[f1035,f462]) ).
fof(f1484,plain,
( spl0_139
| ~ spl0_138
| ~ spl0_24
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f1481,f1033,f461,f1038,f1043]) ).
fof(f1489,plain,
( spl0_72
| spl0_150
| ~ spl0_17
| spl0_71 ),
inference(avatar_split_clause,[],[f1115,f681,f431,f1125,f686]) ).
fof(f1492,plain,
( spl0_64
| spl0_164
| ~ spl0_35
| spl0_62 ),
inference(avatar_split_clause,[],[f1327,f633,f508,f1254,f643]) ).
fof(f1493,plain,
( spl0_38
| ~ spl0_21
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f1328,f508,f448,f520]) ).
fof(f1525,plain,
( c0_1(a1186)
| ~ c2_1(a1186)
| ~ spl0_30
| ~ spl0_113 ),
inference(resolution,[],[f907,f485]) ).
fof(f1538,plain,
( ~ c1_1(a1178)
| c0_1(a1178)
| ~ spl0_24
| ~ spl0_128 ),
inference(resolution,[],[f987,f462]) ).
fof(f1547,plain,
( ~ c0_1(a1187)
| ~ spl0_46
| ~ spl0_50
| ~ spl0_166 ),
inference(resolution,[],[f1472,f1275]) ).
fof(f1553,plain,
( ~ spl0_112
| ~ spl0_46
| ~ spl0_50
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f1547,f1273,f577,f559,f899]) ).
fof(f1556,plain,
( ~ spl0_114
| spl0_115
| ~ spl0_30
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f1525,f905,f484,f915,f910]) ).
fof(f1581,plain,
( c0_1(a1181)
| c1_1(a1181)
| ~ spl0_40
| ~ spl0_119 ),
inference(resolution,[],[f939,f531]) ).
fof(f1598,plain,
( c0_1(a1207)
| c2_1(a1207)
| ~ spl0_17
| spl0_84 ),
inference(resolution,[],[f432,f752]) ).
fof(f1628,plain,
( c0_1(a1182)
| ~ c1_1(a1182)
| ~ spl0_31
| spl0_71 ),
inference(resolution,[],[f491,f683]) ).
fof(f1630,plain,
( c0_1(a1236)
| ~ c1_1(a1236)
| ~ spl0_31
| spl0_62 ),
inference(resolution,[],[f491,f635]) ).
fof(f1643,plain,
( c1_1(a1207)
| c0_1(a1207)
| ~ spl0_35
| spl0_84 ),
inference(resolution,[],[f509,f752]) ).
fof(f1670,plain,
( c0_1(a1236)
| ~ c1_1(a1236)
| ~ spl0_36
| spl0_63 ),
inference(resolution,[],[f513,f640]) ).
fof(f1720,plain,
( c2_1(a1178)
| ~ c1_1(a1178)
| ~ spl0_47
| ~ spl0_128 ),
inference(resolution,[],[f564,f987]) ).
fof(f1735,plain,
( ~ spl0_73
| ~ spl0_150
| ~ spl0_46
| spl0_71 ),
inference(avatar_split_clause,[],[f1465,f681,f559,f1125,f691]) ).
fof(f1740,plain,
( ~ spl0_130
| spl0_129
| ~ spl0_47
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1720,f985,f563,f990,f995]) ).
fof(f1742,plain,
( ~ spl0_162
| spl0_139
| ~ spl0_30
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f1479,f1033,f484,f1043,f1190]) ).
fof(f1744,plain,
( spl0_85
| spl0_154
| ~ spl0_17
| spl0_84 ),
inference(avatar_split_clause,[],[f1598,f750,f431,f1145,f755]) ).
fof(f1760,plain,
( c0_1(a1236)
| c2_1(a1236)
| ~ spl0_17
| spl0_62 ),
inference(resolution,[],[f432,f635]) ).
fof(f1762,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_25
| ~ spl0_36 ),
inference(resolution,[],[f465,f513]) ).
fof(f1772,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_25
| ~ spl0_36 ),
inference(duplicate_literal_removal,[],[f1762]) ).
fof(f1808,plain,
( ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_35
| ~ spl0_41 ),
inference(resolution,[],[f537,f509]) ).
fof(f1817,plain,
( c1_1(a1187)
| ~ c2_1(a1187)
| ~ spl0_41
| ~ spl0_110 ),
inference(resolution,[],[f537,f891]) ).
fof(f1824,plain,
( ! [X0] :
( c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_35
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f1808]) ).
fof(f1834,plain,
( c2_1(a1180)
| ~ c1_1(a1180)
| ~ spl0_47
| ~ spl0_122 ),
inference(resolution,[],[f564,f955]) ).
fof(f1839,plain,
( c2_1(a1199)
| ~ c1_1(a1199)
| ~ spl0_47
| ~ spl0_98 ),
inference(resolution,[],[f564,f827]) ).
fof(f1851,plain,
( ~ c0_1(a1175)
| ~ c1_1(a1175)
| ~ spl0_48
| spl0_135 ),
inference(resolution,[],[f570,f1024]) ).
fof(f1873,plain,
( ~ spl0_136
| ~ spl0_134
| ~ spl0_48
| spl0_135 ),
inference(avatar_split_clause,[],[f1851,f1022,f569,f1017,f1027]) ).
fof(f1880,plain,
( ~ c1_1(a1178)
| ~ c0_1(a1178)
| ~ spl0_50
| ~ spl0_128 ),
inference(resolution,[],[f578,f987]) ).
fof(f1882,plain,
( ~ c1_1(a1180)
| ~ c0_1(a1180)
| ~ spl0_50
| ~ spl0_122 ),
inference(resolution,[],[f578,f955]) ).
fof(f1887,plain,
( ~ c1_1(a1199)
| ~ c0_1(a1199)
| ~ spl0_50
| ~ spl0_98 ),
inference(resolution,[],[f578,f827]) ).
fof(f1931,plain,
( ~ c1_1(a1192)
| ~ c0_1(a1192)
| ~ spl0_52
| ~ spl0_107 ),
inference(resolution,[],[f587,f875]) ).
fof(f1935,plain,
( ~ spl0_108
| ~ spl0_109
| ~ spl0_52
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f1931,f873,f586,f883,f878]) ).
fof(f1940,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_51
| ~ spl0_54 ),
inference(resolution,[],[f597,f582]) ).
fof(f1941,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22
| ~ spl0_54 ),
inference(resolution,[],[f597,f454]) ).
fof(f1945,plain,
( ~ c0_1(a1169)
| ~ c2_1(a1169)
| ~ spl0_54
| ~ spl0_143 ),
inference(resolution,[],[f597,f1067]) ).
fof(f1950,plain,
( ~ c0_1(a1180)
| ~ c2_1(a1180)
| ~ spl0_54
| ~ spl0_122 ),
inference(resolution,[],[f597,f955]) ).
fof(f1962,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22
| ~ spl0_54 ),
inference(duplicate_literal_removal,[],[f1941]) ).
fof(f1963,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_51
| ~ spl0_54 ),
inference(duplicate_literal_removal,[],[f1940]) ).
fof(f1967,plain,
( ~ spl0_159
| ~ spl0_123
| ~ spl0_54
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1950,f953,f596,f958,f1174]) ).
fof(f1968,plain,
( spl0_52
| ~ spl0_22
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1962,f596,f453,f586]) ).
fof(f1995,plain,
( spl0_40
| ~ spl0_30
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f1330,f508,f484,f530]) ).
fof(f2032,plain,
( c0_1(a1174)
| ~ spl0_25
| ~ spl0_36
| ~ spl0_138 ),
inference(resolution,[],[f1040,f1772]) ).
fof(f2035,plain,
( ~ c1_1(a1168)
| c0_1(a1168)
| ~ spl0_25
| ~ spl0_146 ),
inference(resolution,[],[f1083,f465]) ).
fof(f2048,plain,
( c2_1(a1176)
| c0_1(a1176)
| ~ spl0_21
| ~ spl0_131 ),
inference(resolution,[],[f449,f1003]) ).
fof(f2104,plain,
( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_38
| ~ spl0_40 ),
inference(resolution,[],[f531,f521]) ).
fof(f2116,plain,
( c0_1(a1211)
| c1_1(a1211)
| ~ spl0_40
| ~ spl0_153 ),
inference(resolution,[],[f531,f1142]) ).
fof(f2120,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0) )
| ~ spl0_38
| ~ spl0_40 ),
inference(duplicate_literal_removal,[],[f2104]) ).
fof(f2144,plain,
( ~ c2_1(a1181)
| ~ c1_1(a1181)
| ~ spl0_22
| spl0_120 ),
inference(resolution,[],[f944,f454]) ).
fof(f2150,plain,
( ~ c0_1(a1172)
| ~ c1_1(a1172)
| ~ spl0_46
| spl0_141 ),
inference(resolution,[],[f560,f1056]) ).
fof(f2161,plain,
( ~ c1_1(a1169)
| ~ c0_1(a1169)
| ~ spl0_52
| ~ spl0_144 ),
inference(resolution,[],[f587,f1072]) ).
fof(f2172,plain,
( ~ spl0_163
| ~ spl0_145
| ~ spl0_52
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f2161,f1070,f586,f1075,f1196]) ).
fof(f2195,plain,
( ~ c0_1(a1172)
| c1_1(a1172)
| ~ spl0_55
| spl0_142 ),
inference(resolution,[],[f602,f1061]) ).
fof(f2204,plain,
( ~ c0_1(a1194)
| c1_1(a1194)
| ~ spl0_55
| spl0_106 ),
inference(resolution,[],[f602,f869]) ).
fof(f2208,plain,
( ~ c0_1(a1207)
| c1_1(a1207)
| ~ spl0_55
| spl0_85 ),
inference(resolution,[],[f602,f757]) ).
fof(f2233,plain,
( spl0_85
| spl0_83
| ~ spl0_33
| spl0_84 ),
inference(avatar_split_clause,[],[f1245,f750,f499,f745,f755]) ).
fof(f2240,plain,
( spl0_133
| spl0_132
| ~ spl0_21
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f2048,f1001,f448,f1006,f1011]) ).
fof(f2245,plain,
( spl0_63
| spl0_64
| ~ spl0_17
| spl0_62 ),
inference(avatar_split_clause,[],[f1760,f633,f431,f643,f638]) ).
fof(f2257,plain,
( c1_1(a1207)
| c0_1(a1207)
| ~ spl0_38
| spl0_85 ),
inference(resolution,[],[f757,f521]) ).
fof(f2387,plain,
( ~ c0_1(a1172)
| c1_1(a1172)
| ~ spl0_56
| spl0_141 ),
inference(resolution,[],[f606,f1056]) ).
fof(f2391,plain,
( ~ c0_1(a1207)
| c1_1(a1207)
| ~ spl0_56
| spl0_84 ),
inference(resolution,[],[f606,f752]) ).
fof(f2398,plain,
( spl0_83
| ~ spl0_154
| ~ spl0_56
| spl0_84 ),
inference(avatar_split_clause,[],[f2391,f750,f605,f1145,f745]) ).
fof(f2404,plain,
( spl0_154
| spl0_83
| ~ spl0_35
| spl0_84 ),
inference(avatar_split_clause,[],[f1643,f750,f508,f745,f1145]) ).
fof(f2412,plain,
( spl0_161
| ~ spl0_130
| ~ spl0_24
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1538,f985,f461,f995,f1184]) ).
fof(f2478,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22
| ~ spl0_30 ),
inference(resolution,[],[f485,f454]) ).
fof(f2479,plain,
( c0_1(a1169)
| ~ c2_1(a1169)
| ~ spl0_30
| ~ spl0_143 ),
inference(resolution,[],[f485,f1067]) ).
fof(f2493,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22
| ~ spl0_30 ),
inference(duplicate_literal_removal,[],[f2478]) ).
fof(f2511,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_56
| ~ spl0_57 ),
inference(resolution,[],[f611,f606]) ).
fof(f2523,plain,
( ~ c0_1(a1199)
| c1_1(a1199)
| ~ spl0_57
| ~ spl0_98 ),
inference(resolution,[],[f611,f827]) ).
fof(f2526,plain,
( ~ c0_1(a1218)
| c1_1(a1218)
| ~ spl0_57
| ~ spl0_77 ),
inference(resolution,[],[f611,f715]) ).
fof(f2531,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_56
| ~ spl0_57 ),
inference(duplicate_literal_removal,[],[f2511]) ).
fof(f2534,plain,
( spl0_78
| ~ spl0_79
| ~ spl0_57
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2526,f713,f610,f723,f718]) ).
fof(f2538,plain,
( spl0_148
| ~ spl0_147
| ~ spl0_25
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f2035,f1081,f464,f1086,f1091]) ).
fof(f2545,plain,
( ~ c0_1(a1194)
| ~ spl0_56
| ~ spl0_57
| spl0_104 ),
inference(resolution,[],[f2531,f859]) ).
fof(f2548,plain,
( ~ spl0_105
| ~ spl0_56
| ~ spl0_57
| spl0_104 ),
inference(avatar_split_clause,[],[f2545,f857,f610,f605,f862]) ).
fof(f2554,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_27
| ~ spl0_51 ),
inference(resolution,[],[f473,f582]) ).
fof(f2557,plain,
( ~ c1_1(a1169)
| ~ c2_1(a1169)
| ~ spl0_27
| ~ spl0_143 ),
inference(resolution,[],[f473,f1067]) ).
fof(f2561,plain,
( ~ c1_1(a1180)
| ~ c2_1(a1180)
| ~ spl0_27
| ~ spl0_122 ),
inference(resolution,[],[f473,f955]) ).
fof(f2573,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_27
| ~ spl0_51 ),
inference(duplicate_literal_removal,[],[f2554]) ).
fof(f2576,plain,
( ~ spl0_144
| ~ spl0_145
| ~ spl0_27
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f2557,f1065,f472,f1075,f1070]) ).
fof(f2595,plain,
( c1_1(a1172)
| c2_1(a1172)
| ~ spl0_33
| spl0_141 ),
inference(resolution,[],[f500,f1056]) ).
fof(f2623,plain,
( ~ spl0_124
| spl0_159
| ~ spl0_47
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1834,f953,f563,f1174,f963]) ).
fof(f2627,plain,
( ~ spl0_165
| spl0_100
| ~ spl0_47
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f1839,f825,f563,f835,f1267]) ).
fof(f2643,plain,
( ~ spl0_159
| ~ spl0_124
| ~ spl0_27
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f2561,f953,f472,f963,f1174]) ).
fof(f2691,plain,
( c2_1(a1174)
| c0_1(a1174)
| ~ spl0_21
| ~ spl0_137 ),
inference(resolution,[],[f1035,f449]) ).
fof(f2697,plain,
( c2_1(a1174)
| ~ c1_1(a1174)
| ~ spl0_47
| ~ spl0_137 ),
inference(resolution,[],[f564,f1035]) ).
fof(f2712,plain,
( ~ c0_1(a1192)
| ~ spl0_51
| ~ spl0_54
| ~ spl0_107 ),
inference(resolution,[],[f1963,f875]) ).
fof(f2715,plain,
( ~ spl0_108
| ~ spl0_51
| ~ spl0_54
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f2712,f873,f596,f581,f878]) ).
fof(f2734,plain,
( c0_1(a1211)
| ~ spl0_38
| ~ spl0_40
| spl0_80 ),
inference(resolution,[],[f731,f2120]) ).
fof(f2735,plain,
( c1_1(a1211)
| c0_1(a1211)
| ~ spl0_35
| spl0_81 ),
inference(resolution,[],[f736,f509]) ).
fof(f2738,plain,
( ~ c0_1(a1184)
| ~ spl0_51
| ~ spl0_54
| ~ spl0_116 ),
inference(resolution,[],[f923,f1963]) ).
fof(f2739,plain,
( ~ spl0_118
| ~ spl0_51
| ~ spl0_54
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f2738,f921,f596,f581,f931]) ).
fof(f2740,plain,
( ~ spl0_89
| spl0_90
| ~ spl0_39
| spl0_91 ),
inference(avatar_split_clause,[],[f1416,f787,f525,f782,f777]) ).
fof(f2757,plain,
( spl0_82
| ~ spl0_38
| ~ spl0_40
| spl0_80 ),
inference(avatar_split_clause,[],[f2734,f729,f530,f520,f739]) ).
fof(f2758,plain,
( spl0_52
| ~ spl0_27
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f2573,f581,f472,f586]) ).
fof(f2765,plain,
( spl0_139
| spl0_162
| ~ spl0_21
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f2691,f1033,f448,f1190,f1043]) ).
fof(f2770,plain,
( ~ spl0_73
| spl0_150
| ~ spl0_31
| spl0_71 ),
inference(avatar_split_clause,[],[f1628,f681,f490,f1125,f691]) ).
fof(f2772,plain,
( ~ spl0_164
| spl0_64
| ~ spl0_31
| spl0_62 ),
inference(avatar_split_clause,[],[f1630,f633,f490,f643,f1254]) ).
fof(f2774,plain,
( spl0_142
| spl0_170
| ~ spl0_33
| spl0_141 ),
inference(avatar_split_clause,[],[f2595,f1054,f499,f1297,f1059]) ).
fof(f2776,plain,
( spl0_40
| ~ spl0_35
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1824,f536,f508,f530]) ).
fof(f2778,plain,
( spl0_82
| spl0_80
| ~ spl0_35
| spl0_81 ),
inference(avatar_split_clause,[],[f2735,f734,f508,f729,f739]) ).
fof(f2784,plain,
( ~ spl0_161
| ~ spl0_130
| ~ spl0_50
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1880,f985,f577,f995,f1184]) ).
fof(f2785,plain,
( ~ spl0_123
| ~ spl0_124
| ~ spl0_50
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1882,f953,f577,f963,f958]) ).
fof(f2786,plain,
( ~ spl0_99
| ~ spl0_165
| ~ spl0_50
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f1887,f825,f577,f1267,f830]) ).
fof(f2812,plain,
( spl0_139
| ~ spl0_25
| ~ spl0_36
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f2032,f1038,f512,f464,f1043]) ).
fof(f2821,plain,
( ~ spl0_170
| ~ spl0_140
| ~ spl0_46
| spl0_141 ),
inference(avatar_split_clause,[],[f2150,f1054,f559,f1049,f1297]) ).
fof(f2824,plain,
( spl0_104
| ~ spl0_105
| ~ spl0_55
| spl0_106 ),
inference(avatar_split_clause,[],[f2204,f867,f601,f862,f857]) ).
fof(f2829,plain,
( spl0_165
| ~ spl0_99
| ~ spl0_57
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f2523,f825,f610,f830,f1267]) ).
fof(f2831,plain,
( ~ spl0_111
| spl0_166
| ~ spl0_41
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f1817,f889,f536,f1273,f894]) ).
fof(f2848,plain,
( ~ spl0_138
| spl0_162
| ~ spl0_47
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f2697,f1033,f563,f1190,f1038]) ).
fof(f2852,plain,
( ~ spl0_144
| ~ spl0_163
| ~ spl0_54
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f1945,f1065,f596,f1196,f1070]) ).
fof(f2856,plain,
( spl0_154
| spl0_83
| ~ spl0_38
| spl0_85 ),
inference(avatar_split_clause,[],[f2257,f755,f520,f745,f1145]) ).
fof(f2867,plain,
( ~ spl0_144
| spl0_163
| ~ spl0_30
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f2479,f1065,f484,f1196,f1070]) ).
fof(f2869,plain,
( ~ spl0_164
| spl0_64
| ~ spl0_36
| spl0_63 ),
inference(avatar_split_clause,[],[f1670,f638,f512,f643,f1254]) ).
fof(f2870,plain,
( spl0_168
| spl0_121
| ~ spl0_40
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1581,f937,f530,f947,f1283]) ).
fof(f2872,plain,
( spl0_80
| spl0_82
| ~ spl0_40
| ~ spl0_153 ),
inference(avatar_split_clause,[],[f2116,f1140,f530,f739,f729]) ).
fof(f2882,plain,
( spl0_25
| ~ spl0_22
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f2493,f484,f453,f464]) ).
fof(f2883,plain,
( ~ spl0_168
| ~ spl0_119
| ~ spl0_22
| spl0_120 ),
inference(avatar_split_clause,[],[f2144,f942,f453,f937,f1283]) ).
fof(f2887,plain,
( spl0_170
| ~ spl0_140
| ~ spl0_55
| spl0_142 ),
inference(avatar_split_clause,[],[f2195,f1059,f601,f1049,f1297]) ).
fof(f2890,plain,
( spl0_83
| ~ spl0_154
| ~ spl0_55
| spl0_85 ),
inference(avatar_split_clause,[],[f2208,f755,f601,f1145,f745]) ).
fof(f2891,plain,
( spl0_170
| ~ spl0_140
| ~ spl0_56
| spl0_141 ),
inference(avatar_split_clause,[],[f2387,f1054,f605,f1049,f1297]) ).
cnf(s1,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f371]) ).
cnf(s4,plain,
( spl0_8
| ~ spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f402]) ).
cnf(s5,plain,
( ~ spl0_3
| ~ spl0_11 ),
inference(sat_conversion,[],[f407]) ).
cnf(s6,plain,
( spl0_4
| spl0_7
| spl0_12 ),
inference(sat_conversion,[],[f412]) ).
cnf(s8,plain,
( spl0_10
| spl0_15
| ~ spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f433]) ).
cnf(s9,plain,
( ~ spl0_9
| ~ spl0_16
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f438]) ).
cnf(s11,plain,
( spl0_4
| ~ spl0_16
| spl0_18
| spl0_21 ),
inference(sat_conversion,[],[f451]) ).
cnf(s13,plain,
( ~ spl0_16
| ~ spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f466]) ).
cnf(s14,plain,
( spl0_1
| ~ spl0_16
| ~ spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f474]) ).
cnf(s16,plain,
( spl0_4
| ~ spl0_16
| spl0_18
| spl0_30 ),
inference(sat_conversion,[],[f487]) ).
cnf(s17,plain,
( spl0_8
| ~ spl0_16
| spl0_18
| spl0_30 ),
inference(sat_conversion,[],[f488]) ).
cnf(s20,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f501]) ).
cnf(s22,plain,
( spl0_1
| spl0_10
| ~ spl0_16
| spl0_35 ),
inference(sat_conversion,[],[f510]) ).
cnf(s23,plain,
( ~ spl0_16
| spl0_27
| spl0_35
| spl0_36 ),
inference(sat_conversion,[],[f514]) ).
cnf(s25,plain,
( spl0_8
| ~ spl0_16
| spl0_30
| spl0_38 ),
inference(sat_conversion,[],[f523]) ).
cnf(s26,plain,
( ~ spl0_6
| spl0_12
| ~ spl0_16
| spl0_39 ),
inference(sat_conversion,[],[f527]) ).
cnf(s27,plain,
( ~ spl0_16
| spl0_20
| spl0_24
| spl0_39 ),
inference(sat_conversion,[],[f528]) ).
cnf(s28,plain,
( spl0_12
| ~ spl0_16
| spl0_40 ),
inference(sat_conversion,[],[f532]) ).
cnf(s29,plain,
( ~ spl0_16
| spl0_31
| spl0_40 ),
inference(sat_conversion,[],[f533]) ).
cnf(s30,plain,
( ~ spl0_16
| spl0_25
| spl0_35
| spl0_40 ),
inference(sat_conversion,[],[f534]) ).
cnf(s33,plain,
( spl0_10
| ~ spl0_16
| spl0_22
| spl0_41 ),
inference(sat_conversion,[],[f544]) ).
cnf(s34,plain,
( spl0_5
| ~ spl0_16
| spl0_25
| spl0_41 ),
inference(sat_conversion,[],[f545]) ).
cnf(s37,plain,
( ~ spl0_16
| spl0_21
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f565]) ).
cnf(s39,plain,
( ~ spl0_16
| spl0_20
| spl0_39
| spl0_46 ),
inference(sat_conversion,[],[f567]) ).
cnf(s40,plain,
( ~ spl0_16
| spl0_17
| spl0_21
| spl0_48 ),
inference(sat_conversion,[],[f571]) ).
cnf(s42,plain,
( ~ spl0_16
| spl0_22
| spl0_42
| spl0_50 ),
inference(sat_conversion,[],[f579]) ).
cnf(s44,plain,
( spl0_7
| ~ spl0_16
| spl0_33
| spl0_51 ),
inference(sat_conversion,[],[f584]) ).
cnf(s45,plain,
( ~ spl0_16
| ~ spl0_23
| spl0_29
| spl0_52 ),
inference(sat_conversion,[],[f588]) ).
cnf(s48,plain,
( spl0_5
| ~ spl0_16
| spl0_42
| spl0_54 ),
inference(sat_conversion,[],[f598]) ).
cnf(s49,plain,
( ~ spl0_16
| spl0_35
| spl0_38
| spl0_54 ),
inference(sat_conversion,[],[f599]) ).
cnf(s50,plain,
( ~ spl0_16
| spl0_41
| spl0_45
| spl0_55 ),
inference(sat_conversion,[],[f603]) ).
cnf(s51,plain,
( ~ spl0_16
| spl0_44
| spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f607]) ).
cnf(s52,plain,
( ~ spl0_16
| spl0_47
| spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f608]) ).
cnf(s53,plain,
( spl0_12
| ~ spl0_16
| spl0_42
| spl0_57 ),
inference(sat_conversion,[],[f612]) ).
cnf(s56,plain,
( spl0_12
| ~ spl0_16
| spl0_55
| spl0_57 ),
inference(sat_conversion,[],[f621]) ).
cnf(s61,plain,
( spl0_11
| ~ spl0_62 ),
inference(sat_conversion,[],[f636]) ).
cnf(s62,plain,
( spl0_11
| ~ spl0_63 ),
inference(sat_conversion,[],[f641]) ).
cnf(s63,plain,
( spl0_11
| ~ spl0_64 ),
inference(sat_conversion,[],[f646]) ).
cnf(s73,plain,
( spl0_23
| ~ spl0_71 ),
inference(sat_conversion,[],[f684]) ).
cnf(s74,plain,
( spl0_23
| ~ spl0_72 ),
inference(sat_conversion,[],[f689]) ).
cnf(s75,plain,
( spl0_23
| spl0_73 ),
inference(sat_conversion,[],[f694]) ).
cnf(s81,plain,
( spl0_26
| spl0_77 ),
inference(sat_conversion,[],[f716]) ).
cnf(s82,plain,
( spl0_26
| ~ spl0_78 ),
inference(sat_conversion,[],[f721]) ).
cnf(s83,plain,
( spl0_26
| spl0_79 ),
inference(sat_conversion,[],[f726]) ).
cnf(s85,plain,
( ~ spl0_18
| ~ spl0_80 ),
inference(sat_conversion,[],[f732]) ).
cnf(s86,plain,
( ~ spl0_18
| ~ spl0_81 ),
inference(sat_conversion,[],[f737]) ).
cnf(s87,plain,
( ~ spl0_18
| ~ spl0_82 ),
inference(sat_conversion,[],[f742]) ).
cnf(s89,plain,
( spl0_2
| ~ spl0_83 ),
inference(sat_conversion,[],[f748]) ).
cnf(s90,plain,
( spl0_2
| ~ spl0_84 ),
inference(sat_conversion,[],[f753]) ).
cnf(s91,plain,
( spl0_2
| ~ spl0_85 ),
inference(sat_conversion,[],[f758]) ).
cnf(s92,plain,
( spl0_2
| spl0_16 ),
inference(sat_conversion,[],[f759]) ).
cnf(s97,plain,
( ~ spl0_1
| spl0_89 ),
inference(sat_conversion,[],[f780]) ).
cnf(s98,plain,
( ~ spl0_1
| ~ spl0_90 ),
inference(sat_conversion,[],[f785]) ).
cnf(s99,plain,
( ~ spl0_1
| ~ spl0_91 ),
inference(sat_conversion,[],[f790]) ).
cnf(s100,plain,
( ~ spl0_1
| spl0_16 ),
inference(sat_conversion,[],[f791]) ).
cnf(s105,plain,
( ~ spl0_8
| spl0_95 ),
inference(sat_conversion,[],[f812]) ).
cnf(s106,plain,
( ~ spl0_8
| ~ spl0_96 ),
inference(sat_conversion,[],[f817]) ).
cnf(s107,plain,
( ~ spl0_8
| ~ spl0_97 ),
inference(sat_conversion,[],[f822]) ).
cnf(s109,plain,
( spl0_6
| spl0_98 ),
inference(sat_conversion,[],[f828]) ).
cnf(s110,plain,
( spl0_6
| spl0_99 ),
inference(sat_conversion,[],[f833]) ).
cnf(s111,plain,
( spl0_6
| ~ spl0_100 ),
inference(sat_conversion,[],[f838]) ).
cnf(s117,plain,
( ~ spl0_4
| ~ spl0_104 ),
inference(sat_conversion,[],[f860]) ).
cnf(s118,plain,
( ~ spl0_4
| spl0_105 ),
inference(sat_conversion,[],[f865]) ).
cnf(s119,plain,
( ~ spl0_4
| ~ spl0_106 ),
inference(sat_conversion,[],[f870]) ).
cnf(s121,plain,
( ~ spl0_10
| spl0_107 ),
inference(sat_conversion,[],[f876]) ).
cnf(s122,plain,
( ~ spl0_10
| spl0_108 ),
inference(sat_conversion,[],[f881]) ).
cnf(s123,plain,
( ~ spl0_10
| spl0_109 ),
inference(sat_conversion,[],[f886]) ).
cnf(s125,plain,
( spl0_32
| spl0_110 ),
inference(sat_conversion,[],[f892]) ).
cnf(s126,plain,
( spl0_32
| spl0_111 ),
inference(sat_conversion,[],[f897]) ).
cnf(s127,plain,
( spl0_32
| spl0_112 ),
inference(sat_conversion,[],[f902]) ).
cnf(s129,plain,
( ~ spl0_20
| spl0_113 ),
inference(sat_conversion,[],[f908]) ).
cnf(s130,plain,
( ~ spl0_20
| spl0_114 ),
inference(sat_conversion,[],[f913]) ).
cnf(s131,plain,
( ~ spl0_20
| ~ spl0_115 ),
inference(sat_conversion,[],[f918]) ).
cnf(s133,plain,
( ~ spl0_15
| spl0_116 ),
inference(sat_conversion,[],[f924]) ).
cnf(s135,plain,
( ~ spl0_15
| spl0_118 ),
inference(sat_conversion,[],[f934]) ).
cnf(s137,plain,
( ~ spl0_29
| spl0_119 ),
inference(sat_conversion,[],[f940]) ).
cnf(s138,plain,
( ~ spl0_29
| ~ spl0_120 ),
inference(sat_conversion,[],[f945]) ).
cnf(s139,plain,
( ~ spl0_29
| ~ spl0_121 ),
inference(sat_conversion,[],[f950]) ).
cnf(s141,plain,
( spl0_3
| spl0_122 ),
inference(sat_conversion,[],[f956]) ).
cnf(s142,plain,
( spl0_3
| spl0_123 ),
inference(sat_conversion,[],[f961]) ).
cnf(s143,plain,
( spl0_3
| spl0_124 ),
inference(sat_conversion,[],[f966]) ).
cnf(s144,plain,
( spl0_3
| spl0_16 ),
inference(sat_conversion,[],[f967]) ).
cnf(s149,plain,
( ~ spl0_5
| spl0_128 ),
inference(sat_conversion,[],[f988]) ).
cnf(s150,plain,
( ~ spl0_5
| ~ spl0_129 ),
inference(sat_conversion,[],[f993]) ).
cnf(s151,plain,
( ~ spl0_5
| spl0_130 ),
inference(sat_conversion,[],[f998]) ).
cnf(s153,plain,
( ~ spl0_45
| spl0_131 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s154,plain,
( ~ spl0_45
| ~ spl0_132 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s155,plain,
( ~ spl0_45
| ~ spl0_133 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s157,plain,
( ~ spl0_44
| spl0_134 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s158,plain,
( ~ spl0_44
| ~ spl0_135 ),
inference(sat_conversion,[],[f1025]) ).
cnf(s159,plain,
( ~ spl0_44
| spl0_136 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s161,plain,
( ~ spl0_42
| spl0_137 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s162,plain,
( ~ spl0_42
| spl0_138 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s163,plain,
( ~ spl0_42
| ~ spl0_139 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s165,plain,
( spl0_9
| spl0_140 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s166,plain,
( spl0_9
| ~ spl0_141 ),
inference(sat_conversion,[],[f1057]) ).
cnf(s167,plain,
( spl0_9
| ~ spl0_142 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s169,plain,
( ~ spl0_7
| spl0_143 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s170,plain,
( ~ spl0_7
| spl0_144 ),
inference(sat_conversion,[],[f1073]) ).
cnf(s171,plain,
( ~ spl0_7
| spl0_145 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s173,plain,
( ~ spl0_12
| spl0_146 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s174,plain,
( ~ spl0_12
| spl0_147 ),
inference(sat_conversion,[],[f1089]) ).
cnf(s175,plain,
( ~ spl0_12
| ~ spl0_148 ),
inference(sat_conversion,[],[f1094]) ).
cnf(s199,plain,
( ~ spl0_22
| ~ spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s204,plain,
( ~ spl0_33
| spl0_80
| spl0_81
| spl0_153 ),
inference(sat_conversion,[],[f1261]) ).
cnf(s226,plain,
( ~ spl0_35
| spl0_83
| spl0_84
| spl0_154 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s240,plain,
( ~ spl0_38
| spl0_63
| spl0_64
| spl0_164 ),
inference(sat_conversion,[],[f1376]) ).
cnf(s263,plain,
( ~ spl0_40
| ~ spl0_95
| spl0_96
| spl0_97 ),
inference(sat_conversion,[],[f1430]) ).
cnf(s265,plain,
( ~ spl0_46
| ~ spl0_50
| ~ spl0_108
| ~ spl0_109 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s267,plain,
( ~ spl0_24
| ~ spl0_137
| ~ spl0_138
| spl0_139 ),
inference(sat_conversion,[],[f1484]) ).
cnf(s272,plain,
( ~ spl0_17
| spl0_71
| spl0_72
| spl0_150 ),
inference(sat_conversion,[],[f1489]) ).
cnf(s275,plain,
( ~ spl0_35
| spl0_62
| spl0_64
| spl0_164 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s276,plain,
( ~ spl0_21
| ~ spl0_35
| spl0_38 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s287,plain,
( ~ spl0_46
| ~ spl0_50
| ~ spl0_112
| ~ spl0_166 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s290,plain,
( ~ spl0_30
| ~ spl0_113
| ~ spl0_114
| spl0_115 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s335,plain,
( ~ spl0_46
| spl0_71
| ~ spl0_73
| ~ spl0_150 ),
inference(sat_conversion,[],[f1735]) ).
cnf(s340,plain,
( ~ spl0_47
| ~ spl0_128
| spl0_129
| ~ spl0_130 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s342,plain,
( ~ spl0_30
| ~ spl0_137
| spl0_139
| ~ spl0_162 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s344,plain,
( ~ spl0_17
| spl0_84
| spl0_85
| spl0_154 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s356,plain,
( ~ spl0_48
| ~ spl0_134
| spl0_135
| ~ spl0_136 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s366,plain,
( ~ spl0_52
| ~ spl0_107
| ~ spl0_108
| ~ spl0_109 ),
inference(sat_conversion,[],[f1935]) ).
cnf(s374,plain,
( ~ spl0_54
| ~ spl0_122
| ~ spl0_123
| ~ spl0_159 ),
inference(sat_conversion,[],[f1967]) ).
cnf(s375,plain,
( ~ spl0_22
| spl0_52
| ~ spl0_54 ),
inference(sat_conversion,[],[f1968]) ).
cnf(s403,plain,
( ~ spl0_30
| ~ spl0_35
| spl0_40 ),
inference(sat_conversion,[],[f1995]) ).
cnf(s424,plain,
( ~ spl0_52
| ~ spl0_144
| ~ spl0_145
| ~ spl0_163 ),
inference(sat_conversion,[],[f2172]) ).
cnf(s440,plain,
( ~ spl0_33
| spl0_83
| spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f2233]) ).
cnf(s452,plain,
( ~ spl0_21
| ~ spl0_131
| spl0_132
| spl0_133 ),
inference(sat_conversion,[],[f2240]) ).
cnf(s456,plain,
( ~ spl0_17
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s481,plain,
( ~ spl0_56
| spl0_83
| spl0_84
| ~ spl0_154 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s488,plain,
( ~ spl0_35
| spl0_83
| spl0_84
| spl0_154 ),
inference(sat_conversion,[],[f2404]) ).
cnf(s498,plain,
( ~ spl0_24
| ~ spl0_128
| ~ spl0_130
| spl0_161 ),
inference(sat_conversion,[],[f2412]) ).
cnf(s514,plain,
( ~ spl0_57
| ~ spl0_77
| spl0_78
| ~ spl0_79 ),
inference(sat_conversion,[],[f2534]) ).
cnf(s519,plain,
( ~ spl0_25
| ~ spl0_146
| ~ spl0_147
| spl0_148 ),
inference(sat_conversion,[],[f2538]) ).
cnf(s524,plain,
( ~ spl0_56
| ~ spl0_57
| spl0_104
| ~ spl0_105 ),
inference(sat_conversion,[],[f2548]) ).
cnf(s529,plain,
( ~ spl0_27
| ~ spl0_143
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f2576]) ).
cnf(s548,plain,
( ~ spl0_47
| ~ spl0_122
| ~ spl0_124
| spl0_159 ),
inference(sat_conversion,[],[f2623]) ).
cnf(s552,plain,
( ~ spl0_47
| ~ spl0_98
| spl0_100
| ~ spl0_165 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s568,plain,
( ~ spl0_27
| ~ spl0_122
| ~ spl0_124
| ~ spl0_159 ),
inference(sat_conversion,[],[f2643]) ).
cnf(s591,plain,
( ~ spl0_51
| ~ spl0_54
| ~ spl0_107
| ~ spl0_108 ),
inference(sat_conversion,[],[f2715]) ).
cnf(s606,plain,
( ~ spl0_51
| ~ spl0_54
| ~ spl0_116
| ~ spl0_118 ),
inference(sat_conversion,[],[f2739]) ).
cnf(s607,plain,
( ~ spl0_39
| ~ spl0_89
| spl0_90
| spl0_91 ),
inference(sat_conversion,[],[f2740]) ).
cnf(s624,plain,
( ~ spl0_38
| ~ spl0_40
| spl0_80
| spl0_82 ),
inference(sat_conversion,[],[f2757]) ).
cnf(s625,plain,
( ~ spl0_27
| ~ spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s634,plain,
( ~ spl0_21
| ~ spl0_137
| spl0_139
| spl0_162 ),
inference(sat_conversion,[],[f2765]) ).
cnf(s641,plain,
( ~ spl0_31
| spl0_71
| ~ spl0_73
| spl0_150 ),
inference(sat_conversion,[],[f2770]) ).
cnf(s643,plain,
( ~ spl0_31
| spl0_62
| spl0_64
| ~ spl0_164 ),
inference(sat_conversion,[],[f2772]) ).
cnf(s645,plain,
( ~ spl0_33
| spl0_141
| spl0_142
| spl0_170 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s647,plain,
( ~ spl0_35
| spl0_40
| ~ spl0_41 ),
inference(sat_conversion,[],[f2776]) ).
cnf(s649,plain,
( ~ spl0_35
| spl0_80
| spl0_81
| spl0_82 ),
inference(sat_conversion,[],[f2778]) ).
cnf(s655,plain,
( ~ spl0_50
| ~ spl0_128
| ~ spl0_130
| ~ spl0_161 ),
inference(sat_conversion,[],[f2784]) ).
cnf(s656,plain,
( ~ spl0_50
| ~ spl0_122
| ~ spl0_123
| ~ spl0_124 ),
inference(sat_conversion,[],[f2785]) ).
cnf(s657,plain,
( ~ spl0_50
| ~ spl0_98
| ~ spl0_99
| ~ spl0_165 ),
inference(sat_conversion,[],[f2786]) ).
cnf(s684,plain,
( ~ spl0_25
| ~ spl0_36
| ~ spl0_138
| spl0_139 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s695,plain,
( ~ spl0_46
| ~ spl0_140
| spl0_141
| ~ spl0_170 ),
inference(sat_conversion,[],[f2821]) ).
cnf(s698,plain,
( ~ spl0_55
| spl0_104
| ~ spl0_105
| spl0_106 ),
inference(sat_conversion,[],[f2824]) ).
cnf(s703,plain,
( ~ spl0_57
| ~ spl0_98
| ~ spl0_99
| spl0_165 ),
inference(sat_conversion,[],[f2829]) ).
cnf(s705,plain,
( ~ spl0_41
| ~ spl0_110
| ~ spl0_111
| spl0_166 ),
inference(sat_conversion,[],[f2831]) ).
cnf(s717,plain,
( ~ spl0_47
| ~ spl0_137
| ~ spl0_138
| spl0_162 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s724,plain,
( ~ spl0_54
| ~ spl0_143
| ~ spl0_144
| ~ spl0_163 ),
inference(sat_conversion,[],[f2852]) ).
cnf(s729,plain,
( ~ spl0_38
| spl0_83
| spl0_85
| spl0_154 ),
inference(sat_conversion,[],[f2856]) ).
cnf(s740,plain,
( ~ spl0_30
| ~ spl0_143
| ~ spl0_144
| spl0_163 ),
inference(sat_conversion,[],[f2867]) ).
cnf(s742,plain,
( ~ spl0_36
| spl0_63
| spl0_64
| ~ spl0_164 ),
inference(sat_conversion,[],[f2869]) ).
cnf(s743,plain,
( ~ spl0_40
| ~ spl0_119
| spl0_121
| spl0_168 ),
inference(sat_conversion,[],[f2870]) ).
cnf(s745,plain,
( ~ spl0_40
| spl0_80
| spl0_82
| ~ spl0_153 ),
inference(sat_conversion,[],[f2872]) ).
cnf(s756,plain,
( ~ spl0_22
| spl0_25
| ~ spl0_30 ),
inference(sat_conversion,[],[f2882]) ).
cnf(s758,plain,
( ~ spl0_22
| ~ spl0_119
| spl0_120
| ~ spl0_168 ),
inference(sat_conversion,[],[f2883]) ).
cnf(s768,plain,
( ~ spl0_55
| ~ spl0_140
| spl0_142
| spl0_170 ),
inference(sat_conversion,[],[f2887]) ).
cnf(s771,plain,
( ~ spl0_55
| spl0_83
| spl0_85
| ~ spl0_154 ),
inference(sat_conversion,[],[f2890]) ).
cnf(s772,plain,
( ~ spl0_56
| ~ spl0_140
| spl0_141
| spl0_170 ),
inference(sat_conversion,[],[f2891]) ).
cnf(s790,plain,
( spl0_38
| spl0_35
| spl0_8
| ~ spl0_7
| ~ spl0_16 ),
inference(rat,[],[s724,s740,s49,s25,s170,s169]) ).
cnf(s795,plain,
( ~ spl0_154
| spl0_47
| spl0_2 ),
inference(rat,[],[s52,s481,s771,s92,s91,s90,s89]) ).
cnf(s796,plain,
( spl0_154
| spl0_50
| spl0_2
| spl0_1 ),
inference(rat,[],[s30,s684,s263,s23,s162,s163,s105,s106,s107,s529,s42,s790,s169,s170,s171,s375,s44,s366,s591,s121,s122,s123,s22,s49,s488,s729,s92,s440,s89,s90,s91]) ).
cnf(s797,plain,
( ~ spl0_18
| ~ spl0_40
| ~ spl0_38 ),
inference(rat,[],[s624,s85,s87]) ).
cnf(s798,plain,
( ~ spl0_30
| spl0_25
| ~ spl0_47
| spl0_50
| ~ spl0_16 ),
inference(rat,[],[s717,s342,s161,s162,s163,s42,s756]) ).
cnf(s799,plain,
( spl0_8
| spl0_30
| spl0_25
| ~ spl0_16 ),
inference(rat,[],[s30,s649,s797,s85,s86,s87,s17,s25]) ).
cnf(s800,plain,
( spl0_25
| ~ spl0_47
| ~ spl0_16
| spl0_50 ),
inference(rat,[],[s340,s149,s150,s151,s34,s647,s30,s263,s105,s106,s107,s799,s798]) ).
cnf(s801,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s800,s519,s173,s174,s175,s56,s514,s81,s82,s83,s14,s568,s548,s795,s771,s796,s656,s141,s142,s143,s92,s91,s89]) ).
cnf(s802,plain,
( ~ spl0_27
| spl0_52
| spl0_2 ),
inference(rat,[],[s529,s169,s170,s171,s44,s625,s92,s440,s89,s90,s91]) ).
cnf(s803,plain,
( spl0_35
| spl0_8
| spl0_2
| spl0_1 ),
inference(rat,[],[s44,s591,s790,s49,s240,s742,s23,s802,s366,s121,s122,s123,s22,s92,s440,s89,s90,s91,s63,s62,s5,s801]) ).
cnf(s804,plain,
( ~ spl0_42
| ~ spl0_21
| ~ spl0_30 ),
inference(rat,[],[s634,s342,s161,s163]) ).
cnf(s805,plain,
( ~ spl0_5
| ~ spl0_47 ),
inference(rat,[],[s340,s149,s150,s151]) ).
cnf(s806,plain,
( ~ spl0_7
| ~ spl0_54
| ~ spl0_30 ),
inference(rat,[],[s724,s740,s169,s170]) ).
cnf(s809,plain,
( ~ spl0_10
| ~ spl0_51
| ~ spl0_54 ),
inference(rat,[],[s591,s121,s122]) ).
cnf(s810,plain,
( spl0_8
| spl0_25
| spl0_2
| spl0_1 ),
inference(rat,[],[s606,s133,s135,s8,s809,s44,s806,s48,s805,s804,s40,s356,s157,s158,s159,s51,s795,s481,s771,s226,s803,s799,s92,s440,s89,s90,s91,s456,s61,s62,s63,s5,s801]) ).
cnf(s811,plain,
( spl0_25
| spl0_2
| spl0_1 ),
inference(rat,[],[s275,s643,s30,s29,s263,s105,s106,s107,s810,s92,s63,s61,s5,s801]) ).
cnf(s812,plain,
( spl0_8
| spl0_2
| spl0_1 ),
inference(rat,[],[s606,s133,s135,s8,s809,s44,s806,s48,s804,s17,s797,s276,s40,s356,s157,s158,s159,s29,s805,s51,s643,s795,s481,s771,s275,s226,s803,s92,s440,s89,s90,s91,s456,s61,s62,s63,s5,s801]) ).
cnf(s813,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s519,s173,s174,s175,s28,s263,s105,s106,s107,s812,s811,s92]) ).
cnf(s814,plain,
( spl0_9
| ~ spl0_56
| ~ spl0_46 ),
inference(rat,[],[s772,s695,s165,s166]) ).
cnf(s815,plain,
( ~ spl0_18
| ~ spl0_35 ),
inference(rat,[],[s649,s85,s86,s87]) ).
cnf(s816,plain,
( spl0_18
| spl0_17
| spl0_21
| spl0_47
| ~ spl0_16 ),
inference(rat,[],[s698,s52,s117,s118,s119,s814,s11,s9,s37]) ).
cnf(s817,plain,
( spl0_25
| spl0_8
| spl0_1 ),
inference(rat,[],[s809,s44,s22,s790,s49,s204,s745,s815,s797,s85,s86,s87,s816,s29,s272,s641,s335,s73,s74,s75,s13,s37,s267,s804,s161,s162,s163,s42,s756,s799,s800,s144,s656,s142,s143,s141,s1,s813]) ).
cnf(s818,plain,
( ~ spl0_47
| ~ spl0_30
| spl0_3 ),
inference(rat,[],[s717,s342,s161,s162,s163,s48,s374,s548,s805,s144,s143,s142,s141]) ).
cnf(s819,plain,
( ~ spl0_12
| ~ spl0_25 ),
inference(rat,[],[s519,s173,s174,s175]) ).
cnf(s820,plain,
( ~ spl0_4
| ~ spl0_57
| spl0_47
| ~ spl0_16 ),
inference(rat,[],[s52,s524,s698,s117,s118,s119]) ).
cnf(s821,plain,
( ~ spl0_57
| spl0_47
| spl0_12
| spl0_1 ),
inference(rat,[],[s514,s81,s82,s83,s14,s529,s169,s170,s171,s6,s820,s144,s1,s813]) ).
cnf(s822,plain,
( spl0_18
| spl0_8
| spl0_1 ),
inference(rat,[],[s698,s117,s118,s119,s11,s804,s53,s56,s821,s818,s17,s144,s1,s813,s819,s817]) ).
cnf(s823,plain,
( spl0_8
| spl0_1 ),
inference(rat,[],[s809,s44,s22,s790,s49,s204,s745,s815,s797,s85,s86,s87,s28,s822,s819,s817,s144,s1,s813]) ).
cnf(s824,plain,
( spl0_23
| spl0_1 ),
inference(rat,[],[s272,s335,s73,s74,s75,s37,s816,s452,s153,s154,s155,s50,s698,s117,s118,s119,s16,s403,s647,s815,s30,s800,s819,s28,s263,s105,s106,s107,s823,s656,s142,s143,s141,s144,s1,s813]) ).
cnf(s825,plain,
( ~ spl0_2
| spl0_1 ),
inference(rat,[],[s267,s161,s162,s163,s42,s199,s13,s824,s819,s28,s263,s105,s106,s107,s823,s656,s141,s142,s143,s144,s1]) ).
cnf(s826,plain,
spl0_1,
inference(rat,[],[s825,s813]) ).
cnf(s827,plain,
spl0_16,
inference(rat,[],[s100,s826]) ).
cnf(s828,plain,
~ spl0_91,
inference(rat,[],[s99,s826]) ).
cnf(s829,plain,
~ spl0_90,
inference(rat,[],[s98,s826]) ).
cnf(s830,plain,
spl0_89,
inference(rat,[],[s97,s826]) ).
cnf(s831,plain,
~ spl0_39,
inference(rat,[],[s607,s828,s829,s830]) ).
cnf(s832,plain,
( ~ spl0_54
| spl0_17
| spl0_33
| ~ spl0_30 ),
inference(rat,[],[s606,s133,s135,s8,s809,s44,s806,s827]) ).
cnf(s833,plain,
( spl0_54
| spl0_42
| spl0_2 ),
inference(rat,[],[s49,s488,s729,s795,s805,s48,s91,s90,s89,s827]) ).
cnf(s834,plain,
( ~ spl0_17
| spl0_2
| ~ spl0_30 ),
inference(rat,[],[s456,s61,s62,s63,s5,s818,s795,s344,s91,s90]) ).
cnf(s835,plain,
( ~ spl0_20
| ~ spl0_30 ),
inference(rat,[],[s290,s129,s130,s131]) ).
cnf(s836,plain,
( ~ spl0_42
| ~ spl0_24 ),
inference(rat,[],[s267,s161,s162,s163]) ).
cnf(s837,plain,
( spl0_2
| ~ spl0_30 ),
inference(rat,[],[s832,s440,s833,s834,s89,s90,s91,s836,s27,s835,s831,s827]) ).
cnf(s838,plain,
( spl0_9
| ~ spl0_33
| ~ spl0_46 ),
inference(rat,[],[s695,s645,s165,s166,s167]) ).
cnf(s839,plain,
( ~ spl0_10
| ~ spl0_50
| ~ spl0_46 ),
inference(rat,[],[s265,s122,s123]) ).
cnf(s840,plain,
( spl0_25
| spl0_8 ),
inference(rat,[],[s705,s287,s125,s126,s127,s20,s838,s4,s33,s839,s837,s42,s836,s39,s27,s835,s756,s799,s831,s827]) ).
cnf(s841,plain,
( spl0_9
| spl0_47
| ~ spl0_46 ),
inference(rat,[],[s768,s52,s695,s814,s165,s166,s167,s827]) ).
cnf(s842,plain,
( ~ spl0_18
| spl0_54
| ~ spl0_40 ),
inference(rat,[],[s49,s815,s797,s827]) ).
cnf(s843,plain,
( spl0_23
| ~ spl0_17
| ~ spl0_46 ),
inference(rat,[],[s272,s335,s73,s74,s75]) ).
cnf(s844,plain,
( ~ spl0_30
| spl0_12 ),
inference(rat,[],[s743,s758,s137,s138,s139,s45,s843,s9,s842,s841,s424,s740,s806,s169,s170,s171,s6,s42,s820,s657,s552,s703,s53,s836,s39,s27,s835,s28,s111,s110,s109,s26,s827,s831]) ).
cnf(s845,plain,
spl0_8,
inference(rat,[],[s797,s17,s25,s844,s28,s819,s840,s827]) ).
cnf(s846,plain,
~ spl0_97,
inference(rat,[],[s107,s845]) ).
cnf(s847,plain,
~ spl0_96,
inference(rat,[],[s106,s845]) ).
cnf(s848,plain,
spl0_95,
inference(rat,[],[s105,s845]) ).
cnf(s849,plain,
~ spl0_40,
inference(rat,[],[s263,s846,s847,s848]) ).
cnf(s851,plain,
spl0_12,
inference(rat,[],[s28,s827,s849]) ).
cnf(s855,plain,
~ spl0_25,
inference(rat,[],[s819,s851]) ).
cnf(s856,plain,
spl0_35,
inference(rat,[],[s30,s849,s827,s855]) ).
cnf(s857,plain,
~ spl0_18,
inference(rat,[],[s815,s856]) ).
cnf(s858,plain,
~ spl0_30,
inference(rat,[],[s403,s849,s856]) ).
cnf(s859,plain,
~ spl0_41,
inference(rat,[],[s647,s849,s856]) ).
cnf(s861,plain,
spl0_4,
inference(rat,[],[s16,s858,s827,s857]) ).
cnf(s862,plain,
spl0_5,
inference(rat,[],[s34,s855,s827,s859]) ).
cnf(s863,plain,
~ spl0_106,
inference(rat,[],[s119,s861]) ).
cnf(s864,plain,
spl0_105,
inference(rat,[],[s118,s861]) ).
cnf(s865,plain,
~ spl0_104,
inference(rat,[],[s117,s861]) ).
cnf(s866,plain,
spl0_130,
inference(rat,[],[s151,s862]) ).
cnf(s868,plain,
spl0_128,
inference(rat,[],[s149,s862]) ).
cnf(s869,plain,
~ spl0_47,
inference(rat,[],[s805,s862]) ).
cnf(s870,plain,
~ spl0_55,
inference(rat,[],[s698,s863,s864,s865]) ).
cnf(s873,plain,
spl0_45,
inference(rat,[],[s50,s827,s859,s870]) ).
cnf(s874,plain,
~ spl0_133,
inference(rat,[],[s155,s873]) ).
cnf(s875,plain,
~ spl0_132,
inference(rat,[],[s154,s873]) ).
cnf(s876,plain,
spl0_131,
inference(rat,[],[s153,s873]) ).
cnf(s877,plain,
~ spl0_21,
inference(rat,[],[s452,s874,s875,s876]) ).
cnf(s878,plain,
spl0_17,
inference(rat,[],[s816,s827,s869,s857,s877]) ).
cnf(s879,plain,
spl0_46,
inference(rat,[],[s37,s869,s827,s877]) ).
cnf(s880,plain,
spl0_23,
inference(rat,[],[s843,s879,s878]) ).
cnf(s882,plain,
spl0_24,
inference(rat,[],[s13,s855,s827,s880]) ).
cnf(s884,plain,
~ spl0_22,
inference(rat,[],[s199,s855,s882]) ).
cnf(s885,plain,
~ spl0_42,
inference(rat,[],[s836,s882]) ).
cnf(s886,plain,
spl0_161,
inference(rat,[],[s498,s868,s866,s882]) ).
cnf(s889,plain,
spl0_50,
inference(rat,[],[s42,s885,s827,s884]) ).
cnf(s892,plain,
$false,
inference(rat,[],[s655,s868,s866,s889,s886]) ).
fof(f2905,plain,
$false,
inference(avatar_sat_refutation,[],[s892]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN461+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 16:06:49 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.12 Running first-order model finding
% 0.08/0.12 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.18 % (3487965)Will run a generic schedule for satisfiability detection.
% 0.08/0.18 % (3487971)% WARNING: option uhcvi not known.
% 0.08/0.18 % (3487973)dis+10_1_sil=32000:sp=arity:random_seed=1644186287:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.18 % (3487970)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1021813590_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.18 % (3487971)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=224358144:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.18 % (3487972)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4058682217:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.18 % (3487976)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2494654249:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.18 % (3487974)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2708831665:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.18 % (3487975)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1714878632:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.18 % Detected minimum model sizes of [1]
% 0.08/0.18 % Detected maximum model sizes of [29]
% 0.08/0.18 % TRYING [1]
% 0.08/0.18 % TRYING [2]
% 0.08/0.18 % TRYING [3]
% 0.08/0.18 % TRYING [4]
% 0.08/0.18 % (3487976) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3487965-3487976"...
% 0.08/0.18 % TRYING [5]
% 0.08/0.18 % (3487976)...printing done.
% 0.08/0.18 % (3487976)Refutation found. Thanks to Tanya!
% 0.08/0.18 % SZS status Theorem for theBenchmark
% 0.08/0.18 % SZS output start Proof for theBenchmark
% See solution above
% 0.08/0.18 % (3487976)------------------------------
% 0.08/0.18 % (3487976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.18 % (3487976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.18 % (3487976)CaDiCaL version: 2.1.3
% 0.08/0.18 % (3487976)Termination reason: Refutation
% 0.08/0.18 % (3487976)Time elapsed: 0.023 s
% 0.08/0.18 % (3487976)Peak memory usage: 13 MB
% 0.08/0.18 % (3487976)Instructions burned: 74 (million)
% 0.08/0.18 % (3487965)Success in time 0.051 s
% 0.08/0.18 % Vampire exiting
%------------------------------------------------------------------------------