%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN499+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:58:13 PM UTC 2026
% Result : Theorem 3.04s 1.10s
% Output : Refutation 3.67s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ~ hskp0
| ( ndr1_0
& c2_1(a123)
& ~ c0_1(a123)
& ~ c1_1(a123) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a124)
& c2_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a125)
& c2_1(a125)
& ~ c0_1(a125) ) )
& ( ~ hskp3
| ( ndr1_0
& c1_1(a127)
& ~ c2_1(a127)
& ~ c3_1(a127) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& ~ c3_1(a128) ) )
& ( ~ hskp5
| ( ndr1_0
& ~ c0_1(a130)
& ~ c1_1(a130)
& ~ c3_1(a130) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c0_1(a131)
& ~ c1_1(a131)
& ~ c2_1(a131) ) )
& ( ~ hskp7
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c2_1(a132) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a134)
& ~ c0_1(a134)
& ~ c3_1(a134) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a138)
& c1_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp10
| ( ndr1_0
& c0_1(a140)
& ~ c2_1(a140)
& ~ c3_1(a140) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c1_1(a141)
& ~ c2_1(a141)
& ~ c3_1(a141) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a142)
& c3_1(a142)
& ~ c1_1(a142) ) )
& ( ~ hskp13
| ( ndr1_0
& c2_1(a143)
& c3_1(a143)
& ~ c1_1(a143) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a153)
& c3_1(a153)
& ~ c0_1(a153) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a154)
& c3_1(a154)
& ~ c0_1(a154) ) )
& ( ~ hskp17
| ( ndr1_0
& c1_1(a155)
& ~ c0_1(a155)
& ~ c2_1(a155) ) )
& ( ~ hskp18
| ( ndr1_0
& c3_1(a160)
& ~ c1_1(a160)
& ~ c2_1(a160) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a164)
& c3_1(a164)
& ~ c2_1(a164) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a168)
& ~ c0_1(a168)
& ~ c3_1(a168) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a170)
& c2_1(a170)
& ~ c1_1(a170) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a176)
& ~ c1_1(a176)
& ~ c2_1(a176) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a179)
& ~ c1_1(a179)
& ~ c3_1(a179) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a182)
& ~ c2_1(a182)
& ~ c3_1(a182) ) )
& ( ~ hskp25
| ( ndr1_0
& c3_1(a189)
& ~ c0_1(a189)
& ~ c1_1(a189) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a225)
& c2_1(a225)
& ~ c3_1(a225) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a122)
& c2_1(a122)
& c3_1(a122) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a133)
& c2_1(a133)
& c3_1(a133) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a136)
& c1_1(a136)
& c2_1(a136) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a167)
& c1_1(a167)
& c3_1(a167) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c1_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c2_1(X4)
| ~ c1_1(X4) ) )
| ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c2_1(X5)
| ~ c3_1(X5) ) ) )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c2_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c2_1(X7)
| ~ c1_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c2_1(X8)
| c3_1(X8)
| ~ c0_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c3_1(X10)
| ~ c2_1(X10) ) )
| hskp27 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c2_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c2_1(X12)
| c3_1(X12)
| ~ c1_1(X12) ) )
| hskp0 )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| c2_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( c3_1(X14)
| ~ c0_1(X14)
| ~ c1_1(X14) ) )
| hskp1 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| c2_1(X15) ) )
| hskp2
| hskp1 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| c3_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( c2_1(X17)
| c3_1(X17)
| ~ c1_1(X17) ) )
| hskp3 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c2_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c2_1(X19)
| ~ c1_1(X19) ) )
| hskp4 )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c1_1(X21)
| ~ c0_1(X21)
| ~ c2_1(X21) ) )
| ! [X22] :
( ndr1_0
=> ( ~ c1_1(X22)
| ~ c2_1(X22)
| ~ c3_1(X22) ) ) )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c1_1(X23)
| ~ c2_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c3_1(X24)
| ~ c0_1(X24)
| ~ c2_1(X24) ) )
| hskp27 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c1_1(X25)
| ~ c2_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( ~ c0_1(X26)
| ~ c1_1(X26)
| ~ c2_1(X26) ) )
| hskp5 )
& ( ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c1_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c3_1(X29)
| ~ c1_1(X29)
| ~ c2_1(X29) ) ) )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c1_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c1_1(X31)
| c2_1(X31)
| ~ c3_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( c1_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32) ) ) )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c1_1(X33)
| ~ c3_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c0_1(X34)
| ~ c3_1(X34) ) )
| hskp6 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c1_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c2_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36) ) )
| hskp7 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c1_1(X37)
| ~ c3_1(X37) ) )
| hskp28
| hskp8 )
& ( ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| c2_1(X38)
| c3_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( ~ c0_1(X39)
| ~ c2_1(X39)
| ~ c3_1(X39) ) )
| hskp8 )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| c3_1(X40) ) )
| hskp29
| hskp7 )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c2_1(X41)
| c3_1(X41) ) )
| hskp9
| hskp7 )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| c3_1(X42) ) )
| hskp10
| hskp11 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c2_1(X43)
| ~ c1_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c2_1(X45)
| ~ c0_1(X45)
| ~ c3_1(X45) ) ) )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c2_1(X46)
| ~ c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47) ) )
| hskp12 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c2_1(X48)
| ~ c1_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c1_1(X49)
| c2_1(X49)
| ~ c0_1(X49) ) )
| hskp13 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| c2_1(X50)
| ~ c1_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51) ) )
| hskp28 )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| c2_1(X52)
| ~ c1_1(X52) ) )
| hskp28
| hskp3 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| c2_1(X53)
| ~ c3_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| hskp14 )
& ( ! [X55] :
( ndr1_0
=> ( c0_1(X55)
| c2_1(X55)
| ~ c3_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56) ) )
| ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57) ) ) )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| c2_1(X58)
| ~ c3_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c2_1(X59)
| c3_1(X59)
| ~ c1_1(X59) ) )
| hskp29 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| c2_1(X60)
| ~ c3_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c3_1(X61)
| ~ c0_1(X61)
| ~ c2_1(X61) ) )
| hskp12 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| c2_1(X62)
| ~ c3_1(X62) ) )
| hskp14
| hskp7 )
& ( ! [X63] :
( ndr1_0
=> ( c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63) ) )
| hskp10
| hskp15 )
& ( ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| c3_1(X64)
| ~ c1_1(X64) ) )
| ! [X65] :
( ndr1_0
=> ( c3_1(X65)
| ~ c1_1(X65)
| ~ c2_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66) ) ) )
& ( ! [X67] :
( ndr1_0
=> ( c0_1(X67)
| c3_1(X67)
| ~ c1_1(X67) ) )
| ! [X68] :
( ndr1_0
=> ( ~ c1_1(X68)
| ~ c2_1(X68)
| ~ c3_1(X68) ) )
| hskp16 )
& ( ! [X69] :
( ndr1_0
=> ( c0_1(X69)
| c3_1(X69)
| ~ c2_1(X69) ) )
| ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c2_1(X71) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( c0_1(X72)
| c3_1(X72)
| ~ c2_1(X72) ) )
| ! [X73] :
( ndr1_0
=> ( c2_1(X73)
| c3_1(X73)
| ~ c1_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c2_1(X74)
| ~ c1_1(X74)
| ~ c3_1(X74) ) ) )
& ( ! [X75] :
( ndr1_0
=> ( c0_1(X75)
| ~ c1_1(X75)
| ~ c2_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c1_1(X76)
| c3_1(X76)
| ~ c2_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( c3_1(X77)
| ~ c1_1(X77)
| ~ c2_1(X77) ) ) )
& ( ! [X78] :
( ndr1_0
=> ( c0_1(X78)
| ~ c1_1(X78)
| ~ c3_1(X78) ) )
| hskp17
| hskp0 )
& ( ! [X79] :
( ndr1_0
=> ( c0_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79) ) )
| ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) ) )
& ( ! [X82] :
( ndr1_0
=> ( c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82) ) )
| hskp29
| hskp7 )
& ( ! [X83] :
( ndr1_0
=> ( c0_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83) ) )
| hskp0
| hskp18 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| c2_1(X84)
| c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85) ) )
| hskp12 )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| c2_1(X86)
| c3_1(X86) ) )
| hskp2
| hskp16 )
& ( ! [X87] :
( ndr1_0
=> ( c1_1(X87)
| c2_1(X87)
| ~ c0_1(X87) ) )
| hskp19
| hskp17 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| c2_1(X88)
| ~ c3_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89) ) )
| ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90) ) ) )
& ( ! [X91] :
( ndr1_0
=> ( c1_1(X91)
| c2_1(X91)
| ~ c3_1(X91) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c0_1(X92)
| ~ c2_1(X92)
| ~ c3_1(X92) ) )
| hskp6 )
& ( ! [X93] :
( ndr1_0
=> ( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) ) )
| hskp30
| hskp20 )
& ( ! [X94] :
( ndr1_0
=> ( c1_1(X94)
| ~ c0_1(X94)
| ~ c3_1(X94) ) )
| ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| hskp7 )
& ( ! [X96] :
( ndr1_0
=> ( c1_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96) ) )
| hskp21
| hskp6 )
& ( ! [X97] :
( ndr1_0
=> ( c1_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97) ) )
| hskp3
| hskp15 )
& ( ! [X98] :
( ndr1_0
=> ( c1_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp0
| hskp7 )
& ( ! [X99] :
( ndr1_0
=> ( c1_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99) ) )
| ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c1_1(X100)
| ~ c2_1(X100) ) )
| ! [X101] :
( ndr1_0
=> ( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101) ) ) )
& ( ! [X102] :
( ndr1_0
=> ( c1_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102) ) )
| hskp22
| hskp7 )
& ( ! [X103] :
( ndr1_0
=> ( c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103) ) )
| hskp8
| hskp23 )
& ( ! [X104] :
( ndr1_0
=> ( c2_1(X104)
| c3_1(X104)
| ~ c1_1(X104) ) )
| ! [X105] :
( ndr1_0
=> ( c3_1(X105)
| ~ c0_1(X105)
| ~ c1_1(X105) ) )
| hskp9 )
& ( ! [X106] :
( ndr1_0
=> ( c2_1(X106)
| c3_1(X106)
| ~ c1_1(X106) ) )
| ! [X107] :
( ndr1_0
=> ( c3_1(X107)
| ~ c1_1(X107)
| ~ c2_1(X107) ) )
| ! [X108] :
( ndr1_0
=> ( ~ c1_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108) ) ) )
& ( ! [X109] :
( ndr1_0
=> ( c2_1(X109)
| c3_1(X109)
| ~ c1_1(X109) ) )
| hskp15
| hskp24 )
& ( ! [X110] :
( ndr1_0
=> ( c2_1(X110)
| ~ c0_1(X110)
| ~ c1_1(X110) ) )
| hskp9
| hskp22 )
& ( ! [X111] :
( ndr1_0
=> ( c2_1(X111)
| ~ c0_1(X111)
| ~ c1_1(X111) ) )
| hskp10
| hskp18 )
& ( ! [X112] :
( ndr1_0
=> ( c2_1(X112)
| ~ c0_1(X112)
| ~ c3_1(X112) ) )
| hskp1
| hskp3 )
& ( ! [X113] :
( ndr1_0
=> ( c2_1(X113)
| ~ c0_1(X113)
| ~ c3_1(X113) ) )
| hskp25
| hskp6 )
& ( ! [X114] :
( ndr1_0
=> ( c2_1(X114)
| ~ c1_1(X114)
| ~ c3_1(X114) ) )
| hskp17
| hskp13 )
& ( ! [X115] :
( ndr1_0
=> ( c2_1(X115)
| ~ c1_1(X115)
| ~ c3_1(X115) ) )
| hskp17
| hskp24 )
& ( ! [X116] :
( ndr1_0
=> ( c2_1(X116)
| ~ c1_1(X116)
| ~ c3_1(X116) ) )
| hskp15
| hskp13 )
& ( ! [X117] :
( ndr1_0
=> ( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117) ) )
| hskp12
| hskp11 )
& ( ! [X118] :
( ndr1_0
=> ( c3_1(X118)
| ~ c0_1(X118)
| ~ c1_1(X118) ) )
| hskp7
| hskp24 )
& ( ! [X119] :
( ndr1_0
=> ( c3_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119) ) )
| hskp27
| hskp19 )
& ( ! [X120] :
( ndr1_0
=> ( c3_1(X120)
| ~ c1_1(X120)
| ~ c2_1(X120) ) )
| hskp22 )
& ( ! [X121] :
( ndr1_0
=> ( c3_1(X121)
| ~ c1_1(X121)
| ~ c2_1(X121) ) )
| hskp14
| hskp23 )
& ( ! [X122] :
( ndr1_0
=> ( ~ c0_1(X122)
| ~ c1_1(X122)
| ~ c2_1(X122) ) )
| hskp14
| hskp25 )
& ( ! [X123] :
( ndr1_0
=> ( ~ c0_1(X123)
| ~ c1_1(X123)
| ~ c3_1(X123) ) )
| hskp22
| hskp10 )
& ( ! [X124] :
( ndr1_0
=> ( ~ c0_1(X124)
| ~ c1_1(X124)
| ~ c3_1(X124) ) )
| hskp2
| hskp19 )
& ( ! [X125] :
( ndr1_0
=> ( ~ c1_1(X125)
| ~ c2_1(X125)
| ~ c3_1(X125) ) )
| hskp9
| hskp8 )
& ( ! [X126] :
( ndr1_0
=> ( ~ c1_1(X126)
| ~ c2_1(X126)
| ~ c3_1(X126) ) )
| hskp3
| hskp13 )
& ( hskp30
| hskp9
| hskp6 )
& ( hskp27
| hskp3
| hskp15 )
& ( hskp21
| hskp20
| hskp6 )
& ( hskp26
| hskp20
| hskp15 )
& ( hskp12
| hskp19
| hskp13 )
& ( hskp2
| hskp19
| hskp8 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ~ ( ( ~ hskp0
| ( ndr1_0
& c2_1(a123)
& ~ c0_1(a123)
& ~ c1_1(a123) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a124)
& c2_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a125)
& c2_1(a125)
& ~ c0_1(a125) ) )
& ( ~ hskp3
| ( ndr1_0
& c1_1(a127)
& ~ c2_1(a127)
& ~ c3_1(a127) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& ~ c3_1(a128) ) )
& ( ~ hskp5
| ( ndr1_0
& ~ c0_1(a130)
& ~ c1_1(a130)
& ~ c3_1(a130) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c0_1(a131)
& ~ c1_1(a131)
& ~ c2_1(a131) ) )
& ( ~ hskp7
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c2_1(a132) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a134)
& ~ c0_1(a134)
& ~ c3_1(a134) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a138)
& c1_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp10
| ( ndr1_0
& c0_1(a140)
& ~ c2_1(a140)
& ~ c3_1(a140) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c1_1(a141)
& ~ c2_1(a141)
& ~ c3_1(a141) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a142)
& c3_1(a142)
& ~ c1_1(a142) ) )
& ( ~ hskp13
| ( ndr1_0
& c2_1(a143)
& c3_1(a143)
& ~ c1_1(a143) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a153)
& c3_1(a153)
& ~ c0_1(a153) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a154)
& c3_1(a154)
& ~ c0_1(a154) ) )
& ( ~ hskp17
| ( ndr1_0
& c1_1(a155)
& ~ c0_1(a155)
& ~ c2_1(a155) ) )
& ( ~ hskp18
| ( ndr1_0
& c3_1(a160)
& ~ c1_1(a160)
& ~ c2_1(a160) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a164)
& c3_1(a164)
& ~ c2_1(a164) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a168)
& ~ c0_1(a168)
& ~ c3_1(a168) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a170)
& c2_1(a170)
& ~ c1_1(a170) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a176)
& ~ c1_1(a176)
& ~ c2_1(a176) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a179)
& ~ c1_1(a179)
& ~ c3_1(a179) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a182)
& ~ c2_1(a182)
& ~ c3_1(a182) ) )
& ( ~ hskp25
| ( ndr1_0
& c3_1(a189)
& ~ c0_1(a189)
& ~ c1_1(a189) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a225)
& c2_1(a225)
& ~ c3_1(a225) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a122)
& c2_1(a122)
& c3_1(a122) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a133)
& c2_1(a133)
& c3_1(a133) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a136)
& c1_1(a136)
& c2_1(a136) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a167)
& c1_1(a167)
& c3_1(a167) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c1_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c2_1(X4)
| ~ c1_1(X4) ) )
| ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c2_1(X5)
| ~ c3_1(X5) ) ) )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c2_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c2_1(X7)
| ~ c1_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c2_1(X8)
| c3_1(X8)
| ~ c0_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c3_1(X10)
| ~ c2_1(X10) ) )
| hskp27 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c2_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c2_1(X12)
| c3_1(X12)
| ~ c1_1(X12) ) )
| hskp0 )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| c2_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( c3_1(X14)
| ~ c0_1(X14)
| ~ c1_1(X14) ) )
| hskp1 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| c2_1(X15) ) )
| hskp2
| hskp1 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| c3_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( c2_1(X17)
| c3_1(X17)
| ~ c1_1(X17) ) )
| hskp3 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c2_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c2_1(X19)
| ~ c1_1(X19) ) )
| hskp4 )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c1_1(X21)
| ~ c0_1(X21)
| ~ c2_1(X21) ) )
| ! [X22] :
( ndr1_0
=> ( ~ c1_1(X22)
| ~ c2_1(X22)
| ~ c3_1(X22) ) ) )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c1_1(X23)
| ~ c2_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c3_1(X24)
| ~ c0_1(X24)
| ~ c2_1(X24) ) )
| hskp27 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c1_1(X25)
| ~ c2_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( ~ c0_1(X26)
| ~ c1_1(X26)
| ~ c2_1(X26) ) )
| hskp5 )
& ( ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c1_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c3_1(X29)
| ~ c1_1(X29)
| ~ c2_1(X29) ) ) )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c1_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c1_1(X31)
| c2_1(X31)
| ~ c3_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( c1_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32) ) ) )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c1_1(X33)
| ~ c3_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c0_1(X34)
| ~ c3_1(X34) ) )
| hskp6 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c1_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c2_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36) ) )
| hskp7 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c1_1(X37)
| ~ c3_1(X37) ) )
| hskp28
| hskp8 )
& ( ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| c2_1(X38)
| c3_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( ~ c0_1(X39)
| ~ c2_1(X39)
| ~ c3_1(X39) ) )
| hskp8 )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| c3_1(X40) ) )
| hskp29
| hskp7 )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c2_1(X41)
| c3_1(X41) ) )
| hskp9
| hskp7 )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| c3_1(X42) ) )
| hskp10
| hskp11 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c2_1(X43)
| ~ c1_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c2_1(X45)
| ~ c0_1(X45)
| ~ c3_1(X45) ) ) )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c2_1(X46)
| ~ c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47) ) )
| hskp12 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c2_1(X48)
| ~ c1_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c1_1(X49)
| c2_1(X49)
| ~ c0_1(X49) ) )
| hskp13 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| c2_1(X50)
| ~ c1_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51) ) )
| hskp28 )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| c2_1(X52)
| ~ c1_1(X52) ) )
| hskp28
| hskp3 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| c2_1(X53)
| ~ c3_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| hskp14 )
& ( ! [X55] :
( ndr1_0
=> ( c0_1(X55)
| c2_1(X55)
| ~ c3_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56) ) )
| ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57) ) ) )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| c2_1(X58)
| ~ c3_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c2_1(X59)
| c3_1(X59)
| ~ c1_1(X59) ) )
| hskp29 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| c2_1(X60)
| ~ c3_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c3_1(X61)
| ~ c0_1(X61)
| ~ c2_1(X61) ) )
| hskp12 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| c2_1(X62)
| ~ c3_1(X62) ) )
| hskp14
| hskp7 )
& ( ! [X63] :
( ndr1_0
=> ( c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63) ) )
| hskp10
| hskp15 )
& ( ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| c3_1(X64)
| ~ c1_1(X64) ) )
| ! [X65] :
( ndr1_0
=> ( c3_1(X65)
| ~ c1_1(X65)
| ~ c2_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66) ) ) )
& ( ! [X67] :
( ndr1_0
=> ( c0_1(X67)
| c3_1(X67)
| ~ c1_1(X67) ) )
| ! [X68] :
( ndr1_0
=> ( ~ c1_1(X68)
| ~ c2_1(X68)
| ~ c3_1(X68) ) )
| hskp16 )
& ( ! [X69] :
( ndr1_0
=> ( c0_1(X69)
| c3_1(X69)
| ~ c2_1(X69) ) )
| ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c2_1(X71) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( c0_1(X72)
| c3_1(X72)
| ~ c2_1(X72) ) )
| ! [X73] :
( ndr1_0
=> ( c2_1(X73)
| c3_1(X73)
| ~ c1_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c2_1(X74)
| ~ c1_1(X74)
| ~ c3_1(X74) ) ) )
& ( ! [X75] :
( ndr1_0
=> ( c0_1(X75)
| ~ c1_1(X75)
| ~ c2_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c1_1(X76)
| c3_1(X76)
| ~ c2_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( c3_1(X77)
| ~ c1_1(X77)
| ~ c2_1(X77) ) ) )
& ( ! [X78] :
( ndr1_0
=> ( c0_1(X78)
| ~ c1_1(X78)
| ~ c3_1(X78) ) )
| hskp17
| hskp0 )
& ( ! [X79] :
( ndr1_0
=> ( c0_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79) ) )
| ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) ) )
& ( ! [X82] :
( ndr1_0
=> ( c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82) ) )
| hskp29
| hskp7 )
& ( ! [X83] :
( ndr1_0
=> ( c0_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83) ) )
| hskp0
| hskp18 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| c2_1(X84)
| c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85) ) )
| hskp12 )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| c2_1(X86)
| c3_1(X86) ) )
| hskp2
| hskp16 )
& ( ! [X87] :
( ndr1_0
=> ( c1_1(X87)
| c2_1(X87)
| ~ c0_1(X87) ) )
| hskp19
| hskp17 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| c2_1(X88)
| ~ c3_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89) ) )
| ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90) ) ) )
& ( ! [X91] :
( ndr1_0
=> ( c1_1(X91)
| c2_1(X91)
| ~ c3_1(X91) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c0_1(X92)
| ~ c2_1(X92)
| ~ c3_1(X92) ) )
| hskp6 )
& ( ! [X93] :
( ndr1_0
=> ( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) ) )
| hskp30
| hskp20 )
& ( ! [X94] :
( ndr1_0
=> ( c1_1(X94)
| ~ c0_1(X94)
| ~ c3_1(X94) ) )
| ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| hskp7 )
& ( ! [X96] :
( ndr1_0
=> ( c1_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96) ) )
| hskp21
| hskp6 )
& ( ! [X97] :
( ndr1_0
=> ( c1_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97) ) )
| hskp3
| hskp15 )
& ( ! [X98] :
( ndr1_0
=> ( c1_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp0
| hskp7 )
& ( ! [X99] :
( ndr1_0
=> ( c1_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99) ) )
| ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c1_1(X100)
| ~ c2_1(X100) ) )
| ! [X101] :
( ndr1_0
=> ( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101) ) ) )
& ( ! [X102] :
( ndr1_0
=> ( c1_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102) ) )
| hskp22
| hskp7 )
& ( ! [X103] :
( ndr1_0
=> ( c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103) ) )
| hskp8
| hskp23 )
& ( ! [X104] :
( ndr1_0
=> ( c2_1(X104)
| c3_1(X104)
| ~ c1_1(X104) ) )
| ! [X105] :
( ndr1_0
=> ( c3_1(X105)
| ~ c0_1(X105)
| ~ c1_1(X105) ) )
| hskp9 )
& ( ! [X106] :
( ndr1_0
=> ( c2_1(X106)
| c3_1(X106)
| ~ c1_1(X106) ) )
| ! [X107] :
( ndr1_0
=> ( c3_1(X107)
| ~ c1_1(X107)
| ~ c2_1(X107) ) )
| ! [X108] :
( ndr1_0
=> ( ~ c1_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108) ) ) )
& ( ! [X109] :
( ndr1_0
=> ( c2_1(X109)
| c3_1(X109)
| ~ c1_1(X109) ) )
| hskp15
| hskp24 )
& ( ! [X110] :
( ndr1_0
=> ( c2_1(X110)
| ~ c0_1(X110)
| ~ c1_1(X110) ) )
| hskp9
| hskp22 )
& ( ! [X111] :
( ndr1_0
=> ( c2_1(X111)
| ~ c0_1(X111)
| ~ c1_1(X111) ) )
| hskp10
| hskp18 )
& ( ! [X112] :
( ndr1_0
=> ( c2_1(X112)
| ~ c0_1(X112)
| ~ c3_1(X112) ) )
| hskp1
| hskp3 )
& ( ! [X113] :
( ndr1_0
=> ( c2_1(X113)
| ~ c0_1(X113)
| ~ c3_1(X113) ) )
| hskp25
| hskp6 )
& ( ! [X114] :
( ndr1_0
=> ( c2_1(X114)
| ~ c1_1(X114)
| ~ c3_1(X114) ) )
| hskp17
| hskp13 )
& ( ! [X115] :
( ndr1_0
=> ( c2_1(X115)
| ~ c1_1(X115)
| ~ c3_1(X115) ) )
| hskp17
| hskp24 )
& ( ! [X116] :
( ndr1_0
=> ( c2_1(X116)
| ~ c1_1(X116)
| ~ c3_1(X116) ) )
| hskp15
| hskp13 )
& ( ! [X117] :
( ndr1_0
=> ( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117) ) )
| hskp12
| hskp11 )
& ( ! [X118] :
( ndr1_0
=> ( c3_1(X118)
| ~ c0_1(X118)
| ~ c1_1(X118) ) )
| hskp7
| hskp24 )
& ( ! [X119] :
( ndr1_0
=> ( c3_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119) ) )
| hskp27
| hskp19 )
& ( ! [X120] :
( ndr1_0
=> ( c3_1(X120)
| ~ c1_1(X120)
| ~ c2_1(X120) ) )
| hskp22 )
& ( ! [X121] :
( ndr1_0
=> ( c3_1(X121)
| ~ c1_1(X121)
| ~ c2_1(X121) ) )
| hskp14
| hskp23 )
& ( ! [X122] :
( ndr1_0
=> ( ~ c0_1(X122)
| ~ c1_1(X122)
| ~ c2_1(X122) ) )
| hskp14
| hskp25 )
& ( ! [X123] :
( ndr1_0
=> ( ~ c0_1(X123)
| ~ c1_1(X123)
| ~ c3_1(X123) ) )
| hskp22
| hskp10 )
& ( ! [X124] :
( ndr1_0
=> ( ~ c0_1(X124)
| ~ c1_1(X124)
| ~ c3_1(X124) ) )
| hskp2
| hskp19 )
& ( ! [X125] :
( ndr1_0
=> ( ~ c1_1(X125)
| ~ c2_1(X125)
| ~ c3_1(X125) ) )
| hskp9
| hskp8 )
& ( ! [X126] :
( ndr1_0
=> ( ~ c1_1(X126)
| ~ c2_1(X126)
| ~ c3_1(X126) ) )
| hskp3
| hskp13 )
& ( hskp30
| hskp9
| hskp6 )
& ( hskp27
| hskp3
| hskp15 )
& ( hskp21
| hskp20
| hskp6 )
& ( hskp26
| hskp20
| hskp15 )
& ( hskp12
| hskp19
| hskp13 )
& ( hskp2
| hskp19
| hskp8 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ~ hskp0
| ( ndr1_0
& c2_1(a123)
& ~ c0_1(a123)
& ~ c1_1(a123) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a124)
& c2_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a125)
& c2_1(a125)
& ~ c0_1(a125) ) )
& ( ~ hskp3
| ( ndr1_0
& c1_1(a127)
& ~ c2_1(a127)
& ~ c3_1(a127) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& ~ c3_1(a128) ) )
& ( ~ hskp5
| ( ndr1_0
& ~ c0_1(a130)
& ~ c1_1(a130)
& ~ c3_1(a130) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c0_1(a131)
& ~ c1_1(a131)
& ~ c2_1(a131) ) )
& ( ~ hskp7
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c2_1(a132) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a134)
& ~ c0_1(a134)
& ~ c3_1(a134) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a138)
& c1_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp10
| ( ndr1_0
& c0_1(a140)
& ~ c2_1(a140)
& ~ c3_1(a140) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c1_1(a141)
& ~ c2_1(a141)
& ~ c3_1(a141) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a142)
& c3_1(a142)
& ~ c1_1(a142) ) )
& ( ~ hskp13
| ( ndr1_0
& c2_1(a143)
& c3_1(a143)
& ~ c1_1(a143) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a153)
& c3_1(a153)
& ~ c0_1(a153) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a154)
& c3_1(a154)
& ~ c0_1(a154) ) )
& ( ~ hskp17
| ( ndr1_0
& c1_1(a155)
& ~ c0_1(a155)
& ~ c2_1(a155) ) )
& ( ~ hskp18
| ( ndr1_0
& c3_1(a160)
& ~ c1_1(a160)
& ~ c2_1(a160) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a164)
& c3_1(a164)
& ~ c2_1(a164) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a168)
& ~ c0_1(a168)
& ~ c3_1(a168) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a170)
& c2_1(a170)
& ~ c1_1(a170) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a176)
& ~ c1_1(a176)
& ~ c2_1(a176) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a179)
& ~ c1_1(a179)
& ~ c3_1(a179) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a182)
& ~ c2_1(a182)
& ~ c3_1(a182) ) )
& ( ~ hskp25
| ( ndr1_0
& c3_1(a189)
& ~ c0_1(a189)
& ~ c1_1(a189) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a225)
& c2_1(a225)
& ~ c3_1(a225) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a122)
& c2_1(a122)
& c3_1(a122) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a133)
& c2_1(a133)
& c3_1(a133) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a136)
& c1_1(a136)
& c2_1(a136) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a167)
& c1_1(a167)
& c3_1(a167) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c1_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c2_1(X4)
| ~ c1_1(X4) ) )
| ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c2_1(X5)
| ~ c3_1(X5) ) ) )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c2_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c2_1(X7)
| ~ c1_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c2_1(X8)
| c3_1(X8)
| ~ c0_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c3_1(X10)
| ~ c2_1(X10) ) )
| hskp27 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c2_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c2_1(X12)
| c3_1(X12)
| ~ c1_1(X12) ) )
| hskp0 )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| c2_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( c3_1(X14)
| ~ c0_1(X14)
| ~ c1_1(X14) ) )
| hskp1 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| c2_1(X15) ) )
| hskp2
| hskp1 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| c3_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( c2_1(X17)
| c3_1(X17)
| ~ c1_1(X17) ) )
| hskp3 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c2_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c2_1(X19)
| ~ c1_1(X19) ) )
| hskp4 )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c1_1(X21)
| ~ c0_1(X21)
| ~ c2_1(X21) ) )
| ! [X22] :
( ndr1_0
=> ( ~ c1_1(X22)
| ~ c2_1(X22)
| ~ c3_1(X22) ) ) )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c1_1(X23)
| ~ c2_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c3_1(X24)
| ~ c0_1(X24)
| ~ c2_1(X24) ) )
| hskp27 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c1_1(X25)
| ~ c2_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( ~ c0_1(X26)
| ~ c1_1(X26)
| ~ c2_1(X26) ) )
| hskp5 )
& ( ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c1_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c3_1(X29)
| ~ c1_1(X29)
| ~ c2_1(X29) ) ) )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c1_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c1_1(X31)
| c2_1(X31)
| ~ c3_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( c1_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32) ) ) )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c1_1(X33)
| ~ c3_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c0_1(X34)
| ~ c3_1(X34) ) )
| hskp6 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c1_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c2_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36) ) )
| hskp7 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c1_1(X37)
| ~ c3_1(X37) ) )
| hskp28
| hskp8 )
& ( ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| c2_1(X38)
| c3_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( ~ c0_1(X39)
| ~ c2_1(X39)
| ~ c3_1(X39) ) )
| hskp8 )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| c3_1(X40) ) )
| hskp29
| hskp7 )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c2_1(X41)
| c3_1(X41) ) )
| hskp9
| hskp7 )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| c3_1(X42) ) )
| hskp10
| hskp11 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c2_1(X43)
| ~ c1_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c2_1(X45)
| ~ c0_1(X45)
| ~ c3_1(X45) ) ) )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c2_1(X46)
| ~ c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47) ) )
| hskp12 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c2_1(X48)
| ~ c1_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c1_1(X49)
| c2_1(X49)
| ~ c0_1(X49) ) )
| hskp13 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| c2_1(X50)
| ~ c1_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51) ) )
| hskp28 )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| c2_1(X52)
| ~ c1_1(X52) ) )
| hskp28
| hskp3 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| c2_1(X53)
| ~ c3_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| hskp14 )
& ( ! [X55] :
( ndr1_0
=> ( c0_1(X55)
| c2_1(X55)
| ~ c3_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56) ) )
| ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57) ) ) )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| c2_1(X58)
| ~ c3_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c2_1(X59)
| c3_1(X59)
| ~ c1_1(X59) ) )
| hskp29 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| c2_1(X60)
| ~ c3_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c3_1(X61)
| ~ c0_1(X61)
| ~ c2_1(X61) ) )
| hskp12 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| c2_1(X62)
| ~ c3_1(X62) ) )
| hskp14
| hskp7 )
& ( ! [X63] :
( ndr1_0
=> ( c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63) ) )
| hskp10
| hskp15 )
& ( ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| c3_1(X64)
| ~ c1_1(X64) ) )
| ! [X65] :
( ndr1_0
=> ( c3_1(X65)
| ~ c1_1(X65)
| ~ c2_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66) ) ) )
& ( ! [X67] :
( ndr1_0
=> ( c0_1(X67)
| c3_1(X67)
| ~ c1_1(X67) ) )
| ! [X68] :
( ndr1_0
=> ( ~ c1_1(X68)
| ~ c2_1(X68)
| ~ c3_1(X68) ) )
| hskp16 )
& ( ! [X69] :
( ndr1_0
=> ( c0_1(X69)
| c3_1(X69)
| ~ c2_1(X69) ) )
| ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c2_1(X71) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( c0_1(X72)
| c3_1(X72)
| ~ c2_1(X72) ) )
| ! [X73] :
( ndr1_0
=> ( c2_1(X73)
| c3_1(X73)
| ~ c1_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c2_1(X74)
| ~ c1_1(X74)
| ~ c3_1(X74) ) ) )
& ( ! [X75] :
( ndr1_0
=> ( c0_1(X75)
| ~ c1_1(X75)
| ~ c2_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c1_1(X76)
| c3_1(X76)
| ~ c2_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( c3_1(X77)
| ~ c1_1(X77)
| ~ c2_1(X77) ) ) )
& ( ! [X78] :
( ndr1_0
=> ( c0_1(X78)
| ~ c1_1(X78)
| ~ c3_1(X78) ) )
| hskp17
| hskp0 )
& ( ! [X79] :
( ndr1_0
=> ( c0_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79) ) )
| ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) ) )
& ( ! [X82] :
( ndr1_0
=> ( c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82) ) )
| hskp29
| hskp7 )
& ( ! [X83] :
( ndr1_0
=> ( c0_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83) ) )
| hskp0
| hskp18 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| c2_1(X84)
| c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85) ) )
| hskp12 )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| c2_1(X86)
| c3_1(X86) ) )
| hskp2
| hskp16 )
& ( ! [X87] :
( ndr1_0
=> ( c1_1(X87)
| c2_1(X87)
| ~ c0_1(X87) ) )
| hskp19
| hskp17 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| c2_1(X88)
| ~ c3_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89) ) )
| ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90) ) ) )
& ( ! [X91] :
( ndr1_0
=> ( c1_1(X91)
| c2_1(X91)
| ~ c3_1(X91) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c0_1(X92)
| ~ c2_1(X92)
| ~ c3_1(X92) ) )
| hskp6 )
& ( ! [X93] :
( ndr1_0
=> ( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) ) )
| hskp30
| hskp20 )
& ( ! [X94] :
( ndr1_0
=> ( c1_1(X94)
| ~ c0_1(X94)
| ~ c3_1(X94) ) )
| ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| hskp7 )
& ( ! [X96] :
( ndr1_0
=> ( c1_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96) ) )
| hskp21
| hskp6 )
& ( ! [X97] :
( ndr1_0
=> ( c1_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97) ) )
| hskp3
| hskp15 )
& ( ! [X98] :
( ndr1_0
=> ( c1_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp0
| hskp7 )
& ( ! [X99] :
( ndr1_0
=> ( c1_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99) ) )
| ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c1_1(X100)
| ~ c2_1(X100) ) )
| ! [X101] :
( ndr1_0
=> ( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101) ) ) )
& ( ! [X102] :
( ndr1_0
=> ( c1_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102) ) )
| hskp22
| hskp7 )
& ( ! [X103] :
( ndr1_0
=> ( c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103) ) )
| hskp8
| hskp23 )
& ( ! [X104] :
( ndr1_0
=> ( c2_1(X104)
| c3_1(X104)
| ~ c1_1(X104) ) )
| ! [X105] :
( ndr1_0
=> ( c3_1(X105)
| ~ c0_1(X105)
| ~ c1_1(X105) ) )
| hskp9 )
& ( ! [X106] :
( ndr1_0
=> ( c2_1(X106)
| c3_1(X106)
| ~ c1_1(X106) ) )
| ! [X107] :
( ndr1_0
=> ( c3_1(X107)
| ~ c1_1(X107)
| ~ c2_1(X107) ) )
| ! [X108] :
( ndr1_0
=> ( ~ c1_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108) ) ) )
& ( ! [X109] :
( ndr1_0
=> ( c2_1(X109)
| c3_1(X109)
| ~ c1_1(X109) ) )
| hskp15
| hskp24 )
& ( ! [X110] :
( ndr1_0
=> ( c2_1(X110)
| ~ c0_1(X110)
| ~ c1_1(X110) ) )
| hskp9
| hskp22 )
& ( ! [X111] :
( ndr1_0
=> ( c2_1(X111)
| ~ c0_1(X111)
| ~ c1_1(X111) ) )
| hskp10
| hskp18 )
& ( ! [X112] :
( ndr1_0
=> ( c2_1(X112)
| ~ c0_1(X112)
| ~ c3_1(X112) ) )
| hskp1
| hskp3 )
& ( ! [X113] :
( ndr1_0
=> ( c2_1(X113)
| ~ c0_1(X113)
| ~ c3_1(X113) ) )
| hskp25
| hskp6 )
& ( ! [X114] :
( ndr1_0
=> ( c2_1(X114)
| ~ c1_1(X114)
| ~ c3_1(X114) ) )
| hskp17
| hskp13 )
& ( ! [X115] :
( ndr1_0
=> ( c2_1(X115)
| ~ c1_1(X115)
| ~ c3_1(X115) ) )
| hskp17
| hskp24 )
& ( ! [X116] :
( ndr1_0
=> ( c2_1(X116)
| ~ c1_1(X116)
| ~ c3_1(X116) ) )
| hskp15
| hskp13 )
& ( ! [X117] :
( ndr1_0
=> ( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117) ) )
| hskp12
| hskp11 )
& ( ! [X118] :
( ndr1_0
=> ( c3_1(X118)
| ~ c0_1(X118)
| ~ c1_1(X118) ) )
| hskp7
| hskp24 )
& ( ! [X119] :
( ndr1_0
=> ( c3_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119) ) )
| hskp27
| hskp19 )
& ( ! [X120] :
( ndr1_0
=> ( c3_1(X120)
| ~ c1_1(X120)
| ~ c2_1(X120) ) )
| hskp22 )
& ( ! [X121] :
( ndr1_0
=> ( c3_1(X121)
| ~ c1_1(X121)
| ~ c2_1(X121) ) )
| hskp14
| hskp23 )
& ( ! [X122] :
( ndr1_0
=> ( ~ c0_1(X122)
| ~ c1_1(X122)
| ~ c2_1(X122) ) )
| hskp14
| hskp25 )
& ( ! [X123] :
( ndr1_0
=> ( ~ c0_1(X123)
| ~ c1_1(X123)
| ~ c3_1(X123) ) )
| hskp22
| hskp10 )
& ( ! [X124] :
( ndr1_0
=> ( ~ c0_1(X124)
| ~ c1_1(X124)
| ~ c3_1(X124) ) )
| hskp2
| hskp19 )
& ( ! [X125] :
( ndr1_0
=> ( ~ c1_1(X125)
| ~ c2_1(X125)
| ~ c3_1(X125) ) )
| hskp9
| hskp8 )
& ( ! [X126] :
( ndr1_0
=> ( ~ c1_1(X126)
| ~ c2_1(X126)
| ~ c3_1(X126) ) )
| hskp3
| hskp13 )
& ( hskp30
| hskp9
| hskp6 )
& ( hskp27
| hskp3
| hskp15 )
& ( hskp21
| hskp20
| hskp6 )
& ( hskp26
| hskp20
| hskp15 )
& ( hskp12
| hskp19
| hskp13 )
& ( hskp2
| hskp19
| hskp8 ) ),
inference(flattening,[],[f2]) ).
fof(f4,plain,
( ( ~ hskp0
| ( ndr1_0
& c2_1(a123)
& ~ c0_1(a123)
& ~ c1_1(a123) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a124)
& c2_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a125)
& c2_1(a125)
& ~ c0_1(a125) ) )
& ( ~ hskp3
| ( ndr1_0
& c1_1(a127)
& ~ c2_1(a127)
& ~ c3_1(a127) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& ~ c3_1(a128) ) )
& ( ~ hskp5
| ( ndr1_0
& ~ c0_1(a130)
& ~ c1_1(a130)
& ~ c3_1(a130) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c0_1(a131)
& ~ c1_1(a131)
& ~ c2_1(a131) ) )
& ( ~ hskp7
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c2_1(a132) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a134)
& ~ c0_1(a134)
& ~ c3_1(a134) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a138)
& c1_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp10
| ( ndr1_0
& c0_1(a140)
& ~ c2_1(a140)
& ~ c3_1(a140) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c1_1(a141)
& ~ c2_1(a141)
& ~ c3_1(a141) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a142)
& c3_1(a142)
& ~ c1_1(a142) ) )
& ( ~ hskp13
| ( ndr1_0
& c2_1(a143)
& c3_1(a143)
& ~ c1_1(a143) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a153)
& c3_1(a153)
& ~ c0_1(a153) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a154)
& c3_1(a154)
& ~ c0_1(a154) ) )
& ( ~ hskp17
| ( ndr1_0
& c1_1(a155)
& ~ c0_1(a155)
& ~ c2_1(a155) ) )
& ( ~ hskp18
| ( ndr1_0
& c3_1(a160)
& ~ c1_1(a160)
& ~ c2_1(a160) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a164)
& c3_1(a164)
& ~ c2_1(a164) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a168)
& ~ c0_1(a168)
& ~ c3_1(a168) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a170)
& c2_1(a170)
& ~ c1_1(a170) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a176)
& ~ c1_1(a176)
& ~ c2_1(a176) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a179)
& ~ c1_1(a179)
& ~ c3_1(a179) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a182)
& ~ c2_1(a182)
& ~ c3_1(a182) ) )
& ( ~ hskp25
| ( ndr1_0
& c3_1(a189)
& ~ c0_1(a189)
& ~ c1_1(a189) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a225)
& c2_1(a225)
& ~ c3_1(a225) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a122)
& c2_1(a122)
& c3_1(a122) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a133)
& c2_1(a133)
& c3_1(a133) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a136)
& c1_1(a136)
& c2_1(a136) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a167)
& c1_1(a167)
& c3_1(a167) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c0_1(X4)
| c2_1(X4)
| ~ c1_1(X4)
| ~ ndr1_0 )
| ! [X5] :
( c0_1(X5)
| c2_1(X5)
| ~ c3_1(X5)
| ~ ndr1_0 ) )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c2_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c0_1(X7)
| c2_1(X7)
| ~ c1_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c2_1(X8)
| c3_1(X8)
| ~ c0_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c0_1(X10)
| c3_1(X10)
| ~ c2_1(X10)
| ~ ndr1_0 )
| hskp27 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| c2_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c2_1(X12)
| c3_1(X12)
| ~ c1_1(X12)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X13] :
( c0_1(X13)
| c1_1(X13)
| c2_1(X13)
| ~ ndr1_0 )
| ! [X14] :
( c3_1(X14)
| ~ c0_1(X14)
| ~ c1_1(X14)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| c2_1(X15)
| ~ ndr1_0 )
| hskp2
| hskp1 )
& ( ! [X16] :
( c0_1(X16)
| c1_1(X16)
| c3_1(X16)
| ~ ndr1_0 )
| ! [X17] :
( c2_1(X17)
| c3_1(X17)
| ~ c1_1(X17)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c2_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c0_1(X19)
| c2_1(X19)
| ~ c1_1(X19)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( c1_1(X21)
| ~ c0_1(X21)
| ~ c2_1(X21)
| ~ ndr1_0 )
| ! [X22] :
( ~ c1_1(X22)
| ~ c2_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0 ) )
& ( ! [X23] :
( c0_1(X23)
| c1_1(X23)
| ~ c2_1(X23)
| ~ ndr1_0 )
| ! [X24] :
( c3_1(X24)
| ~ c0_1(X24)
| ~ c2_1(X24)
| ~ ndr1_0 )
| hskp27 )
& ( ! [X25] :
( c0_1(X25)
| c1_1(X25)
| ~ c2_1(X25)
| ~ ndr1_0 )
| ! [X26] :
( ~ c0_1(X26)
| ~ c1_1(X26)
| ~ c2_1(X26)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X27] :
( c0_1(X27)
| c1_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( c3_1(X29)
| ~ c1_1(X29)
| ~ c2_1(X29)
| ~ ndr1_0 ) )
& ( ! [X30] :
( c0_1(X30)
| c1_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c1_1(X31)
| c2_1(X31)
| ~ c3_1(X31)
| ~ ndr1_0 )
| ! [X32] :
( c1_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 ) )
& ( ! [X33] :
( c0_1(X33)
| c1_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| ~ c0_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X35] :
( c0_1(X35)
| c1_1(X35)
| ~ c3_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c2_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X37] :
( c0_1(X37)
| c1_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0 )
| hskp28
| hskp8 )
& ( ! [X38] :
( c0_1(X38)
| c2_1(X38)
| c3_1(X38)
| ~ ndr1_0 )
| ! [X39] :
( ~ c0_1(X39)
| ~ c2_1(X39)
| ~ c3_1(X39)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X40] :
( c0_1(X40)
| c2_1(X40)
| c3_1(X40)
| ~ ndr1_0 )
| hskp29
| hskp7 )
& ( ! [X41] :
( c0_1(X41)
| c2_1(X41)
| c3_1(X41)
| ~ ndr1_0 )
| hskp9
| hskp7 )
& ( ! [X42] :
( c0_1(X42)
| c2_1(X42)
| c3_1(X42)
| ~ ndr1_0 )
| hskp10
| hskp11 )
& ( ! [X43] :
( c0_1(X43)
| c2_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0 )
| ! [X44] :
( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( c2_1(X45)
| ~ c0_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 ) )
& ( ! [X46] :
( c0_1(X46)
| c2_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X48] :
( c0_1(X48)
| c2_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0 )
| ! [X49] :
( c1_1(X49)
| c2_1(X49)
| ~ c0_1(X49)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X50] :
( c0_1(X50)
| c2_1(X50)
| ~ c1_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X52] :
( c0_1(X52)
| c2_1(X52)
| ~ c1_1(X52)
| ~ ndr1_0 )
| hskp28
| hskp3 )
& ( ! [X53] :
( c0_1(X53)
| c2_1(X53)
| ~ c3_1(X53)
| ~ ndr1_0 )
| ! [X54] :
( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X55] :
( c0_1(X55)
| c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0 )
| ! [X57] :
( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57)
| ~ ndr1_0 ) )
& ( ! [X58] :
( c0_1(X58)
| c2_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( c2_1(X59)
| c3_1(X59)
| ~ c1_1(X59)
| ~ ndr1_0 )
| hskp29 )
& ( ! [X60] :
( c0_1(X60)
| c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| ! [X61] :
( c3_1(X61)
| ~ c0_1(X61)
| ~ c2_1(X61)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X62] :
( c0_1(X62)
| c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0 )
| hskp14
| hskp7 )
& ( ! [X63] :
( c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0 )
| hskp10
| hskp15 )
& ( ! [X64] :
( c0_1(X64)
| c3_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 )
| ! [X65] :
( c3_1(X65)
| ~ c1_1(X65)
| ~ c2_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( ~ c0_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 ) )
& ( ! [X67] :
( c0_1(X67)
| c3_1(X67)
| ~ c1_1(X67)
| ~ ndr1_0 )
| ! [X68] :
( ~ c1_1(X68)
| ~ c2_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X69] :
( c0_1(X69)
| c3_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0 )
| ! [X70] :
( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0 )
| ! [X71] :
( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 ) )
& ( ! [X72] :
( c0_1(X72)
| c3_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| ! [X73] :
( c2_1(X73)
| c3_1(X73)
| ~ c1_1(X73)
| ~ ndr1_0 )
| ! [X74] :
( c2_1(X74)
| ~ c1_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0 ) )
& ( ! [X75] :
( c0_1(X75)
| ~ c1_1(X75)
| ~ c2_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c1_1(X76)
| c3_1(X76)
| ~ c2_1(X76)
| ~ ndr1_0 )
| ! [X77] :
( c3_1(X77)
| ~ c1_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0 ) )
& ( ! [X78] :
( c0_1(X78)
| ~ c1_1(X78)
| ~ c3_1(X78)
| ~ ndr1_0 )
| hskp17
| hskp0 )
& ( ! [X79] :
( c0_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0 )
| ! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 ) )
& ( ! [X82] :
( c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 )
| hskp29
| hskp7 )
& ( ! [X83] :
( c0_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp0
| hskp18 )
& ( ! [X84] :
( c1_1(X84)
| c2_1(X84)
| c3_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X86] :
( c1_1(X86)
| c2_1(X86)
| c3_1(X86)
| ~ ndr1_0 )
| hskp2
| hskp16 )
& ( ! [X87] :
( c1_1(X87)
| c2_1(X87)
| ~ c0_1(X87)
| ~ ndr1_0 )
| hskp19
| hskp17 )
& ( ! [X88] :
( c1_1(X88)
| c2_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0 )
| ! [X90] :
( c2_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 ) )
& ( ! [X91] :
( c1_1(X91)
| c2_1(X91)
| ~ c3_1(X91)
| ~ ndr1_0 )
| ! [X92] :
( ~ c0_1(X92)
| ~ c2_1(X92)
| ~ c3_1(X92)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X93] :
( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93)
| ~ ndr1_0 )
| hskp30
| hskp20 )
& ( ! [X94] :
( c1_1(X94)
| ~ c0_1(X94)
| ~ c3_1(X94)
| ~ ndr1_0 )
| ! [X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X96] :
( c1_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0 )
| hskp21
| hskp6 )
& ( ! [X97] :
( c1_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97)
| ~ ndr1_0 )
| hskp3
| hskp15 )
& ( ! [X98] :
( c1_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| hskp0
| hskp7 )
& ( ! [X99] :
( c1_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99)
| ~ ndr1_0 )
| ! [X100] :
( c3_1(X100)
| ~ c1_1(X100)
| ~ c2_1(X100)
| ~ ndr1_0 )
| ! [X101] :
( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101)
| ~ ndr1_0 ) )
& ( ! [X102] :
( c1_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0 )
| hskp22
| hskp7 )
& ( ! [X103] :
( c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp8
| hskp23 )
& ( ! [X104] :
( c2_1(X104)
| c3_1(X104)
| ~ c1_1(X104)
| ~ ndr1_0 )
| ! [X105] :
( c3_1(X105)
| ~ c0_1(X105)
| ~ c1_1(X105)
| ~ ndr1_0 )
| hskp9 )
& ( ! [X106] :
( c2_1(X106)
| c3_1(X106)
| ~ c1_1(X106)
| ~ ndr1_0 )
| ! [X107] :
( c3_1(X107)
| ~ c1_1(X107)
| ~ c2_1(X107)
| ~ ndr1_0 )
| ! [X108] :
( ~ c1_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108)
| ~ ndr1_0 ) )
& ( ! [X109] :
( c2_1(X109)
| c3_1(X109)
| ~ c1_1(X109)
| ~ ndr1_0 )
| hskp15
| hskp24 )
& ( ! [X110] :
( c2_1(X110)
| ~ c0_1(X110)
| ~ c1_1(X110)
| ~ ndr1_0 )
| hskp9
| hskp22 )
& ( ! [X111] :
( c2_1(X111)
| ~ c0_1(X111)
| ~ c1_1(X111)
| ~ ndr1_0 )
| hskp10
| hskp18 )
& ( ! [X112] :
( c2_1(X112)
| ~ c0_1(X112)
| ~ c3_1(X112)
| ~ ndr1_0 )
| hskp1
| hskp3 )
& ( ! [X113] :
( c2_1(X113)
| ~ c0_1(X113)
| ~ c3_1(X113)
| ~ ndr1_0 )
| hskp25
| hskp6 )
& ( ! [X114] :
( c2_1(X114)
| ~ c1_1(X114)
| ~ c3_1(X114)
| ~ ndr1_0 )
| hskp17
| hskp13 )
& ( ! [X115] :
( c2_1(X115)
| ~ c1_1(X115)
| ~ c3_1(X115)
| ~ ndr1_0 )
| hskp17
| hskp24 )
& ( ! [X116] :
( c2_1(X116)
| ~ c1_1(X116)
| ~ c3_1(X116)
| ~ ndr1_0 )
| hskp15
| hskp13 )
& ( ! [X117] :
( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117)
| ~ ndr1_0 )
| hskp12
| hskp11 )
& ( ! [X118] :
( c3_1(X118)
| ~ c0_1(X118)
| ~ c1_1(X118)
| ~ ndr1_0 )
| hskp7
| hskp24 )
& ( ! [X119] :
( c3_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119)
| ~ ndr1_0 )
| hskp27
| hskp19 )
& ( ! [X120] :
( c3_1(X120)
| ~ c1_1(X120)
| ~ c2_1(X120)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X121] :
( c3_1(X121)
| ~ c1_1(X121)
| ~ c2_1(X121)
| ~ ndr1_0 )
| hskp14
| hskp23 )
& ( ! [X122] :
( ~ c0_1(X122)
| ~ c1_1(X122)
| ~ c2_1(X122)
| ~ ndr1_0 )
| hskp14
| hskp25 )
& ( ! [X123] :
( ~ c0_1(X123)
| ~ c1_1(X123)
| ~ c3_1(X123)
| ~ ndr1_0 )
| hskp22
| hskp10 )
& ( ! [X124] :
( ~ c0_1(X124)
| ~ c1_1(X124)
| ~ c3_1(X124)
| ~ ndr1_0 )
| hskp2
| hskp19 )
& ( ! [X125] :
( ~ c1_1(X125)
| ~ c2_1(X125)
| ~ c3_1(X125)
| ~ ndr1_0 )
| hskp9
| hskp8 )
& ( ! [X126] :
( ~ c1_1(X126)
| ~ c2_1(X126)
| ~ c3_1(X126)
| ~ ndr1_0 )
| hskp3
| hskp13 )
& ( hskp30
| hskp9
| hskp6 )
& ( hskp27
| hskp3
| hskp15 )
& ( hskp21
| hskp20
| hskp6 )
& ( hskp26
| hskp20
| hskp15 )
& ( hskp12
| hskp19
| hskp13 )
& ( hskp2
| hskp19
| hskp8 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ~ hskp0
| ( ndr1_0
& c2_1(a123)
& ~ c0_1(a123)
& ~ c1_1(a123) ) )
& ( ~ hskp1
| ( ndr1_0
& c1_1(a124)
& c2_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a125)
& c2_1(a125)
& ~ c0_1(a125) ) )
& ( ~ hskp3
| ( ndr1_0
& c1_1(a127)
& ~ c2_1(a127)
& ~ c3_1(a127) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& ~ c3_1(a128) ) )
& ( ~ hskp5
| ( ndr1_0
& ~ c0_1(a130)
& ~ c1_1(a130)
& ~ c3_1(a130) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c0_1(a131)
& ~ c1_1(a131)
& ~ c2_1(a131) ) )
& ( ~ hskp7
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c2_1(a132) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a134)
& ~ c0_1(a134)
& ~ c3_1(a134) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a138)
& c1_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp10
| ( ndr1_0
& c0_1(a140)
& ~ c2_1(a140)
& ~ c3_1(a140) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c1_1(a141)
& ~ c2_1(a141)
& ~ c3_1(a141) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a142)
& c3_1(a142)
& ~ c1_1(a142) ) )
& ( ~ hskp13
| ( ndr1_0
& c2_1(a143)
& c3_1(a143)
& ~ c1_1(a143) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a153)
& c3_1(a153)
& ~ c0_1(a153) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a154)
& c3_1(a154)
& ~ c0_1(a154) ) )
& ( ~ hskp17
| ( ndr1_0
& c1_1(a155)
& ~ c0_1(a155)
& ~ c2_1(a155) ) )
& ( ~ hskp18
| ( ndr1_0
& c3_1(a160)
& ~ c1_1(a160)
& ~ c2_1(a160) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a164)
& c3_1(a164)
& ~ c2_1(a164) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a168)
& ~ c0_1(a168)
& ~ c3_1(a168) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a170)
& c2_1(a170)
& ~ c1_1(a170) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a176)
& ~ c1_1(a176)
& ~ c2_1(a176) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a179)
& ~ c1_1(a179)
& ~ c3_1(a179) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a182)
& ~ c2_1(a182)
& ~ c3_1(a182) ) )
& ( ~ hskp25
| ( ndr1_0
& c3_1(a189)
& ~ c0_1(a189)
& ~ c1_1(a189) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a225)
& c2_1(a225)
& ~ c3_1(a225) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a122)
& c2_1(a122)
& c3_1(a122) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a133)
& c2_1(a133)
& c3_1(a133) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a136)
& c1_1(a136)
& c2_1(a136) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a167)
& c1_1(a167)
& c3_1(a167) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c0_1(X4)
| c2_1(X4)
| ~ c1_1(X4)
| ~ ndr1_0 )
| ! [X5] :
( c0_1(X5)
| c2_1(X5)
| ~ c3_1(X5)
| ~ ndr1_0 ) )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c2_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c0_1(X7)
| c2_1(X7)
| ~ c1_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c2_1(X8)
| c3_1(X8)
| ~ c0_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c0_1(X10)
| c3_1(X10)
| ~ c2_1(X10)
| ~ ndr1_0 )
| hskp27 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| c2_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c2_1(X12)
| c3_1(X12)
| ~ c1_1(X12)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X13] :
( c0_1(X13)
| c1_1(X13)
| c2_1(X13)
| ~ ndr1_0 )
| ! [X14] :
( c3_1(X14)
| ~ c0_1(X14)
| ~ c1_1(X14)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| c2_1(X15)
| ~ ndr1_0 )
| hskp2
| hskp1 )
& ( ! [X16] :
( c0_1(X16)
| c1_1(X16)
| c3_1(X16)
| ~ ndr1_0 )
| ! [X17] :
( c2_1(X17)
| c3_1(X17)
| ~ c1_1(X17)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c2_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c0_1(X19)
| c2_1(X19)
| ~ c1_1(X19)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( c1_1(X21)
| ~ c0_1(X21)
| ~ c2_1(X21)
| ~ ndr1_0 )
| ! [X22] :
( ~ c1_1(X22)
| ~ c2_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0 ) )
& ( ! [X23] :
( c0_1(X23)
| c1_1(X23)
| ~ c2_1(X23)
| ~ ndr1_0 )
| ! [X24] :
( c3_1(X24)
| ~ c0_1(X24)
| ~ c2_1(X24)
| ~ ndr1_0 )
| hskp27 )
& ( ! [X25] :
( c0_1(X25)
| c1_1(X25)
| ~ c2_1(X25)
| ~ ndr1_0 )
| ! [X26] :
( ~ c0_1(X26)
| ~ c1_1(X26)
| ~ c2_1(X26)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X27] :
( c0_1(X27)
| c1_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( c3_1(X29)
| ~ c1_1(X29)
| ~ c2_1(X29)
| ~ ndr1_0 ) )
& ( ! [X30] :
( c0_1(X30)
| c1_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c1_1(X31)
| c2_1(X31)
| ~ c3_1(X31)
| ~ ndr1_0 )
| ! [X32] :
( c1_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 ) )
& ( ! [X33] :
( c0_1(X33)
| c1_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| ~ c0_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X35] :
( c0_1(X35)
| c1_1(X35)
| ~ c3_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c2_1(X36)
| ~ c0_1(X36)
| ~ c1_1(X36)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X37] :
( c0_1(X37)
| c1_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0 )
| hskp28
| hskp8 )
& ( ! [X38] :
( c0_1(X38)
| c2_1(X38)
| c3_1(X38)
| ~ ndr1_0 )
| ! [X39] :
( ~ c0_1(X39)
| ~ c2_1(X39)
| ~ c3_1(X39)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X40] :
( c0_1(X40)
| c2_1(X40)
| c3_1(X40)
| ~ ndr1_0 )
| hskp29
| hskp7 )
& ( ! [X41] :
( c0_1(X41)
| c2_1(X41)
| c3_1(X41)
| ~ ndr1_0 )
| hskp9
| hskp7 )
& ( ! [X42] :
( c0_1(X42)
| c2_1(X42)
| c3_1(X42)
| ~ ndr1_0 )
| hskp10
| hskp11 )
& ( ! [X43] :
( c0_1(X43)
| c2_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0 )
| ! [X44] :
( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( c2_1(X45)
| ~ c0_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 ) )
& ( ! [X46] :
( c0_1(X46)
| c2_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X48] :
( c0_1(X48)
| c2_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0 )
| ! [X49] :
( c1_1(X49)
| c2_1(X49)
| ~ c0_1(X49)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X50] :
( c0_1(X50)
| c2_1(X50)
| ~ c1_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X52] :
( c0_1(X52)
| c2_1(X52)
| ~ c1_1(X52)
| ~ ndr1_0 )
| hskp28
| hskp3 )
& ( ! [X53] :
( c0_1(X53)
| c2_1(X53)
| ~ c3_1(X53)
| ~ ndr1_0 )
| ! [X54] :
( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X55] :
( c0_1(X55)
| c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0 )
| ! [X57] :
( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57)
| ~ ndr1_0 ) )
& ( ! [X58] :
( c0_1(X58)
| c2_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( c2_1(X59)
| c3_1(X59)
| ~ c1_1(X59)
| ~ ndr1_0 )
| hskp29 )
& ( ! [X60] :
( c0_1(X60)
| c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| ! [X61] :
( c3_1(X61)
| ~ c0_1(X61)
| ~ c2_1(X61)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X62] :
( c0_1(X62)
| c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0 )
| hskp14
| hskp7 )
& ( ! [X63] :
( c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0 )
| hskp10
| hskp15 )
& ( ! [X64] :
( c0_1(X64)
| c3_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 )
| ! [X65] :
( c3_1(X65)
| ~ c1_1(X65)
| ~ c2_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( ~ c0_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 ) )
& ( ! [X67] :
( c0_1(X67)
| c3_1(X67)
| ~ c1_1(X67)
| ~ ndr1_0 )
| ! [X68] :
( ~ c1_1(X68)
| ~ c2_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X69] :
( c0_1(X69)
| c3_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0 )
| ! [X70] :
( c1_1(X70)
| c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0 )
| ! [X71] :
( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 ) )
& ( ! [X72] :
( c0_1(X72)
| c3_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| ! [X73] :
( c2_1(X73)
| c3_1(X73)
| ~ c1_1(X73)
| ~ ndr1_0 )
| ! [X74] :
( c2_1(X74)
| ~ c1_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0 ) )
& ( ! [X75] :
( c0_1(X75)
| ~ c1_1(X75)
| ~ c2_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c1_1(X76)
| c3_1(X76)
| ~ c2_1(X76)
| ~ ndr1_0 )
| ! [X77] :
( c3_1(X77)
| ~ c1_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0 ) )
& ( ! [X78] :
( c0_1(X78)
| ~ c1_1(X78)
| ~ c3_1(X78)
| ~ ndr1_0 )
| hskp17
| hskp0 )
& ( ! [X79] :
( c0_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0 )
| ! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 ) )
& ( ! [X82] :
( c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 )
| hskp29
| hskp7 )
& ( ! [X83] :
( c0_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp0
| hskp18 )
& ( ! [X84] :
( c1_1(X84)
| c2_1(X84)
| c3_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X86] :
( c1_1(X86)
| c2_1(X86)
| c3_1(X86)
| ~ ndr1_0 )
| hskp2
| hskp16 )
& ( ! [X87] :
( c1_1(X87)
| c2_1(X87)
| ~ c0_1(X87)
| ~ ndr1_0 )
| hskp19
| hskp17 )
& ( ! [X88] :
( c1_1(X88)
| c2_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0 )
| ! [X90] :
( c2_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 ) )
& ( ! [X91] :
( c1_1(X91)
| c2_1(X91)
| ~ c3_1(X91)
| ~ ndr1_0 )
| ! [X92] :
( ~ c0_1(X92)
| ~ c2_1(X92)
| ~ c3_1(X92)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X93] :
( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93)
| ~ ndr1_0 )
| hskp30
| hskp20 )
& ( ! [X94] :
( c1_1(X94)
| ~ c0_1(X94)
| ~ c3_1(X94)
| ~ ndr1_0 )
| ! [X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X96] :
( c1_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0 )
| hskp21
| hskp6 )
& ( ! [X97] :
( c1_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97)
| ~ ndr1_0 )
| hskp3
| hskp15 )
& ( ! [X98] :
( c1_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| hskp0
| hskp7 )
& ( ! [X99] :
( c1_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99)
| ~ ndr1_0 )
| ! [X100] :
( c3_1(X100)
| ~ c1_1(X100)
| ~ c2_1(X100)
| ~ ndr1_0 )
| ! [X101] :
( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101)
| ~ ndr1_0 ) )
& ( ! [X102] :
( c1_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0 )
| hskp22
| hskp7 )
& ( ! [X103] :
( c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp8
| hskp23 )
& ( ! [X104] :
( c2_1(X104)
| c3_1(X104)
| ~ c1_1(X104)
| ~ ndr1_0 )
| ! [X105] :
( c3_1(X105)
| ~ c0_1(X105)
| ~ c1_1(X105)
| ~ ndr1_0 )
| hskp9 )
& ( ! [X106] :
( c2_1(X106)
| c3_1(X106)
| ~ c1_1(X106)
| ~ ndr1_0 )
| ! [X107] :
( c3_1(X107)
| ~ c1_1(X107)
| ~ c2_1(X107)
| ~ ndr1_0 )
| ! [X108] :
( ~ c1_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108)
| ~ ndr1_0 ) )
& ( ! [X109] :
( c2_1(X109)
| c3_1(X109)
| ~ c1_1(X109)
| ~ ndr1_0 )
| hskp15
| hskp24 )
& ( ! [X110] :
( c2_1(X110)
| ~ c0_1(X110)
| ~ c1_1(X110)
| ~ ndr1_0 )
| hskp9
| hskp22 )
& ( ! [X111] :
( c2_1(X111)
| ~ c0_1(X111)
| ~ c1_1(X111)
| ~ ndr1_0 )
| hskp10
| hskp18 )
& ( ! [X112] :
( c2_1(X112)
| ~ c0_1(X112)
| ~ c3_1(X112)
| ~ ndr1_0 )
| hskp1
| hskp3 )
& ( ! [X113] :
( c2_1(X113)
| ~ c0_1(X113)
| ~ c3_1(X113)
| ~ ndr1_0 )
| hskp25
| hskp6 )
& ( ! [X114] :
( c2_1(X114)
| ~ c1_1(X114)
| ~ c3_1(X114)
| ~ ndr1_0 )
| hskp17
| hskp13 )
& ( ! [X115] :
( c2_1(X115)
| ~ c1_1(X115)
| ~ c3_1(X115)
| ~ ndr1_0 )
| hskp17
| hskp24 )
& ( ! [X116] :
( c2_1(X116)
| ~ c1_1(X116)
| ~ c3_1(X116)
| ~ ndr1_0 )
| hskp15
| hskp13 )
& ( ! [X117] :
( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117)
| ~ ndr1_0 )
| hskp12
| hskp11 )
& ( ! [X118] :
( c3_1(X118)
| ~ c0_1(X118)
| ~ c1_1(X118)
| ~ ndr1_0 )
| hskp7
| hskp24 )
& ( ! [X119] :
( c3_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119)
| ~ ndr1_0 )
| hskp27
| hskp19 )
& ( ! [X120] :
( c3_1(X120)
| ~ c1_1(X120)
| ~ c2_1(X120)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X121] :
( c3_1(X121)
| ~ c1_1(X121)
| ~ c2_1(X121)
| ~ ndr1_0 )
| hskp14
| hskp23 )
& ( ! [X122] :
( ~ c0_1(X122)
| ~ c1_1(X122)
| ~ c2_1(X122)
| ~ ndr1_0 )
| hskp14
| hskp25 )
& ( ! [X123] :
( ~ c0_1(X123)
| ~ c1_1(X123)
| ~ c3_1(X123)
| ~ ndr1_0 )
| hskp22
| hskp10 )
& ( ! [X124] :
( ~ c0_1(X124)
| ~ c1_1(X124)
| ~ c3_1(X124)
| ~ ndr1_0 )
| hskp2
| hskp19 )
& ( ! [X125] :
( ~ c1_1(X125)
| ~ c2_1(X125)
| ~ c3_1(X125)
| ~ ndr1_0 )
| hskp9
| hskp8 )
& ( ! [X126] :
( ~ c1_1(X126)
| ~ c2_1(X126)
| ~ c3_1(X126)
| ~ ndr1_0 )
| hskp3
| hskp13 )
& ( hskp30
| hskp9
| hskp6 )
& ( hskp27
| hskp3
| hskp15 )
& ( hskp21
| hskp20
| hskp6 )
& ( hskp26
| hskp20
| hskp15 )
& ( hskp12
| hskp19
| hskp13 )
& ( hskp2
| hskp19
| hskp8 ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
( hskp2
| hskp19
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f7,plain,
( hskp12
| hskp19
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f12,plain,
! [X126] :
( ~ c1_1(X126)
| ~ c2_1(X126)
| ~ c3_1(X126)
| ~ ndr1_0
| hskp3
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f13,plain,
! [X125] :
( ~ c1_1(X125)
| ~ c2_1(X125)
| ~ c3_1(X125)
| ~ ndr1_0
| hskp9
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f15,plain,
! [X123] :
( ~ c0_1(X123)
| ~ c1_1(X123)
| ~ c3_1(X123)
| ~ ndr1_0
| hskp22
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f18,plain,
! [X120] :
( c3_1(X120)
| ~ c1_1(X120)
| ~ c2_1(X120)
| ~ ndr1_0
| hskp22 ),
inference(cnf_transformation,[],[f5]) ).
fof(f20,plain,
! [X118] :
( c3_1(X118)
| ~ c0_1(X118)
| ~ c1_1(X118)
| ~ ndr1_0
| hskp7
| hskp24 ),
inference(cnf_transformation,[],[f5]) ).
fof(f21,plain,
! [X117] :
( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117)
| ~ ndr1_0
| hskp12
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f22,plain,
! [X116] :
( c2_1(X116)
| ~ c1_1(X116)
| ~ c3_1(X116)
| ~ ndr1_0
| hskp15
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X115] :
( c2_1(X115)
| ~ c1_1(X115)
| ~ c3_1(X115)
| ~ ndr1_0
| hskp17
| hskp24 ),
inference(cnf_transformation,[],[f5]) ).
fof(f24,plain,
! [X114] :
( c2_1(X114)
| ~ c1_1(X114)
| ~ c3_1(X114)
| ~ ndr1_0
| hskp17
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X111] :
( c2_1(X111)
| ~ c0_1(X111)
| ~ c1_1(X111)
| ~ ndr1_0
| hskp10
| hskp18 ),
inference(cnf_transformation,[],[f5]) ).
fof(f29,plain,
! [X109] :
( c2_1(X109)
| c3_1(X109)
| ~ c1_1(X109)
| ~ ndr1_0
| hskp15
| hskp24 ),
inference(cnf_transformation,[],[f5]) ).
fof(f32,plain,
! [X103] :
( c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0
| hskp8
| hskp23 ),
inference(cnf_transformation,[],[f5]) ).
fof(f33,plain,
! [X102] :
( c1_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0
| hskp22
| hskp7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f34,plain,
! [X101,X99,X100] :
( c1_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99)
| ~ ndr1_0
| c3_1(X100)
| ~ c1_1(X100)
| ~ c2_1(X100)
| ~ ndr1_0
| ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f35,plain,
! [X98] :
( c1_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0
| hskp0
| hskp7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X97] :
( c1_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97)
| ~ ndr1_0
| hskp3
| hskp15 ),
inference(cnf_transformation,[],[f5]) ).
fof(f38,plain,
! [X94,X95] :
( c1_1(X94)
| ~ c0_1(X94)
| ~ c3_1(X94)
| ~ ndr1_0
| c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0
| hskp7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f40,plain,
! [X91,X92] :
( c1_1(X91)
| c2_1(X91)
| ~ c3_1(X91)
| ~ ndr1_0
| ~ c0_1(X92)
| ~ c2_1(X92)
| ~ c3_1(X92)
| ~ ndr1_0
| hskp6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f41,plain,
! [X90,X88,X89] :
( c1_1(X88)
| c2_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0
| c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0
| c2_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f42,plain,
! [X87] :
( c1_1(X87)
| c2_1(X87)
| ~ c0_1(X87)
| ~ ndr1_0
| hskp19
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f44,plain,
! [X84,X85] :
( c1_1(X84)
| c2_1(X84)
| c3_1(X84)
| ~ ndr1_0
| c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85)
| ~ ndr1_0
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f45,plain,
! [X83] :
( c0_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0
| hskp0
| hskp18 ),
inference(cnf_transformation,[],[f5]) ).
fof(f47,plain,
! [X80,X81,X79] :
( c0_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0
| c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0
| ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f49,plain,
! [X76,X77,X75] :
( c0_1(X75)
| ~ c1_1(X75)
| ~ c2_1(X75)
| ~ ndr1_0
| c1_1(X76)
| c3_1(X76)
| ~ c2_1(X76)
| ~ ndr1_0
| c3_1(X77)
| ~ c1_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f50,plain,
! [X72,X73,X74] :
( c0_1(X72)
| c3_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0
| c2_1(X73)
| c3_1(X73)
| ~ c1_1(X73)
| ~ ndr1_0
| c2_1(X74)
| ~ c1_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f54,plain,
! [X63] :
( c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0
| hskp10
| hskp15 ),
inference(cnf_transformation,[],[f5]) ).
fof(f57,plain,
! [X58,X59] :
( c0_1(X58)
| c2_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0
| c2_1(X59)
| c3_1(X59)
| ~ c1_1(X59)
| ~ ndr1_0
| hskp29 ),
inference(cnf_transformation,[],[f5]) ).
fof(f58,plain,
! [X56,X57,X55] :
( c0_1(X55)
| c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0
| c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0
| c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f62,plain,
! [X48,X49] :
( c0_1(X48)
| c2_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0
| c1_1(X49)
| c2_1(X49)
| ~ c0_1(X49)
| ~ ndr1_0
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f63,plain,
! [X46,X47] :
( c0_1(X46)
| c2_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0
| c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47)
| ~ ndr1_0
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f64,plain,
! [X44,X45,X43] :
( c0_1(X43)
| c2_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0
| c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0
| c2_1(X45)
| ~ c0_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f66,plain,
! [X41] :
( c0_1(X41)
| c2_1(X41)
| c3_1(X41)
| ~ ndr1_0
| hskp9
| hskp7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f67,plain,
! [X40] :
( c0_1(X40)
| c2_1(X40)
| c3_1(X40)
| ~ ndr1_0
| hskp29
| hskp7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f68,plain,
! [X38,X39] :
( c0_1(X38)
| c2_1(X38)
| c3_1(X38)
| ~ ndr1_0
| ~ c0_1(X39)
| ~ c2_1(X39)
| ~ c3_1(X39)
| ~ ndr1_0
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f71,plain,
! [X34,X33] :
( c0_1(X33)
| c1_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0
| c1_1(X34)
| ~ c0_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0
| hskp6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f72,plain,
! [X31,X32,X30] :
( c0_1(X30)
| c1_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0
| c1_1(X31)
| c2_1(X31)
| ~ c3_1(X31)
| ~ ndr1_0
| c1_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f73,plain,
! [X28,X29,X27] :
( c0_1(X27)
| c1_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0
| c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0
| c3_1(X29)
| ~ c1_1(X29)
| ~ c2_1(X29)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f74,plain,
! [X26,X25] :
( c0_1(X25)
| c1_1(X25)
| ~ c2_1(X25)
| ~ ndr1_0
| ~ c0_1(X26)
| ~ c1_1(X26)
| ~ c2_1(X26)
| ~ ndr1_0
| hskp5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f77,plain,
! [X18,X19] :
( c0_1(X18)
| c1_1(X18)
| ~ c2_1(X18)
| ~ ndr1_0
| c0_1(X19)
| c2_1(X19)
| ~ c1_1(X19)
| ~ ndr1_0
| hskp4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
! [X3,X4,X5] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0
| c0_1(X4)
| c2_1(X4)
| ~ c1_1(X4)
| ~ ndr1_0
| c0_1(X5)
| c2_1(X5)
| ~ c3_1(X5)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f90,plain,
( ~ hskp29
| c2_1(a136) ),
inference(cnf_transformation,[],[f5]) ).
fof(f91,plain,
( ~ hskp29
| c1_1(a136) ),
inference(cnf_transformation,[],[f5]) ).
fof(f92,plain,
( ~ hskp29
| c0_1(a136) ),
inference(cnf_transformation,[],[f5]) ).
fof(f110,plain,
( ~ hskp24
| ~ c3_1(a182) ),
inference(cnf_transformation,[],[f5]) ).
fof(f111,plain,
( ~ hskp24
| ~ c2_1(a182) ),
inference(cnf_transformation,[],[f5]) ).
fof(f112,plain,
( ~ hskp24
| ~ c0_1(a182) ),
inference(cnf_transformation,[],[f5]) ).
fof(f114,plain,
( ~ hskp23
| ~ c3_1(a179) ),
inference(cnf_transformation,[],[f5]) ).
fof(f115,plain,
( ~ hskp23
| ~ c1_1(a179) ),
inference(cnf_transformation,[],[f5]) ).
fof(f116,plain,
( ~ hskp23
| c2_1(a179) ),
inference(cnf_transformation,[],[f5]) ).
fof(f118,plain,
( ~ hskp22
| ~ c2_1(a176) ),
inference(cnf_transformation,[],[f5]) ).
fof(f119,plain,
( ~ hskp22
| ~ c1_1(a176) ),
inference(cnf_transformation,[],[f5]) ).
fof(f120,plain,
( ~ hskp22
| c0_1(a176) ),
inference(cnf_transformation,[],[f5]) ).
fof(f130,plain,
( ~ hskp19
| ~ c2_1(a164) ),
inference(cnf_transformation,[],[f5]) ).
fof(f131,plain,
( ~ hskp19
| c3_1(a164) ),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
( ~ hskp19
| c1_1(a164) ),
inference(cnf_transformation,[],[f5]) ).
fof(f133,plain,
( ~ hskp19
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
( ~ hskp18
| ~ c2_1(a160) ),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
( ~ hskp18
| ~ c1_1(a160) ),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
( ~ hskp18
| c3_1(a160) ),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
( ~ hskp17
| ~ c2_1(a155) ),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
( ~ hskp17
| ~ c0_1(a155) ),
inference(cnf_transformation,[],[f5]) ).
fof(f140,plain,
( ~ hskp17
| c1_1(a155) ),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
( ~ hskp15
| ~ c0_1(a153) ),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
( ~ hskp15
| c3_1(a153) ),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
( ~ hskp15
| c2_1(a153) ),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
( ~ hskp13
| ~ c1_1(a143) ),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
( ~ hskp13
| c3_1(a143) ),
inference(cnf_transformation,[],[f5]) ).
fof(f156,plain,
( ~ hskp13
| c2_1(a143) ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( ~ hskp12
| ~ c1_1(a142) ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( ~ hskp12
| c3_1(a142) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( ~ hskp12
| c0_1(a142) ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( ~ hskp11
| ~ c3_1(a141) ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( ~ hskp11
| ~ c2_1(a141) ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( ~ hskp11
| ~ c1_1(a141) ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( ~ hskp10
| ~ c3_1(a140) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( ~ hskp10
| ~ c2_1(a140) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( ~ hskp10
| c0_1(a140) ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( ~ hskp9
| ~ c2_1(a138) ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( ~ hskp9
| c1_1(a138) ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( ~ hskp9
| c0_1(a138) ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( ~ hskp8
| ~ c3_1(a134) ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( ~ hskp8
| ~ c0_1(a134) ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( ~ hskp8
| c2_1(a134) ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( ~ hskp8
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( ~ hskp7
| ~ c2_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( ~ hskp7
| ~ c0_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( ~ hskp7
| c3_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( ~ hskp6
| ~ c2_1(a131) ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( ~ hskp6
| ~ c1_1(a131) ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( ~ hskp6
| ~ c0_1(a131) ),
inference(cnf_transformation,[],[f5]) ).
fof(f186,plain,
( ~ hskp5
| ~ c3_1(a130) ),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
( ~ hskp5
| ~ c1_1(a130) ),
inference(cnf_transformation,[],[f5]) ).
fof(f188,plain,
( ~ hskp5
| ~ c0_1(a130) ),
inference(cnf_transformation,[],[f5]) ).
fof(f190,plain,
( ~ hskp4
| ~ c3_1(a128) ),
inference(cnf_transformation,[],[f5]) ).
fof(f191,plain,
( ~ hskp4
| c1_1(a128) ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( ~ hskp4
| c0_1(a128) ),
inference(cnf_transformation,[],[f5]) ).
fof(f194,plain,
( ~ hskp3
| ~ c3_1(a127) ),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
( ~ hskp3
| ~ c2_1(a127) ),
inference(cnf_transformation,[],[f5]) ).
fof(f196,plain,
( ~ hskp3
| c1_1(a127) ),
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
( ~ hskp2
| ~ c0_1(a125) ),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
( ~ hskp2
| c2_1(a125) ),
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
( ~ hskp2
| c1_1(a125) ),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
( ~ hskp2
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
( ~ hskp0
| ~ c1_1(a123) ),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
( ~ hskp0
| ~ c0_1(a123) ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( ~ hskp0
| c2_1(a123) ),
inference(cnf_transformation,[],[f5]) ).
fof(f212,plain,
! [X101,X99,X100] :
( c1_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99)
| ~ ndr1_0
| c3_1(X100)
| ~ c1_1(X100)
| ~ c2_1(X100)
| ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101) ),
inference(duplicate_literal_removal,[],[f34]) ).
fof(f213,plain,
! [X94,X95] :
( c1_1(X94)
| ~ c0_1(X94)
| ~ c3_1(X94)
| ~ ndr1_0
| c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| hskp7 ),
inference(duplicate_literal_removal,[],[f38]) ).
fof(f214,plain,
! [X91,X92] :
( c1_1(X91)
| c2_1(X91)
| ~ c3_1(X91)
| ~ ndr1_0
| ~ c0_1(X92)
| ~ c2_1(X92)
| ~ c3_1(X92)
| hskp6 ),
inference(duplicate_literal_removal,[],[f40]) ).
fof(f215,plain,
! [X90,X88,X89] :
( c1_1(X88)
| c2_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0
| c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89)
| c2_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90) ),
inference(duplicate_literal_removal,[],[f41]) ).
fof(f216,plain,
! [X84,X85] :
( c1_1(X84)
| c2_1(X84)
| c3_1(X84)
| ~ ndr1_0
| c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85)
| hskp12 ),
inference(duplicate_literal_removal,[],[f44]) ).
fof(f217,plain,
! [X80,X81,X79] :
( c0_1(X79)
| ~ c2_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0
| c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80)
| ~ c0_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ),
inference(duplicate_literal_removal,[],[f47]) ).
fof(f218,plain,
! [X76,X77,X75] :
( c0_1(X75)
| ~ c1_1(X75)
| ~ c2_1(X75)
| ~ ndr1_0
| c1_1(X76)
| c3_1(X76)
| ~ c2_1(X76)
| c3_1(X77)
| ~ c1_1(X77)
| ~ c2_1(X77) ),
inference(duplicate_literal_removal,[],[f49]) ).
fof(f219,plain,
! [X72,X73,X74] :
( c0_1(X72)
| c3_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0
| c2_1(X73)
| c3_1(X73)
| ~ c1_1(X73)
| c2_1(X74)
| ~ c1_1(X74)
| ~ c3_1(X74) ),
inference(duplicate_literal_removal,[],[f50]) ).
fof(f224,plain,
! [X58,X59] :
( c0_1(X58)
| c2_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0
| c2_1(X59)
| c3_1(X59)
| ~ c1_1(X59)
| hskp29 ),
inference(duplicate_literal_removal,[],[f57]) ).
fof(f225,plain,
! [X56,X57,X55] :
( c0_1(X55)
| c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0
| c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56)
| c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57) ),
inference(duplicate_literal_removal,[],[f58]) ).
fof(f228,plain,
! [X48,X49] :
( c0_1(X48)
| c2_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0
| c1_1(X49)
| c2_1(X49)
| ~ c0_1(X49)
| hskp13 ),
inference(duplicate_literal_removal,[],[f62]) ).
fof(f229,plain,
! [X46,X47] :
( c0_1(X46)
| c2_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0
| c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47)
| hskp12 ),
inference(duplicate_literal_removal,[],[f63]) ).
fof(f230,plain,
! [X44,X45,X43] :
( c0_1(X43)
| c2_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0
| c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44)
| c2_1(X45)
| ~ c0_1(X45)
| ~ c3_1(X45) ),
inference(duplicate_literal_removal,[],[f64]) ).
fof(f231,plain,
! [X38,X39] :
( c0_1(X38)
| c2_1(X38)
| c3_1(X38)
| ~ ndr1_0
| ~ c0_1(X39)
| ~ c2_1(X39)
| ~ c3_1(X39)
| hskp8 ),
inference(duplicate_literal_removal,[],[f68]) ).
fof(f233,plain,
! [X34,X33] :
( c0_1(X33)
| c1_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0
| c1_1(X34)
| ~ c0_1(X34)
| ~ c3_1(X34)
| hskp6 ),
inference(duplicate_literal_removal,[],[f71]) ).
fof(f234,plain,
! [X31,X32,X30] :
( c0_1(X30)
| c1_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0
| c1_1(X31)
| c2_1(X31)
| ~ c3_1(X31)
| c1_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32) ),
inference(duplicate_literal_removal,[],[f72]) ).
fof(f235,plain,
! [X28,X29,X27] :
( c0_1(X27)
| c1_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0
| c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| c3_1(X29)
| ~ c1_1(X29)
| ~ c2_1(X29) ),
inference(duplicate_literal_removal,[],[f73]) ).
fof(f236,plain,
! [X26,X25] :
( c0_1(X25)
| c1_1(X25)
| ~ c2_1(X25)
| ~ ndr1_0
| ~ c0_1(X26)
| ~ c1_1(X26)
| ~ c2_1(X26)
| hskp5 ),
inference(duplicate_literal_removal,[],[f74]) ).
fof(f239,plain,
! [X18,X19] :
( c0_1(X18)
| c1_1(X18)
| ~ c2_1(X18)
| ~ ndr1_0
| c0_1(X19)
| c2_1(X19)
| ~ c1_1(X19)
| hskp4 ),
inference(duplicate_literal_removal,[],[f77]) ).
fof(f245,plain,
! [X3,X4,X5] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0
| c0_1(X4)
| c2_1(X4)
| ~ c1_1(X4)
| c0_1(X5)
| c2_1(X5)
| ~ c3_1(X5) ),
inference(duplicate_literal_removal,[],[f84]) ).
fof(f248,definition,
( spl0_1
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f251,definition,
( spl0_2
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f254,definition,
( spl0_3
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f256,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f6,f254,f251,f248]) ).
fof(f258,definition,
( spl0_4
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f261,definition,
( spl0_5
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f263,plain,
( spl0_4
| spl0_2
| spl0_5 ),
inference(avatar_split_clause,[],[f7,f261,f251,f258]) ).
fof(f265,definition,
( spl0_6
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f275,definition,
( spl0_9
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f282,definition,
( spl0_11
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f289,definition,
( spl0_13
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f296,definition,
( spl0_15
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f299,definition,
( spl0_16
<=> ! [X126] :
( ~ c1_1(X126)
| ~ c3_1(X126)
| ~ c2_1(X126) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f300,plain,
( ! [X126] :
( ~ c3_1(X126)
| ~ c1_1(X126)
| ~ c2_1(X126) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f301,plain,
( spl0_4
| spl0_11
| ~ spl0_15
| spl0_16 ),
inference(avatar_split_clause,[],[f12,f299,f296,f282,f258]) ).
fof(f302,plain,
( spl0_1
| spl0_13
| ~ spl0_15
| spl0_16 ),
inference(avatar_split_clause,[],[f13,f299,f296,f289,f248]) ).
fof(f304,definition,
( spl0_17
<=> ! [X124] :
( ~ c0_1(X124)
| ~ c3_1(X124)
| ~ c1_1(X124) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f305,plain,
( ! [X124] :
( ~ c0_1(X124)
| ~ c3_1(X124)
| ~ c1_1(X124) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl0_18
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f311,definition,
( spl0_19
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f313,plain,
( spl0_18
| spl0_19
| ~ spl0_15
| spl0_17 ),
inference(avatar_split_clause,[],[f15,f304,f296,f311,f308]) ).
fof(f321,definition,
( spl0_22
<=> ! [X122] :
( ~ c0_1(X122)
| ~ c2_1(X122)
| ~ c1_1(X122) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f322,plain,
( ! [X122] :
( ~ c0_1(X122)
| ~ c2_1(X122)
| ~ c1_1(X122) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f325,definition,
( spl0_23
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f328,definition,
( spl0_24
<=> ! [X121] :
( c3_1(X121)
| ~ c2_1(X121)
| ~ c1_1(X121) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f329,plain,
( ! [X121] :
( c3_1(X121)
| ~ c2_1(X121)
| ~ c1_1(X121) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f331,plain,
( spl0_19
| ~ spl0_15
| spl0_24 ),
inference(avatar_split_clause,[],[f18,f328,f296,f311]) ).
fof(f334,definition,
( spl0_25
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f337,definition,
( spl0_26
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f340,definition,
( spl0_27
<=> ! [X118] :
( c3_1(X118)
| ~ c1_1(X118)
| ~ c0_1(X118) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f341,plain,
( ! [X118] :
( ~ c0_1(X118)
| ~ c1_1(X118)
| c3_1(X118) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f342,plain,
( spl0_25
| spl0_26
| ~ spl0_15
| spl0_27 ),
inference(avatar_split_clause,[],[f20,f340,f296,f337,f334]) ).
fof(f344,definition,
( spl0_28
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f346,plain,
( spl0_28
| spl0_5
| ~ spl0_15
| spl0_27 ),
inference(avatar_split_clause,[],[f21,f340,f296,f261,f344]) ).
fof(f348,definition,
( spl0_29
<=> ! [X116] :
( c2_1(X116)
| ~ c3_1(X116)
| ~ c1_1(X116) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f349,plain,
( ! [X116] :
( ~ c3_1(X116)
| c2_1(X116)
| ~ c1_1(X116) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f350,plain,
( spl0_4
| spl0_6
| ~ spl0_15
| spl0_29 ),
inference(avatar_split_clause,[],[f22,f348,f296,f265,f258]) ).
fof(f352,definition,
( spl0_30
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f354,plain,
( spl0_25
| spl0_30
| ~ spl0_15
| spl0_29 ),
inference(avatar_split_clause,[],[f23,f348,f296,f352,f334]) ).
fof(f355,plain,
( spl0_4
| spl0_30
| ~ spl0_15
| spl0_29 ),
inference(avatar_split_clause,[],[f24,f348,f296,f352,f258]) ).
fof(f357,definition,
( spl0_31
<=> ! [X113] :
( c2_1(X113)
| ~ c3_1(X113)
| ~ c0_1(X113) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f358,plain,
( ! [X113] :
( ~ c0_1(X113)
| ~ c3_1(X113)
| c2_1(X113) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f365,definition,
( spl0_33
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f368,definition,
( spl0_34
<=> ! [X111] :
( c2_1(X111)
| ~ c1_1(X111)
| ~ c0_1(X111) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f369,plain,
( ! [X111] :
( ~ c0_1(X111)
| ~ c1_1(X111)
| c2_1(X111) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f370,plain,
( spl0_33
| spl0_18
| ~ spl0_15
| spl0_34 ),
inference(avatar_split_clause,[],[f27,f368,f296,f308,f365]) ).
fof(f373,definition,
( spl0_35
<=> ! [X109] :
( c2_1(X109)
| ~ c1_1(X109)
| c3_1(X109) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f374,plain,
( ! [X109] :
( c3_1(X109)
| ~ c1_1(X109)
| c2_1(X109) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f375,plain,
( spl0_25
| spl0_6
| ~ spl0_15
| spl0_35 ),
inference(avatar_split_clause,[],[f29,f373,f296,f265,f334]) ).
fof(f379,definition,
( spl0_36
<=> ! [X103] :
( c1_1(X103)
| ~ c3_1(X103)
| ~ c2_1(X103) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f380,plain,
( ! [X103] :
( ~ c3_1(X103)
| c1_1(X103)
| ~ c2_1(X103) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f381,plain,
( spl0_23
| spl0_1
| ~ spl0_15
| spl0_36 ),
inference(avatar_split_clause,[],[f32,f379,f296,f248,f325]) ).
fof(f382,plain,
( spl0_26
| spl0_19
| ~ spl0_15
| spl0_36 ),
inference(avatar_split_clause,[],[f33,f379,f296,f311,f337]) ).
fof(f383,plain,
( spl0_17
| spl0_24
| ~ spl0_15
| spl0_36 ),
inference(avatar_split_clause,[],[f212,f379,f296,f328,f304]) ).
fof(f385,definition,
( spl0_37
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f388,definition,
( spl0_38
<=> ! [X98] :
( c1_1(X98)
| ~ c3_1(X98)
| ~ c0_1(X98) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f389,plain,
( ! [X98] :
( ~ c0_1(X98)
| ~ c3_1(X98)
| c1_1(X98) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f390,plain,
( spl0_26
| spl0_37
| ~ spl0_15
| spl0_38 ),
inference(avatar_split_clause,[],[f35,f388,f296,f385,f337]) ).
fof(f391,plain,
( spl0_6
| spl0_11
| ~ spl0_15
| spl0_38 ),
inference(avatar_split_clause,[],[f36,f388,f296,f282,f265]) ).
fof(f393,plain,
( spl0_26
| spl0_34
| ~ spl0_15
| spl0_38 ),
inference(avatar_split_clause,[],[f213,f388,f296,f368,f337]) ).
fof(f395,definition,
( spl0_39
<=> ! [X93] :
( c1_1(X93)
| ~ c2_1(X93)
| c3_1(X93) ) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f396,plain,
( ! [X93] :
( c3_1(X93)
| ~ c2_1(X93)
| c1_1(X93) )
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f399,definition,
( spl0_40
<=> ! [X92] :
( ~ c0_1(X92)
| ~ c3_1(X92)
| ~ c2_1(X92) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f400,plain,
( ! [X92] :
( ~ c0_1(X92)
| ~ c3_1(X92)
| ~ c2_1(X92) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f402,definition,
( spl0_41
<=> ! [X91] :
( c1_1(X91)
| ~ c3_1(X91)
| c2_1(X91) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f403,plain,
( ! [X91] :
( ~ c3_1(X91)
| c1_1(X91)
| c2_1(X91) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( spl0_9
| spl0_40
| ~ spl0_15
| spl0_41 ),
inference(avatar_split_clause,[],[f214,f402,f296,f399,f275]) ).
fof(f405,plain,
( spl0_31
| spl0_35
| ~ spl0_15
| spl0_41 ),
inference(avatar_split_clause,[],[f215,f402,f296,f373,f357]) ).
fof(f407,definition,
( spl0_42
<=> ! [X87] :
( c1_1(X87)
| ~ c0_1(X87)
| c2_1(X87) ) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f408,plain,
( ! [X87] :
( ~ c0_1(X87)
| c1_1(X87)
| c2_1(X87) )
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f409,plain,
( spl0_30
| spl0_2
| ~ spl0_15
| spl0_42 ),
inference(avatar_split_clause,[],[f42,f407,f296,f251,f352]) ).
fof(f414,definition,
( spl0_44
<=> ! [X86] :
( c1_1(X86)
| c3_1(X86)
| c2_1(X86) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f415,plain,
( ! [X86] :
( c3_1(X86)
| c1_1(X86)
| c2_1(X86) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f417,plain,
( spl0_5
| spl0_27
| ~ spl0_15
| spl0_44 ),
inference(avatar_split_clause,[],[f216,f414,f296,f340,f261]) ).
fof(f419,definition,
( spl0_45
<=> ! [X83] :
( c0_1(X83)
| ~ c3_1(X83)
| ~ c2_1(X83) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f420,plain,
( ! [X83] :
( c0_1(X83)
| ~ c3_1(X83)
| ~ c2_1(X83) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f421,plain,
( spl0_33
| spl0_37
| ~ spl0_15
| spl0_45 ),
inference(avatar_split_clause,[],[f45,f419,f296,f385,f365]) ).
fof(f423,definition,
( spl0_46
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f426,plain,
( spl0_17
| spl0_42
| ~ spl0_15
| spl0_45 ),
inference(avatar_split_clause,[],[f217,f419,f296,f407,f304]) ).
fof(f432,definition,
( spl0_48
<=> ! [X75] :
( c0_1(X75)
| ~ c2_1(X75)
| ~ c1_1(X75) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f433,plain,
( ! [X75] :
( c0_1(X75)
| ~ c2_1(X75)
| ~ c1_1(X75) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f434,plain,
( spl0_24
| spl0_39
| ~ spl0_15
| spl0_48 ),
inference(avatar_split_clause,[],[f218,f432,f296,f395,f328]) ).
fof(f436,definition,
( spl0_49
<=> ! [X72] :
( c0_1(X72)
| ~ c2_1(X72)
| c3_1(X72) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f437,plain,
( ! [X72] :
( c0_1(X72)
| ~ c2_1(X72)
| c3_1(X72) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f438,plain,
( spl0_29
| spl0_35
| ~ spl0_15
| spl0_49 ),
inference(avatar_split_clause,[],[f219,f436,f296,f373,f348]) ).
fof(f446,definition,
( spl0_51
<=> ! [X63] :
( c0_1(X63)
| ~ c3_1(X63)
| c2_1(X63) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f447,plain,
( ! [X63] :
( c0_1(X63)
| ~ c3_1(X63)
| c2_1(X63) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f448,plain,
( spl0_6
| spl0_18
| ~ spl0_15
| spl0_51 ),
inference(avatar_split_clause,[],[f54,f446,f296,f308,f265]) ).
fof(f454,plain,
( spl0_46
| spl0_35
| ~ spl0_15
| spl0_51 ),
inference(avatar_split_clause,[],[f224,f446,f296,f373,f423]) ).
fof(f455,plain,
( spl0_42
| spl0_48
| ~ spl0_15
| spl0_51 ),
inference(avatar_split_clause,[],[f225,f446,f296,f432,f407]) ).
fof(f461,definition,
( spl0_54
<=> ! [X52] :
( c0_1(X52)
| ~ c1_1(X52)
| c2_1(X52) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f462,plain,
( ! [X52] :
( c0_1(X52)
| ~ c1_1(X52)
| c2_1(X52) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f465,plain,
( spl0_4
| spl0_42
| ~ spl0_15
| spl0_54 ),
inference(avatar_split_clause,[],[f228,f461,f296,f407,f258]) ).
fof(f466,plain,
( spl0_5
| spl0_51
| ~ spl0_15
| spl0_54 ),
inference(avatar_split_clause,[],[f229,f461,f296,f446,f261]) ).
fof(f467,plain,
( spl0_31
| spl0_51
| ~ spl0_15
| spl0_54 ),
inference(avatar_split_clause,[],[f230,f461,f296,f446,f357]) ).
fof(f469,definition,
( spl0_55
<=> ! [X42] :
( c0_1(X42)
| c3_1(X42)
| c2_1(X42) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f470,plain,
( ! [X42] :
( c0_1(X42)
| c3_1(X42)
| c2_1(X42) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f469]) ).
fof(f472,plain,
( spl0_26
| spl0_13
| ~ spl0_15
| spl0_55 ),
inference(avatar_split_clause,[],[f66,f469,f296,f289,f337]) ).
fof(f473,plain,
( spl0_26
| spl0_46
| ~ spl0_15
| spl0_55 ),
inference(avatar_split_clause,[],[f67,f469,f296,f423,f337]) ).
fof(f474,plain,
( spl0_1
| spl0_40
| ~ spl0_15
| spl0_55 ),
inference(avatar_split_clause,[],[f231,f469,f296,f399,f248]) ).
fof(f476,definition,
( spl0_56
<=> ! [X37] :
( c0_1(X37)
| ~ c3_1(X37)
| c1_1(X37) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f477,plain,
( ! [X37] :
( c0_1(X37)
| ~ c3_1(X37)
| c1_1(X37) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f480,plain,
( spl0_9
| spl0_38
| ~ spl0_15
| spl0_56 ),
inference(avatar_split_clause,[],[f233,f476,f296,f388,f275]) ).
fof(f481,plain,
( spl0_36
| spl0_41
| ~ spl0_15
| spl0_56 ),
inference(avatar_split_clause,[],[f234,f476,f296,f402,f379]) ).
fof(f482,plain,
( spl0_24
| spl0_54
| ~ spl0_15
| spl0_56 ),
inference(avatar_split_clause,[],[f235,f476,f296,f461,f328]) ).
fof(f484,definition,
( spl0_57
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f487,definition,
( spl0_58
<=> ! [X25] :
( c0_1(X25)
| ~ c2_1(X25)
| c1_1(X25) ) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f488,plain,
( ! [X25] :
( c0_1(X25)
| ~ c2_1(X25)
| c1_1(X25) )
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f489,plain,
( spl0_57
| spl0_22
| ~ spl0_15
| spl0_58 ),
inference(avatar_split_clause,[],[f236,f487,f296,f321,f484]) ).
fof(f496,definition,
( spl0_60
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f498,plain,
( spl0_60
| spl0_54
| ~ spl0_15
| spl0_58 ),
inference(avatar_split_clause,[],[f239,f487,f296,f461,f496]) ).
fof(f504,definition,
( spl0_62
<=> ! [X15] :
( c0_1(X15)
| c2_1(X15)
| c1_1(X15) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f505,plain,
( ! [X15] :
( c0_1(X15)
| c2_1(X15)
| c1_1(X15) )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f504]) ).
fof(f514,plain,
( spl0_51
| spl0_54
| ~ spl0_15
| spl0_62 ),
inference(avatar_split_clause,[],[f245,f504,f296,f461,f446]) ).
fof(f532,definition,
( spl0_67
<=> c2_1(a136) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f535,plain,
( spl0_67
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f90,f423,f532]) ).
fof(f537,definition,
( spl0_68
<=> c1_1(a136) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f539,plain,
( spl0_68
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f91,f423,f537]) ).
fof(f541,definition,
( spl0_69
<=> c0_1(a136) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f542,plain,
( c0_1(a136)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f543,plain,
( spl0_69
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f92,f423,f541]) ).
fof(f602,definition,
( spl0_82
<=> c3_1(a182) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f605,plain,
( ~ spl0_82
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f110,f334,f602]) ).
fof(f607,definition,
( spl0_83
<=> c2_1(a182) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f609,plain,
( ~ spl0_83
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f111,f334,f607]) ).
fof(f611,definition,
( spl0_84
<=> c0_1(a182) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f612,plain,
( ~ c0_1(a182)
| spl0_84 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f613,plain,
( ~ spl0_84
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f112,f334,f611]) ).
fof(f616,definition,
( spl0_85
<=> c3_1(a179) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f617,plain,
( ~ c3_1(a179)
| spl0_85 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f619,plain,
( ~ spl0_85
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f114,f325,f616]) ).
fof(f621,definition,
( spl0_86
<=> c1_1(a179) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f623,plain,
( ~ spl0_86
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f115,f325,f621]) ).
fof(f625,definition,
( spl0_87
<=> c2_1(a179) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f627,plain,
( spl0_87
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f116,f325,f625]) ).
fof(f630,definition,
( spl0_88
<=> c2_1(a176) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f633,plain,
( ~ spl0_88
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f118,f311,f630]) ).
fof(f635,definition,
( spl0_89
<=> c1_1(a176) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f637,plain,
( ~ spl0_89
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f119,f311,f635]) ).
fof(f639,definition,
( spl0_90
<=> c0_1(a176) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f640,plain,
( c0_1(a176)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f641,plain,
( spl0_90
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f120,f311,f639]) ).
fof(f672,definition,
( spl0_97
<=> c2_1(a164) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f675,plain,
( ~ spl0_97
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f130,f251,f672]) ).
fof(f677,definition,
( spl0_98
<=> c3_1(a164) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f678,plain,
( c3_1(a164)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f679,plain,
( spl0_98
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f131,f251,f677]) ).
fof(f681,definition,
( spl0_99
<=> c1_1(a164) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f683,plain,
( spl0_99
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f132,f251,f681]) ).
fof(f684,plain,
( spl0_15
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f133,f251,f296]) ).
fof(f686,definition,
( spl0_100
<=> c2_1(a160) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f689,plain,
( ~ spl0_100
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f134,f365,f686]) ).
fof(f691,definition,
( spl0_101
<=> c1_1(a160) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f693,plain,
( ~ spl0_101
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f135,f365,f691]) ).
fof(f695,definition,
( spl0_102
<=> c3_1(a160) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f696,plain,
( c3_1(a160)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f697,plain,
( spl0_102
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f136,f365,f695]) ).
fof(f700,definition,
( spl0_103
<=> c2_1(a155) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f703,plain,
( ~ spl0_103
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f138,f352,f700]) ).
fof(f705,definition,
( spl0_104
<=> c0_1(a155) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f706,plain,
( ~ c0_1(a155)
| spl0_104 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f707,plain,
( ~ spl0_104
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f139,f352,f705]) ).
fof(f709,definition,
( spl0_105
<=> c1_1(a155) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f711,plain,
( spl0_105
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f140,f352,f709]) ).
fof(f728,definition,
( spl0_109
<=> c0_1(a153) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f729,plain,
( ~ c0_1(a153)
| spl0_109 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f731,plain,
( ~ spl0_109
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f146,f265,f728]) ).
fof(f733,definition,
( spl0_110
<=> c3_1(a153) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f734,plain,
( c3_1(a153)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( spl0_110
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f147,f265,f733]) ).
fof(f737,definition,
( spl0_111
<=> c2_1(a153) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f739,plain,
( spl0_111
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f148,f265,f737]) ).
fof(f756,definition,
( spl0_115
<=> c1_1(a143) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f759,plain,
( ~ spl0_115
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f154,f258,f756]) ).
fof(f761,definition,
( spl0_116
<=> c3_1(a143) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f762,plain,
( c3_1(a143)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f763,plain,
( spl0_116
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f155,f258,f761]) ).
fof(f765,definition,
( spl0_117
<=> c2_1(a143) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f767,plain,
( spl0_117
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f156,f258,f765]) ).
fof(f770,definition,
( spl0_118
<=> c1_1(a142) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f773,plain,
( ~ spl0_118
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f158,f261,f770]) ).
fof(f775,definition,
( spl0_119
<=> c3_1(a142) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f776,plain,
( c3_1(a142)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f777,plain,
( spl0_119
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f159,f261,f775]) ).
fof(f779,definition,
( spl0_120
<=> c0_1(a142) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f780,plain,
( c0_1(a142)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f781,plain,
( spl0_120
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f160,f261,f779]) ).
fof(f784,definition,
( spl0_121
<=> c3_1(a141) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f785,plain,
( ~ c3_1(a141)
| spl0_121 ),
inference(avatar_component_clause,[],[f784]) ).
fof(f787,plain,
( ~ spl0_121
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f162,f344,f784]) ).
fof(f789,definition,
( spl0_122
<=> c2_1(a141) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f791,plain,
( ~ spl0_122
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f163,f344,f789]) ).
fof(f793,definition,
( spl0_123
<=> c1_1(a141) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f795,plain,
( ~ spl0_123
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f164,f344,f793]) ).
fof(f798,definition,
( spl0_124
<=> c3_1(a140) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f799,plain,
( ~ c3_1(a140)
| spl0_124 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f801,plain,
( ~ spl0_124
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f166,f308,f798]) ).
fof(f803,definition,
( spl0_125
<=> c2_1(a140) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f805,plain,
( ~ spl0_125
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f167,f308,f803]) ).
fof(f807,definition,
( spl0_126
<=> c0_1(a140) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f808,plain,
( c0_1(a140)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f809,plain,
( spl0_126
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f168,f308,f807]) ).
fof(f812,definition,
( spl0_127
<=> c2_1(a138) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f815,plain,
( ~ spl0_127
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f170,f289,f812]) ).
fof(f817,definition,
( spl0_128
<=> c1_1(a138) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f819,plain,
( spl0_128
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f171,f289,f817]) ).
fof(f821,definition,
( spl0_129
<=> c0_1(a138) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f822,plain,
( c0_1(a138)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f823,plain,
( spl0_129
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f172,f289,f821]) ).
fof(f826,definition,
( spl0_130
<=> c3_1(a134) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f827,plain,
( ~ c3_1(a134)
| spl0_130 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f829,plain,
( ~ spl0_130
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f174,f248,f826]) ).
fof(f831,definition,
( spl0_131
<=> c0_1(a134) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f832,plain,
( ~ c0_1(a134)
| spl0_131 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f833,plain,
( ~ spl0_131
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f175,f248,f831]) ).
fof(f835,definition,
( spl0_132
<=> c2_1(a134) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f837,plain,
( spl0_132
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f176,f248,f835]) ).
fof(f838,plain,
( spl0_15
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f177,f248,f296]) ).
fof(f840,definition,
( spl0_133
<=> c2_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f843,plain,
( ~ spl0_133
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f178,f337,f840]) ).
fof(f845,definition,
( spl0_134
<=> c0_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f846,plain,
( ~ c0_1(a132)
| spl0_134 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f847,plain,
( ~ spl0_134
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f179,f337,f845]) ).
fof(f849,definition,
( spl0_135
<=> c3_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f850,plain,
( c3_1(a132)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f849]) ).
fof(f851,plain,
( spl0_135
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f180,f337,f849]) ).
fof(f854,definition,
( spl0_136
<=> c2_1(a131) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f857,plain,
( ~ spl0_136
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f182,f275,f854]) ).
fof(f859,definition,
( spl0_137
<=> c1_1(a131) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f861,plain,
( ~ spl0_137
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f183,f275,f859]) ).
fof(f863,definition,
( spl0_138
<=> c0_1(a131) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f864,plain,
( ~ c0_1(a131)
| spl0_138 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f865,plain,
( ~ spl0_138
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f184,f275,f863]) ).
fof(f868,definition,
( spl0_139
<=> c3_1(a130) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f871,plain,
( ~ spl0_139
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f186,f484,f868]) ).
fof(f873,definition,
( spl0_140
<=> c1_1(a130) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f875,plain,
( ~ spl0_140
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f187,f484,f873]) ).
fof(f877,definition,
( spl0_141
<=> c0_1(a130) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f878,plain,
( ~ c0_1(a130)
| spl0_141 ),
inference(avatar_component_clause,[],[f877]) ).
fof(f879,plain,
( ~ spl0_141
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f188,f484,f877]) ).
fof(f882,definition,
( spl0_142
<=> c3_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f883,plain,
( ~ c3_1(a128)
| spl0_142 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f885,plain,
( ~ spl0_142
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f190,f496,f882]) ).
fof(f887,definition,
( spl0_143
<=> c1_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f889,plain,
( spl0_143
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f191,f496,f887]) ).
fof(f891,definition,
( spl0_144
<=> c0_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f892,plain,
( c0_1(a128)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f893,plain,
( spl0_144
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f192,f496,f891]) ).
fof(f896,definition,
( spl0_145
<=> c3_1(a127) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f897,plain,
( ~ c3_1(a127)
| spl0_145 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f899,plain,
( ~ spl0_145
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f194,f282,f896]) ).
fof(f901,definition,
( spl0_146
<=> c2_1(a127) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f903,plain,
( ~ spl0_146
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f195,f282,f901]) ).
fof(f905,definition,
( spl0_147
<=> c1_1(a127) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f907,plain,
( spl0_147
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f196,f282,f905]) ).
fof(f910,definition,
( spl0_148
<=> c0_1(a125) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f911,plain,
( ~ c0_1(a125)
| spl0_148 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f913,plain,
( ~ spl0_148
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f198,f254,f910]) ).
fof(f915,definition,
( spl0_149
<=> c2_1(a125) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f917,plain,
( spl0_149
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f199,f254,f915]) ).
fof(f919,definition,
( spl0_150
<=> c1_1(a125) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f921,plain,
( spl0_150
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f200,f254,f919]) ).
fof(f922,plain,
( spl0_15
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f201,f254,f296]) ).
fof(f938,definition,
( spl0_154
<=> c1_1(a123) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f941,plain,
( ~ spl0_154
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f206,f385,f938]) ).
fof(f943,definition,
( spl0_155
<=> c0_1(a123) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f944,plain,
( ~ c0_1(a123)
| spl0_155 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f945,plain,
( ~ spl0_155
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f207,f385,f943]) ).
fof(f947,definition,
( spl0_156
<=> c2_1(a123) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f949,plain,
( spl0_156
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f208,f385,f947]) ).
fof(f970,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_16
| ~ spl0_24 ),
inference(resolution,[],[f329,f300]) ).
fof(f971,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_16
| ~ spl0_24 ),
inference(duplicate_literal_removal,[],[f970]) ).
fof(f976,plain,
( c2_1(a164)
| ~ c1_1(a164)
| ~ spl0_29
| ~ spl0_98 ),
inference(resolution,[],[f349,f678]) ).
fof(f1001,definition,
( spl0_159
<=> c1_1(a153) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1002,plain,
( c1_1(a153)
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f1001]) ).
fof(f1025,plain,
( ~ c2_1(a179)
| c1_1(a179)
| ~ spl0_39
| spl0_85 ),
inference(resolution,[],[f396,f617]) ).
fof(f1029,plain,
( spl0_86
| ~ spl0_87
| ~ spl0_39
| spl0_85 ),
inference(avatar_split_clause,[],[f1025,f616,f395,f625,f621]) ).
fof(f1063,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_38
| ~ spl0_45 ),
inference(resolution,[],[f420,f389]) ).
fof(f1070,plain,
( ~ c3_1(a153)
| ~ c2_1(a153)
| ~ spl0_45
| spl0_109 ),
inference(resolution,[],[f420,f729]) ).
fof(f1076,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_38
| ~ spl0_45 ),
inference(duplicate_literal_removal,[],[f1063]) ).
fof(f1079,plain,
( spl0_36
| ~ spl0_38
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1076,f419,f388,f379]) ).
fof(f1085,plain,
( ~ c2_1(a136)
| ~ c1_1(a136)
| ~ spl0_22
| ~ spl0_69 ),
inference(resolution,[],[f542,f322]) ).
fof(f1086,plain,
( ~ c3_1(a136)
| ~ c1_1(a136)
| ~ spl0_17
| ~ spl0_69 ),
inference(resolution,[],[f542,f305]) ).
fof(f1089,definition,
( spl0_163
<=> c3_1(a136) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1090,plain,
( ~ c3_1(a136)
| spl0_163 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1091,plain,
( ~ spl0_68
| ~ spl0_163
| ~ spl0_17
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1086,f541,f304,f1089,f537]) ).
fof(f1095,plain,
( ~ spl0_111
| ~ spl0_110
| ~ spl0_45
| spl0_109 ),
inference(avatar_split_clause,[],[f1070,f728,f419,f733,f737]) ).
fof(f1116,plain,
( c1_1(a143)
| ~ c2_1(a143)
| ~ spl0_36
| ~ spl0_116 ),
inference(resolution,[],[f380,f762]) ).
fof(f1117,plain,
( c1_1(a153)
| ~ c2_1(a153)
| ~ spl0_36
| ~ spl0_110 ),
inference(resolution,[],[f380,f734]) ).
fof(f1125,plain,
( ~ spl0_117
| spl0_115
| ~ spl0_36
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1116,f761,f379,f756,f765]) ).
fof(f1126,plain,
( ~ spl0_99
| spl0_97
| ~ spl0_29
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f976,f677,f348,f672,f681]) ).
fof(f1127,plain,
( c1_1(a142)
| ~ c2_1(a142)
| ~ spl0_36
| ~ spl0_119 ),
inference(resolution,[],[f776,f380]) ).
fof(f1130,definition,
( spl0_165
<=> c2_1(a142) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1133,plain,
( ~ spl0_165
| spl0_118
| ~ spl0_36
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1127,f775,f379,f770,f1130]) ).
fof(f1134,plain,
( ~ c3_1(a142)
| c1_1(a142)
| ~ spl0_38
| ~ spl0_120 ),
inference(resolution,[],[f780,f389]) ).
fof(f1136,plain,
( ~ c3_1(a142)
| c2_1(a142)
| ~ spl0_31
| ~ spl0_120 ),
inference(resolution,[],[f780,f358]) ).
fof(f1143,plain,
( spl0_118
| ~ spl0_119
| ~ spl0_38
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1134,f779,f388,f775,f770]) ).
fof(f1145,plain,
( ~ c2_1(a134)
| ~ c1_1(a134)
| ~ spl0_24
| spl0_130 ),
inference(resolution,[],[f827,f329]) ).
fof(f1147,definition,
( spl0_166
<=> c1_1(a134) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1154,plain,
( c2_1(a132)
| ~ c1_1(a132)
| ~ spl0_29
| ~ spl0_135 ),
inference(resolution,[],[f349,f850]) ).
fof(f1167,definition,
( spl0_167
<=> c1_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1170,plain,
( ~ spl0_167
| spl0_133
| ~ spl0_29
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1154,f849,f348,f840,f1167]) ).
fof(f1177,plain,
( c1_1(a142)
| c2_1(a142)
| ~ spl0_41
| ~ spl0_119 ),
inference(resolution,[],[f403,f776]) ).
fof(f1180,plain,
( c1_1(a160)
| c2_1(a160)
| ~ spl0_41
| ~ spl0_102 ),
inference(resolution,[],[f403,f696]) ).
fof(f1187,plain,
( spl0_100
| spl0_101
| ~ spl0_41
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1180,f695,f402,f691,f686]) ).
fof(f1195,plain,
( ~ spl0_111
| spl0_159
| ~ spl0_36
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f1117,f733,f379,f1001,f737]) ).
fof(f1211,plain,
( ~ c2_1(a153)
| ~ spl0_16
| ~ spl0_24
| ~ spl0_159 ),
inference(resolution,[],[f1002,f971]) ).
fof(f1212,plain,
( ~ spl0_111
| ~ spl0_16
| ~ spl0_24
| ~ spl0_159 ),
inference(avatar_split_clause,[],[f1211,f1001,f328,f299,f737]) ).
fof(f1216,plain,
( ~ c1_1(a127)
| c2_1(a127)
| ~ spl0_35
| spl0_145 ),
inference(resolution,[],[f374,f897]) ).
fof(f1228,plain,
( spl0_146
| ~ spl0_147
| ~ spl0_35
| spl0_145 ),
inference(avatar_split_clause,[],[f1216,f896,f373,f905,f901]) ).
fof(f1248,definition,
( spl0_169
<=> c3_1(a155) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1291,plain,
( ~ c3_1(a131)
| c2_1(a131)
| ~ spl0_51
| spl0_138 ),
inference(resolution,[],[f447,f864]) ).
fof(f1292,plain,
( ~ c3_1(a132)
| c2_1(a132)
| ~ spl0_51
| spl0_134 ),
inference(resolution,[],[f447,f846]) ).
fof(f1296,plain,
( ~ c3_1(a155)
| c2_1(a155)
| ~ spl0_51
| spl0_104 ),
inference(resolution,[],[f447,f706]) ).
fof(f1302,plain,
( spl0_103
| ~ spl0_169
| ~ spl0_51
| spl0_104 ),
inference(avatar_split_clause,[],[f1296,f705,f446,f1248,f700]) ).
fof(f1304,plain,
( spl0_133
| ~ spl0_135
| ~ spl0_51
| spl0_134 ),
inference(avatar_split_clause,[],[f1292,f845,f446,f849,f840]) ).
fof(f1307,definition,
( spl0_171
<=> c3_1(a131) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1309,plain,
( spl0_136
| ~ spl0_171
| ~ spl0_51
| spl0_138 ),
inference(avatar_split_clause,[],[f1291,f863,f446,f1307,f854]) ).
fof(f1321,plain,
( ~ c2_1(a136)
| ~ c1_1(a136)
| ~ spl0_24
| spl0_163 ),
inference(resolution,[],[f1090,f329]) ).
fof(f1344,plain,
( ~ c1_1(a132)
| c2_1(a132)
| ~ spl0_54
| spl0_134 ),
inference(resolution,[],[f462,f846]) ).
fof(f1348,plain,
( ~ c1_1(a155)
| c2_1(a155)
| ~ spl0_54
| spl0_104 ),
inference(resolution,[],[f462,f706]) ).
fof(f1356,plain,
( spl0_103
| ~ spl0_105
| ~ spl0_54
| spl0_104 ),
inference(avatar_split_clause,[],[f1348,f705,f461,f709,f700]) ).
fof(f1358,plain,
( spl0_133
| ~ spl0_167
| ~ spl0_54
| spl0_134 ),
inference(avatar_split_clause,[],[f1344,f845,f461,f1167,f840]) ).
fof(f1361,plain,
( c1_1(a142)
| c2_1(a142)
| ~ spl0_42
| ~ spl0_120 ),
inference(resolution,[],[f408,f780]) ).
fof(f1363,plain,
( c1_1(a176)
| c2_1(a176)
| ~ spl0_42
| ~ spl0_90 ),
inference(resolution,[],[f408,f640]) ).
fof(f1372,plain,
( spl0_165
| spl0_118
| ~ spl0_42
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1361,f779,f407,f770,f1130]) ).
fof(f1373,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c2_1(X0) )
| ~ spl0_42
| ~ spl0_55 ),
inference(resolution,[],[f470,f408]) ).
fof(f1389,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c1_1(X0) )
| ~ spl0_42
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f1373]) ).
fof(f1397,plain,
( spl0_44
| ~ spl0_42
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1389,f469,f407,f414]) ).
fof(f1402,definition,
( spl0_173
<=> c1_1(a140) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1407,plain,
( ~ c1_1(a140)
| c3_1(a140)
| ~ spl0_27
| ~ spl0_126 ),
inference(resolution,[],[f808,f341]) ).
fof(f1411,plain,
( spl0_124
| ~ spl0_173
| ~ spl0_27
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1407,f807,f340,f1402,f798]) ).
fof(f1422,plain,
( ~ c1_1(a138)
| c3_1(a138)
| ~ spl0_27
| ~ spl0_129 ),
inference(resolution,[],[f822,f341]) ).
fof(f1424,plain,
( ~ c3_1(a138)
| ~ c1_1(a138)
| ~ spl0_17
| ~ spl0_129 ),
inference(resolution,[],[f822,f305]) ).
fof(f1427,definition,
( spl0_174
<=> c3_1(a138) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f1429,plain,
( ~ spl0_128
| ~ spl0_174
| ~ spl0_17
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1424,f821,f304,f1427,f817]) ).
fof(f1431,plain,
( spl0_174
| ~ spl0_128
| ~ spl0_27
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1422,f821,f340,f817,f1427]) ).
fof(f1442,plain,
( ~ c1_1(a138)
| c2_1(a138)
| ~ spl0_34
| ~ spl0_129 ),
inference(resolution,[],[f369,f822]) ).
fof(f1449,plain,
( spl0_127
| ~ spl0_128
| ~ spl0_34
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1442,f821,f368,f817,f812]) ).
fof(f1451,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c1_1(X0)
| c2_1(X0) )
| ~ spl0_42
| ~ spl0_56 ),
inference(resolution,[],[f477,f408]) ).
fof(f1456,plain,
( ~ c3_1(a131)
| c1_1(a131)
| ~ spl0_56
| spl0_138 ),
inference(resolution,[],[f477,f864]) ).
fof(f1457,plain,
( ~ c3_1(a132)
| c1_1(a132)
| ~ spl0_56
| spl0_134 ),
inference(resolution,[],[f477,f846]) ).
fof(f1459,plain,
( ~ c3_1(a153)
| c1_1(a153)
| ~ spl0_56
| spl0_109 ),
inference(resolution,[],[f477,f729]) ).
fof(f1465,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c2_1(X0) )
| ~ spl0_42
| ~ spl0_56 ),
inference(duplicate_literal_removal,[],[f1451]) ).
fof(f1469,plain,
( spl0_167
| ~ spl0_135
| ~ spl0_56
| spl0_134 ),
inference(avatar_split_clause,[],[f1457,f845,f476,f849,f1167]) ).
fof(f1472,plain,
( spl0_41
| ~ spl0_42
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f1465,f476,f407,f402]) ).
fof(f1473,plain,
( spl0_165
| ~ spl0_119
| ~ spl0_31
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1136,f779,f357,f775,f1130]) ).
fof(f1475,plain,
( spl0_165
| spl0_118
| ~ spl0_41
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1177,f775,f402,f770,f1130]) ).
fof(f1488,plain,
( c1_1(a132)
| c2_1(a132)
| ~ spl0_41
| ~ spl0_135 ),
inference(resolution,[],[f403,f850]) ).
fof(f1495,plain,
( spl0_133
| spl0_167
| ~ spl0_41
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1488,f849,f402,f1167,f840]) ).
fof(f1503,plain,
( ~ c2_1(a123)
| c1_1(a123)
| ~ spl0_58
| spl0_155 ),
inference(resolution,[],[f488,f944]) ).
fof(f1507,plain,
( ~ c2_1(a134)
| c1_1(a134)
| ~ spl0_58
| spl0_131 ),
inference(resolution,[],[f488,f832]) ).
fof(f1517,plain,
( spl0_166
| ~ spl0_132
| ~ spl0_58
| spl0_131 ),
inference(avatar_split_clause,[],[f1507,f831,f487,f835,f1147]) ).
fof(f1520,plain,
( spl0_154
| ~ spl0_156
| ~ spl0_58
| spl0_155 ),
inference(avatar_split_clause,[],[f1503,f943,f487,f947,f938]) ).
fof(f1523,plain,
( ~ c1_1(a128)
| c2_1(a128)
| ~ spl0_35
| spl0_142 ),
inference(resolution,[],[f883,f374]) ).
fof(f1526,definition,
( spl0_175
<=> c2_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1529,plain,
( spl0_175
| ~ spl0_143
| ~ spl0_35
| spl0_142 ),
inference(avatar_split_clause,[],[f1523,f882,f373,f887,f1526]) ).
fof(f1532,plain,
( ~ c1_1(a128)
| c2_1(a128)
| ~ spl0_34
| ~ spl0_144 ),
inference(resolution,[],[f892,f369]) ).
fof(f1534,plain,
( ~ c1_1(a128)
| c3_1(a128)
| ~ spl0_27
| ~ spl0_144 ),
inference(resolution,[],[f892,f341]) ).
fof(f1538,plain,
( spl0_142
| ~ spl0_143
| ~ spl0_27
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1534,f891,f340,f887,f882]) ).
fof(f1539,plain,
( spl0_175
| ~ spl0_143
| ~ spl0_34
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1532,f891,f368,f887,f1526]) ).
fof(f1551,plain,
( ~ c3_1(a142)
| ~ c2_1(a142)
| ~ spl0_40
| ~ spl0_120 ),
inference(resolution,[],[f400,f780]) ).
fof(f1555,plain,
( ~ spl0_165
| ~ spl0_119
| ~ spl0_40
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1551,f779,f399,f775,f1130]) ).
fof(f1589,plain,
( c3_1(a131)
| c2_1(a131)
| ~ spl0_55
| spl0_138 ),
inference(resolution,[],[f470,f864]) ).
fof(f1593,plain,
( c3_1(a155)
| c2_1(a155)
| ~ spl0_55
| spl0_104 ),
inference(resolution,[],[f470,f706]) ).
fof(f1595,plain,
( c3_1(a182)
| c2_1(a182)
| ~ spl0_55
| spl0_84 ),
inference(resolution,[],[f470,f612]) ).
fof(f1599,plain,
( spl0_83
| spl0_82
| ~ spl0_55
| spl0_84 ),
inference(avatar_split_clause,[],[f1595,f611,f469,f602,f607]) ).
fof(f1600,plain,
( spl0_103
| spl0_169
| ~ spl0_55
| spl0_104 ),
inference(avatar_split_clause,[],[f1593,f705,f469,f1248,f700]) ).
fof(f1601,plain,
( spl0_136
| spl0_171
| ~ spl0_55
| spl0_138 ),
inference(avatar_split_clause,[],[f1589,f863,f469,f1307,f854]) ).
fof(f1609,plain,
( c2_1(a131)
| c1_1(a131)
| ~ spl0_62
| spl0_138 ),
inference(resolution,[],[f505,f864]) ).
fof(f1619,plain,
( spl0_137
| spl0_136
| ~ spl0_62
| spl0_138 ),
inference(avatar_split_clause,[],[f1609,f863,f504,f854,f859]) ).
fof(f1621,plain,
( spl0_137
| ~ spl0_171
| ~ spl0_56
| spl0_138 ),
inference(avatar_split_clause,[],[f1456,f863,f476,f1307,f859]) ).
fof(f1622,plain,
( spl0_159
| ~ spl0_110
| ~ spl0_56
| spl0_109 ),
inference(avatar_split_clause,[],[f1459,f728,f476,f733,f1001]) ).
fof(f1623,plain,
( ~ spl0_68
| ~ spl0_67
| ~ spl0_22
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1085,f541,f321,f532,f537]) ).
fof(f1638,plain,
( ~ spl0_68
| ~ spl0_67
| ~ spl0_24
| spl0_163 ),
inference(avatar_split_clause,[],[f1321,f1089,f328,f532,f537]) ).
fof(f1649,plain,
( ~ c1_1(a140)
| c2_1(a140)
| ~ spl0_35
| spl0_124 ),
inference(resolution,[],[f799,f374]) ).
fof(f1650,plain,
( spl0_125
| ~ spl0_173
| ~ spl0_35
| spl0_124 ),
inference(avatar_split_clause,[],[f1649,f798,f373,f1402,f803]) ).
fof(f1655,definition,
( spl0_176
<=> c2_1(a130) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f1658,plain,
( c2_1(a130)
| c1_1(a130)
| ~ spl0_62
| spl0_141 ),
inference(resolution,[],[f878,f505]) ).
fof(f1663,plain,
( spl0_140
| spl0_176
| ~ spl0_62
| spl0_141 ),
inference(avatar_split_clause,[],[f1658,f877,f504,f1655,f873]) ).
fof(f1667,plain,
( ~ c2_1(a125)
| ~ c1_1(a125)
| ~ spl0_48
| spl0_148 ),
inference(resolution,[],[f433,f911]) ).
fof(f1671,plain,
( ~ c2_1(a134)
| ~ c1_1(a134)
| ~ spl0_48
| spl0_131 ),
inference(resolution,[],[f433,f832]) ).
fof(f1672,plain,
( ~ c2_1(a153)
| ~ c1_1(a153)
| ~ spl0_48
| spl0_109 ),
inference(resolution,[],[f433,f729]) ).
fof(f1679,plain,
( ~ spl0_159
| ~ spl0_111
| ~ spl0_48
| spl0_109 ),
inference(avatar_split_clause,[],[f1672,f728,f432,f737,f1001]) ).
fof(f1680,plain,
( ~ spl0_166
| ~ spl0_132
| ~ spl0_48
| spl0_131 ),
inference(avatar_split_clause,[],[f1671,f831,f432,f835,f1147]) ).
fof(f1681,plain,
( ~ spl0_150
| ~ spl0_149
| ~ spl0_48
| spl0_148 ),
inference(avatar_split_clause,[],[f1667,f910,f432,f915,f919]) ).
fof(f1684,plain,
( ~ spl0_166
| ~ spl0_132
| ~ spl0_24
| spl0_130 ),
inference(avatar_split_clause,[],[f1145,f826,f328,f835,f1147]) ).
fof(f1688,plain,
( spl0_88
| spl0_89
| ~ spl0_42
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1363,f639,f407,f635,f630]) ).
fof(f1708,plain,
( ~ c2_1(a128)
| ~ c1_1(a128)
| ~ spl0_24
| spl0_142 ),
inference(resolution,[],[f329,f883]) ).
fof(f1715,plain,
( ~ spl0_143
| ~ spl0_175
| ~ spl0_24
| spl0_142 ),
inference(avatar_split_clause,[],[f1708,f882,f328,f1526,f887]) ).
fof(f1722,plain,
( c1_1(a140)
| c2_1(a140)
| ~ spl0_42
| ~ spl0_126 ),
inference(resolution,[],[f408,f808]) ).
fof(f1733,plain,
( spl0_125
| spl0_173
| ~ spl0_42
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1722,f807,f407,f1402,f803]) ).
fof(f1739,plain,
( c1_1(a140)
| c2_1(a140)
| ~ spl0_44
| spl0_124 ),
inference(resolution,[],[f415,f799]) ).
fof(f1740,plain,
( c1_1(a141)
| c2_1(a141)
| ~ spl0_44
| spl0_121 ),
inference(resolution,[],[f415,f785]) ).
fof(f1747,plain,
( spl0_122
| spl0_123
| ~ spl0_44
| spl0_121 ),
inference(avatar_split_clause,[],[f1740,f784,f414,f793,f789]) ).
fof(f1748,plain,
( spl0_125
| spl0_173
| ~ spl0_44
| spl0_124 ),
inference(avatar_split_clause,[],[f1739,f798,f414,f1402,f803]) ).
fof(f1754,plain,
( ~ c2_1(a130)
| c3_1(a130)
| ~ spl0_49
| spl0_141 ),
inference(resolution,[],[f437,f878]) ).
fof(f1757,plain,
( ~ c2_1(a134)
| c3_1(a134)
| ~ spl0_49
| spl0_131 ),
inference(resolution,[],[f437,f832]) ).
fof(f1764,plain,
( spl0_130
| ~ spl0_132
| ~ spl0_49
| spl0_131 ),
inference(avatar_split_clause,[],[f1757,f831,f436,f835,f826]) ).
fof(f1766,plain,
( spl0_139
| ~ spl0_176
| ~ spl0_49
| spl0_141 ),
inference(avatar_split_clause,[],[f1754,f877,f436,f1655,f868]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f256]) ).
cnf(s2,plain,
( spl0_2
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f263]) ).
cnf(s7,plain,
( spl0_4
| spl0_11
| ~ spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f301]) ).
cnf(s8,plain,
( spl0_1
| spl0_13
| ~ spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f302]) ).
cnf(s10,plain,
( ~ spl0_15
| spl0_17
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f313]) ).
cnf(s13,plain,
( ~ spl0_15
| spl0_19
| spl0_24 ),
inference(sat_conversion,[],[f331]) ).
cnf(s15,plain,
( ~ spl0_15
| spl0_25
| spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f342]) ).
cnf(s16,plain,
( spl0_5
| ~ spl0_15
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f346]) ).
cnf(s17,plain,
( spl0_4
| spl0_6
| ~ spl0_15
| spl0_29 ),
inference(sat_conversion,[],[f350]) ).
cnf(s18,plain,
( ~ spl0_15
| spl0_25
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f354]) ).
cnf(s19,plain,
( spl0_4
| ~ spl0_15
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f355]) ).
cnf(s22,plain,
( ~ spl0_15
| spl0_18
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f370]) ).
cnf(s24,plain,
( spl0_6
| ~ spl0_15
| spl0_25
| spl0_35 ),
inference(sat_conversion,[],[f375]) ).
cnf(s27,plain,
( spl0_1
| ~ spl0_15
| spl0_23
| spl0_36 ),
inference(sat_conversion,[],[f381]) ).
cnf(s28,plain,
( ~ spl0_15
| spl0_19
| spl0_26
| spl0_36 ),
inference(sat_conversion,[],[f382]) ).
cnf(s29,plain,
( ~ spl0_15
| spl0_17
| spl0_24
| spl0_36 ),
inference(sat_conversion,[],[f383]) ).
cnf(s30,plain,
( ~ spl0_15
| spl0_26
| spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f390]) ).
cnf(s31,plain,
( spl0_6
| spl0_11
| ~ spl0_15
| spl0_38 ),
inference(sat_conversion,[],[f391]) ).
cnf(s33,plain,
( ~ spl0_15
| spl0_26
| spl0_34
| spl0_38 ),
inference(sat_conversion,[],[f393]) ).
cnf(s35,plain,
( spl0_9
| ~ spl0_15
| spl0_40
| spl0_41 ),
inference(sat_conversion,[],[f404]) ).
cnf(s36,plain,
( ~ spl0_15
| spl0_31
| spl0_35
| spl0_41 ),
inference(sat_conversion,[],[f405]) ).
cnf(s37,plain,
( spl0_2
| ~ spl0_15
| spl0_30
| spl0_42 ),
inference(sat_conversion,[],[f409]) ).
cnf(s39,plain,
( spl0_5
| ~ spl0_15
| spl0_27
| spl0_44 ),
inference(sat_conversion,[],[f417]) ).
cnf(s40,plain,
( ~ spl0_15
| spl0_33
| spl0_37
| spl0_45 ),
inference(sat_conversion,[],[f421]) ).
cnf(s42,plain,
( ~ spl0_15
| spl0_17
| spl0_42
| spl0_45 ),
inference(sat_conversion,[],[f426]) ).
cnf(s44,plain,
( ~ spl0_15
| spl0_24
| spl0_39
| spl0_48 ),
inference(sat_conversion,[],[f434]) ).
cnf(s45,plain,
( ~ spl0_15
| spl0_29
| spl0_35
| spl0_49 ),
inference(sat_conversion,[],[f438]) ).
cnf(s49,plain,
( spl0_6
| ~ spl0_15
| spl0_18
| spl0_51 ),
inference(sat_conversion,[],[f448]) ).
cnf(s52,plain,
( ~ spl0_15
| spl0_35
| spl0_46
| spl0_51 ),
inference(sat_conversion,[],[f454]) ).
cnf(s53,plain,
( ~ spl0_15
| spl0_42
| spl0_48
| spl0_51 ),
inference(sat_conversion,[],[f455]) ).
cnf(s57,plain,
( spl0_4
| ~ spl0_15
| spl0_42
| spl0_54 ),
inference(sat_conversion,[],[f465]) ).
cnf(s58,plain,
( spl0_5
| ~ spl0_15
| spl0_51
| spl0_54 ),
inference(sat_conversion,[],[f466]) ).
cnf(s59,plain,
( ~ spl0_15
| spl0_31
| spl0_51
| spl0_54 ),
inference(sat_conversion,[],[f467]) ).
cnf(s61,plain,
( spl0_13
| ~ spl0_15
| spl0_26
| spl0_55 ),
inference(sat_conversion,[],[f472]) ).
cnf(s62,plain,
( ~ spl0_15
| spl0_26
| spl0_46
| spl0_55 ),
inference(sat_conversion,[],[f473]) ).
cnf(s63,plain,
( spl0_1
| ~ spl0_15
| spl0_40
| spl0_55 ),
inference(sat_conversion,[],[f474]) ).
cnf(s66,plain,
( spl0_9
| ~ spl0_15
| spl0_38
| spl0_56 ),
inference(sat_conversion,[],[f480]) ).
cnf(s67,plain,
( ~ spl0_15
| spl0_36
| spl0_41
| spl0_56 ),
inference(sat_conversion,[],[f481]) ).
cnf(s68,plain,
( ~ spl0_15
| spl0_24
| spl0_54
| spl0_56 ),
inference(sat_conversion,[],[f482]) ).
cnf(s69,plain,
( ~ spl0_15
| spl0_22
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f489]) ).
cnf(s72,plain,
( ~ spl0_15
| spl0_54
| spl0_58
| spl0_60 ),
inference(sat_conversion,[],[f498]) ).
cnf(s79,plain,
( ~ spl0_15
| spl0_51
| spl0_54
| spl0_62 ),
inference(sat_conversion,[],[f514]) ).
cnf(s85,plain,
( ~ spl0_46
| spl0_67 ),
inference(sat_conversion,[],[f535]) ).
cnf(s86,plain,
( ~ spl0_46
| spl0_68 ),
inference(sat_conversion,[],[f539]) ).
cnf(s87,plain,
( ~ spl0_46
| spl0_69 ),
inference(sat_conversion,[],[f543]) ).
cnf(s105,plain,
( ~ spl0_25
| ~ spl0_82 ),
inference(sat_conversion,[],[f605]) ).
cnf(s106,plain,
( ~ spl0_25
| ~ spl0_83 ),
inference(sat_conversion,[],[f609]) ).
cnf(s107,plain,
( ~ spl0_25
| ~ spl0_84 ),
inference(sat_conversion,[],[f613]) ).
cnf(s109,plain,
( ~ spl0_23
| ~ spl0_85 ),
inference(sat_conversion,[],[f619]) ).
cnf(s110,plain,
( ~ spl0_23
| ~ spl0_86 ),
inference(sat_conversion,[],[f623]) ).
cnf(s111,plain,
( ~ spl0_23
| spl0_87 ),
inference(sat_conversion,[],[f627]) ).
cnf(s113,plain,
( ~ spl0_19
| ~ spl0_88 ),
inference(sat_conversion,[],[f633]) ).
cnf(s114,plain,
( ~ spl0_19
| ~ spl0_89 ),
inference(sat_conversion,[],[f637]) ).
cnf(s115,plain,
( ~ spl0_19
| spl0_90 ),
inference(sat_conversion,[],[f641]) ).
cnf(s125,plain,
( ~ spl0_2
| ~ spl0_97 ),
inference(sat_conversion,[],[f675]) ).
cnf(s126,plain,
( ~ spl0_2
| spl0_98 ),
inference(sat_conversion,[],[f679]) ).
cnf(s127,plain,
( ~ spl0_2
| spl0_99 ),
inference(sat_conversion,[],[f683]) ).
cnf(s128,plain,
( ~ spl0_2
| spl0_15 ),
inference(sat_conversion,[],[f684]) ).
cnf(s129,plain,
( ~ spl0_33
| ~ spl0_100 ),
inference(sat_conversion,[],[f689]) ).
cnf(s130,plain,
( ~ spl0_33
| ~ spl0_101 ),
inference(sat_conversion,[],[f693]) ).
cnf(s131,plain,
( ~ spl0_33
| spl0_102 ),
inference(sat_conversion,[],[f697]) ).
cnf(s133,plain,
( ~ spl0_30
| ~ spl0_103 ),
inference(sat_conversion,[],[f703]) ).
cnf(s134,plain,
( ~ spl0_30
| ~ spl0_104 ),
inference(sat_conversion,[],[f707]) ).
cnf(s135,plain,
( ~ spl0_30
| spl0_105 ),
inference(sat_conversion,[],[f711]) ).
cnf(s141,plain,
( ~ spl0_6
| ~ spl0_109 ),
inference(sat_conversion,[],[f731]) ).
cnf(s142,plain,
( ~ spl0_6
| spl0_110 ),
inference(sat_conversion,[],[f735]) ).
cnf(s143,plain,
( ~ spl0_6
| spl0_111 ),
inference(sat_conversion,[],[f739]) ).
cnf(s149,plain,
( ~ spl0_4
| ~ spl0_115 ),
inference(sat_conversion,[],[f759]) ).
cnf(s150,plain,
( ~ spl0_4
| spl0_116 ),
inference(sat_conversion,[],[f763]) ).
cnf(s151,plain,
( ~ spl0_4
| spl0_117 ),
inference(sat_conversion,[],[f767]) ).
cnf(s153,plain,
( ~ spl0_5
| ~ spl0_118 ),
inference(sat_conversion,[],[f773]) ).
cnf(s154,plain,
( ~ spl0_5
| spl0_119 ),
inference(sat_conversion,[],[f777]) ).
cnf(s155,plain,
( ~ spl0_5
| spl0_120 ),
inference(sat_conversion,[],[f781]) ).
cnf(s157,plain,
( ~ spl0_28
| ~ spl0_121 ),
inference(sat_conversion,[],[f787]) ).
cnf(s158,plain,
( ~ spl0_28
| ~ spl0_122 ),
inference(sat_conversion,[],[f791]) ).
cnf(s159,plain,
( ~ spl0_28
| ~ spl0_123 ),
inference(sat_conversion,[],[f795]) ).
cnf(s161,plain,
( ~ spl0_18
| ~ spl0_124 ),
inference(sat_conversion,[],[f801]) ).
cnf(s162,plain,
( ~ spl0_18
| ~ spl0_125 ),
inference(sat_conversion,[],[f805]) ).
cnf(s163,plain,
( ~ spl0_18
| spl0_126 ),
inference(sat_conversion,[],[f809]) ).
cnf(s165,plain,
( ~ spl0_13
| ~ spl0_127 ),
inference(sat_conversion,[],[f815]) ).
cnf(s166,plain,
( ~ spl0_13
| spl0_128 ),
inference(sat_conversion,[],[f819]) ).
cnf(s167,plain,
( ~ spl0_13
| spl0_129 ),
inference(sat_conversion,[],[f823]) ).
cnf(s169,plain,
( ~ spl0_1
| ~ spl0_130 ),
inference(sat_conversion,[],[f829]) ).
cnf(s170,plain,
( ~ spl0_1
| ~ spl0_131 ),
inference(sat_conversion,[],[f833]) ).
cnf(s171,plain,
( ~ spl0_1
| spl0_132 ),
inference(sat_conversion,[],[f837]) ).
cnf(s172,plain,
( ~ spl0_1
| spl0_15 ),
inference(sat_conversion,[],[f838]) ).
cnf(s173,plain,
( ~ spl0_26
| ~ spl0_133 ),
inference(sat_conversion,[],[f843]) ).
cnf(s174,plain,
( ~ spl0_26
| ~ spl0_134 ),
inference(sat_conversion,[],[f847]) ).
cnf(s175,plain,
( ~ spl0_26
| spl0_135 ),
inference(sat_conversion,[],[f851]) ).
cnf(s177,plain,
( ~ spl0_9
| ~ spl0_136 ),
inference(sat_conversion,[],[f857]) ).
cnf(s178,plain,
( ~ spl0_9
| ~ spl0_137 ),
inference(sat_conversion,[],[f861]) ).
cnf(s179,plain,
( ~ spl0_9
| ~ spl0_138 ),
inference(sat_conversion,[],[f865]) ).
cnf(s181,plain,
( ~ spl0_57
| ~ spl0_139 ),
inference(sat_conversion,[],[f871]) ).
cnf(s182,plain,
( ~ spl0_57
| ~ spl0_140 ),
inference(sat_conversion,[],[f875]) ).
cnf(s183,plain,
( ~ spl0_57
| ~ spl0_141 ),
inference(sat_conversion,[],[f879]) ).
cnf(s185,plain,
( ~ spl0_60
| ~ spl0_142 ),
inference(sat_conversion,[],[f885]) ).
cnf(s186,plain,
( ~ spl0_60
| spl0_143 ),
inference(sat_conversion,[],[f889]) ).
cnf(s187,plain,
( ~ spl0_60
| spl0_144 ),
inference(sat_conversion,[],[f893]) ).
cnf(s189,plain,
( ~ spl0_11
| ~ spl0_145 ),
inference(sat_conversion,[],[f899]) ).
cnf(s190,plain,
( ~ spl0_11
| ~ spl0_146 ),
inference(sat_conversion,[],[f903]) ).
cnf(s191,plain,
( ~ spl0_11
| spl0_147 ),
inference(sat_conversion,[],[f907]) ).
cnf(s193,plain,
( ~ spl0_3
| ~ spl0_148 ),
inference(sat_conversion,[],[f913]) ).
cnf(s194,plain,
( ~ spl0_3
| spl0_149 ),
inference(sat_conversion,[],[f917]) ).
cnf(s195,plain,
( ~ spl0_3
| spl0_150 ),
inference(sat_conversion,[],[f921]) ).
cnf(s196,plain,
( ~ spl0_3
| spl0_15 ),
inference(sat_conversion,[],[f922]) ).
cnf(s201,plain,
( ~ spl0_37
| ~ spl0_154 ),
inference(sat_conversion,[],[f941]) ).
cnf(s202,plain,
( ~ spl0_37
| ~ spl0_155 ),
inference(sat_conversion,[],[f945]) ).
cnf(s203,plain,
( ~ spl0_37
| spl0_156 ),
inference(sat_conversion,[],[f949]) ).
cnf(s215,plain,
( ~ spl0_39
| spl0_85
| spl0_86
| ~ spl0_87 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s222,plain,
( spl0_36
| ~ spl0_38
| ~ spl0_45 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s223,plain,
( ~ spl0_17
| ~ spl0_68
| ~ spl0_69
| ~ spl0_163 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s227,plain,
( ~ spl0_45
| spl0_109
| ~ spl0_110
| ~ spl0_111 ),
inference(sat_conversion,[],[f1095]) ).
cnf(s232,plain,
( ~ spl0_36
| spl0_115
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s233,plain,
( ~ spl0_29
| spl0_97
| ~ spl0_98
| ~ spl0_99 ),
inference(sat_conversion,[],[f1126]) ).
cnf(s234,plain,
( ~ spl0_36
| spl0_118
| ~ spl0_119
| ~ spl0_165 ),
inference(sat_conversion,[],[f1133]) ).
cnf(s236,plain,
( ~ spl0_38
| spl0_118
| ~ spl0_119
| ~ spl0_120 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s240,plain,
( ~ spl0_29
| spl0_133
| ~ spl0_135
| ~ spl0_167 ),
inference(sat_conversion,[],[f1170]) ).
cnf(s243,plain,
( ~ spl0_41
| spl0_100
| spl0_101
| ~ spl0_102 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s250,plain,
( ~ spl0_36
| ~ spl0_110
| ~ spl0_111
| spl0_159 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s254,plain,
( ~ spl0_16
| ~ spl0_24
| ~ spl0_111
| ~ spl0_159 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s257,plain,
( ~ spl0_35
| spl0_145
| spl0_146
| ~ spl0_147 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s267,plain,
( ~ spl0_51
| spl0_103
| spl0_104
| ~ spl0_169 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s269,plain,
( ~ spl0_51
| spl0_133
| spl0_134
| ~ spl0_135 ),
inference(sat_conversion,[],[f1304]) ).
cnf(s270,plain,
( ~ spl0_51
| spl0_136
| spl0_138
| ~ spl0_171 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s277,plain,
( ~ spl0_54
| spl0_103
| spl0_104
| ~ spl0_105 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s279,plain,
( ~ spl0_54
| spl0_133
| spl0_134
| ~ spl0_167 ),
inference(sat_conversion,[],[f1358]) ).
cnf(s284,plain,
( ~ spl0_42
| spl0_118
| ~ spl0_120
| spl0_165 ),
inference(sat_conversion,[],[f1372]) ).
cnf(s289,plain,
( ~ spl0_42
| spl0_44
| ~ spl0_55 ),
inference(sat_conversion,[],[f1397]) ).
cnf(s291,plain,
( ~ spl0_27
| spl0_124
| ~ spl0_126
| ~ spl0_173 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s296,plain,
( ~ spl0_17
| ~ spl0_128
| ~ spl0_129
| ~ spl0_174 ),
inference(sat_conversion,[],[f1429]) ).
cnf(s297,plain,
( ~ spl0_27
| ~ spl0_128
| ~ spl0_129
| spl0_174 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s303,plain,
( ~ spl0_34
| spl0_127
| ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f1449]) ).
cnf(s307,plain,
( ~ spl0_56
| spl0_134
| ~ spl0_135
| spl0_167 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s309,plain,
( spl0_41
| ~ spl0_42
| ~ spl0_56 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s310,plain,
( ~ spl0_31
| ~ spl0_119
| ~ spl0_120
| spl0_165 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s312,plain,
( ~ spl0_41
| spl0_118
| ~ spl0_119
| spl0_165 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s315,plain,
( ~ spl0_41
| spl0_133
| ~ spl0_135
| spl0_167 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s318,plain,
( ~ spl0_58
| spl0_131
| ~ spl0_132
| spl0_166 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s319,plain,
( ~ spl0_58
| spl0_154
| spl0_155
| ~ spl0_156 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s320,plain,
( ~ spl0_35
| spl0_142
| ~ spl0_143
| spl0_175 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s321,plain,
( ~ spl0_27
| spl0_142
| ~ spl0_143
| ~ spl0_144 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s322,plain,
( ~ spl0_34
| ~ spl0_143
| ~ spl0_144
| spl0_175 ),
inference(sat_conversion,[],[f1539]) ).
cnf(s330,plain,
( ~ spl0_40
| ~ spl0_119
| ~ spl0_120
| ~ spl0_165 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s343,plain,
( ~ spl0_55
| spl0_82
| spl0_83
| spl0_84 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s344,plain,
( ~ spl0_55
| spl0_103
| spl0_104
| spl0_169 ),
inference(sat_conversion,[],[f1600]) ).
cnf(s345,plain,
( ~ spl0_55
| spl0_136
| spl0_138
| spl0_171 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s346,plain,
( ~ spl0_62
| spl0_136
| spl0_137
| spl0_138 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s348,plain,
( ~ spl0_56
| spl0_137
| spl0_138
| ~ spl0_171 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s349,plain,
( ~ spl0_56
| spl0_109
| ~ spl0_110
| spl0_159 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s350,plain,
( ~ spl0_22
| ~ spl0_67
| ~ spl0_68
| ~ spl0_69 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s361,plain,
( ~ spl0_24
| ~ spl0_67
| ~ spl0_68
| spl0_163 ),
inference(sat_conversion,[],[f1638]) ).
cnf(s365,plain,
( ~ spl0_35
| spl0_124
| spl0_125
| ~ spl0_173 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s368,plain,
( ~ spl0_62
| spl0_140
| spl0_141
| spl0_176 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s371,plain,
( ~ spl0_48
| spl0_109
| ~ spl0_111
| ~ spl0_159 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s372,plain,
( ~ spl0_48
| spl0_131
| ~ spl0_132
| ~ spl0_166 ),
inference(sat_conversion,[],[f1680]) ).
cnf(s373,plain,
( ~ spl0_48
| spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f1681]) ).
cnf(s376,plain,
( ~ spl0_24
| spl0_130
| ~ spl0_132
| ~ spl0_166 ),
inference(sat_conversion,[],[f1684]) ).
cnf(s381,plain,
( ~ spl0_42
| spl0_88
| spl0_89
| ~ spl0_90 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s399,plain,
( ~ spl0_24
| spl0_142
| ~ spl0_143
| ~ spl0_175 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s402,plain,
( ~ spl0_42
| spl0_125
| ~ spl0_126
| spl0_173 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s405,plain,
( ~ spl0_44
| spl0_121
| spl0_122
| spl0_123 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s406,plain,
( ~ spl0_44
| spl0_124
| spl0_125
| spl0_173 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s410,plain,
( ~ spl0_49
| spl0_130
| spl0_131
| ~ spl0_132 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s411,plain,
( ~ spl0_49
| spl0_139
| spl0_141
| ~ spl0_176 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s414,plain,
( spl0_6
| ~ spl0_5
| ~ spl0_15
| spl0_1 ),
inference(rat,[],[s36,s312,s310,s330,s63,s343,s105,s106,s107,s24,s257,s189,s190,s191,s31,s236,s153,s154,s155]) ).
cnf(s415,plain,
( spl0_165
| spl0_35
| ~ spl0_5
| ~ spl0_15 ),
inference(rat,[],[s36,s312,s310,s155,s154,s153]) ).
cnf(s416,plain,
( ~ spl0_25
| ~ spl0_55 ),
inference(rat,[],[s343,s105,s106,s107]) ).
cnf(s417,plain,
( ~ spl0_56
| spl0_31
| ~ spl0_24
| ~ spl0_5
| ~ spl0_15
| spl0_1 ),
inference(rat,[],[s59,s269,s279,s307,s173,s174,s175,s33,s303,s165,s166,s167,s8,s254,s349,s236,s153,s154,s155,s143,s142,s141,s414]) ).
cnf(s419,plain,
( ~ spl0_19
| ~ spl0_42 ),
inference(rat,[],[s381,s113,s114,s115]) ).
cnf(s420,plain,
( ~ spl0_33
| ~ spl0_41 ),
inference(rat,[],[s243,s129,s130,s131]) ).
cnf(s421,plain,
( ~ spl0_56
| spl0_58
| ~ spl0_24
| spl0_35
| ~ spl0_5
| ~ spl0_15
| spl0_1 ),
inference(rat,[],[s411,s368,s181,s182,s183,s69,s350,s85,s86,s87,s79,s45,s52,s279,s240,s269,s307,s173,s174,s175,s33,s303,s165,s166,s167,s8,s254,s349,s236,s153,s154,s155,s143,s142,s141,s414]) ).
cnf(s422,plain,
( ~ spl0_41
| spl0_35
| ~ spl0_5
| ~ spl0_3
| spl0_1 ),
inference(rat,[],[s279,s315,s173,s174,s175,s28,s419,s53,s79,s270,s346,s345,s177,s178,s179,s66,s421,s319,s201,s202,s203,s40,s420,s236,s227,s141,s142,s143,s414,s63,s330,s155,s44,s215,s109,s110,s111,s27,s234,s415,s154,s153,s196,s373,s193,s194,s195]) ).
cnf(s423,plain,
( spl0_35
| ~ spl0_5
| ~ spl0_3
| spl0_1 ),
inference(rat,[],[s348,s345,s177,s178,s179,s35,s67,s422,s63,s234,s330,s415,s196,s155,s154,s153]) ).
cnf(s424,plain,
( ~ spl0_11
| ~ spl0_35 ),
inference(rat,[],[s257,s189,s190,s191]) ).
cnf(s425,plain,
( spl0_42
| spl0_4
| ~ spl0_15
| spl0_2 ),
inference(rat,[],[s277,s133,s134,s135,s57,s37]) ).
cnf(s426,plain,
( spl0_4
| spl0_2
| spl0_1 ),
inference(rat,[],[s79,s346,s279,s177,s178,s179,s315,s66,s67,s269,s349,s173,s174,s175,s254,s28,s13,s234,s419,s284,s425,s7,s424,s423,s141,s142,s143,s414,s236,s153,s154,s155,s2,s196,s1]) ).
cnf(s427,plain,
( ~ spl0_55
| spl0_44
| spl0_48
| ~ spl0_15
| spl0_2 ),
inference(rat,[],[s344,s267,s133,s134,s53,s37,s289]) ).
cnf(s428,plain,
( spl0_165
| ~ spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s67,s417,s312,s310,s44,s215,s109,s110,s111,s27,s232,s149,s150,s151,s426,s196,s373,s193,s194,s195,s1,s155,s154,s153]) ).
cnf(s430,plain,
( ~ spl0_18
| ~ spl0_44
| ~ spl0_35 ),
inference(rat,[],[s365,s406,s161,s162]) ).
cnf(s431,plain,
( ~ spl0_13
| ~ spl0_34 ),
inference(rat,[],[s303,s165,s166,s167]) ).
cnf(s432,plain,
( ~ spl0_41
| ~ spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s279,s315,s173,s174,s175,s28,s419,s53,s79,s270,s346,s345,s177,s178,s179,s66,s349,s254,s8,s431,s22,s420,s44,s215,s109,s110,s111,s27,s232,s149,s150,s151,s426,s236,s153,s143,s142,s141,s414,s430,s427,s63,s330,s428,s155,s154,s373,s193,s194,s195,s196,s423,s1]) ).
cnf(s433,plain,
( ~ spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s348,s345,s177,s178,s179,s35,s67,s432,s63,s330,s428,s154,s155,s196,s1,s232,s149,s150,s151,s426]) ).
cnf(s434,plain,
( ~ spl0_28
| ~ spl0_44 ),
inference(rat,[],[s405,s157,s158,s159]) ).
cnf(s437,plain,
( ~ spl0_26
| ~ spl0_41
| spl0_5
| ~ spl0_15 ),
inference(rat,[],[s279,s58,s315,s269,s173,s174,s175]) ).
cnf(s439,plain,
( spl0_42
| ~ spl0_55
| spl0_48
| ~ spl0_15
| spl0_2 ),
inference(rat,[],[s344,s267,s133,s134,s53,s37]) ).
cnf(s440,plain,
( ~ spl0_42
| spl0_5
| spl0_36
| ~ spl0_15 ),
inference(rat,[],[s309,s67,s437,s28,s419]) ).
cnf(s441,plain,
( spl0_26
| spl0_55
| spl0_42
| ~ spl0_24
| spl0_36
| ~ spl0_15 ),
inference(rat,[],[s42,s222,s223,s33,s361,s431,s85,s86,s87,s61,s62]) ).
cnf(s442,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s269,s173,s174,s175,s441,s439,s53,s440,s433,s44,s215,s109,s110,s111,s27,s232,s149,s150,s151,s426,s373,s193,s194,s195,s196,s1]) ).
cnf(s443,plain,
( spl0_33
| spl0_18
| ~ spl0_24
| spl0_54
| spl0_45
| ~ spl0_15 ),
inference(rat,[],[s399,s322,s185,s186,s187,s72,s319,s201,s202,s203,s22,s40]) ).
cnf(s446,plain,
( ~ spl0_26
| ~ spl0_51 ),
inference(rat,[],[s269,s173,s174,s175]) ).
cnf(s448,plain,
( ~ spl0_55
| spl0_5
| ~ spl0_2 ),
inference(rat,[],[s267,s58,s344,s277,s133,s134,s135,s18,s416,s128,s233,s125,s126,s127]) ).
cnf(s449,plain,
( spl0_27
| spl0_5
| ~ spl0_15 ),
inference(rat,[],[s434,s16,s39]) ).
cnf(s450,plain,
( ~ spl0_18
| ~ spl0_42
| ~ spl0_27 ),
inference(rat,[],[s291,s402,s161,s162,s163]) ).
cnf(s452,plain,
( ~ spl0_13
| ~ spl0_17
| ~ spl0_27 ),
inference(rat,[],[s296,s297,s166,s167]) ).
cnf(s453,plain,
( ~ spl0_42
| spl0_5
| spl0_1 ),
inference(rat,[],[s250,s254,s142,s143,s49,s446,s8,s61,s452,s10,s450,s13,s440,s419,s448,s449,s128,s442]) ).
cnf(s454,plain,
( ~ spl0_4
| ~ spl0_36 ),
inference(rat,[],[s232,s149,s150,s151]) ).
cnf(s456,plain,
( ~ spl0_57
| ~ spl0_49
| ~ spl0_62 ),
inference(rat,[],[s411,s368,s181,s182,s183]) ).
cnf(s457,plain,
( ~ spl0_37
| ~ spl0_58 ),
inference(rat,[],[s319,s201,s202,s203]) ).
cnf(s458,plain,
( spl0_41
| spl0_36
| ~ spl0_42
| ~ spl0_15 ),
inference(rat,[],[s67,s309]) ).
cnf(s459,plain,
( ~ spl0_42
| ~ spl0_5
| spl0_1 ),
inference(rat,[],[s350,s69,s85,s86,s87,s456,s52,s45,s430,s457,s443,s40,s420,s458,s79,s277,s133,s134,s135,s18,s446,s289,s416,s28,s63,s234,s330,s13,s284,s419,s233,s125,s126,s127,s155,s154,s153,s227,s141,s142,s143,s414,s128,s442]) ).
cnf(s460,plain,
( ~ spl0_55
| spl0_42
| spl0_109
| ~ spl0_110
| ~ spl0_111
| spl0_38
| ~ spl0_2 ),
inference(rat,[],[s346,s177,s178,s179,s66,s349,s371,s79,s53,s267,s344,s277,s133,s134,s135,s18,s416,s128,s233,s125,s126,s127]) ).
cnf(s461,plain,
( spl0_159
| spl0_41
| spl0_109
| ~ spl0_110
| ~ spl0_111
| ~ spl0_15 ),
inference(rat,[],[s67,s250,s349]) ).
cnf(s462,plain,
( ~ spl0_5
| spl0_1 ),
inference(rat,[],[s431,s33,s61,s446,s53,s371,s461,s312,s330,s63,s460,s459,s141,s142,s143,s236,s414,s153,s154,s155,s128,s442]) ).
cnf(s463,plain,
( spl0_4
| spl0_1 ),
inference(rat,[],[s277,s133,s134,s135,s57,s19,s128,s233,s125,s126,s127,s442,s453,s462]) ).
cnf(s465,plain,
( ~ spl0_26
| ~ spl0_54
| spl0_1 ),
inference(rat,[],[s307,s67,s279,s437,s173,s174,s175,s128,s442,s462,s454,s463]) ).
cnf(s466,plain,
( spl0_26
| spl0_1 ),
inference(rat,[],[s29,s452,s441,s61,s448,s449,s128,s442,s453,s462,s454,s463]) ).
cnf(s467,plain,
spl0_1,
inference(rat,[],[s58,s465,s446,s466,s462,s128,s442]) ).
cnf(s468,plain,
spl0_15,
inference(rat,[],[s172,s467]) ).
cnf(s469,plain,
spl0_132,
inference(rat,[],[s171,s467]) ).
cnf(s470,plain,
~ spl0_131,
inference(rat,[],[s170,s467]) ).
cnf(s471,plain,
~ spl0_130,
inference(rat,[],[s169,s467]) ).
cnf(s472,plain,
~ spl0_49,
inference(rat,[],[s410,s469,s470,s471]) ).
cnf(s473,plain,
( ~ spl0_42
| ~ spl0_5 ),
inference(rat,[],[s320,s399,s185,s186,s72,s45,s279,s240,s315,s173,s174,s175,s318,s28,s458,s376,s234,s13,s284,s419,s155,s154,s153,s468,s472,s469,s470,s471]) ).
cnf(s474,plain,
( ~ spl0_35
| ~ spl0_48
| spl0_54
| spl0_38 ),
inference(rat,[],[s371,s349,s68,s141,s142,s143,s399,s31,s320,s424,s186,s185,s72,s318,s372,s468,s470,s469]) ).
cnf(s475,plain,
( ~ spl0_6
| spl0_41
| ~ spl0_48 ),
inference(rat,[],[s461,s371,s141,s142,s143,s468]) ).
cnf(s476,plain,
( ~ spl0_26
| spl0_2
| ~ spl0_5 ),
inference(rat,[],[s67,s315,s307,s240,s45,s474,s53,s446,s173,s174,s175,s236,s153,s154,s155,s454,s425,s277,s133,s134,s135,s37,s473,s468,s472]) ).
cnf(s477,plain,
( spl0_2
| ~ spl0_5 ),
inference(rat,[],[s321,s15,s185,s186,s187,s416,s72,s61,s457,s431,s30,s33,s476,s277,s133,s134,s135,s37,s236,s153,s154,s155,s473,s468]) ).
cnf(s478,plain,
( ~ spl0_26
| ~ spl0_5 ),
inference(rat,[],[s315,s279,s475,s474,s53,s446,s173,s174,s175,s473,s31,s424,s45,s233,s125,s126,s127,s477,s236,s153,s154,s155,s468,s472]) ).
cnf(s479,plain,
~ spl0_5,
inference(rat,[],[s431,s61,s33,s478,s460,s141,s142,s143,s31,s424,s45,s233,s125,s126,s127,s477,s473,s236,s153,s154,s155,s468,s472]) ).
cnf(s480,plain,
spl0_27,
inference(rat,[],[s449,s468,s479]) ).
cnf(s481,plain,
~ spl0_42,
inference(rat,[],[s277,s133,s134,s135,s58,s19,s446,s233,s61,s448,s125,s126,s127,s452,s2,s10,s454,s450,s440,s419,s468,s479,s480]) ).
cnf(s482,plain,
~ spl0_26,
inference(rat,[],[s233,s125,s126,s127,s17,s2,s454,s67,s307,s475,s279,s53,s58,s446,s437,s173,s174,s175,s468,s479,s481]) ).
cnf(s483,plain,
spl0_2,
inference(rat,[],[s29,s452,s441,s61,s344,s267,s58,s277,s454,s133,s134,s135,s425,s37,s468,s480,s481,s482,s479]) ).
cnf(s484,plain,
spl0_99,
inference(rat,[],[s127,s483]) ).
cnf(s485,plain,
spl0_98,
inference(rat,[],[s126,s483]) ).
cnf(s486,plain,
~ spl0_97,
inference(rat,[],[s125,s483]) ).
cnf(s487,plain,
~ spl0_55,
inference(rat,[],[s448,s479,s483]) ).
cnf(s488,plain,
~ spl0_29,
inference(rat,[],[s233,s484,s485,s486]) ).
cnf(s490,plain,
spl0_13,
inference(rat,[],[s61,s468,s482,s487]) ).
cnf(s498,plain,
~ spl0_34,
inference(rat,[],[s431,s490]) ).
cnf(s499,plain,
~ spl0_17,
inference(rat,[],[s452,s480,s490]) ).
cnf(s505,plain,
spl0_38,
inference(rat,[],[s33,s468,s482,s498]) ).
cnf(s506,plain,
spl0_45,
inference(rat,[],[s42,s481,s468,s499]) ).
cnf(s509,plain,
spl0_36,
inference(rat,[],[s222,s505,s506]) ).
cnf(s513,plain,
~ spl0_4,
inference(rat,[],[s454,s509]) ).
cnf(s522,plain,
spl0_6,
inference(rat,[],[s17,s488,s468,s513]) ).
cnf(s527,plain,
spl0_111,
inference(rat,[],[s143,s522]) ).
cnf(s528,plain,
spl0_110,
inference(rat,[],[s142,s522]) ).
cnf(s529,plain,
~ spl0_109,
inference(rat,[],[s141,s522]) ).
cnf(s535,plain,
$false,
inference(rat,[],[s227,s527,s506,s528,s529]) ).
fof(f1772,plain,
$false,
inference(avatar_sat_refutation,[],[s535]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN499+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n009.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 16:17:15 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.04/1.10 % (3196876)Detected formulas, will run a generic FOF schedule.
% 3.04/1.10 % (3196883)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1908590423:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.04/1.10 % (3196886)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1077606943:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.04/1.10 % (3196885)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2702166888:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.04/1.10 % (3196887)dis-21_1_sil=8000:lcm=predicate:random_seed=4159450053:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.04/1.10 % (3196881)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3705117101:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.04/1.10 % (3196882)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2097138048:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.04/1.10 % (3196884)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2413211247:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.04/1.10 % (3196887)First to succeed.
% 3.04/1.10 % (3196887)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3196876"
% 3.04/1.10 % (3196886)Also succeeded, but the first one will report.
% 3.04/1.10 % (3196885)Instruction limit reached!
% 3.04/1.10 % (3196885)------------------------------
% 3.04/1.10 % (3196885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.10 % (3196885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.10 % (3196885)CaDiCaL version: 2.1.3
% 3.04/1.10 % (3196885)Termination reason: Instruction limit
% 3.04/1.10 % (3196885)Termination phase: Saturation
% 3.04/1.10 % (3196885)Time elapsed: 0.057 s
% 3.04/1.10 % (3196885)Peak memory usage: 88 MB
% 3.04/1.10 % (3196885)Instructions burned: 121 (million)
% 3.04/1.10 % (3196884)Instruction limit reached!
% 3.04/1.10 % (3196884)------------------------------
% 3.04/1.10 % (3196884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.10 % (3196884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.10 % (3196884)CaDiCaL version: 2.1.3
% 3.04/1.10 % (3196884)Termination reason: Instruction limit
% 3.04/1.10 % (3196884)Termination phase: Saturation
% 3.04/1.10 % (3196884)Time elapsed: 0.070 s
% 3.04/1.10 % (3196884)Peak memory usage: 90 MB
% 3.04/1.10 % (3196884)Instructions burned: 109 (million)
% 3.04/1.10 % (3196895)lrs+10_1_sil=8000:sp=occurrence:random_seed=1564058157:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.04/1.10 % (3196896)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1548506784:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.04/1.10 % (3196895)Also succeeded, but the first one will report.
% 3.04/1.10 % (3196896)Also succeeded, but the first one will report.
% 3.04/1.10 % (3196887)Refutation found. Thanks to Tanya!
% 3.04/1.10 % SZS status Theorem for theBenchmark
% 3.04/1.10 % SZS output start Proof for theBenchmark
% See solution above
% 3.67/1.29 % (3196887)------------------------------
% 3.67/1.29 % (3196887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.29 % (3196887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.29 % (3196887)CaDiCaL version: 2.1.3
% 3.67/1.29 % (3196887)Termination reason: Refutation
% 3.67/1.29 % (3196887)Time elapsed: 0.029 s
% 3.67/1.29 % (3196887)Peak memory usage: 90 MB
% 3.67/1.29 % (3196887)Instructions burned: 49 (million)
% 3.67/1.29 % (3196887)------------------------------
% 3.67/1.29 % (3196887)------------------------------
% 3.67/1.29 % (3196876)Success in time 0.442 s
% 3.67/1.29 % Vampire exiting
%------------------------------------------------------------------------------