%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN473+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 : n015.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:54:16 PM UTC 2026
% Result : Theorem 3.58s 1.17s
% Output : Refutation 4.01s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a793)
& c2_1(a793)
& ~ c1_1(a793) ) )
& ( ~ hskp1
| ( ndr1_0
& c3_1(a794)
& ~ c0_1(a794)
& ~ c2_1(a794) ) )
& ( ~ hskp2
| ( ndr1_0
& ~ c0_1(a795)
& ~ c1_1(a795)
& ~ c3_1(a795) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a798)
& c2_1(a798)
& ~ c3_1(a798) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a799)
& c3_1(a799)
& ~ c1_1(a799) ) )
& ( ~ hskp5
| ( ndr1_0
& c3_1(a800)
& ~ c0_1(a800)
& ~ c1_1(a800) ) )
& ( ~ hskp6
| ( ndr1_0
& c2_1(a802)
& ~ c0_1(a802)
& ~ c1_1(a802) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a803)
& c3_1(a803)
& ~ c2_1(a803) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a805)
& ~ c2_1(a805)
& ~ c3_1(a805) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a806)
& c1_1(a806)
& ~ c3_1(a806) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a807)
& ~ c2_1(a807)
& ~ c3_1(a807) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a808)
& ~ c1_1(a808)
& ~ c2_1(a808) ) )
& ( ~ hskp12
| ( ndr1_0
& c1_1(a809)
& c2_1(a809)
& ~ c0_1(a809) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a814)
& ~ c0_1(a814)
& ~ c3_1(a814) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a816)
& ~ c1_1(a816)
& ~ c2_1(a816) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a817)
& c3_1(a817)
& ~ c1_1(a817) ) )
& ( ~ hskp16
| ( ndr1_0
& ~ c0_1(a821)
& ~ c1_1(a821)
& ~ c2_1(a821) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a825)
& c1_1(a825)
& ~ c2_1(a825) ) )
& ( ~ hskp18
| ( ndr1_0
& ~ c1_1(a828)
& ~ c2_1(a828)
& ~ c3_1(a828) ) )
& ( ~ hskp19
| ( ndr1_0
& c2_1(a832)
& ~ c1_1(a832)
& ~ c3_1(a832) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a833)
& ~ c0_1(a833)
& ~ c2_1(a833) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a838)
& c3_1(a838)
& ~ c2_1(a838) ) )
& ( ~ hskp22
| ( ndr1_0
& c1_1(a840)
& c3_1(a840)
& ~ c0_1(a840) ) )
& ( ~ hskp23
| ( ndr1_0
& c0_1(a856)
& ~ c2_1(a856)
& ~ c3_1(a856) ) )
& ( ~ hskp24
| ( ndr1_0
& c0_1(a862)
& ~ c1_1(a862)
& ~ c3_1(a862) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a865)
& c2_1(a865)
& ~ c3_1(a865) ) )
& ( ~ hskp26
| ( ndr1_0
& c2_1(a869)
& c3_1(a869)
& ~ c0_1(a869) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a796)
& c2_1(a796)
& c3_1(a796) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a797)
& c2_1(a797)
& c3_1(a797) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a829)
& c1_1(a829)
& c2_1(a829) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a867)
& c1_1(a867)
& c3_1(a867) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c3_1(X4)
| ~ c0_1(X4)
| ~ c2_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| hskp1
| hskp2 )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c3_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| ~ c1_1(X7)
| ~ c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c1_1(X8)
| c3_1(X8)
| ~ c2_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| hskp27
| hskp28 )
& ( ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| c3_1(X10) ) )
| hskp3
| hskp4 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| ~ c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12) ) )
| hskp5 )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| ~ c3_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( c1_1(X14)
| c3_1(X14)
| ~ c2_1(X14) ) )
| hskp4 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| ~ c3_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c1_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( c2_1(X17)
| ~ c0_1(X17)
| ~ c1_1(X17) ) ) )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c2_1(X19)
| ~ c1_1(X19)
| ~ c3_1(X19) ) )
| hskp6 )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( ~ c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21) ) )
| hskp7 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22) ) )
| hskp4
| hskp8 )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c2_1(X23)
| c3_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c3_1(X25)
| ~ c0_1(X25)
| ~ c1_1(X25) ) ) )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| c2_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c1_1(X28)
| c3_1(X28)
| ~ c0_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c2_1(X29)
| c3_1(X29) ) )
| hskp9
| hskp10 )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c3_1(X31)
| ~ c1_1(X31) ) )
| hskp11 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| ~ c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c3_1(X33)
| ~ c2_1(X33) ) )
| hskp12 )
& ( ! [X34] :
( ndr1_0
=> ( c0_1(X34)
| c2_1(X34)
| ~ c3_1(X34) ) )
| ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| ~ c1_1(X35)
| ~ c2_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c3_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36) ) ) )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( c3_1(X39)
| ~ c1_1(X39)
| ~ c2_1(X39) ) ) )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| ~ c3_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( c2_1(X41)
| ~ c0_1(X41)
| ~ c1_1(X41) ) )
| hskp9 )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| ~ c3_1(X42) ) )
| hskp1
| hskp10 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c3_1(X43)
| ~ c1_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( c1_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c0_1(X45)
| ~ c2_1(X45)
| ~ c3_1(X45) ) ) )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c2_1(X47)
| c3_1(X47)
| ~ c1_1(X47) ) )
| hskp3 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48) ) )
| hskp13
| hskp6 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| c3_1(X49)
| ~ c2_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| ~ c1_1(X50)
| ~ c3_1(X50) ) )
| hskp14 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| c3_1(X51)
| ~ c2_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c2_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52) ) )
| ! [X53] :
( ndr1_0
=> ( c3_1(X53)
| ~ c0_1(X53)
| ~ c1_1(X53) ) ) )
& ( ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c1_1(X55)
| ~ c2_1(X55)
| ~ c3_1(X55) ) )
| hskp15 )
& ( ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| c3_1(X56)
| ~ c2_1(X56) ) )
| hskp0
| hskp5 )
& ( ! [X57] :
( ndr1_0
=> ( c0_1(X57)
| c3_1(X57)
| ~ c2_1(X57) ) )
| hskp13
| hskp16 )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| ~ c1_1(X58)
| ~ c2_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| ~ c0_1(X59)
| ~ c3_1(X59) ) )
| hskp14 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| ~ c1_1(X60)
| ~ c2_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| ~ c0_1(X61)
| ~ c3_1(X61) ) )
| hskp13 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| ~ c1_1(X62)
| ~ c2_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( c2_1(X63)
| c3_1(X63)
| ~ c1_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( c0_1(X65)
| ~ c1_1(X65)
| ~ c3_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c1_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66) ) )
| hskp8 )
& ( ! [X67] :
( ndr1_0
=> ( c0_1(X67)
| ~ c1_1(X67)
| ~ c3_1(X67) ) )
| hskp17
| hskp0 )
& ( ! [X68] :
( ndr1_0
=> ( c0_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68) ) )
| hskp14
| hskp18 )
& ( ! [X69] :
( ndr1_0
=> ( c0_1(X69)
| ~ c2_1(X69)
| ~ c3_1(X69) ) )
| ! [X70] :
( ndr1_0
=> ( ~ c0_1(X70)
| ~ c1_1(X70)
| ~ c2_1(X70) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( c0_1(X72)
| ~ c2_1(X72)
| ~ c3_1(X72) ) )
| hskp29
| hskp9 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| c2_1(X73)
| c3_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| c2_1(X74)
| ~ c0_1(X74) ) )
| hskp29 )
& ( ! [X75] :
( ndr1_0
=> ( c1_1(X75)
| c2_1(X75)
| c3_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) )
| hskp19 )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| c2_1(X77)
| c3_1(X77) ) )
| hskp20
| hskp2 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78) ) )
| ! [X79] :
( ndr1_0
=> ( c2_1(X79)
| c3_1(X79)
| ~ c1_1(X79) ) )
| hskp29 )
& ( ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80) ) )
| hskp20
| hskp1 )
& ( ! [X81] :
( ndr1_0
=> ( c1_1(X81)
| c2_1(X81)
| ~ c3_1(X81) ) )
| hskp21
| hskp18 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| c3_1(X82)
| ~ c0_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83) ) )
| hskp22 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| c3_1(X84)
| ~ c2_1(X84) ) )
| hskp0
| hskp21 )
& ( ! [X85] :
( ndr1_0
=> ( c1_1(X85)
| ~ c2_1(X85)
| ~ c3_1(X85) ) )
| ! [X86] :
( ndr1_0
=> ( ~ c0_1(X86)
| ~ c1_1(X86)
| ~ c3_1(X86) ) )
| hskp28 )
& ( ! [X87] :
( ndr1_0
=> ( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87) ) )
| ! [X88] :
( ndr1_0
=> ( c2_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89) ) ) )
& ( ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90) ) )
| ! [X91] :
( ndr1_0
=> ( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c3_1(X91) ) )
| hskp12 )
& ( ! [X92] :
( ndr1_0
=> ( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92) ) )
| hskp17
| hskp8 )
& ( ! [X93] :
( ndr1_0
=> ( c2_1(X93)
| c3_1(X93)
| ~ c1_1(X93) ) )
| hskp28
| hskp19 )
& ( ! [X94] :
( ndr1_0
=> ( c2_1(X94)
| c3_1(X94)
| ~ c1_1(X94) ) )
| hskp13
| hskp1 )
& ( ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| ! [X96] :
( ndr1_0
=> ( c2_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96) ) )
| hskp28 )
& ( ! [X97] :
( ndr1_0
=> ( c2_1(X97)
| ~ c0_1(X97)
| ~ c1_1(X97) ) )
| hskp4
| hskp28 )
& ( ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp9
| hskp20 )
& ( ! [X99] :
( ndr1_0
=> ( c3_1(X99)
| ~ c0_1(X99)
| ~ c1_1(X99) ) )
| hskp23
| hskp13 )
& ( ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c2_1(X100) ) )
| ! [X101] :
( ndr1_0
=> ( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101) ) )
| hskp5 )
& ( ! [X102] :
( ndr1_0
=> ( c3_1(X102)
| ~ c0_1(X102)
| ~ c2_1(X102) ) )
| hskp27
| hskp3 )
& ( ! [X103] :
( ndr1_0
=> ( ~ c0_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103) ) )
| hskp14
| hskp24 )
& ( ! [X104] :
( ndr1_0
=> ( ~ c0_1(X104)
| ~ c1_1(X104)
| ~ c3_1(X104) ) )
| hskp14
| hskp22 )
& ( ! [X105] :
( ndr1_0
=> ( ~ c0_1(X105)
| ~ c1_1(X105)
| ~ c3_1(X105) ) )
| hskp25
| hskp1 )
& ( ! [X106] :
( ndr1_0
=> ( ~ c0_1(X106)
| ~ c2_1(X106)
| ~ c3_1(X106) ) )
| hskp30
| hskp20 )
& ( ! [X107] :
( ndr1_0
=> ( ~ c0_1(X107)
| ~ c2_1(X107)
| ~ c3_1(X107) ) )
| hskp26
| hskp11 )
& ( ! [X108] :
( ndr1_0
=> ( ~ c0_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108) ) )
| hskp15
| hskp16 )
& ( ! [X109] :
( ndr1_0
=> ( ~ c1_1(X109)
| ~ c2_1(X109)
| ~ c3_1(X109) ) )
| hskp27
| hskp19 )
& ( ! [X110] :
( ndr1_0
=> ( ~ c1_1(X110)
| ~ c2_1(X110)
| ~ c3_1(X110) ) )
| hskp21
| hskp11 )
& ( hskp30
| hskp28
| hskp19 )
& ( hskp9
| hskp3
| hskp26 )
& ( hskp27
| hskp21
| hskp28 )
& ( hskp4
| hskp24
| hskp5 )
& ( hskp4
| hskp26
| hskp5 )
& ( hskp28
| hskp8
| hskp10 )
& ( hskp22
| hskp1
| hskp11 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a793)
& c2_1(a793)
& ~ c1_1(a793) ) )
& ( ~ hskp1
| ( ndr1_0
& c3_1(a794)
& ~ c0_1(a794)
& ~ c2_1(a794) ) )
& ( ~ hskp2
| ( ndr1_0
& ~ c0_1(a795)
& ~ c1_1(a795)
& ~ c3_1(a795) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a798)
& c2_1(a798)
& ~ c3_1(a798) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a799)
& c3_1(a799)
& ~ c1_1(a799) ) )
& ( ~ hskp5
| ( ndr1_0
& c3_1(a800)
& ~ c0_1(a800)
& ~ c1_1(a800) ) )
& ( ~ hskp6
| ( ndr1_0
& c2_1(a802)
& ~ c0_1(a802)
& ~ c1_1(a802) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a803)
& c3_1(a803)
& ~ c2_1(a803) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a805)
& ~ c2_1(a805)
& ~ c3_1(a805) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a806)
& c1_1(a806)
& ~ c3_1(a806) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a807)
& ~ c2_1(a807)
& ~ c3_1(a807) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a808)
& ~ c1_1(a808)
& ~ c2_1(a808) ) )
& ( ~ hskp12
| ( ndr1_0
& c1_1(a809)
& c2_1(a809)
& ~ c0_1(a809) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a814)
& ~ c0_1(a814)
& ~ c3_1(a814) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a816)
& ~ c1_1(a816)
& ~ c2_1(a816) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a817)
& c3_1(a817)
& ~ c1_1(a817) ) )
& ( ~ hskp16
| ( ndr1_0
& ~ c0_1(a821)
& ~ c1_1(a821)
& ~ c2_1(a821) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a825)
& c1_1(a825)
& ~ c2_1(a825) ) )
& ( ~ hskp18
| ( ndr1_0
& ~ c1_1(a828)
& ~ c2_1(a828)
& ~ c3_1(a828) ) )
& ( ~ hskp19
| ( ndr1_0
& c2_1(a832)
& ~ c1_1(a832)
& ~ c3_1(a832) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a833)
& ~ c0_1(a833)
& ~ c2_1(a833) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a838)
& c3_1(a838)
& ~ c2_1(a838) ) )
& ( ~ hskp22
| ( ndr1_0
& c1_1(a840)
& c3_1(a840)
& ~ c0_1(a840) ) )
& ( ~ hskp23
| ( ndr1_0
& c0_1(a856)
& ~ c2_1(a856)
& ~ c3_1(a856) ) )
& ( ~ hskp24
| ( ndr1_0
& c0_1(a862)
& ~ c1_1(a862)
& ~ c3_1(a862) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a865)
& c2_1(a865)
& ~ c3_1(a865) ) )
& ( ~ hskp26
| ( ndr1_0
& c2_1(a869)
& c3_1(a869)
& ~ c0_1(a869) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a796)
& c2_1(a796)
& c3_1(a796) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a797)
& c2_1(a797)
& c3_1(a797) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a829)
& c1_1(a829)
& c2_1(a829) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a867)
& c1_1(a867)
& c3_1(a867) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c3_1(X4)
| ~ c0_1(X4)
| ~ c2_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| hskp1
| hskp2 )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c3_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| ~ c1_1(X7)
| ~ c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c1_1(X8)
| c3_1(X8)
| ~ c2_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| hskp27
| hskp28 )
& ( ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| c3_1(X10) ) )
| hskp3
| hskp4 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| ~ c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12) ) )
| hskp5 )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| ~ c3_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( c1_1(X14)
| c3_1(X14)
| ~ c2_1(X14) ) )
| hskp4 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| ~ c3_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c1_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( c2_1(X17)
| ~ c0_1(X17)
| ~ c1_1(X17) ) ) )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c2_1(X19)
| ~ c1_1(X19)
| ~ c3_1(X19) ) )
| hskp6 )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( ~ c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21) ) )
| hskp7 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22) ) )
| hskp4
| hskp8 )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c2_1(X23)
| c3_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c3_1(X25)
| ~ c0_1(X25)
| ~ c1_1(X25) ) ) )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| c2_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c1_1(X28)
| c3_1(X28)
| ~ c0_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c2_1(X29)
| c3_1(X29) ) )
| hskp9
| hskp10 )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c3_1(X31)
| ~ c1_1(X31) ) )
| hskp11 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| ~ c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c3_1(X33)
| ~ c2_1(X33) ) )
| hskp12 )
& ( ! [X34] :
( ndr1_0
=> ( c0_1(X34)
| c2_1(X34)
| ~ c3_1(X34) ) )
| ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| ~ c1_1(X35)
| ~ c2_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c3_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36) ) ) )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( c3_1(X39)
| ~ c1_1(X39)
| ~ c2_1(X39) ) ) )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| ~ c3_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( c2_1(X41)
| ~ c0_1(X41)
| ~ c1_1(X41) ) )
| hskp9 )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| ~ c3_1(X42) ) )
| hskp1
| hskp10 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c3_1(X43)
| ~ c1_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( c1_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c0_1(X45)
| ~ c2_1(X45)
| ~ c3_1(X45) ) ) )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c2_1(X47)
| c3_1(X47)
| ~ c1_1(X47) ) )
| hskp3 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48) ) )
| hskp13
| hskp6 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| c3_1(X49)
| ~ c2_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| ~ c1_1(X50)
| ~ c3_1(X50) ) )
| hskp14 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| c3_1(X51)
| ~ c2_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c2_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52) ) )
| ! [X53] :
( ndr1_0
=> ( c3_1(X53)
| ~ c0_1(X53)
| ~ c1_1(X53) ) ) )
& ( ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c1_1(X55)
| ~ c2_1(X55)
| ~ c3_1(X55) ) )
| hskp15 )
& ( ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| c3_1(X56)
| ~ c2_1(X56) ) )
| hskp0
| hskp5 )
& ( ! [X57] :
( ndr1_0
=> ( c0_1(X57)
| c3_1(X57)
| ~ c2_1(X57) ) )
| hskp13
| hskp16 )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| ~ c1_1(X58)
| ~ c2_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| ~ c0_1(X59)
| ~ c3_1(X59) ) )
| hskp14 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| ~ c1_1(X60)
| ~ c2_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| ~ c0_1(X61)
| ~ c3_1(X61) ) )
| hskp13 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| ~ c1_1(X62)
| ~ c2_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( c2_1(X63)
| c3_1(X63)
| ~ c1_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( c0_1(X65)
| ~ c1_1(X65)
| ~ c3_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c1_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66) ) )
| hskp8 )
& ( ! [X67] :
( ndr1_0
=> ( c0_1(X67)
| ~ c1_1(X67)
| ~ c3_1(X67) ) )
| hskp17
| hskp0 )
& ( ! [X68] :
( ndr1_0
=> ( c0_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68) ) )
| hskp14
| hskp18 )
& ( ! [X69] :
( ndr1_0
=> ( c0_1(X69)
| ~ c2_1(X69)
| ~ c3_1(X69) ) )
| ! [X70] :
( ndr1_0
=> ( ~ c0_1(X70)
| ~ c1_1(X70)
| ~ c2_1(X70) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( c0_1(X72)
| ~ c2_1(X72)
| ~ c3_1(X72) ) )
| hskp29
| hskp9 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| c2_1(X73)
| c3_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| c2_1(X74)
| ~ c0_1(X74) ) )
| hskp29 )
& ( ! [X75] :
( ndr1_0
=> ( c1_1(X75)
| c2_1(X75)
| c3_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) )
| hskp19 )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| c2_1(X77)
| c3_1(X77) ) )
| hskp20
| hskp2 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78) ) )
| ! [X79] :
( ndr1_0
=> ( c2_1(X79)
| c3_1(X79)
| ~ c1_1(X79) ) )
| hskp29 )
& ( ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80) ) )
| hskp20
| hskp1 )
& ( ! [X81] :
( ndr1_0
=> ( c1_1(X81)
| c2_1(X81)
| ~ c3_1(X81) ) )
| hskp21
| hskp18 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| c3_1(X82)
| ~ c0_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83) ) )
| hskp22 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| c3_1(X84)
| ~ c2_1(X84) ) )
| hskp0
| hskp21 )
& ( ! [X85] :
( ndr1_0
=> ( c1_1(X85)
| ~ c2_1(X85)
| ~ c3_1(X85) ) )
| ! [X86] :
( ndr1_0
=> ( ~ c0_1(X86)
| ~ c1_1(X86)
| ~ c3_1(X86) ) )
| hskp28 )
& ( ! [X87] :
( ndr1_0
=> ( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87) ) )
| ! [X88] :
( ndr1_0
=> ( c2_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89) ) ) )
& ( ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90) ) )
| ! [X91] :
( ndr1_0
=> ( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c3_1(X91) ) )
| hskp12 )
& ( ! [X92] :
( ndr1_0
=> ( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92) ) )
| hskp17
| hskp8 )
& ( ! [X93] :
( ndr1_0
=> ( c2_1(X93)
| c3_1(X93)
| ~ c1_1(X93) ) )
| hskp28
| hskp19 )
& ( ! [X94] :
( ndr1_0
=> ( c2_1(X94)
| c3_1(X94)
| ~ c1_1(X94) ) )
| hskp13
| hskp1 )
& ( ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| ! [X96] :
( ndr1_0
=> ( c2_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96) ) )
| hskp28 )
& ( ! [X97] :
( ndr1_0
=> ( c2_1(X97)
| ~ c0_1(X97)
| ~ c1_1(X97) ) )
| hskp4
| hskp28 )
& ( ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp9
| hskp20 )
& ( ! [X99] :
( ndr1_0
=> ( c3_1(X99)
| ~ c0_1(X99)
| ~ c1_1(X99) ) )
| hskp23
| hskp13 )
& ( ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c2_1(X100) ) )
| ! [X101] :
( ndr1_0
=> ( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101) ) )
| hskp5 )
& ( ! [X102] :
( ndr1_0
=> ( c3_1(X102)
| ~ c0_1(X102)
| ~ c2_1(X102) ) )
| hskp27
| hskp3 )
& ( ! [X103] :
( ndr1_0
=> ( ~ c0_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103) ) )
| hskp14
| hskp24 )
& ( ! [X104] :
( ndr1_0
=> ( ~ c0_1(X104)
| ~ c1_1(X104)
| ~ c3_1(X104) ) )
| hskp14
| hskp22 )
& ( ! [X105] :
( ndr1_0
=> ( ~ c0_1(X105)
| ~ c1_1(X105)
| ~ c3_1(X105) ) )
| hskp25
| hskp1 )
& ( ! [X106] :
( ndr1_0
=> ( ~ c0_1(X106)
| ~ c2_1(X106)
| ~ c3_1(X106) ) )
| hskp30
| hskp20 )
& ( ! [X107] :
( ndr1_0
=> ( ~ c0_1(X107)
| ~ c2_1(X107)
| ~ c3_1(X107) ) )
| hskp26
| hskp11 )
& ( ! [X108] :
( ndr1_0
=> ( ~ c0_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108) ) )
| hskp15
| hskp16 )
& ( ! [X109] :
( ndr1_0
=> ( ~ c1_1(X109)
| ~ c2_1(X109)
| ~ c3_1(X109) ) )
| hskp27
| hskp19 )
& ( ! [X110] :
( ndr1_0
=> ( ~ c1_1(X110)
| ~ c2_1(X110)
| ~ c3_1(X110) ) )
| hskp21
| hskp11 )
& ( hskp30
| hskp28
| hskp19 )
& ( hskp9
| hskp3
| hskp26 )
& ( hskp27
| hskp21
| hskp28 )
& ( hskp4
| hskp24
| hskp5 )
& ( hskp4
| hskp26
| hskp5 )
& ( hskp28
| hskp8
| hskp10 )
& ( hskp22
| hskp1
| hskp11 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a793)
& c2_1(a793)
& ~ c1_1(a793) ) )
& ( ~ hskp1
| ( ndr1_0
& c3_1(a794)
& ~ c0_1(a794)
& ~ c2_1(a794) ) )
& ( ~ hskp2
| ( ndr1_0
& ~ c0_1(a795)
& ~ c1_1(a795)
& ~ c3_1(a795) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a798)
& c2_1(a798)
& ~ c3_1(a798) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a799)
& c3_1(a799)
& ~ c1_1(a799) ) )
& ( ~ hskp5
| ( ndr1_0
& c3_1(a800)
& ~ c0_1(a800)
& ~ c1_1(a800) ) )
& ( ~ hskp6
| ( ndr1_0
& c2_1(a802)
& ~ c0_1(a802)
& ~ c1_1(a802) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a803)
& c3_1(a803)
& ~ c2_1(a803) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a805)
& ~ c2_1(a805)
& ~ c3_1(a805) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a806)
& c1_1(a806)
& ~ c3_1(a806) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a807)
& ~ c2_1(a807)
& ~ c3_1(a807) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a808)
& ~ c1_1(a808)
& ~ c2_1(a808) ) )
& ( ~ hskp12
| ( ndr1_0
& c1_1(a809)
& c2_1(a809)
& ~ c0_1(a809) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a814)
& ~ c0_1(a814)
& ~ c3_1(a814) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a816)
& ~ c1_1(a816)
& ~ c2_1(a816) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a817)
& c3_1(a817)
& ~ c1_1(a817) ) )
& ( ~ hskp16
| ( ndr1_0
& ~ c0_1(a821)
& ~ c1_1(a821)
& ~ c2_1(a821) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a825)
& c1_1(a825)
& ~ c2_1(a825) ) )
& ( ~ hskp18
| ( ndr1_0
& ~ c1_1(a828)
& ~ c2_1(a828)
& ~ c3_1(a828) ) )
& ( ~ hskp19
| ( ndr1_0
& c2_1(a832)
& ~ c1_1(a832)
& ~ c3_1(a832) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a833)
& ~ c0_1(a833)
& ~ c2_1(a833) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a838)
& c3_1(a838)
& ~ c2_1(a838) ) )
& ( ~ hskp22
| ( ndr1_0
& c1_1(a840)
& c3_1(a840)
& ~ c0_1(a840) ) )
& ( ~ hskp23
| ( ndr1_0
& c0_1(a856)
& ~ c2_1(a856)
& ~ c3_1(a856) ) )
& ( ~ hskp24
| ( ndr1_0
& c0_1(a862)
& ~ c1_1(a862)
& ~ c3_1(a862) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a865)
& c2_1(a865)
& ~ c3_1(a865) ) )
& ( ~ hskp26
| ( ndr1_0
& c2_1(a869)
& c3_1(a869)
& ~ c0_1(a869) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a796)
& c2_1(a796)
& c3_1(a796) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a797)
& c2_1(a797)
& c3_1(a797) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a829)
& c1_1(a829)
& c2_1(a829) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a867)
& c1_1(a867)
& c3_1(a867) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c3_1(X4)
| ~ c0_1(X4)
| ~ c2_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| hskp1
| hskp2 )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c3_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| ~ c1_1(X7)
| ~ c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c1_1(X8)
| c3_1(X8)
| ~ c2_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| hskp27
| hskp28 )
& ( ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| c3_1(X10) ) )
| hskp3
| hskp4 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| ~ c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12) ) )
| hskp5 )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| ~ c3_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( c1_1(X14)
| c3_1(X14)
| ~ c2_1(X14) ) )
| hskp4 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| ~ c3_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c1_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( c2_1(X17)
| ~ c0_1(X17)
| ~ c1_1(X17) ) ) )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c2_1(X19)
| ~ c1_1(X19)
| ~ c3_1(X19) ) )
| hskp6 )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( ~ c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21) ) )
| hskp7 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22) ) )
| hskp4
| hskp8 )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c2_1(X23)
| c3_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c3_1(X25)
| ~ c0_1(X25)
| ~ c1_1(X25) ) ) )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| c2_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c1_1(X28)
| c3_1(X28)
| ~ c0_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c2_1(X29)
| c3_1(X29) ) )
| hskp9
| hskp10 )
& ( ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c3_1(X31)
| ~ c1_1(X31) ) )
| hskp11 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| ~ c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c3_1(X33)
| ~ c2_1(X33) ) )
| hskp12 )
& ( ! [X34] :
( ndr1_0
=> ( c0_1(X34)
| c2_1(X34)
| ~ c3_1(X34) ) )
| ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| ~ c1_1(X35)
| ~ c2_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c3_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36) ) ) )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( c3_1(X39)
| ~ c1_1(X39)
| ~ c2_1(X39) ) ) )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| ~ c3_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( c2_1(X41)
| ~ c0_1(X41)
| ~ c1_1(X41) ) )
| hskp9 )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| ~ c3_1(X42) ) )
| hskp1
| hskp10 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c3_1(X43)
| ~ c1_1(X43) ) )
| ! [X44] :
( ndr1_0
=> ( c1_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c0_1(X45)
| ~ c2_1(X45)
| ~ c3_1(X45) ) ) )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c2_1(X47)
| c3_1(X47)
| ~ c1_1(X47) ) )
| hskp3 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48) ) )
| hskp13
| hskp6 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| c3_1(X49)
| ~ c2_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| ~ c1_1(X50)
| ~ c3_1(X50) ) )
| hskp14 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| c3_1(X51)
| ~ c2_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c2_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52) ) )
| ! [X53] :
( ndr1_0
=> ( c3_1(X53)
| ~ c0_1(X53)
| ~ c1_1(X53) ) ) )
& ( ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c1_1(X55)
| ~ c2_1(X55)
| ~ c3_1(X55) ) )
| hskp15 )
& ( ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| c3_1(X56)
| ~ c2_1(X56) ) )
| hskp0
| hskp5 )
& ( ! [X57] :
( ndr1_0
=> ( c0_1(X57)
| c3_1(X57)
| ~ c2_1(X57) ) )
| hskp13
| hskp16 )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| ~ c1_1(X58)
| ~ c2_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| ~ c0_1(X59)
| ~ c3_1(X59) ) )
| hskp14 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| ~ c1_1(X60)
| ~ c2_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| ~ c0_1(X61)
| ~ c3_1(X61) ) )
| hskp13 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| ~ c1_1(X62)
| ~ c2_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( c2_1(X63)
| c3_1(X63)
| ~ c1_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( c0_1(X65)
| ~ c1_1(X65)
| ~ c3_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c1_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66) ) )
| hskp8 )
& ( ! [X67] :
( ndr1_0
=> ( c0_1(X67)
| ~ c1_1(X67)
| ~ c3_1(X67) ) )
| hskp17
| hskp0 )
& ( ! [X68] :
( ndr1_0
=> ( c0_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68) ) )
| hskp14
| hskp18 )
& ( ! [X69] :
( ndr1_0
=> ( c0_1(X69)
| ~ c2_1(X69)
| ~ c3_1(X69) ) )
| ! [X70] :
( ndr1_0
=> ( ~ c0_1(X70)
| ~ c1_1(X70)
| ~ c2_1(X70) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( c0_1(X72)
| ~ c2_1(X72)
| ~ c3_1(X72) ) )
| hskp29
| hskp9 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| c2_1(X73)
| c3_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| c2_1(X74)
| ~ c0_1(X74) ) )
| hskp29 )
& ( ! [X75] :
( ndr1_0
=> ( c1_1(X75)
| c2_1(X75)
| c3_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) )
| hskp19 )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| c2_1(X77)
| c3_1(X77) ) )
| hskp20
| hskp2 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78) ) )
| ! [X79] :
( ndr1_0
=> ( c2_1(X79)
| c3_1(X79)
| ~ c1_1(X79) ) )
| hskp29 )
& ( ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80) ) )
| hskp20
| hskp1 )
& ( ! [X81] :
( ndr1_0
=> ( c1_1(X81)
| c2_1(X81)
| ~ c3_1(X81) ) )
| hskp21
| hskp18 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| c3_1(X82)
| ~ c0_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83) ) )
| hskp22 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| c3_1(X84)
| ~ c2_1(X84) ) )
| hskp0
| hskp21 )
& ( ! [X85] :
( ndr1_0
=> ( c1_1(X85)
| ~ c2_1(X85)
| ~ c3_1(X85) ) )
| ! [X86] :
( ndr1_0
=> ( ~ c0_1(X86)
| ~ c1_1(X86)
| ~ c3_1(X86) ) )
| hskp28 )
& ( ! [X87] :
( ndr1_0
=> ( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87) ) )
| ! [X88] :
( ndr1_0
=> ( c2_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89) ) ) )
& ( ! [X90] :
( ndr1_0
=> ( c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90) ) )
| ! [X91] :
( ndr1_0
=> ( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c3_1(X91) ) )
| hskp12 )
& ( ! [X92] :
( ndr1_0
=> ( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92) ) )
| hskp17
| hskp8 )
& ( ! [X93] :
( ndr1_0
=> ( c2_1(X93)
| c3_1(X93)
| ~ c1_1(X93) ) )
| hskp28
| hskp19 )
& ( ! [X94] :
( ndr1_0
=> ( c2_1(X94)
| c3_1(X94)
| ~ c1_1(X94) ) )
| hskp13
| hskp1 )
& ( ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| ! [X96] :
( ndr1_0
=> ( c2_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96) ) )
| hskp28 )
& ( ! [X97] :
( ndr1_0
=> ( c2_1(X97)
| ~ c0_1(X97)
| ~ c1_1(X97) ) )
| hskp4
| hskp28 )
& ( ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp9
| hskp20 )
& ( ! [X99] :
( ndr1_0
=> ( c3_1(X99)
| ~ c0_1(X99)
| ~ c1_1(X99) ) )
| hskp23
| hskp13 )
& ( ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c2_1(X100) ) )
| ! [X101] :
( ndr1_0
=> ( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101) ) )
| hskp5 )
& ( ! [X102] :
( ndr1_0
=> ( c3_1(X102)
| ~ c0_1(X102)
| ~ c2_1(X102) ) )
| hskp27
| hskp3 )
& ( ! [X103] :
( ndr1_0
=> ( ~ c0_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103) ) )
| hskp14
| hskp24 )
& ( ! [X104] :
( ndr1_0
=> ( ~ c0_1(X104)
| ~ c1_1(X104)
| ~ c3_1(X104) ) )
| hskp14
| hskp22 )
& ( ! [X105] :
( ndr1_0
=> ( ~ c0_1(X105)
| ~ c1_1(X105)
| ~ c3_1(X105) ) )
| hskp25
| hskp1 )
& ( ! [X106] :
( ndr1_0
=> ( ~ c0_1(X106)
| ~ c2_1(X106)
| ~ c3_1(X106) ) )
| hskp30
| hskp20 )
& ( ! [X107] :
( ndr1_0
=> ( ~ c0_1(X107)
| ~ c2_1(X107)
| ~ c3_1(X107) ) )
| hskp26
| hskp11 )
& ( ! [X108] :
( ndr1_0
=> ( ~ c0_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108) ) )
| hskp15
| hskp16 )
& ( ! [X109] :
( ndr1_0
=> ( ~ c1_1(X109)
| ~ c2_1(X109)
| ~ c3_1(X109) ) )
| hskp27
| hskp19 )
& ( ! [X110] :
( ndr1_0
=> ( ~ c1_1(X110)
| ~ c2_1(X110)
| ~ c3_1(X110) ) )
| hskp21
| hskp11 )
& ( hskp30
| hskp28
| hskp19 )
& ( hskp9
| hskp3
| hskp26 )
& ( hskp27
| hskp21
| hskp28 )
& ( hskp4
| hskp24
| hskp5 )
& ( hskp4
| hskp26
| hskp5 )
& ( hskp28
| hskp8
| hskp10 )
& ( hskp22
| hskp1
| hskp11 ) ),
inference(flattening,[],[f2]) ).
fof(f4,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a793)
& c2_1(a793)
& ~ c1_1(a793) ) )
& ( ~ hskp1
| ( ndr1_0
& c3_1(a794)
& ~ c0_1(a794)
& ~ c2_1(a794) ) )
& ( ~ hskp2
| ( ndr1_0
& ~ c0_1(a795)
& ~ c1_1(a795)
& ~ c3_1(a795) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a798)
& c2_1(a798)
& ~ c3_1(a798) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a799)
& c3_1(a799)
& ~ c1_1(a799) ) )
& ( ~ hskp5
| ( ndr1_0
& c3_1(a800)
& ~ c0_1(a800)
& ~ c1_1(a800) ) )
& ( ~ hskp6
| ( ndr1_0
& c2_1(a802)
& ~ c0_1(a802)
& ~ c1_1(a802) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a803)
& c3_1(a803)
& ~ c2_1(a803) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a805)
& ~ c2_1(a805)
& ~ c3_1(a805) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a806)
& c1_1(a806)
& ~ c3_1(a806) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a807)
& ~ c2_1(a807)
& ~ c3_1(a807) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a808)
& ~ c1_1(a808)
& ~ c2_1(a808) ) )
& ( ~ hskp12
| ( ndr1_0
& c1_1(a809)
& c2_1(a809)
& ~ c0_1(a809) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a814)
& ~ c0_1(a814)
& ~ c3_1(a814) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a816)
& ~ c1_1(a816)
& ~ c2_1(a816) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a817)
& c3_1(a817)
& ~ c1_1(a817) ) )
& ( ~ hskp16
| ( ndr1_0
& ~ c0_1(a821)
& ~ c1_1(a821)
& ~ c2_1(a821) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a825)
& c1_1(a825)
& ~ c2_1(a825) ) )
& ( ~ hskp18
| ( ndr1_0
& ~ c1_1(a828)
& ~ c2_1(a828)
& ~ c3_1(a828) ) )
& ( ~ hskp19
| ( ndr1_0
& c2_1(a832)
& ~ c1_1(a832)
& ~ c3_1(a832) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a833)
& ~ c0_1(a833)
& ~ c2_1(a833) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a838)
& c3_1(a838)
& ~ c2_1(a838) ) )
& ( ~ hskp22
| ( ndr1_0
& c1_1(a840)
& c3_1(a840)
& ~ c0_1(a840) ) )
& ( ~ hskp23
| ( ndr1_0
& c0_1(a856)
& ~ c2_1(a856)
& ~ c3_1(a856) ) )
& ( ~ hskp24
| ( ndr1_0
& c0_1(a862)
& ~ c1_1(a862)
& ~ c3_1(a862) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a865)
& c2_1(a865)
& ~ c3_1(a865) ) )
& ( ~ hskp26
| ( ndr1_0
& c2_1(a869)
& c3_1(a869)
& ~ c0_1(a869) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a796)
& c2_1(a796)
& c3_1(a796) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a797)
& c2_1(a797)
& c3_1(a797) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a829)
& c1_1(a829)
& c2_1(a829) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a867)
& c1_1(a867)
& c3_1(a867) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c3_1(X4)
| ~ c0_1(X4)
| ~ c2_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| hskp1
| hskp2 )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c3_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c0_1(X7)
| ~ c1_1(X7)
| ~ c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c1_1(X8)
| c3_1(X8)
| ~ c2_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| hskp27
| hskp28 )
& ( ! [X10] :
( c0_1(X10)
| c1_1(X10)
| c3_1(X10)
| ~ ndr1_0 )
| hskp3
| hskp4 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| ~ c3_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X13] :
( c0_1(X13)
| c1_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0 )
| ! [X14] :
( c1_1(X14)
| c3_1(X14)
| ~ c2_1(X14)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| ~ c3_1(X15)
| ~ ndr1_0 )
| ! [X16] :
( c1_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 )
| ! [X17] :
( c2_1(X17)
| ~ c0_1(X17)
| ~ c1_1(X17)
| ~ ndr1_0 ) )
& ( ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c2_1(X19)
| ~ c1_1(X19)
| ~ c3_1(X19)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( ~ c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0 )
| hskp4
| hskp8 )
& ( ! [X23] :
( c0_1(X23)
| c2_1(X23)
| c3_1(X23)
| ~ ndr1_0 )
| ! [X24] :
( c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( c3_1(X25)
| ~ c0_1(X25)
| ~ c1_1(X25)
| ~ ndr1_0 ) )
& ( ! [X26] :
( c0_1(X26)
| c2_1(X26)
| c3_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c1_1(X27)
| c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( c1_1(X28)
| c3_1(X28)
| ~ c0_1(X28)
| ~ ndr1_0 ) )
& ( ! [X29] :
( c0_1(X29)
| c2_1(X29)
| c3_1(X29)
| ~ ndr1_0 )
| hskp9
| hskp10 )
& ( ! [X30] :
( c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c0_1(X31)
| c3_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X32] :
( c0_1(X32)
| c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 )
| ! [X33] :
( c0_1(X33)
| c3_1(X33)
| ~ c2_1(X33)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X34] :
( c0_1(X34)
| c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| ! [X35] :
( c0_1(X35)
| ~ c1_1(X35)
| ~ c2_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c3_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0 ) )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c0_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38)
| ~ ndr1_0 )
| ! [X39] :
( c3_1(X39)
| ~ c1_1(X39)
| ~ c2_1(X39)
| ~ ndr1_0 ) )
& ( ! [X40] :
( c0_1(X40)
| c2_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0 )
| ! [X41] :
( c2_1(X41)
| ~ c0_1(X41)
| ~ c1_1(X41)
| ~ ndr1_0 )
| hskp9 )
& ( ! [X42] :
( c0_1(X42)
| c2_1(X42)
| ~ c3_1(X42)
| ~ ndr1_0 )
| hskp1
| hskp10 )
& ( ! [X43] :
( c0_1(X43)
| c3_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0 )
| ! [X44] :
( c1_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( ~ c0_1(X45)
| ~ c2_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 ) )
& ( ! [X46] :
( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c2_1(X47)
| c3_1(X47)
| ~ c1_1(X47)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X48] :
( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0 )
| hskp13
| hskp6 )
& ( ! [X49] :
( c0_1(X49)
| c3_1(X49)
| ~ c2_1(X49)
| ~ ndr1_0 )
| ! [X50] :
( c0_1(X50)
| ~ c1_1(X50)
| ~ c3_1(X50)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X51] :
( c0_1(X51)
| c3_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c2_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| ! [X53] :
( c3_1(X53)
| ~ c0_1(X53)
| ~ c1_1(X53)
| ~ ndr1_0 ) )
& ( ! [X54] :
( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54)
| ~ ndr1_0 )
| ! [X55] :
( ~ c1_1(X55)
| ~ c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0 )
| hskp15 )
& ( ! [X56] :
( c0_1(X56)
| c3_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0 )
| hskp0
| hskp5 )
& ( ! [X57] :
( c0_1(X57)
| c3_1(X57)
| ~ c2_1(X57)
| ~ ndr1_0 )
| hskp13
| hskp16 )
& ( ! [X58] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c2_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( c1_1(X59)
| ~ c0_1(X59)
| ~ c3_1(X59)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X60] :
( c0_1(X60)
| ~ c1_1(X60)
| ~ c2_1(X60)
| ~ ndr1_0 )
| ! [X61] :
( c1_1(X61)
| ~ c0_1(X61)
| ~ c3_1(X61)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X62] :
( c0_1(X62)
| ~ c1_1(X62)
| ~ c2_1(X62)
| ~ ndr1_0 )
| ! [X63] :
( c2_1(X63)
| c3_1(X63)
| ~ c1_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 ) )
& ( ! [X65] :
( c0_1(X65)
| ~ c1_1(X65)
| ~ c3_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c1_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X67] :
( c0_1(X67)
| ~ c1_1(X67)
| ~ c3_1(X67)
| ~ ndr1_0 )
| hskp17
| hskp0 )
& ( ! [X68] :
( c0_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| hskp14
| hskp18 )
& ( ! [X69] :
( c0_1(X69)
| ~ c2_1(X69)
| ~ c3_1(X69)
| ~ ndr1_0 )
| ! [X70] :
( ~ c0_1(X70)
| ~ c1_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0 )
| ! [X71] :
( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71)
| ~ ndr1_0 ) )
& ( ! [X72] :
( c0_1(X72)
| ~ c2_1(X72)
| ~ c3_1(X72)
| ~ ndr1_0 )
| hskp29
| hskp9 )
& ( ! [X73] :
( c1_1(X73)
| c2_1(X73)
| c3_1(X73)
| ~ ndr1_0 )
| ! [X74] :
( c1_1(X74)
| c2_1(X74)
| ~ c0_1(X74)
| ~ ndr1_0 )
| hskp29 )
& ( ! [X75] :
( c1_1(X75)
| c2_1(X75)
| c3_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 )
| hskp19 )
& ( ! [X77] :
( c1_1(X77)
| c2_1(X77)
| c3_1(X77)
| ~ ndr1_0 )
| hskp20
| hskp2 )
& ( ! [X78] :
( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78)
| ~ ndr1_0 )
| ! [X79] :
( c2_1(X79)
| c3_1(X79)
| ~ c1_1(X79)
| ~ ndr1_0 )
| hskp29 )
& ( ! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0 )
| hskp20
| hskp1 )
& ( ! [X81] :
( c1_1(X81)
| c2_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 )
| hskp21
| hskp18 )
& ( ! [X82] :
( c1_1(X82)
| c3_1(X82)
| ~ c0_1(X82)
| ~ ndr1_0 )
| ! [X83] :
( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X84] :
( c1_1(X84)
| c3_1(X84)
| ~ c2_1(X84)
| ~ ndr1_0 )
| hskp0
| hskp21 )
& ( ! [X85] :
( c1_1(X85)
| ~ c2_1(X85)
| ~ c3_1(X85)
| ~ ndr1_0 )
| ! [X86] :
( ~ c0_1(X86)
| ~ c1_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X87] :
( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0 )
| ! [X88] :
( c2_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c3_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0 ) )
& ( ! [X90] :
( c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90)
| ~ ndr1_0 )
| ! [X91] :
( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c3_1(X91)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X92] :
( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92)
| ~ ndr1_0 )
| hskp17
| hskp8 )
& ( ! [X93] :
( c2_1(X93)
| c3_1(X93)
| ~ c1_1(X93)
| ~ ndr1_0 )
| hskp28
| hskp19 )
& ( ! [X94] :
( c2_1(X94)
| c3_1(X94)
| ~ c1_1(X94)
| ~ ndr1_0 )
| hskp13
| hskp1 )
& ( ! [X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0 )
| ! [X96] :
( c2_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X97] :
( c2_1(X97)
| ~ c0_1(X97)
| ~ c1_1(X97)
| ~ ndr1_0 )
| hskp4
| hskp28 )
& ( ! [X98] :
( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| hskp9
| hskp20 )
& ( ! [X99] :
( c3_1(X99)
| ~ c0_1(X99)
| ~ c1_1(X99)
| ~ ndr1_0 )
| hskp23
| hskp13 )
& ( ! [X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c2_1(X100)
| ~ ndr1_0 )
| ! [X101] :
( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X102] :
( c3_1(X102)
| ~ c0_1(X102)
| ~ c2_1(X102)
| ~ ndr1_0 )
| hskp27
| hskp3 )
& ( ! [X103] :
( ~ c0_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp14
| hskp24 )
& ( ! [X104] :
( ~ c0_1(X104)
| ~ c1_1(X104)
| ~ c3_1(X104)
| ~ ndr1_0 )
| hskp14
| hskp22 )
& ( ! [X105] :
( ~ c0_1(X105)
| ~ c1_1(X105)
| ~ c3_1(X105)
| ~ ndr1_0 )
| hskp25
| hskp1 )
& ( ! [X106] :
( ~ c0_1(X106)
| ~ c2_1(X106)
| ~ c3_1(X106)
| ~ ndr1_0 )
| hskp30
| hskp20 )
& ( ! [X107] :
( ~ c0_1(X107)
| ~ c2_1(X107)
| ~ c3_1(X107)
| ~ ndr1_0 )
| hskp26
| hskp11 )
& ( ! [X108] :
( ~ c0_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108)
| ~ ndr1_0 )
| hskp15
| hskp16 )
& ( ! [X109] :
( ~ c1_1(X109)
| ~ c2_1(X109)
| ~ c3_1(X109)
| ~ ndr1_0 )
| hskp27
| hskp19 )
& ( ! [X110] :
( ~ c1_1(X110)
| ~ c2_1(X110)
| ~ c3_1(X110)
| ~ ndr1_0 )
| hskp21
| hskp11 )
& ( hskp30
| hskp28
| hskp19 )
& ( hskp9
| hskp3
| hskp26 )
& ( hskp27
| hskp21
| hskp28 )
& ( hskp4
| hskp24
| hskp5 )
& ( hskp4
| hskp26
| hskp5 )
& ( hskp28
| hskp8
| hskp10 )
& ( hskp22
| hskp1
| hskp11 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a793)
& c2_1(a793)
& ~ c1_1(a793) ) )
& ( ~ hskp1
| ( ndr1_0
& c3_1(a794)
& ~ c0_1(a794)
& ~ c2_1(a794) ) )
& ( ~ hskp2
| ( ndr1_0
& ~ c0_1(a795)
& ~ c1_1(a795)
& ~ c3_1(a795) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a798)
& c2_1(a798)
& ~ c3_1(a798) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a799)
& c3_1(a799)
& ~ c1_1(a799) ) )
& ( ~ hskp5
| ( ndr1_0
& c3_1(a800)
& ~ c0_1(a800)
& ~ c1_1(a800) ) )
& ( ~ hskp6
| ( ndr1_0
& c2_1(a802)
& ~ c0_1(a802)
& ~ c1_1(a802) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a803)
& c3_1(a803)
& ~ c2_1(a803) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a805)
& ~ c2_1(a805)
& ~ c3_1(a805) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a806)
& c1_1(a806)
& ~ c3_1(a806) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a807)
& ~ c2_1(a807)
& ~ c3_1(a807) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a808)
& ~ c1_1(a808)
& ~ c2_1(a808) ) )
& ( ~ hskp12
| ( ndr1_0
& c1_1(a809)
& c2_1(a809)
& ~ c0_1(a809) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a814)
& ~ c0_1(a814)
& ~ c3_1(a814) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a816)
& ~ c1_1(a816)
& ~ c2_1(a816) ) )
& ( ~ hskp15
| ( ndr1_0
& c2_1(a817)
& c3_1(a817)
& ~ c1_1(a817) ) )
& ( ~ hskp16
| ( ndr1_0
& ~ c0_1(a821)
& ~ c1_1(a821)
& ~ c2_1(a821) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a825)
& c1_1(a825)
& ~ c2_1(a825) ) )
& ( ~ hskp18
| ( ndr1_0
& ~ c1_1(a828)
& ~ c2_1(a828)
& ~ c3_1(a828) ) )
& ( ~ hskp19
| ( ndr1_0
& c2_1(a832)
& ~ c1_1(a832)
& ~ c3_1(a832) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a833)
& ~ c0_1(a833)
& ~ c2_1(a833) ) )
& ( ~ hskp21
| ( ndr1_0
& c0_1(a838)
& c3_1(a838)
& ~ c2_1(a838) ) )
& ( ~ hskp22
| ( ndr1_0
& c1_1(a840)
& c3_1(a840)
& ~ c0_1(a840) ) )
& ( ~ hskp23
| ( ndr1_0
& c0_1(a856)
& ~ c2_1(a856)
& ~ c3_1(a856) ) )
& ( ~ hskp24
| ( ndr1_0
& c0_1(a862)
& ~ c1_1(a862)
& ~ c3_1(a862) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a865)
& c2_1(a865)
& ~ c3_1(a865) ) )
& ( ~ hskp26
| ( ndr1_0
& c2_1(a869)
& c3_1(a869)
& ~ c0_1(a869) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a796)
& c2_1(a796)
& c3_1(a796) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a797)
& c2_1(a797)
& c3_1(a797) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a829)
& c1_1(a829)
& c2_1(a829) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a867)
& c1_1(a867)
& c3_1(a867) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c3_1(X4)
| ~ c0_1(X4)
| ~ c2_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| hskp1
| hskp2 )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c3_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c0_1(X7)
| ~ c1_1(X7)
| ~ c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c1_1(X8)
| c3_1(X8)
| ~ c2_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| hskp27
| hskp28 )
& ( ! [X10] :
( c0_1(X10)
| c1_1(X10)
| c3_1(X10)
| ~ ndr1_0 )
| hskp3
| hskp4 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| ~ c3_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c0_1(X12)
| c3_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X13] :
( c0_1(X13)
| c1_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0 )
| ! [X14] :
( c1_1(X14)
| c3_1(X14)
| ~ c2_1(X14)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| ~ c3_1(X15)
| ~ ndr1_0 )
| ! [X16] :
( c1_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 )
| ! [X17] :
( c2_1(X17)
| ~ c0_1(X17)
| ~ c1_1(X17)
| ~ ndr1_0 ) )
& ( ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c2_1(X19)
| ~ c1_1(X19)
| ~ c3_1(X19)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( ~ c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0 )
| hskp4
| hskp8 )
& ( ! [X23] :
( c0_1(X23)
| c2_1(X23)
| c3_1(X23)
| ~ ndr1_0 )
| ! [X24] :
( c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( c3_1(X25)
| ~ c0_1(X25)
| ~ c1_1(X25)
| ~ ndr1_0 ) )
& ( ! [X26] :
( c0_1(X26)
| c2_1(X26)
| c3_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c1_1(X27)
| c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( c1_1(X28)
| c3_1(X28)
| ~ c0_1(X28)
| ~ ndr1_0 ) )
& ( ! [X29] :
( c0_1(X29)
| c2_1(X29)
| c3_1(X29)
| ~ ndr1_0 )
| hskp9
| hskp10 )
& ( ! [X30] :
( c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c0_1(X31)
| c3_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X32] :
( c0_1(X32)
| c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 )
| ! [X33] :
( c0_1(X33)
| c3_1(X33)
| ~ c2_1(X33)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X34] :
( c0_1(X34)
| c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| ! [X35] :
( c0_1(X35)
| ~ c1_1(X35)
| ~ c2_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c3_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0 ) )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c0_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38)
| ~ ndr1_0 )
| ! [X39] :
( c3_1(X39)
| ~ c1_1(X39)
| ~ c2_1(X39)
| ~ ndr1_0 ) )
& ( ! [X40] :
( c0_1(X40)
| c2_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0 )
| ! [X41] :
( c2_1(X41)
| ~ c0_1(X41)
| ~ c1_1(X41)
| ~ ndr1_0 )
| hskp9 )
& ( ! [X42] :
( c0_1(X42)
| c2_1(X42)
| ~ c3_1(X42)
| ~ ndr1_0 )
| hskp1
| hskp10 )
& ( ! [X43] :
( c0_1(X43)
| c3_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0 )
| ! [X44] :
( c1_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( ~ c0_1(X45)
| ~ c2_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 ) )
& ( ! [X46] :
( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c2_1(X47)
| c3_1(X47)
| ~ c1_1(X47)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X48] :
( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0 )
| hskp13
| hskp6 )
& ( ! [X49] :
( c0_1(X49)
| c3_1(X49)
| ~ c2_1(X49)
| ~ ndr1_0 )
| ! [X50] :
( c0_1(X50)
| ~ c1_1(X50)
| ~ c3_1(X50)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X51] :
( c0_1(X51)
| c3_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c2_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| ! [X53] :
( c3_1(X53)
| ~ c0_1(X53)
| ~ c1_1(X53)
| ~ ndr1_0 ) )
& ( ! [X54] :
( c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54)
| ~ ndr1_0 )
| ! [X55] :
( ~ c1_1(X55)
| ~ c2_1(X55)
| ~ c3_1(X55)
| ~ ndr1_0 )
| hskp15 )
& ( ! [X56] :
( c0_1(X56)
| c3_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0 )
| hskp0
| hskp5 )
& ( ! [X57] :
( c0_1(X57)
| c3_1(X57)
| ~ c2_1(X57)
| ~ ndr1_0 )
| hskp13
| hskp16 )
& ( ! [X58] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c2_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( c1_1(X59)
| ~ c0_1(X59)
| ~ c3_1(X59)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X60] :
( c0_1(X60)
| ~ c1_1(X60)
| ~ c2_1(X60)
| ~ ndr1_0 )
| ! [X61] :
( c1_1(X61)
| ~ c0_1(X61)
| ~ c3_1(X61)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X62] :
( c0_1(X62)
| ~ c1_1(X62)
| ~ c2_1(X62)
| ~ ndr1_0 )
| ! [X63] :
( c2_1(X63)
| c3_1(X63)
| ~ c1_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 ) )
& ( ! [X65] :
( c0_1(X65)
| ~ c1_1(X65)
| ~ c3_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c1_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X67] :
( c0_1(X67)
| ~ c1_1(X67)
| ~ c3_1(X67)
| ~ ndr1_0 )
| hskp17
| hskp0 )
& ( ! [X68] :
( c0_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| hskp14
| hskp18 )
& ( ! [X69] :
( c0_1(X69)
| ~ c2_1(X69)
| ~ c3_1(X69)
| ~ ndr1_0 )
| ! [X70] :
( ~ c0_1(X70)
| ~ c1_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0 )
| ! [X71] :
( ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71)
| ~ ndr1_0 ) )
& ( ! [X72] :
( c0_1(X72)
| ~ c2_1(X72)
| ~ c3_1(X72)
| ~ ndr1_0 )
| hskp29
| hskp9 )
& ( ! [X73] :
( c1_1(X73)
| c2_1(X73)
| c3_1(X73)
| ~ ndr1_0 )
| ! [X74] :
( c1_1(X74)
| c2_1(X74)
| ~ c0_1(X74)
| ~ ndr1_0 )
| hskp29 )
& ( ! [X75] :
( c1_1(X75)
| c2_1(X75)
| c3_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 )
| hskp19 )
& ( ! [X77] :
( c1_1(X77)
| c2_1(X77)
| c3_1(X77)
| ~ ndr1_0 )
| hskp20
| hskp2 )
& ( ! [X78] :
( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78)
| ~ ndr1_0 )
| ! [X79] :
( c2_1(X79)
| c3_1(X79)
| ~ c1_1(X79)
| ~ ndr1_0 )
| hskp29 )
& ( ! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0 )
| hskp20
| hskp1 )
& ( ! [X81] :
( c1_1(X81)
| c2_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 )
| hskp21
| hskp18 )
& ( ! [X82] :
( c1_1(X82)
| c3_1(X82)
| ~ c0_1(X82)
| ~ ndr1_0 )
| ! [X83] :
( ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X84] :
( c1_1(X84)
| c3_1(X84)
| ~ c2_1(X84)
| ~ ndr1_0 )
| hskp0
| hskp21 )
& ( ! [X85] :
( c1_1(X85)
| ~ c2_1(X85)
| ~ c3_1(X85)
| ~ ndr1_0 )
| ! [X86] :
( ~ c0_1(X86)
| ~ c1_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X87] :
( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0 )
| ! [X88] :
( c2_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c3_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0 ) )
& ( ! [X90] :
( c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90)
| ~ ndr1_0 )
| ! [X91] :
( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c3_1(X91)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X92] :
( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92)
| ~ ndr1_0 )
| hskp17
| hskp8 )
& ( ! [X93] :
( c2_1(X93)
| c3_1(X93)
| ~ c1_1(X93)
| ~ ndr1_0 )
| hskp28
| hskp19 )
& ( ! [X94] :
( c2_1(X94)
| c3_1(X94)
| ~ c1_1(X94)
| ~ ndr1_0 )
| hskp13
| hskp1 )
& ( ! [X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0 )
| ! [X96] :
( c2_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X97] :
( c2_1(X97)
| ~ c0_1(X97)
| ~ c1_1(X97)
| ~ ndr1_0 )
| hskp4
| hskp28 )
& ( ! [X98] :
( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| hskp9
| hskp20 )
& ( ! [X99] :
( c3_1(X99)
| ~ c0_1(X99)
| ~ c1_1(X99)
| ~ ndr1_0 )
| hskp23
| hskp13 )
& ( ! [X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c2_1(X100)
| ~ ndr1_0 )
| ! [X101] :
( ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X102] :
( c3_1(X102)
| ~ c0_1(X102)
| ~ c2_1(X102)
| ~ ndr1_0 )
| hskp27
| hskp3 )
& ( ! [X103] :
( ~ c0_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp14
| hskp24 )
& ( ! [X104] :
( ~ c0_1(X104)
| ~ c1_1(X104)
| ~ c3_1(X104)
| ~ ndr1_0 )
| hskp14
| hskp22 )
& ( ! [X105] :
( ~ c0_1(X105)
| ~ c1_1(X105)
| ~ c3_1(X105)
| ~ ndr1_0 )
| hskp25
| hskp1 )
& ( ! [X106] :
( ~ c0_1(X106)
| ~ c2_1(X106)
| ~ c3_1(X106)
| ~ ndr1_0 )
| hskp30
| hskp20 )
& ( ! [X107] :
( ~ c0_1(X107)
| ~ c2_1(X107)
| ~ c3_1(X107)
| ~ ndr1_0 )
| hskp26
| hskp11 )
& ( ! [X108] :
( ~ c0_1(X108)
| ~ c2_1(X108)
| ~ c3_1(X108)
| ~ ndr1_0 )
| hskp15
| hskp16 )
& ( ! [X109] :
( ~ c1_1(X109)
| ~ c2_1(X109)
| ~ c3_1(X109)
| ~ ndr1_0 )
| hskp27
| hskp19 )
& ( ! [X110] :
( ~ c1_1(X110)
| ~ c2_1(X110)
| ~ c3_1(X110)
| ~ ndr1_0 )
| hskp21
| hskp11 )
& ( hskp30
| hskp28
| hskp19 )
& ( hskp9
| hskp3
| hskp26 )
& ( hskp27
| hskp21
| hskp28 )
& ( hskp4
| hskp24
| hskp5 )
& ( hskp4
| hskp26
| hskp5 )
& ( hskp28
| hskp8
| hskp10 )
& ( hskp22
| hskp1
| hskp11 ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
( hskp22
| hskp1
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f7,plain,
( hskp28
| hskp8
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f8,plain,
( hskp4
| hskp26
| hskp5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f10,plain,
( hskp27
| hskp21
| hskp28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f11,plain,
( hskp9
| hskp3
| hskp26 ),
inference(cnf_transformation,[],[f5]) ).
fof(f12,plain,
( hskp30
| hskp28
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f13,plain,
! [X110] :
( ~ c1_1(X110)
| ~ c2_1(X110)
| ~ c3_1(X110)
| ~ ndr1_0
| hskp21
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f16,plain,
! [X107] :
( ~ c0_1(X107)
| ~ c2_1(X107)
| ~ c3_1(X107)
| ~ ndr1_0
| hskp26
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f17,plain,
! [X106] :
( ~ c0_1(X106)
| ~ c2_1(X106)
| ~ c3_1(X106)
| ~ ndr1_0
| hskp30
| hskp20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f18,plain,
! [X105] :
( ~ c0_1(X105)
| ~ c1_1(X105)
| ~ c3_1(X105)
| ~ ndr1_0
| hskp25
| hskp1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f19,plain,
! [X104] :
( ~ c0_1(X104)
| ~ c1_1(X104)
| ~ c3_1(X104)
| ~ ndr1_0
| hskp14
| hskp22 ),
inference(cnf_transformation,[],[f5]) ).
fof(f22,plain,
! [X101,X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c2_1(X100)
| ~ ndr1_0
| ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101)
| ~ ndr1_0
| hskp5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f24,plain,
! [X98] :
( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0
| hskp9
| hskp20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f25,plain,
! [X97] :
( c2_1(X97)
| ~ c0_1(X97)
| ~ c1_1(X97)
| ~ ndr1_0
| hskp4
| hskp28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f26,plain,
! [X96,X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0
| c2_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0
| hskp28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f30,plain,
! [X90,X91] :
( c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90)
| ~ ndr1_0
| ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c3_1(X91)
| ~ ndr1_0
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f31,plain,
! [X88,X89,X87] :
( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0
| c2_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0
| c3_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f34,plain,
! [X82,X83] :
( c1_1(X82)
| c3_1(X82)
| ~ c0_1(X82)
| ~ ndr1_0
| ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0
| hskp22 ),
inference(cnf_transformation,[],[f5]) ).
fof(f35,plain,
! [X81] :
( c1_1(X81)
| c2_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0
| hskp21
| hskp18 ),
inference(cnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c0_1(X80)
| ~ ndr1_0
| hskp20
| hskp1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f37,plain,
! [X78,X79] :
( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78)
| ~ ndr1_0
| c2_1(X79)
| c3_1(X79)
| ~ c1_1(X79)
| ~ ndr1_0
| hskp29 ),
inference(cnf_transformation,[],[f5]) ).
fof(f39,plain,
! [X76,X75] :
( c1_1(X75)
| c2_1(X75)
| c3_1(X75)
| ~ ndr1_0
| c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f40,plain,
! [X73,X74] :
( c1_1(X73)
| c2_1(X73)
| c3_1(X73)
| ~ ndr1_0
| c1_1(X74)
| c2_1(X74)
| ~ c0_1(X74)
| ~ ndr1_0
| hskp29 ),
inference(cnf_transformation,[],[f5]) ).
fof(f41,plain,
! [X72] :
( c0_1(X72)
| ~ c2_1(X72)
| ~ c3_1(X72)
| ~ ndr1_0
| hskp29
| hskp9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f42,plain,
! [X70,X71,X69] :
( c0_1(X69)
| ~ c2_1(X69)
| ~ c3_1(X69)
| ~ ndr1_0
| ~ c0_1(X70)
| ~ c1_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0
| ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f43,plain,
! [X68] :
( c0_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0
| hskp14
| hskp18 ),
inference(cnf_transformation,[],[f5]) ).
fof(f45,plain,
! [X65,X66] :
( c0_1(X65)
| ~ c1_1(X65)
| ~ c3_1(X65)
| ~ ndr1_0
| c1_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f46,plain,
! [X62,X63,X64] :
( c0_1(X62)
| ~ c1_1(X62)
| ~ c2_1(X62)
| ~ ndr1_0
| c2_1(X63)
| c3_1(X63)
| ~ c1_1(X63)
| ~ ndr1_0
| c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f47,plain,
! [X60,X61] :
( c0_1(X60)
| ~ c1_1(X60)
| ~ c2_1(X60)
| ~ ndr1_0
| c1_1(X61)
| ~ c0_1(X61)
| ~ c3_1(X61)
| ~ ndr1_0
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f48,plain,
! [X58,X59] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c2_1(X58)
| ~ ndr1_0
| c1_1(X59)
| ~ c0_1(X59)
| ~ c3_1(X59)
| ~ ndr1_0
| hskp14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f52,plain,
! [X51,X52,X53] :
( c0_1(X51)
| c3_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0
| c2_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0
| c3_1(X53)
| ~ c0_1(X53)
| ~ c1_1(X53)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f53,plain,
! [X50,X49] :
( c0_1(X49)
| c3_1(X49)
| ~ c2_1(X49)
| ~ ndr1_0
| c0_1(X50)
| ~ c1_1(X50)
| ~ c3_1(X50)
| ~ ndr1_0
| hskp14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f55,plain,
! [X46,X47] :
( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0
| c2_1(X47)
| c3_1(X47)
| ~ c1_1(X47)
| ~ ndr1_0
| hskp3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f56,plain,
! [X44,X45,X43] :
( c0_1(X43)
| c3_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0
| c1_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0
| ~ c0_1(X45)
| ~ c2_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f57,plain,
! [X42] :
( c0_1(X42)
| c2_1(X42)
| ~ c3_1(X42)
| ~ ndr1_0
| hskp1
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f58,plain,
! [X40,X41] :
( c0_1(X40)
| c2_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0
| c2_1(X41)
| ~ c0_1(X41)
| ~ c1_1(X41)
| ~ ndr1_0
| hskp9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f59,plain,
! [X38,X39,X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0
| c0_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38)
| ~ ndr1_0
| c3_1(X39)
| ~ c1_1(X39)
| ~ c2_1(X39)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f60,plain,
! [X36,X34,X35] :
( c0_1(X34)
| c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0
| c0_1(X35)
| ~ c1_1(X35)
| ~ c2_1(X35)
| ~ ndr1_0
| c3_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f61,plain,
! [X32,X33] :
( c0_1(X32)
| c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0
| c0_1(X33)
| c3_1(X33)
| ~ c2_1(X33)
| ~ ndr1_0
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f62,plain,
! [X31,X30] :
( c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0
| c0_1(X31)
| c3_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f63,plain,
! [X29] :
( c0_1(X29)
| c2_1(X29)
| c3_1(X29)
| ~ ndr1_0
| hskp9
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f64,plain,
! [X28,X26,X27] :
( c0_1(X26)
| c2_1(X26)
| c3_1(X26)
| ~ ndr1_0
| c1_1(X27)
| c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0
| c1_1(X28)
| c3_1(X28)
| ~ c0_1(X28)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f65,plain,
! [X24,X25,X23] :
( c0_1(X23)
| c2_1(X23)
| c3_1(X23)
| ~ ndr1_0
| c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0
| c3_1(X25)
| ~ c0_1(X25)
| ~ c1_1(X25)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f67,plain,
! [X21,X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20)
| ~ ndr1_0
| ~ c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0
| hskp7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f68,plain,
! [X18,X19] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0
| c2_1(X19)
| ~ c1_1(X19)
| ~ c3_1(X19)
| ~ ndr1_0
| hskp6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f70,plain,
! [X14,X13] :
( c0_1(X13)
| c1_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0
| c1_1(X14)
| c3_1(X14)
| ~ c2_1(X14)
| ~ ndr1_0
| hskp4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f78,plain,
( ~ hskp30
| c3_1(a867) ),
inference(cnf_transformation,[],[f5]) ).
fof(f79,plain,
( ~ hskp30
| c1_1(a867) ),
inference(cnf_transformation,[],[f5]) ).
fof(f80,plain,
( ~ hskp30
| c0_1(a867) ),
inference(cnf_transformation,[],[f5]) ).
fof(f82,plain,
( ~ hskp29
| c2_1(a829) ),
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
( ~ hskp29
| c1_1(a829) ),
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
( ~ hskp29
| c0_1(a829) ),
inference(cnf_transformation,[],[f5]) ).
fof(f86,plain,
( ~ hskp28
| c3_1(a797) ),
inference(cnf_transformation,[],[f5]) ).
fof(f87,plain,
( ~ hskp28
| c2_1(a797) ),
inference(cnf_transformation,[],[f5]) ).
fof(f88,plain,
( ~ hskp28
| c1_1(a797) ),
inference(cnf_transformation,[],[f5]) ).
fof(f90,plain,
( ~ hskp27
| c3_1(a796) ),
inference(cnf_transformation,[],[f5]) ).
fof(f91,plain,
( ~ hskp27
| c2_1(a796) ),
inference(cnf_transformation,[],[f5]) ).
fof(f92,plain,
( ~ hskp27
| c0_1(a796) ),
inference(cnf_transformation,[],[f5]) ).
fof(f94,plain,
( ~ hskp26
| ~ c0_1(a869) ),
inference(cnf_transformation,[],[f5]) ).
fof(f95,plain,
( ~ hskp26
| c3_1(a869) ),
inference(cnf_transformation,[],[f5]) ).
fof(f96,plain,
( ~ hskp26
| c2_1(a869) ),
inference(cnf_transformation,[],[f5]) ).
fof(f98,plain,
( ~ hskp25
| ~ c3_1(a865) ),
inference(cnf_transformation,[],[f5]) ).
fof(f99,plain,
( ~ hskp25
| c2_1(a865) ),
inference(cnf_transformation,[],[f5]) ).
fof(f100,plain,
( ~ hskp25
| c1_1(a865) ),
inference(cnf_transformation,[],[f5]) ).
fof(f110,plain,
( ~ hskp22
| ~ c0_1(a840) ),
inference(cnf_transformation,[],[f5]) ).
fof(f111,plain,
( ~ hskp22
| c3_1(a840) ),
inference(cnf_transformation,[],[f5]) ).
fof(f112,plain,
( ~ hskp22
| c1_1(a840) ),
inference(cnf_transformation,[],[f5]) ).
fof(f113,plain,
( ~ hskp22
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f114,plain,
( ~ hskp21
| ~ c2_1(a838) ),
inference(cnf_transformation,[],[f5]) ).
fof(f115,plain,
( ~ hskp21
| c3_1(a838) ),
inference(cnf_transformation,[],[f5]) ).
fof(f116,plain,
( ~ hskp21
| c0_1(a838) ),
inference(cnf_transformation,[],[f5]) ).
fof(f118,plain,
( ~ hskp20
| ~ c2_1(a833) ),
inference(cnf_transformation,[],[f5]) ).
fof(f119,plain,
( ~ hskp20
| ~ c0_1(a833) ),
inference(cnf_transformation,[],[f5]) ).
fof(f120,plain,
( ~ hskp20
| c1_1(a833) ),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
( ~ hskp19
| ~ c3_1(a832) ),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
( ~ hskp19
| ~ c1_1(a832) ),
inference(cnf_transformation,[],[f5]) ).
fof(f124,plain,
( ~ hskp19
| c2_1(a832) ),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
( ~ hskp18
| ~ c3_1(a828) ),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
( ~ hskp18
| ~ c2_1(a828) ),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
( ~ hskp18
| ~ c1_1(a828) ),
inference(cnf_transformation,[],[f5]) ).
fof(f142,plain,
( ~ hskp14
| ~ c2_1(a816) ),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
( ~ hskp14
| ~ c1_1(a816) ),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
( ~ hskp14
| c0_1(a816) ),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
( ~ hskp13
| ~ c3_1(a814) ),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
( ~ hskp13
| ~ c0_1(a814) ),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
( ~ hskp13
| c1_1(a814) ),
inference(cnf_transformation,[],[f5]) ).
fof(f150,plain,
( ~ hskp12
| ~ c0_1(a809) ),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
( ~ hskp12
| c2_1(a809) ),
inference(cnf_transformation,[],[f5]) ).
fof(f152,plain,
( ~ hskp12
| c1_1(a809) ),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
( ~ hskp11
| ~ c2_1(a808) ),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
( ~ hskp11
| ~ c1_1(a808) ),
inference(cnf_transformation,[],[f5]) ).
fof(f156,plain,
( ~ hskp11
| c3_1(a808) ),
inference(cnf_transformation,[],[f5]) ).
fof(f157,plain,
( ~ hskp11
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( ~ hskp10
| ~ c3_1(a807) ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( ~ hskp10
| ~ c2_1(a807) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( ~ hskp10
| ~ c0_1(a807) ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( ~ hskp9
| ~ c3_1(a806) ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( ~ hskp9
| c1_1(a806) ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( ~ hskp9
| c0_1(a806) ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( ~ hskp8
| ~ c3_1(a805) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( ~ hskp8
| ~ c2_1(a805) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( ~ hskp8
| c1_1(a805) ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( ~ hskp7
| ~ c2_1(a803) ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( ~ hskp7
| c3_1(a803) ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( ~ hskp7
| c1_1(a803) ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( ~ hskp6
| ~ c0_1(a802) ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( ~ hskp6
| c2_1(a802) ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( ~ hskp5
| ~ c1_1(a800) ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( ~ hskp5
| ~ c0_1(a800) ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( ~ hskp5
| c3_1(a800) ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( ~ hskp4
| ~ c1_1(a799) ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( ~ hskp4
| c3_1(a799) ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( ~ hskp4
| c0_1(a799) ),
inference(cnf_transformation,[],[f5]) ).
fof(f186,plain,
( ~ hskp3
| ~ c3_1(a798) ),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
( ~ hskp3
| c2_1(a798) ),
inference(cnf_transformation,[],[f5]) ).
fof(f188,plain,
( ~ hskp3
| c0_1(a798) ),
inference(cnf_transformation,[],[f5]) ).
fof(f194,plain,
( ~ hskp1
| ~ c2_1(a794) ),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
( ~ hskp1
| ~ c0_1(a794) ),
inference(cnf_transformation,[],[f5]) ).
fof(f196,plain,
( ~ hskp1
| c3_1(a794) ),
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
( ~ hskp1
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
! [X101,X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c2_1(X100)
| ~ ndr1_0
| ~ c0_1(X101)
| ~ c1_1(X101)
| ~ c3_1(X101)
| hskp5 ),
inference(duplicate_literal_removal,[],[f22]) ).
fof(f203,plain,
! [X96,X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0
| c2_1(X96)
| ~ c0_1(X96)
| ~ c3_1(X96)
| hskp28 ),
inference(duplicate_literal_removal,[],[f26]) ).
fof(f204,plain,
! [X90,X91] :
( c2_1(X90)
| c3_1(X90)
| ~ c1_1(X90)
| ~ ndr1_0
| ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c3_1(X91)
| hskp12 ),
inference(duplicate_literal_removal,[],[f30]) ).
fof(f205,plain,
! [X88,X89,X87] :
( c2_1(X87)
| c3_1(X87)
| ~ c1_1(X87)
| ~ ndr1_0
| c2_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88)
| c3_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89) ),
inference(duplicate_literal_removal,[],[f31]) ).
fof(f207,plain,
! [X82,X83] :
( c1_1(X82)
| c3_1(X82)
| ~ c0_1(X82)
| ~ ndr1_0
| ~ c0_1(X83)
| ~ c1_1(X83)
| ~ c3_1(X83)
| hskp22 ),
inference(duplicate_literal_removal,[],[f34]) ).
fof(f208,plain,
! [X78,X79] :
( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78)
| ~ ndr1_0
| c2_1(X79)
| c3_1(X79)
| ~ c1_1(X79)
| hskp29 ),
inference(duplicate_literal_removal,[],[f37]) ).
fof(f209,plain,
! [X76,X75] :
( c1_1(X75)
| c2_1(X75)
| c3_1(X75)
| ~ ndr1_0
| c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| hskp19 ),
inference(duplicate_literal_removal,[],[f39]) ).
fof(f210,plain,
! [X73,X74] :
( c1_1(X73)
| c2_1(X73)
| c3_1(X73)
| ~ ndr1_0
| c1_1(X74)
| c2_1(X74)
| ~ c0_1(X74)
| hskp29 ),
inference(duplicate_literal_removal,[],[f40]) ).
fof(f211,plain,
! [X70,X71,X69] :
( c0_1(X69)
| ~ c2_1(X69)
| ~ c3_1(X69)
| ~ ndr1_0
| ~ c0_1(X70)
| ~ c1_1(X70)
| ~ c2_1(X70)
| ~ c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71) ),
inference(duplicate_literal_removal,[],[f42]) ).
fof(f212,plain,
! [X65,X66] :
( c0_1(X65)
| ~ c1_1(X65)
| ~ c3_1(X65)
| ~ ndr1_0
| c1_1(X66)
| ~ c2_1(X66)
| ~ c3_1(X66)
| hskp8 ),
inference(duplicate_literal_removal,[],[f45]) ).
fof(f213,plain,
! [X62,X63,X64] :
( c0_1(X62)
| ~ c1_1(X62)
| ~ c2_1(X62)
| ~ ndr1_0
| c2_1(X63)
| c3_1(X63)
| ~ c1_1(X63)
| c2_1(X64)
| ~ c0_1(X64)
| ~ c1_1(X64) ),
inference(duplicate_literal_removal,[],[f46]) ).
fof(f214,plain,
! [X60,X61] :
( c0_1(X60)
| ~ c1_1(X60)
| ~ c2_1(X60)
| ~ ndr1_0
| c1_1(X61)
| ~ c0_1(X61)
| ~ c3_1(X61)
| hskp13 ),
inference(duplicate_literal_removal,[],[f47]) ).
fof(f215,plain,
! [X58,X59] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c2_1(X58)
| ~ ndr1_0
| c1_1(X59)
| ~ c0_1(X59)
| ~ c3_1(X59)
| hskp14 ),
inference(duplicate_literal_removal,[],[f48]) ).
fof(f217,plain,
! [X51,X52,X53] :
( c0_1(X51)
| c3_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0
| c2_1(X52)
| ~ c1_1(X52)
| ~ c3_1(X52)
| c3_1(X53)
| ~ c0_1(X53)
| ~ c1_1(X53) ),
inference(duplicate_literal_removal,[],[f52]) ).
fof(f218,plain,
! [X50,X49] :
( c0_1(X49)
| c3_1(X49)
| ~ c2_1(X49)
| ~ ndr1_0
| c0_1(X50)
| ~ c1_1(X50)
| ~ c3_1(X50)
| hskp14 ),
inference(duplicate_literal_removal,[],[f53]) ).
fof(f219,plain,
! [X46,X47] :
( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0
| c2_1(X47)
| c3_1(X47)
| ~ c1_1(X47)
| hskp3 ),
inference(duplicate_literal_removal,[],[f55]) ).
fof(f220,plain,
! [X44,X45,X43] :
( c0_1(X43)
| c3_1(X43)
| ~ c1_1(X43)
| ~ ndr1_0
| c1_1(X44)
| ~ c2_1(X44)
| ~ c3_1(X44)
| ~ c0_1(X45)
| ~ c2_1(X45)
| ~ c3_1(X45) ),
inference(duplicate_literal_removal,[],[f56]) ).
fof(f221,plain,
! [X40,X41] :
( c0_1(X40)
| c2_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0
| c2_1(X41)
| ~ c0_1(X41)
| ~ c1_1(X41)
| hskp9 ),
inference(duplicate_literal_removal,[],[f58]) ).
fof(f222,plain,
! [X38,X39,X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0
| c0_1(X38)
| ~ c1_1(X38)
| ~ c3_1(X38)
| c3_1(X39)
| ~ c1_1(X39)
| ~ c2_1(X39) ),
inference(duplicate_literal_removal,[],[f59]) ).
fof(f223,plain,
! [X36,X34,X35] :
( c0_1(X34)
| c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0
| c0_1(X35)
| ~ c1_1(X35)
| ~ c2_1(X35)
| c3_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36) ),
inference(duplicate_literal_removal,[],[f60]) ).
fof(f224,plain,
! [X32,X33] :
( c0_1(X32)
| c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0
| c0_1(X33)
| c3_1(X33)
| ~ c2_1(X33)
| hskp12 ),
inference(duplicate_literal_removal,[],[f61]) ).
fof(f225,plain,
! [X31,X30] :
( c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0
| c0_1(X31)
| c3_1(X31)
| ~ c1_1(X31)
| hskp11 ),
inference(duplicate_literal_removal,[],[f62]) ).
fof(f226,plain,
! [X28,X26,X27] :
( c0_1(X26)
| c2_1(X26)
| c3_1(X26)
| ~ ndr1_0
| c1_1(X27)
| c2_1(X27)
| ~ c3_1(X27)
| c1_1(X28)
| c3_1(X28)
| ~ c0_1(X28) ),
inference(duplicate_literal_removal,[],[f64]) ).
fof(f227,plain,
! [X24,X25,X23] :
( c0_1(X23)
| c2_1(X23)
| c3_1(X23)
| ~ ndr1_0
| c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24)
| c3_1(X25)
| ~ c0_1(X25)
| ~ c1_1(X25) ),
inference(duplicate_literal_removal,[],[f65]) ).
fof(f228,plain,
! [X21,X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20)
| ~ ndr1_0
| ~ c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| hskp7 ),
inference(duplicate_literal_removal,[],[f67]) ).
fof(f229,plain,
! [X18,X19] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0
| c2_1(X19)
| ~ c1_1(X19)
| ~ c3_1(X19)
| hskp6 ),
inference(duplicate_literal_removal,[],[f68]) ).
fof(f231,plain,
! [X14,X13] :
( c0_1(X13)
| c1_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0
| c1_1(X14)
| c3_1(X14)
| ~ c2_1(X14)
| hskp4 ),
inference(duplicate_literal_removal,[],[f70]) ).
fof(f237,definition,
( spl0_1
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f240,definition,
( spl0_2
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f243,definition,
( spl0_3
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f245,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f6,f243,f240,f237]) ).
fof(f247,definition,
( spl0_4
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f250,definition,
( spl0_5
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f253,definition,
( spl0_6
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f255,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f7,f253,f250,f247]) ).
fof(f257,definition,
( spl0_7
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f260,definition,
( spl0_8
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f263,definition,
( spl0_9
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f265,plain,
( spl0_7
| spl0_8
| spl0_9 ),
inference(avatar_split_clause,[],[f8,f263,f260,f257]) ).
fof(f271,definition,
( spl0_11
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f274,definition,
( spl0_12
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f276,plain,
( spl0_6
| spl0_11
| spl0_12 ),
inference(avatar_split_clause,[],[f10,f274,f271,f253]) ).
fof(f278,definition,
( spl0_13
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f281,definition,
( spl0_14
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f283,plain,
( spl0_8
| spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f11,f281,f278,f260]) ).
fof(f285,definition,
( spl0_15
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f288,definition,
( spl0_16
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f290,plain,
( spl0_15
| spl0_6
| spl0_16 ),
inference(avatar_split_clause,[],[f12,f288,f253,f285]) ).
fof(f292,definition,
( spl0_17
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f295,definition,
( spl0_18
<=> ! [X110] :
( ~ c1_1(X110)
| ~ c3_1(X110)
| ~ c2_1(X110) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f296,plain,
( ! [X110] :
( ~ c2_1(X110)
| ~ c3_1(X110)
| ~ c1_1(X110) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f297,plain,
( spl0_1
| spl0_11
| ~ spl0_17
| spl0_18 ),
inference(avatar_split_clause,[],[f13,f295,f292,f271,f237]) ).
fof(f306,definition,
( spl0_21
<=> ! [X108] :
( ~ c0_1(X108)
| ~ c3_1(X108)
| ~ c2_1(X108) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f307,plain,
( ! [X108] :
( ~ c2_1(X108)
| ~ c3_1(X108)
| ~ c0_1(X108) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,plain,
( spl0_1
| spl0_8
| ~ spl0_17
| spl0_21 ),
inference(avatar_split_clause,[],[f16,f306,f292,f260,f237]) ).
fof(f311,definition,
( spl0_22
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f313,plain,
( spl0_22
| spl0_16
| ~ spl0_17
| spl0_21 ),
inference(avatar_split_clause,[],[f17,f306,f292,f288,f311]) ).
fof(f315,definition,
( spl0_23
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f318,definition,
( spl0_24
<=> ! [X105] :
( ~ c0_1(X105)
| ~ c3_1(X105)
| ~ c1_1(X105) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f319,plain,
( ! [X105] :
( ~ c1_1(X105)
| ~ c3_1(X105)
| ~ c0_1(X105) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f320,plain,
( spl0_2
| spl0_23
| ~ spl0_17
| spl0_24 ),
inference(avatar_split_clause,[],[f18,f318,f292,f315,f240]) ).
fof(f322,definition,
( spl0_25
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f324,plain,
( spl0_3
| spl0_25
| ~ spl0_17
| spl0_24 ),
inference(avatar_split_clause,[],[f19,f318,f292,f322,f243]) ).
fof(f327,definition,
( spl0_26
<=> ! [X102] :
( c3_1(X102)
| ~ c2_1(X102)
| ~ c0_1(X102) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f328,plain,
( ! [X102] :
( ~ c2_1(X102)
| c3_1(X102)
| ~ c0_1(X102) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f330,plain,
( spl0_7
| spl0_24
| ~ spl0_17
| spl0_26 ),
inference(avatar_split_clause,[],[f202,f327,f292,f318,f257]) ).
fof(f332,definition,
( spl0_27
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f338,definition,
( spl0_29
<=> ! [X99] :
( c3_1(X99)
| ~ c1_1(X99)
| ~ c0_1(X99) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f339,plain,
( ! [X99] :
( ~ c1_1(X99)
| c3_1(X99)
| ~ c0_1(X99) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f342,definition,
( spl0_30
<=> ! [X98] :
( c2_1(X98)
| ~ c3_1(X98)
| ~ c0_1(X98) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f343,plain,
( ! [X98] :
( c2_1(X98)
| ~ c3_1(X98)
| ~ c0_1(X98) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f344,plain,
( spl0_22
| spl0_14
| ~ spl0_17
| spl0_30 ),
inference(avatar_split_clause,[],[f24,f342,f292,f281,f311]) ).
fof(f346,definition,
( spl0_31
<=> ! [X97] :
( c2_1(X97)
| ~ c1_1(X97)
| ~ c0_1(X97) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f347,plain,
( ! [X97] :
( c2_1(X97)
| ~ c1_1(X97)
| ~ c0_1(X97) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f348,plain,
( spl0_6
| spl0_9
| ~ spl0_17
| spl0_31 ),
inference(avatar_split_clause,[],[f25,f346,f292,f263,f253]) ).
fof(f349,plain,
( spl0_6
| spl0_30
| ~ spl0_17
| spl0_31 ),
inference(avatar_split_clause,[],[f203,f346,f292,f342,f253]) ).
fof(f351,definition,
( spl0_32
<=> ! [X94] :
( c2_1(X94)
| ~ c1_1(X94)
| c3_1(X94) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f352,plain,
( ! [X94] :
( c2_1(X94)
| ~ c1_1(X94)
| c3_1(X94) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f360,definition,
( spl0_34
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f362,plain,
( spl0_34
| spl0_24
| ~ spl0_17
| spl0_32 ),
inference(avatar_split_clause,[],[f204,f351,f292,f318,f360]) ).
fof(f363,plain,
( spl0_26
| spl0_30
| ~ spl0_17
| spl0_32 ),
inference(avatar_split_clause,[],[f205,f351,f292,f342,f327]) ).
fof(f365,definition,
( spl0_35
<=> ! [X85] :
( c1_1(X85)
| ~ c3_1(X85)
| ~ c2_1(X85) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f366,plain,
( ! [X85] :
( ~ c2_1(X85)
| ~ c3_1(X85)
| c1_1(X85) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f372,definition,
( spl0_37
<=> ! [X84] :
( c1_1(X84)
| ~ c2_1(X84)
| c3_1(X84) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f373,plain,
( ! [X84] :
( ~ c2_1(X84)
| c1_1(X84)
| c3_1(X84) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f376,definition,
( spl0_38
<=> ! [X82] :
( c1_1(X82)
| ~ c0_1(X82)
| c3_1(X82) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f377,plain,
( ! [X82] :
( c1_1(X82)
| ~ c0_1(X82)
| c3_1(X82) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f378,plain,
( spl0_3
| spl0_24
| ~ spl0_17
| spl0_38 ),
inference(avatar_split_clause,[],[f207,f376,f292,f318,f243]) ).
fof(f380,definition,
( spl0_39
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f383,definition,
( spl0_40
<=> ! [X81] :
( c1_1(X81)
| ~ c3_1(X81)
| c2_1(X81) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f384,plain,
( ! [X81] :
( c2_1(X81)
| ~ c3_1(X81)
| c1_1(X81) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f385,plain,
( spl0_39
| spl0_11
| ~ spl0_17
| spl0_40 ),
inference(avatar_split_clause,[],[f35,f383,f292,f271,f380]) ).
fof(f387,definition,
( spl0_41
<=> ! [X80] :
( c1_1(X80)
| ~ c0_1(X80)
| c2_1(X80) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f388,plain,
( ! [X80] :
( c2_1(X80)
| ~ c0_1(X80)
| c1_1(X80) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f389,plain,
( spl0_2
| spl0_22
| ~ spl0_17
| spl0_41 ),
inference(avatar_split_clause,[],[f36,f387,f292,f311,f240]) ).
fof(f391,definition,
( spl0_42
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f393,plain,
( spl0_42
| spl0_32
| ~ spl0_17
| spl0_41 ),
inference(avatar_split_clause,[],[f208,f387,f292,f351,f391]) ).
fof(f398,definition,
( spl0_44
<=> ! [X77] :
( c1_1(X77)
| c3_1(X77)
| c2_1(X77) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f399,plain,
( ! [X77] :
( c2_1(X77)
| c3_1(X77)
| c1_1(X77) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f402,definition,
( spl0_45
<=> ! [X76] :
( c2_1(X76)
| ~ c3_1(X76)
| ~ c1_1(X76) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f403,plain,
( ! [X76] :
( c2_1(X76)
| ~ c3_1(X76)
| ~ c1_1(X76) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( spl0_15
| spl0_45
| ~ spl0_17
| spl0_44 ),
inference(avatar_split_clause,[],[f209,f398,f292,f402,f285]) ).
fof(f405,plain,
( spl0_42
| spl0_41
| ~ spl0_17
| spl0_44 ),
inference(avatar_split_clause,[],[f210,f398,f292,f387,f391]) ).
fof(f407,definition,
( spl0_46
<=> ! [X72] :
( c0_1(X72)
| ~ c3_1(X72)
| ~ c2_1(X72) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f408,plain,
( ! [X72] :
( ~ c2_1(X72)
| ~ c3_1(X72)
| c0_1(X72) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f409,plain,
( spl0_14
| spl0_42
| ~ spl0_17
| spl0_46 ),
inference(avatar_split_clause,[],[f41,f407,f292,f391,f281]) ).
fof(f411,definition,
( spl0_47
<=> ! [X70] :
( ~ c0_1(X70)
| ~ c2_1(X70)
| ~ c1_1(X70) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f412,plain,
( ! [X70] :
( ~ c2_1(X70)
| ~ c0_1(X70)
| ~ c1_1(X70) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f413,plain,
( spl0_24
| spl0_47
| ~ spl0_17
| spl0_46 ),
inference(avatar_split_clause,[],[f211,f407,f292,f411,f318]) ).
fof(f415,definition,
( spl0_48
<=> ! [X68] :
( c0_1(X68)
| ~ c3_1(X68)
| ~ c1_1(X68) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f416,plain,
( ! [X68] :
( ~ c1_1(X68)
| ~ c3_1(X68)
| c0_1(X68) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f417,plain,
( spl0_39
| spl0_25
| ~ spl0_17
| spl0_48 ),
inference(avatar_split_clause,[],[f43,f415,f292,f322,f380]) ).
fof(f419,plain,
( spl0_5
| spl0_35
| ~ spl0_17
| spl0_48 ),
inference(avatar_split_clause,[],[f212,f415,f292,f365,f250]) ).
fof(f421,definition,
( spl0_49
<=> ! [X62] :
( c0_1(X62)
| ~ c2_1(X62)
| ~ c1_1(X62) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f422,plain,
( ! [X62] :
( ~ c2_1(X62)
| c0_1(X62)
| ~ c1_1(X62) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f423,plain,
( spl0_31
| spl0_32
| ~ spl0_17
| spl0_49 ),
inference(avatar_split_clause,[],[f213,f421,f292,f351,f346]) ).
fof(f425,definition,
( spl0_50
<=> ! [X61] :
( c1_1(X61)
| ~ c3_1(X61)
| ~ c0_1(X61) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f426,plain,
( ! [X61] :
( c1_1(X61)
| ~ c3_1(X61)
| ~ c0_1(X61) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( spl0_27
| spl0_50
| ~ spl0_17
| spl0_49 ),
inference(avatar_split_clause,[],[f214,f421,f292,f425,f332]) ).
fof(f428,plain,
( spl0_25
| spl0_50
| ~ spl0_17
| spl0_49 ),
inference(avatar_split_clause,[],[f215,f421,f292,f425,f322]) ).
fof(f430,definition,
( spl0_51
<=> ! [X57] :
( c0_1(X57)
| ~ c2_1(X57)
| c3_1(X57) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f431,plain,
( ! [X57] :
( ~ c2_1(X57)
| c0_1(X57)
| c3_1(X57) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f435,plain,
( spl0_29
| spl0_45
| ~ spl0_17
| spl0_51 ),
inference(avatar_split_clause,[],[f217,f430,f292,f402,f338]) ).
fof(f436,plain,
( spl0_25
| spl0_48
| ~ spl0_17
| spl0_51 ),
inference(avatar_split_clause,[],[f218,f430,f292,f415,f322]) ).
fof(f438,definition,
( spl0_52
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f441,definition,
( spl0_53
<=> ! [X48] :
( c0_1(X48)
| ~ c1_1(X48)
| c3_1(X48) ) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f442,plain,
( ! [X48] :
( ~ c1_1(X48)
| c0_1(X48)
| c3_1(X48) )
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f444,plain,
( spl0_13
| spl0_32
| ~ spl0_17
| spl0_53 ),
inference(avatar_split_clause,[],[f219,f441,f292,f351,f278]) ).
fof(f445,plain,
( spl0_21
| spl0_35
| ~ spl0_17
| spl0_53 ),
inference(avatar_split_clause,[],[f220,f441,f292,f365,f306]) ).
fof(f447,definition,
( spl0_54
<=> ! [X42] :
( c0_1(X42)
| ~ c3_1(X42)
| c2_1(X42) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f448,plain,
( ! [X42] :
( c2_1(X42)
| ~ c3_1(X42)
| c0_1(X42) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f449,plain,
( spl0_4
| spl0_2
| ~ spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f57,f447,f292,f240,f247]) ).
fof(f450,plain,
( spl0_14
| spl0_31
| ~ spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f221,f447,f292,f346,f281]) ).
fof(f452,definition,
( spl0_55
<=> ! [X39] :
( c3_1(X39)
| ~ c2_1(X39)
| ~ c1_1(X39) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f453,plain,
( ! [X39] :
( ~ c2_1(X39)
| c3_1(X39)
| ~ c1_1(X39) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f454,plain,
( spl0_55
| spl0_48
| ~ spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f222,f447,f292,f415,f452]) ).
fof(f455,plain,
( spl0_26
| spl0_49
| ~ spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f223,f447,f292,f421,f327]) ).
fof(f456,plain,
( spl0_34
| spl0_51
| ~ spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f224,f447,f292,f430,f360]) ).
fof(f457,plain,
( spl0_1
| spl0_53
| ~ spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f225,f447,f292,f441,f237]) ).
fof(f459,definition,
( spl0_56
<=> ! [X29] :
( c0_1(X29)
| c3_1(X29)
| c2_1(X29) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f460,plain,
( ! [X29] :
( c2_1(X29)
| c3_1(X29)
| c0_1(X29) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( spl0_4
| spl0_14
| ~ spl0_17
| spl0_56 ),
inference(avatar_split_clause,[],[f63,f459,f292,f281,f247]) ).
fof(f462,plain,
( spl0_38
| spl0_40
| ~ spl0_17
| spl0_56 ),
inference(avatar_split_clause,[],[f226,f459,f292,f383,f376]) ).
fof(f463,plain,
( spl0_29
| spl0_48
| ~ spl0_17
| spl0_56 ),
inference(avatar_split_clause,[],[f227,f459,f292,f415,f338]) ).
fof(f465,definition,
( spl0_57
<=> ! [X22] :
( c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22) ) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f466,plain,
( ! [X22] :
( c1_1(X22)
| ~ c3_1(X22)
| c0_1(X22) )
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f469,definition,
( spl0_58
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f471,plain,
( spl0_58
| spl0_18
| ~ spl0_17
| spl0_57 ),
inference(avatar_split_clause,[],[f228,f465,f292,f295,f469]) ).
fof(f472,plain,
( spl0_52
| spl0_45
| ~ spl0_17
| spl0_57 ),
inference(avatar_split_clause,[],[f229,f465,f292,f402,f438]) ).
fof(f477,plain,
( spl0_9
| spl0_37
| ~ spl0_17
| spl0_57 ),
inference(avatar_split_clause,[],[f231,f465,f292,f372,f263]) ).
fof(f492,definition,
( spl0_62
<=> c3_1(a867) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f495,plain,
( spl0_62
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f78,f288,f492]) ).
fof(f497,definition,
( spl0_63
<=> c1_1(a867) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f498,plain,
( c1_1(a867)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f499,plain,
( spl0_63
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f79,f288,f497]) ).
fof(f501,definition,
( spl0_64
<=> c0_1(a867) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f503,plain,
( spl0_64
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f80,f288,f501]) ).
fof(f507,definition,
( spl0_65
<=> c2_1(a829) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f508,plain,
( c2_1(a829)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f510,plain,
( spl0_65
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f82,f391,f507]) ).
fof(f512,definition,
( spl0_66
<=> c1_1(a829) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f513,plain,
( c1_1(a829)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( spl0_66
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f83,f391,f512]) ).
fof(f516,definition,
( spl0_67
<=> c0_1(a829) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f518,plain,
( spl0_67
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f84,f391,f516]) ).
fof(f521,definition,
( spl0_68
<=> c3_1(a797) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f524,plain,
( spl0_68
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f86,f253,f521]) ).
fof(f526,definition,
( spl0_69
<=> c2_1(a797) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f527,plain,
( c2_1(a797)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f528,plain,
( spl0_69
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f87,f253,f526]) ).
fof(f530,definition,
( spl0_70
<=> c1_1(a797) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f531,plain,
( c1_1(a797)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f532,plain,
( spl0_70
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f88,f253,f530]) ).
fof(f535,definition,
( spl0_71
<=> c3_1(a796) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f538,plain,
( spl0_71
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f90,f274,f535]) ).
fof(f540,definition,
( spl0_72
<=> c2_1(a796) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f541,plain,
( c2_1(a796)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f542,plain,
( spl0_72
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f91,f274,f540]) ).
fof(f544,definition,
( spl0_73
<=> c0_1(a796) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f546,plain,
( spl0_73
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f92,f274,f544]) ).
fof(f549,definition,
( spl0_74
<=> c0_1(a869) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f552,plain,
( ~ spl0_74
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f94,f260,f549]) ).
fof(f554,definition,
( spl0_75
<=> c3_1(a869) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f556,plain,
( spl0_75
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f95,f260,f554]) ).
fof(f558,definition,
( spl0_76
<=> c2_1(a869) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f559,plain,
( c2_1(a869)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f560,plain,
( spl0_76
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f96,f260,f558]) ).
fof(f563,definition,
( spl0_77
<=> c3_1(a865) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f566,plain,
( ~ spl0_77
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f98,f315,f563]) ).
fof(f568,definition,
( spl0_78
<=> c2_1(a865) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f569,plain,
( c2_1(a865)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f570,plain,
( spl0_78
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f99,f315,f568]) ).
fof(f572,definition,
( spl0_79
<=> c1_1(a865) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f573,plain,
( c1_1(a865)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f574,plain,
( spl0_79
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f100,f315,f572]) ).
fof(f605,definition,
( spl0_86
<=> c0_1(a840) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f608,plain,
( ~ spl0_86
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f110,f243,f605]) ).
fof(f610,definition,
( spl0_87
<=> c3_1(a840) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f612,plain,
( spl0_87
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f111,f243,f610]) ).
fof(f614,definition,
( spl0_88
<=> c1_1(a840) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f615,plain,
( c1_1(a840)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f616,plain,
( spl0_88
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f112,f243,f614]) ).
fof(f617,plain,
( spl0_17
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f113,f243,f292]) ).
fof(f619,definition,
( spl0_89
<=> c2_1(a838) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f620,plain,
( ~ c2_1(a838)
| spl0_89 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f622,plain,
( ~ spl0_89
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f114,f271,f619]) ).
fof(f624,definition,
( spl0_90
<=> c3_1(a838) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f626,plain,
( spl0_90
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f115,f271,f624]) ).
fof(f628,definition,
( spl0_91
<=> c0_1(a838) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f630,plain,
( spl0_91
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f116,f271,f628]) ).
fof(f633,definition,
( spl0_92
<=> c2_1(a833) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f634,plain,
( ~ c2_1(a833)
| spl0_92 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,plain,
( ~ spl0_92
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f118,f311,f633]) ).
fof(f638,definition,
( spl0_93
<=> c0_1(a833) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f640,plain,
( ~ spl0_93
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f119,f311,f638]) ).
fof(f642,definition,
( spl0_94
<=> c1_1(a833) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f643,plain,
( c1_1(a833)
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f644,plain,
( spl0_94
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f120,f311,f642]) ).
fof(f647,definition,
( spl0_95
<=> c3_1(a832) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f650,plain,
( ~ spl0_95
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f122,f285,f647]) ).
fof(f652,definition,
( spl0_96
<=> c1_1(a832) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f653,plain,
( ~ c1_1(a832)
| spl0_96 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f654,plain,
( ~ spl0_96
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f123,f285,f652]) ).
fof(f656,definition,
( spl0_97
<=> c2_1(a832) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f657,plain,
( c2_1(a832)
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f658,plain,
( spl0_97
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f124,f285,f656]) ).
fof(f661,definition,
( spl0_98
<=> c3_1(a828) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f664,plain,
( ~ spl0_98
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f126,f380,f661]) ).
fof(f666,definition,
( spl0_99
<=> c2_1(a828) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f667,plain,
( ~ c2_1(a828)
| spl0_99 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f668,plain,
( ~ spl0_99
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f127,f380,f666]) ).
fof(f670,definition,
( spl0_100
<=> c1_1(a828) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f672,plain,
( ~ spl0_100
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f128,f380,f670]) ).
fof(f717,definition,
( spl0_110
<=> c2_1(a816) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f718,plain,
( ~ c2_1(a816)
| spl0_110 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f720,plain,
( ~ spl0_110
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f142,f322,f717]) ).
fof(f722,definition,
( spl0_111
<=> c1_1(a816) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f723,plain,
( ~ c1_1(a816)
| spl0_111 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f724,plain,
( ~ spl0_111
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f143,f322,f722]) ).
fof(f726,definition,
( spl0_112
<=> c0_1(a816) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f728,plain,
( spl0_112
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f144,f322,f726]) ).
fof(f731,definition,
( spl0_113
<=> c3_1(a814) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f734,plain,
( ~ spl0_113
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f146,f332,f731]) ).
fof(f736,definition,
( spl0_114
<=> c0_1(a814) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f738,plain,
( ~ spl0_114
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f147,f332,f736]) ).
fof(f740,definition,
( spl0_115
<=> c1_1(a814) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f741,plain,
( c1_1(a814)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f740]) ).
fof(f742,plain,
( spl0_115
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f148,f332,f740]) ).
fof(f745,definition,
( spl0_116
<=> c0_1(a809) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f748,plain,
( ~ spl0_116
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f150,f360,f745]) ).
fof(f750,definition,
( spl0_117
<=> c2_1(a809) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f751,plain,
( c2_1(a809)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f752,plain,
( spl0_117
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f151,f360,f750]) ).
fof(f754,definition,
( spl0_118
<=> c1_1(a809) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f756,plain,
( spl0_118
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f152,f360,f754]) ).
fof(f759,definition,
( spl0_119
<=> c2_1(a808) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f760,plain,
( ~ c2_1(a808)
| spl0_119 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f762,plain,
( ~ spl0_119
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f154,f237,f759]) ).
fof(f764,definition,
( spl0_120
<=> c1_1(a808) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f765,plain,
( ~ c1_1(a808)
| spl0_120 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f766,plain,
( ~ spl0_120
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f155,f237,f764]) ).
fof(f768,definition,
( spl0_121
<=> c3_1(a808) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f770,plain,
( spl0_121
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f156,f237,f768]) ).
fof(f771,plain,
( spl0_17
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f157,f237,f292]) ).
fof(f773,definition,
( spl0_122
<=> c3_1(a807) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f776,plain,
( ~ spl0_122
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f158,f247,f773]) ).
fof(f778,definition,
( spl0_123
<=> c2_1(a807) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f779,plain,
( ~ c2_1(a807)
| spl0_123 ),
inference(avatar_component_clause,[],[f778]) ).
fof(f780,plain,
( ~ spl0_123
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f159,f247,f778]) ).
fof(f782,definition,
( spl0_124
<=> c0_1(a807) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f784,plain,
( ~ spl0_124
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f160,f247,f782]) ).
fof(f787,definition,
( spl0_125
<=> c3_1(a806) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f790,plain,
( ~ spl0_125
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f162,f281,f787]) ).
fof(f792,definition,
( spl0_126
<=> c1_1(a806) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f793,plain,
( c1_1(a806)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f794,plain,
( spl0_126
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f163,f281,f792]) ).
fof(f796,definition,
( spl0_127
<=> c0_1(a806) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f798,plain,
( spl0_127
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f164,f281,f796]) ).
fof(f801,definition,
( spl0_128
<=> c3_1(a805) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f804,plain,
( ~ spl0_128
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f166,f250,f801]) ).
fof(f806,definition,
( spl0_129
<=> c2_1(a805) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f807,plain,
( ~ c2_1(a805)
| spl0_129 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f808,plain,
( ~ spl0_129
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f167,f250,f806]) ).
fof(f810,definition,
( spl0_130
<=> c1_1(a805) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f811,plain,
( c1_1(a805)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f812,plain,
( spl0_130
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f168,f250,f810]) ).
fof(f815,definition,
( spl0_131
<=> c2_1(a803) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f816,plain,
( ~ c2_1(a803)
| spl0_131 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f818,plain,
( ~ spl0_131
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f170,f469,f815]) ).
fof(f820,definition,
( spl0_132
<=> c3_1(a803) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f822,plain,
( spl0_132
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f171,f469,f820]) ).
fof(f824,definition,
( spl0_133
<=> c1_1(a803) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f826,plain,
( spl0_133
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f172,f469,f824]) ).
fof(f834,definition,
( spl0_135
<=> c0_1(a802) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f836,plain,
( ~ spl0_135
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f175,f438,f834]) ).
fof(f838,definition,
( spl0_136
<=> c2_1(a802) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f839,plain,
( c2_1(a802)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f838]) ).
fof(f840,plain,
( spl0_136
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f176,f438,f838]) ).
fof(f843,definition,
( spl0_137
<=> c1_1(a800) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f844,plain,
( ~ c1_1(a800)
| spl0_137 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f846,plain,
( ~ spl0_137
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f178,f257,f843]) ).
fof(f848,definition,
( spl0_138
<=> c0_1(a800) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f850,plain,
( ~ spl0_138
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f179,f257,f848]) ).
fof(f852,definition,
( spl0_139
<=> c3_1(a800) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f854,plain,
( spl0_139
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f180,f257,f852]) ).
fof(f857,definition,
( spl0_140
<=> c1_1(a799) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f858,plain,
( ~ c1_1(a799)
| spl0_140 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f860,plain,
( ~ spl0_140
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f182,f263,f857]) ).
fof(f862,definition,
( spl0_141
<=> c3_1(a799) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f864,plain,
( spl0_141
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f183,f263,f862]) ).
fof(f866,definition,
( spl0_142
<=> c0_1(a799) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f868,plain,
( spl0_142
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f184,f263,f866]) ).
fof(f871,definition,
( spl0_143
<=> c3_1(a798) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f874,plain,
( ~ spl0_143
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f186,f278,f871]) ).
fof(f876,definition,
( spl0_144
<=> c2_1(a798) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f877,plain,
( c2_1(a798)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f878,plain,
( spl0_144
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f187,f278,f876]) ).
fof(f880,definition,
( spl0_145
<=> c0_1(a798) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f882,plain,
( spl0_145
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f188,f278,f880]) ).
fof(f899,definition,
( spl0_149
<=> c2_1(a794) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f900,plain,
( ~ c2_1(a794)
| spl0_149 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f902,plain,
( ~ spl0_149
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f194,f240,f899]) ).
fof(f904,definition,
( spl0_150
<=> c0_1(a794) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f906,plain,
( ~ spl0_150
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f195,f240,f904]) ).
fof(f908,definition,
( spl0_151
<=> c3_1(a794) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f910,plain,
( spl0_151
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f196,f240,f908]) ).
fof(f911,plain,
( spl0_17
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f197,f240,f292]) ).
fof(f929,definition,
( spl0_155
<=> c1_1(a869) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f930,plain,
( ~ c1_1(a869)
| spl0_155 ),
inference(avatar_component_clause,[],[f929]) ).
fof(f943,plain,
( ~ c3_1(a869)
| ~ c0_1(a869)
| ~ spl0_21
| ~ spl0_76 ),
inference(resolution,[],[f307,f559]) ).
fof(f948,definition,
( spl0_157
<=> c0_1(a797) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f962,definition,
( spl0_158
<=> c0_1(a865) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f968,plain,
( c3_1(a865)
| ~ c0_1(a865)
| ~ spl0_29
| ~ spl0_79 ),
inference(resolution,[],[f339,f573]) ).
fof(f971,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_18
| ~ spl0_30 ),
inference(resolution,[],[f343,f296]) ).
fof(f975,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_18
| ~ spl0_30 ),
inference(duplicate_literal_removal,[],[f971]) ).
fof(f977,plain,
( spl0_24
| ~ spl0_18
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f975,f342,f295,f318]) ).
fof(f981,definition,
( spl0_159
<=> c3_1(a833) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f985,plain,
( c3_1(a832)
| ~ c0_1(a832)
| ~ spl0_26
| ~ spl0_97 ),
inference(resolution,[],[f657,f328]) ).
fof(f988,definition,
( spl0_160
<=> c0_1(a832) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f991,plain,
( ~ spl0_160
| spl0_95
| ~ spl0_26
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f985,f656,f327,f647,f988]) ).
fof(f997,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_26
| ~ spl0_31 ),
inference(resolution,[],[f347,f328]) ).
fof(f998,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_18
| ~ spl0_31 ),
inference(resolution,[],[f347,f296]) ).
fof(f1003,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_18
| ~ spl0_31 ),
inference(duplicate_literal_removal,[],[f998]) ).
fof(f1004,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_26
| ~ spl0_31 ),
inference(duplicate_literal_removal,[],[f997]) ).
fof(f1005,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_26
| ~ spl0_32 ),
inference(resolution,[],[f352,f328]) ).
fof(f1007,plain,
( ~ c1_1(a807)
| c3_1(a807)
| ~ spl0_32
| spl0_123 ),
inference(resolution,[],[f352,f779]) ).
fof(f1012,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_26
| ~ spl0_32 ),
inference(duplicate_literal_removal,[],[f1005]) ).
fof(f1018,definition,
( spl0_161
<=> c1_1(a807) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1020,plain,
( spl0_122
| ~ spl0_161
| ~ spl0_32
| spl0_123 ),
inference(avatar_split_clause,[],[f1007,f778,f351,f1018,f773]) ).
fof(f1023,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_30
| ~ spl0_35 ),
inference(resolution,[],[f366,f343]) ).
fof(f1029,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_30
| ~ spl0_35 ),
inference(duplicate_literal_removal,[],[f1023]) ).
fof(f1035,plain,
( spl0_50
| ~ spl0_30
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f1029,f365,f342,f425]) ).
fof(f1063,plain,
( ~ c0_1(a869)
| c3_1(a869)
| ~ spl0_38
| spl0_155 ),
inference(resolution,[],[f377,f930]) ).
fof(f1073,definition,
( spl0_163
<=> c0_1(a828) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1082,plain,
( ~ c0_1(a828)
| c1_1(a828)
| ~ spl0_41
| spl0_99 ),
inference(resolution,[],[f388,f667]) ).
fof(f1086,plain,
( spl0_100
| ~ spl0_163
| ~ spl0_41
| spl0_99 ),
inference(avatar_split_clause,[],[f1082,f666,f387,f1073,f670]) ).
fof(f1089,plain,
( c3_1(a807)
| c1_1(a807)
| ~ spl0_44
| spl0_123 ),
inference(resolution,[],[f399,f779]) ).
fof(f1091,plain,
( c3_1(a828)
| c1_1(a828)
| ~ spl0_44
| spl0_99 ),
inference(resolution,[],[f399,f667]) ).
fof(f1094,plain,
( spl0_100
| spl0_98
| ~ spl0_44
| spl0_99 ),
inference(avatar_split_clause,[],[f1091,f666,f398,f661,f670]) ).
fof(f1101,plain,
( spl0_161
| spl0_122
| ~ spl0_44
| spl0_123 ),
inference(avatar_split_clause,[],[f1089,f778,f398,f773,f1018]) ).
fof(f1122,definition,
( spl0_165
<=> c0_1(a808) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1133,plain,
( c3_1(a798)
| ~ c0_1(a798)
| ~ spl0_26
| ~ spl0_144 ),
inference(resolution,[],[f877,f328]) ).
fof(f1140,plain,
( ~ c3_1(a840)
| c0_1(a840)
| ~ spl0_48
| ~ spl0_88 ),
inference(resolution,[],[f416,f615]) ).
fof(f1154,definition,
( spl0_166
<=> c0_1(a805) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1209,definition,
( spl0_168
<=> c3_1(a816) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1220,definition,
( spl0_169
<=> c3_1(a829) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1225,plain,
( ~ c3_1(a829)
| ~ c0_1(a829)
| ~ spl0_24
| ~ spl0_66 ),
inference(resolution,[],[f513,f319]) ).
fof(f1227,plain,
( ~ spl0_67
| ~ spl0_169
| ~ spl0_24
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f1225,f512,f318,f1220,f516]) ).
fof(f1236,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_45
| ~ spl0_49 ),
inference(resolution,[],[f403,f422]) ).
fof(f1237,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_45
| ~ spl0_46 ),
inference(resolution,[],[f403,f408]) ).
fof(f1248,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_45
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f1237]) ).
fof(f1249,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_45
| ~ spl0_49 ),
inference(duplicate_literal_removal,[],[f1236]) ).
fof(f1253,plain,
( spl0_48
| ~ spl0_45
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f1248,f407,f402,f415]) ).
fof(f1254,plain,
( spl0_48
| ~ spl0_45
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f1249,f421,f402,f415]) ).
fof(f1258,plain,
( ~ c3_1(a833)
| c0_1(a833)
| ~ spl0_48
| ~ spl0_94 ),
inference(resolution,[],[f416,f643]) ).
fof(f1293,definition,
( spl0_170
<=> c1_1(a838) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1314,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_21
| ~ spl0_31 ),
inference(resolution,[],[f347,f307]) ).
fof(f1319,plain,
( ~ c1_1(a805)
| ~ c0_1(a805)
| ~ spl0_31
| spl0_129 ),
inference(resolution,[],[f347,f807]) ).
fof(f1328,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_21
| ~ spl0_31 ),
inference(duplicate_literal_removal,[],[f1314]) ).
fof(f1331,plain,
( ~ spl0_166
| ~ spl0_130
| ~ spl0_31
| spl0_129 ),
inference(avatar_split_clause,[],[f1319,f806,f346,f810,f1154]) ).
fof(f1333,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_32
| ~ spl0_49 ),
inference(resolution,[],[f352,f422]) ).
fof(f1337,plain,
( ~ c1_1(a805)
| c3_1(a805)
| ~ spl0_32
| spl0_129 ),
inference(resolution,[],[f352,f807]) ).
fof(f1345,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0) )
| ~ spl0_32
| ~ spl0_49 ),
inference(duplicate_literal_removal,[],[f1333]) ).
fof(f1347,plain,
( spl0_128
| ~ spl0_130
| ~ spl0_32
| spl0_129 ),
inference(avatar_split_clause,[],[f1337,f806,f351,f810,f801]) ).
fof(f1348,plain,
( spl0_53
| ~ spl0_32
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f1345,f421,f351,f441]) ).
fof(f1374,plain,
( ~ c3_1(a794)
| c0_1(a794)
| ~ spl0_54
| spl0_149 ),
inference(resolution,[],[f448,f900]) ).
fof(f1377,plain,
( ~ c3_1(a808)
| c0_1(a808)
| ~ spl0_54
| spl0_119 ),
inference(resolution,[],[f448,f760]) ).
fof(f1394,plain,
( spl0_29
| ~ spl0_26
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f1004,f346,f327,f338]) ).
fof(f1395,plain,
( ~ spl0_145
| spl0_143
| ~ spl0_26
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1133,f876,f327,f871,f880]) ).
fof(f1396,plain,
( spl0_29
| ~ spl0_26
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f1012,f351,f327,f338]) ).
fof(f1398,definition,
( spl0_171
<=> c1_1(a798) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1430,definition,
( spl0_173
<=> c3_1(a809) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1461,definition,
( spl0_174
<=> c3_1(a802) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f1467,plain,
( ~ c3_1(a802)
| c0_1(a802)
| ~ spl0_46
| ~ spl0_136 ),
inference(resolution,[],[f839,f408]) ).
fof(f1470,plain,
( spl0_135
| ~ spl0_174
| ~ spl0_46
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1467,f838,f407,f1461,f834]) ).
fof(f1479,plain,
( c3_1(a829)
| ~ c0_1(a829)
| ~ spl0_26
| ~ spl0_65 ),
inference(resolution,[],[f328,f508]) ).
fof(f1483,plain,
( ~ spl0_67
| spl0_169
| ~ spl0_26
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f1479,f507,f327,f1220,f516]) ).
fof(f1491,plain,
( c3_1(a806)
| ~ c0_1(a806)
| ~ spl0_29
| ~ spl0_126 ),
inference(resolution,[],[f339,f793]) ).
fof(f1493,plain,
( c3_1(a829)
| ~ c0_1(a829)
| ~ spl0_29
| ~ spl0_66 ),
inference(resolution,[],[f339,f513]) ).
fof(f1512,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_21
| ~ spl0_41 ),
inference(resolution,[],[f388,f307]) ).
fof(f1521,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_21
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f1512]) ).
fof(f1528,plain,
( spl0_50
| ~ spl0_21
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1521,f387,f306,f425]) ).
fof(f1532,plain,
( spl0_150
| ~ spl0_151
| ~ spl0_54
| spl0_149 ),
inference(avatar_split_clause,[],[f1374,f899,f447,f908,f904]) ).
fof(f1533,plain,
( spl0_165
| ~ spl0_121
| ~ spl0_54
| spl0_119 ),
inference(avatar_split_clause,[],[f1377,f759,f447,f768,f1122]) ).
fof(f1545,plain,
( ~ c1_1(a833)
| c3_1(a833)
| ~ spl0_32
| spl0_92 ),
inference(resolution,[],[f634,f352]) ).
fof(f1547,plain,
( spl0_159
| ~ spl0_94
| ~ spl0_32
| spl0_92 ),
inference(avatar_split_clause,[],[f1545,f633,f351,f642,f981]) ).
fof(f1603,plain,
( ~ spl0_158
| spl0_77
| ~ spl0_29
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f968,f572,f338,f563,f962]) ).
fof(f1604,plain,
( ~ spl0_127
| spl0_125
| ~ spl0_29
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1491,f792,f338,f787,f796]) ).
fof(f1605,plain,
( ~ spl0_67
| spl0_169
| ~ spl0_29
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f1493,f512,f338,f1220,f516]) ).
fof(f1635,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_32
| ~ spl0_47 ),
inference(resolution,[],[f412,f352]) ).
fof(f1646,plain,
( ~ c0_1(a829)
| ~ c1_1(a829)
| ~ spl0_47
| ~ spl0_65 ),
inference(resolution,[],[f412,f508]) ).
fof(f1648,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_32
| ~ spl0_47 ),
inference(duplicate_literal_removal,[],[f1635]) ).
fof(f1649,plain,
( ~ spl0_66
| ~ spl0_67
| ~ spl0_47
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f1646,f507,f411,f516,f512]) ).
fof(f1653,plain,
( spl0_29
| ~ spl0_32
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1648,f411,f351,f338]) ).
fof(f1665,plain,
( ~ c3_1(a797)
| ~ c0_1(a797)
| ~ spl0_24
| ~ spl0_70 ),
inference(resolution,[],[f319,f531]) ).
fof(f1674,plain,
( ~ c3_1(a799)
| ~ c0_1(a799)
| ~ spl0_50
| spl0_140 ),
inference(resolution,[],[f426,f858]) ).
fof(f1678,plain,
( ~ c3_1(a808)
| ~ c0_1(a808)
| ~ spl0_50
| spl0_120 ),
inference(resolution,[],[f426,f765]) ).
fof(f1692,plain,
( ~ spl0_165
| ~ spl0_121
| ~ spl0_50
| spl0_120 ),
inference(avatar_split_clause,[],[f1678,f764,f425,f768,f1122]) ).
fof(f1693,plain,
( ~ spl0_142
| ~ spl0_141
| ~ spl0_50
| spl0_140 ),
inference(avatar_split_clause,[],[f1674,f857,f425,f862,f866]) ).
fof(f1703,plain,
( c0_1(a869)
| c3_1(a869)
| ~ spl0_51
| ~ spl0_76 ),
inference(resolution,[],[f431,f559]) ).
fof(f1716,plain,
( c0_1(a814)
| c3_1(a814)
| ~ spl0_53
| ~ spl0_115 ),
inference(resolution,[],[f442,f741]) ).
fof(f1717,plain,
( c0_1(a833)
| c3_1(a833)
| ~ spl0_53
| ~ spl0_94 ),
inference(resolution,[],[f442,f643]) ).
fof(f1724,plain,
( spl0_113
| spl0_114
| ~ spl0_53
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f1716,f740,f441,f736,f731]) ).
fof(f1730,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_35
| ~ spl0_54 ),
inference(resolution,[],[f448,f366]) ).
fof(f1733,plain,
( ~ c3_1(a833)
| c0_1(a833)
| ~ spl0_54
| spl0_92 ),
inference(resolution,[],[f448,f634]) ).
fof(f1736,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c1_1(X0) )
| ~ spl0_35
| ~ spl0_54 ),
inference(duplicate_literal_removal,[],[f1730]) ).
fof(f1738,plain,
( spl0_93
| ~ spl0_159
| ~ spl0_54
| spl0_92 ),
inference(avatar_split_clause,[],[f1733,f633,f447,f981,f638]) ).
fof(f1740,plain,
( spl0_57
| ~ spl0_35
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1736,f447,f365,f465]) ).
fof(f1751,plain,
( spl0_75
| spl0_74
| ~ spl0_51
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1703,f558,f430,f549,f554]) ).
fof(f1763,plain,
( ~ c3_1(a809)
| c0_1(a809)
| ~ spl0_46
| ~ spl0_117 ),
inference(resolution,[],[f408,f751]) ).
fof(f1767,plain,
( ~ c3_1(a869)
| c0_1(a869)
| ~ spl0_46
| ~ spl0_76 ),
inference(resolution,[],[f408,f559]) ).
fof(f1772,plain,
( spl0_74
| ~ spl0_75
| ~ spl0_46
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1767,f558,f407,f554,f549]) ).
fof(f1774,plain,
( spl0_116
| ~ spl0_173
| ~ spl0_46
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1763,f750,f407,f1430,f745]) ).
fof(f1779,plain,
( c0_1(a809)
| ~ c1_1(a809)
| ~ spl0_49
| ~ spl0_117 ),
inference(resolution,[],[f422,f751]) ).
fof(f1782,plain,
( c0_1(a865)
| ~ c1_1(a865)
| ~ spl0_49
| ~ spl0_78 ),
inference(resolution,[],[f422,f569]) ).
fof(f1785,plain,
( c0_1(a797)
| ~ c1_1(a797)
| ~ spl0_49
| ~ spl0_69 ),
inference(resolution,[],[f422,f527]) ).
fof(f1789,plain,
( ~ spl0_70
| spl0_157
| ~ spl0_49
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1785,f526,f421,f948,f530]) ).
fof(f1791,plain,
( ~ spl0_79
| spl0_158
| ~ spl0_49
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f1782,f568,f421,f962,f572]) ).
fof(f1792,plain,
( ~ spl0_118
| spl0_116
| ~ spl0_49
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1779,f750,f421,f745,f754]) ).
fof(f1794,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_31
| ~ spl0_55 ),
inference(resolution,[],[f453,f347]) ).
fof(f1800,plain,
( c3_1(a865)
| ~ c1_1(a865)
| ~ spl0_55
| ~ spl0_78 ),
inference(resolution,[],[f453,f569]) ).
fof(f1801,plain,
( c3_1(a869)
| ~ c1_1(a869)
| ~ spl0_55
| ~ spl0_76 ),
inference(resolution,[],[f453,f559]) ).
fof(f1805,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_31
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f1794]) ).
fof(f1809,plain,
( ~ spl0_79
| spl0_77
| ~ spl0_55
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f1800,f568,f452,f563,f572]) ).
fof(f1812,plain,
( spl0_29
| ~ spl0_31
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1805,f452,f346,f338]) ).
fof(f1826,plain,
( c3_1(a833)
| c0_1(a833)
| ~ spl0_56
| spl0_92 ),
inference(resolution,[],[f460,f634]) ).
fof(f1840,plain,
( ~ c3_1(a800)
| c0_1(a800)
| ~ spl0_57
| spl0_137 ),
inference(resolution,[],[f466,f844]) ).
fof(f1858,plain,
( spl0_138
| ~ spl0_139
| ~ spl0_57
| spl0_137 ),
inference(avatar_split_clause,[],[f1840,f843,f465,f852,f848]) ).
fof(f1862,plain,
( spl0_75
| ~ spl0_74
| ~ spl0_38
| spl0_155 ),
inference(avatar_split_clause,[],[f1063,f929,f376,f549,f554]) ).
fof(f1869,plain,
( spl0_86
| ~ spl0_87
| ~ spl0_48
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f1140,f614,f415,f610,f605]) ).
fof(f1870,plain,
( spl0_93
| ~ spl0_159
| ~ spl0_48
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f1258,f642,f415,f981,f638]) ).
fof(f1879,plain,
( c1_1(a798)
| c3_1(a798)
| ~ spl0_37
| ~ spl0_144 ),
inference(resolution,[],[f373,f877]) ).
fof(f1889,plain,
( spl0_143
| spl0_171
| ~ spl0_37
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1879,f876,f372,f1398,f871]) ).
fof(f1909,plain,
( ~ c0_1(a816)
| c3_1(a816)
| ~ spl0_38
| spl0_111 ),
inference(resolution,[],[f377,f723]) ).
fof(f1913,plain,
( ~ c0_1(a832)
| c3_1(a832)
| ~ spl0_38
| spl0_96 ),
inference(resolution,[],[f377,f653]) ).
fof(f1918,plain,
( spl0_95
| ~ spl0_160
| ~ spl0_38
| spl0_96 ),
inference(avatar_split_clause,[],[f1913,f652,f376,f988,f647]) ).
fof(f1920,plain,
( spl0_168
| ~ spl0_112
| ~ spl0_38
| spl0_111 ),
inference(avatar_split_clause,[],[f1909,f722,f376,f726,f1209]) ).
fof(f1925,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_40
| ~ spl0_46 ),
inference(resolution,[],[f384,f408]) ).
fof(f1930,plain,
( ~ c3_1(a808)
| c1_1(a808)
| ~ spl0_40
| spl0_119 ),
inference(resolution,[],[f384,f760]) ).
fof(f1934,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_40
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f1925]) ).
fof(f1937,plain,
( spl0_120
| ~ spl0_121
| ~ spl0_40
| spl0_119 ),
inference(avatar_split_clause,[],[f1930,f759,f383,f768,f764]) ).
fof(f1939,plain,
( spl0_57
| ~ spl0_40
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f1934,f407,f383,f465]) ).
fof(f1946,plain,
( ~ c3_1(a803)
| ~ c1_1(a803)
| ~ spl0_45
| spl0_131 ),
inference(resolution,[],[f403,f816]) ).
fof(f1957,plain,
( ~ spl0_133
| ~ spl0_132
| ~ spl0_45
| spl0_131 ),
inference(avatar_split_clause,[],[f1946,f815,f402,f820,f824]) ).
fof(f1962,plain,
( spl0_24
| ~ spl0_18
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f1003,f346,f295,f318]) ).
fof(f1978,plain,
( ~ spl0_74
| ~ spl0_75
| ~ spl0_21
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f943,f558,f306,f554,f549]) ).
fof(f1983,plain,
( spl0_24
| ~ spl0_21
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f1328,f346,f306,f318]) ).
fof(f1997,plain,
( ~ spl0_157
| ~ spl0_68
| ~ spl0_24
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f1665,f530,f318,f521,f948]) ).
fof(f2011,plain,
( spl0_159
| spl0_93
| ~ spl0_53
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f1717,f642,f441,f638,f981]) ).
fof(f2015,plain,
( c0_1(a832)
| c3_1(a832)
| ~ spl0_51
| ~ spl0_97 ),
inference(resolution,[],[f657,f431]) ).
fof(f2016,plain,
( spl0_95
| spl0_160
| ~ spl0_51
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f2015,f656,f430,f988,f647]) ).
fof(f2024,plain,
( ~ c3_1(a797)
| ~ c1_1(a797)
| ~ spl0_18
| ~ spl0_69 ),
inference(resolution,[],[f296,f527]) ).
fof(f2028,plain,
( ~ spl0_70
| ~ spl0_68
| ~ spl0_18
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f2024,f526,f295,f521,f530]) ).
fof(f2039,plain,
( ~ c3_1(a796)
| ~ c0_1(a796)
| ~ spl0_21
| ~ spl0_72 ),
inference(resolution,[],[f307,f541]) ).
fof(f2040,plain,
( ~ c3_1(a797)
| ~ c0_1(a797)
| ~ spl0_21
| ~ spl0_69 ),
inference(resolution,[],[f307,f527]) ).
fof(f2041,plain,
( ~ c3_1(a829)
| ~ c0_1(a829)
| ~ spl0_21
| ~ spl0_65 ),
inference(resolution,[],[f307,f508]) ).
fof(f2042,plain,
( ~ spl0_67
| ~ spl0_169
| ~ spl0_21
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f2041,f507,f306,f1220,f516]) ).
fof(f2043,plain,
( ~ spl0_157
| ~ spl0_68
| ~ spl0_21
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f2040,f526,f306,f521,f948]) ).
fof(f2044,plain,
( ~ spl0_73
| ~ spl0_71
| ~ spl0_21
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f2039,f540,f306,f535,f544]) ).
fof(f2052,plain,
( ~ c3_1(a829)
| ~ c0_1(a829)
| ~ spl0_24
| ~ spl0_66 ),
inference(resolution,[],[f319,f513]) ).
fof(f2053,plain,
( ~ c3_1(a867)
| ~ c0_1(a867)
| ~ spl0_24
| ~ spl0_63 ),
inference(resolution,[],[f319,f498]) ).
fof(f2054,plain,
( ~ spl0_64
| ~ spl0_62
| ~ spl0_24
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f2053,f497,f318,f492,f501]) ).
fof(f2055,plain,
( ~ spl0_67
| ~ spl0_169
| ~ spl0_24
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f2052,f512,f318,f1220,f516]) ).
fof(f2071,plain,
( ~ c1_1(a838)
| ~ c0_1(a838)
| ~ spl0_31
| spl0_89 ),
inference(resolution,[],[f347,f620]) ).
fof(f2077,plain,
( ~ spl0_91
| ~ spl0_170
| ~ spl0_31
| spl0_89 ),
inference(avatar_split_clause,[],[f2071,f619,f346,f1293,f628]) ).
fof(f2091,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_21
| ~ spl0_40 ),
inference(resolution,[],[f384,f307]) ).
fof(f2101,plain,
( ~ c3_1(a838)
| c1_1(a838)
| ~ spl0_40
| spl0_89 ),
inference(resolution,[],[f384,f620]) ).
fof(f2105,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_21
| ~ spl0_40 ),
inference(duplicate_literal_removal,[],[f2091]) ).
fof(f2107,plain,
( spl0_170
| ~ spl0_90
| ~ spl0_40
| spl0_89 ),
inference(avatar_split_clause,[],[f2101,f619,f383,f624,f1293]) ).
fof(f2111,plain,
( spl0_50
| ~ spl0_21
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f2105,f383,f306,f425]) ).
fof(f2128,plain,
( ~ spl0_155
| spl0_75
| ~ spl0_55
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1801,f558,f452,f554,f929]) ).
fof(f2133,plain,
( spl0_93
| spl0_159
| ~ spl0_56
| spl0_92 ),
inference(avatar_split_clause,[],[f1826,f633,f459,f981,f638]) ).
fof(f2144,plain,
( c0_1(a805)
| c3_1(a805)
| ~ spl0_53
| ~ spl0_130 ),
inference(resolution,[],[f811,f442]) ).
fof(f2145,plain,
( spl0_128
| spl0_166
| ~ spl0_53
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f2144,f810,f441,f1154,f801]) ).
fof(f2147,plain,
( c0_1(a802)
| c3_1(a802)
| ~ spl0_51
| ~ spl0_136 ),
inference(resolution,[],[f839,f431]) ).
fof(f2148,plain,
( spl0_174
| spl0_135
| ~ spl0_51
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f2147,f838,f430,f834,f1461]) ).
fof(f2158,plain,
( ~ c3_1(a808)
| ~ c0_1(a808)
| ~ spl0_30
| spl0_119 ),
inference(resolution,[],[f343,f760]) ).
fof(f2159,plain,
( ~ c3_1(a816)
| ~ c0_1(a816)
| ~ spl0_30
| spl0_110 ),
inference(resolution,[],[f343,f718]) ).
fof(f2162,plain,
( ~ c3_1(a838)
| ~ c0_1(a838)
| ~ spl0_30
| spl0_89 ),
inference(resolution,[],[f343,f620]) ).
fof(f2164,plain,
( ~ spl0_91
| ~ spl0_90
| ~ spl0_30
| spl0_89 ),
inference(avatar_split_clause,[],[f2162,f619,f342,f624,f628]) ).
fof(f2165,plain,
( ~ spl0_112
| ~ spl0_168
| ~ spl0_30
| spl0_110 ),
inference(avatar_split_clause,[],[f2159,f717,f342,f1209,f726]) ).
fof(f2166,plain,
( ~ spl0_165
| ~ spl0_121
| ~ spl0_30
| spl0_119 ),
inference(avatar_split_clause,[],[f2158,f759,f342,f768,f1122]) ).
fof(f2174,plain,
( ~ c0_1(a808)
| c1_1(a808)
| ~ spl0_41
| spl0_119 ),
inference(resolution,[],[f388,f760]) ).
fof(f2175,plain,
( ~ c0_1(a816)
| c1_1(a816)
| ~ spl0_41
| spl0_110 ),
inference(resolution,[],[f388,f718]) ).
fof(f2178,plain,
( ~ c0_1(a838)
| c1_1(a838)
| ~ spl0_41
| spl0_89 ),
inference(resolution,[],[f388,f620]) ).
fof(f2181,plain,
( spl0_170
| ~ spl0_91
| ~ spl0_41
| spl0_89 ),
inference(avatar_split_clause,[],[f2178,f619,f387,f628,f1293]) ).
fof(f2182,plain,
( spl0_111
| ~ spl0_112
| ~ spl0_41
| spl0_110 ),
inference(avatar_split_clause,[],[f2175,f717,f387,f726,f722]) ).
fof(f2183,plain,
( spl0_120
| ~ spl0_165
| ~ spl0_41
| spl0_119 ),
inference(avatar_split_clause,[],[f2174,f759,f387,f1122,f764]) ).
fof(f2188,plain,
( c3_1(a798)
| ~ c1_1(a798)
| ~ spl0_55
| ~ spl0_144 ),
inference(resolution,[],[f453,f877]) ).
fof(f2190,plain,
( c3_1(a809)
| ~ c1_1(a809)
| ~ spl0_55
| ~ spl0_117 ),
inference(resolution,[],[f453,f751]) ).
fof(f2196,plain,
( c3_1(a829)
| ~ c1_1(a829)
| ~ spl0_55
| ~ spl0_65 ),
inference(resolution,[],[f453,f508]) ).
fof(f2197,plain,
( ~ spl0_66
| spl0_169
| ~ spl0_55
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f2196,f507,f452,f1220,f512]) ).
fof(f2198,plain,
( ~ spl0_118
| spl0_173
| ~ spl0_55
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f2190,f750,f452,f1430,f754]) ).
fof(f2199,plain,
( ~ spl0_171
| spl0_143
| ~ spl0_55
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f2188,f876,f452,f871,f1398]) ).
fof(f2205,plain,
( c3_1(a805)
| c0_1(a805)
| ~ spl0_56
| spl0_129 ),
inference(resolution,[],[f460,f807]) ).
fof(f2206,plain,
( c3_1(a807)
| c0_1(a807)
| ~ spl0_56
| spl0_123 ),
inference(resolution,[],[f460,f779]) ).
fof(f2209,plain,
( c3_1(a828)
| c0_1(a828)
| ~ spl0_56
| spl0_99 ),
inference(resolution,[],[f460,f667]) ).
fof(f2217,plain,
( spl0_163
| spl0_98
| ~ spl0_56
| spl0_99 ),
inference(avatar_split_clause,[],[f2209,f666,f459,f661,f1073]) ).
fof(f2218,plain,
( spl0_124
| spl0_122
| ~ spl0_56
| spl0_123 ),
inference(avatar_split_clause,[],[f2206,f778,f459,f773,f782]) ).
fof(f2219,plain,
( spl0_166
| spl0_128
| ~ spl0_56
| spl0_129 ),
inference(avatar_split_clause,[],[f2205,f806,f459,f801,f1154]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f245]) ).
cnf(s2,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f255]) ).
cnf(s3,plain,
( spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f265]) ).
cnf(s5,plain,
( spl0_6
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f276]) ).
cnf(s6,plain,
( spl0_8
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f283]) ).
cnf(s7,plain,
( spl0_6
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f290]) ).
cnf(s8,plain,
( spl0_1
| spl0_11
| ~ spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f297]) ).
cnf(s11,plain,
( spl0_1
| spl0_8
| ~ spl0_17
| spl0_21 ),
inference(sat_conversion,[],[f309]) ).
cnf(s12,plain,
( spl0_16
| ~ spl0_17
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f313]) ).
cnf(s13,plain,
( spl0_2
| ~ spl0_17
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f320]) ).
cnf(s14,plain,
( spl0_3
| ~ spl0_17
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f324]) ).
cnf(s17,plain,
( spl0_7
| ~ spl0_17
| spl0_24
| spl0_26 ),
inference(sat_conversion,[],[f330]) ).
cnf(s19,plain,
( spl0_14
| ~ spl0_17
| spl0_22
| spl0_30 ),
inference(sat_conversion,[],[f344]) ).
cnf(s20,plain,
( spl0_6
| spl0_9
| ~ spl0_17
| spl0_31 ),
inference(sat_conversion,[],[f348]) ).
cnf(s21,plain,
( spl0_6
| ~ spl0_17
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f349]) ).
cnf(s25,plain,
( ~ spl0_17
| spl0_24
| spl0_32
| spl0_34 ),
inference(sat_conversion,[],[f362]) ).
cnf(s26,plain,
( ~ spl0_17
| spl0_26
| spl0_30
| spl0_32 ),
inference(sat_conversion,[],[f363]) ).
cnf(s29,plain,
( spl0_3
| ~ spl0_17
| spl0_24
| spl0_38 ),
inference(sat_conversion,[],[f378]) ).
cnf(s30,plain,
( spl0_11
| ~ spl0_17
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f385]) ).
cnf(s31,plain,
( spl0_2
| ~ spl0_17
| spl0_22
| spl0_41 ),
inference(sat_conversion,[],[f389]) ).
cnf(s32,plain,
( ~ spl0_17
| spl0_32
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f393]) ).
cnf(s34,plain,
( spl0_15
| ~ spl0_17
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f404]) ).
cnf(s35,plain,
( ~ spl0_17
| spl0_41
| spl0_42
| spl0_44 ),
inference(sat_conversion,[],[f405]) ).
cnf(s36,plain,
( spl0_14
| ~ spl0_17
| spl0_42
| spl0_46 ),
inference(sat_conversion,[],[f409]) ).
cnf(s37,plain,
( ~ spl0_17
| spl0_24
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f413]) ).
cnf(s38,plain,
( ~ spl0_17
| spl0_25
| spl0_39
| spl0_48 ),
inference(sat_conversion,[],[f417]) ).
cnf(s40,plain,
( spl0_5
| ~ spl0_17
| spl0_35
| spl0_48 ),
inference(sat_conversion,[],[f419]) ).
cnf(s41,plain,
( ~ spl0_17
| spl0_31
| spl0_32
| spl0_49 ),
inference(sat_conversion,[],[f423]) ).
cnf(s42,plain,
( ~ spl0_17
| spl0_27
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f427]) ).
cnf(s43,plain,
( ~ spl0_17
| spl0_25
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f428]) ).
cnf(s47,plain,
( ~ spl0_17
| spl0_29
| spl0_45
| spl0_51 ),
inference(sat_conversion,[],[f435]) ).
cnf(s48,plain,
( ~ spl0_17
| spl0_25
| spl0_48
| spl0_51 ),
inference(sat_conversion,[],[f436]) ).
cnf(s50,plain,
( spl0_13
| ~ spl0_17
| spl0_32
| spl0_53 ),
inference(sat_conversion,[],[f444]) ).
cnf(s51,plain,
( ~ spl0_17
| spl0_21
| spl0_35
| spl0_53 ),
inference(sat_conversion,[],[f445]) ).
cnf(s52,plain,
( spl0_2
| spl0_4
| ~ spl0_17
| spl0_54 ),
inference(sat_conversion,[],[f449]) ).
cnf(s53,plain,
( spl0_14
| ~ spl0_17
| spl0_31
| spl0_54 ),
inference(sat_conversion,[],[f450]) ).
cnf(s54,plain,
( ~ spl0_17
| spl0_48
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f454]) ).
cnf(s55,plain,
( ~ spl0_17
| spl0_26
| spl0_49
| spl0_54 ),
inference(sat_conversion,[],[f455]) ).
cnf(s56,plain,
( ~ spl0_17
| spl0_34
| spl0_51
| spl0_54 ),
inference(sat_conversion,[],[f456]) ).
cnf(s57,plain,
( spl0_1
| ~ spl0_17
| spl0_53
| spl0_54 ),
inference(sat_conversion,[],[f457]) ).
cnf(s58,plain,
( spl0_4
| spl0_14
| ~ spl0_17
| spl0_56 ),
inference(sat_conversion,[],[f461]) ).
cnf(s59,plain,
( ~ spl0_17
| spl0_38
| spl0_40
| spl0_56 ),
inference(sat_conversion,[],[f462]) ).
cnf(s60,plain,
( ~ spl0_17
| spl0_29
| spl0_48
| spl0_56 ),
inference(sat_conversion,[],[f463]) ).
cnf(s62,plain,
( ~ spl0_17
| spl0_18
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f471]) ).
cnf(s63,plain,
( ~ spl0_17
| spl0_45
| spl0_52
| spl0_57 ),
inference(sat_conversion,[],[f472]) ).
cnf(s65,plain,
( spl0_9
| ~ spl0_17
| spl0_37
| spl0_57 ),
inference(sat_conversion,[],[f477]) ).
cnf(s73,plain,
( ~ spl0_16
| spl0_62 ),
inference(sat_conversion,[],[f495]) ).
cnf(s74,plain,
( ~ spl0_16
| spl0_63 ),
inference(sat_conversion,[],[f499]) ).
cnf(s75,plain,
( ~ spl0_16
| spl0_64 ),
inference(sat_conversion,[],[f503]) ).
cnf(s77,plain,
( ~ spl0_42
| spl0_65 ),
inference(sat_conversion,[],[f510]) ).
cnf(s78,plain,
( ~ spl0_42
| spl0_66 ),
inference(sat_conversion,[],[f514]) ).
cnf(s79,plain,
( ~ spl0_42
| spl0_67 ),
inference(sat_conversion,[],[f518]) ).
cnf(s81,plain,
( ~ spl0_6
| spl0_68 ),
inference(sat_conversion,[],[f524]) ).
cnf(s82,plain,
( ~ spl0_6
| spl0_69 ),
inference(sat_conversion,[],[f528]) ).
cnf(s83,plain,
( ~ spl0_6
| spl0_70 ),
inference(sat_conversion,[],[f532]) ).
cnf(s85,plain,
( ~ spl0_12
| spl0_71 ),
inference(sat_conversion,[],[f538]) ).
cnf(s86,plain,
( ~ spl0_12
| spl0_72 ),
inference(sat_conversion,[],[f542]) ).
cnf(s87,plain,
( ~ spl0_12
| spl0_73 ),
inference(sat_conversion,[],[f546]) ).
cnf(s89,plain,
( ~ spl0_8
| ~ spl0_74 ),
inference(sat_conversion,[],[f552]) ).
cnf(s90,plain,
( ~ spl0_8
| spl0_75 ),
inference(sat_conversion,[],[f556]) ).
cnf(s91,plain,
( ~ spl0_8
| spl0_76 ),
inference(sat_conversion,[],[f560]) ).
cnf(s93,plain,
( ~ spl0_23
| ~ spl0_77 ),
inference(sat_conversion,[],[f566]) ).
cnf(s94,plain,
( ~ spl0_23
| spl0_78 ),
inference(sat_conversion,[],[f570]) ).
cnf(s95,plain,
( ~ spl0_23
| spl0_79 ),
inference(sat_conversion,[],[f574]) ).
cnf(s105,plain,
( ~ spl0_3
| ~ spl0_86 ),
inference(sat_conversion,[],[f608]) ).
cnf(s106,plain,
( ~ spl0_3
| spl0_87 ),
inference(sat_conversion,[],[f612]) ).
cnf(s107,plain,
( ~ spl0_3
| spl0_88 ),
inference(sat_conversion,[],[f616]) ).
cnf(s108,plain,
( ~ spl0_3
| spl0_17 ),
inference(sat_conversion,[],[f617]) ).
cnf(s109,plain,
( ~ spl0_11
| ~ spl0_89 ),
inference(sat_conversion,[],[f622]) ).
cnf(s110,plain,
( ~ spl0_11
| spl0_90 ),
inference(sat_conversion,[],[f626]) ).
cnf(s111,plain,
( ~ spl0_11
| spl0_91 ),
inference(sat_conversion,[],[f630]) ).
cnf(s113,plain,
( ~ spl0_22
| ~ spl0_92 ),
inference(sat_conversion,[],[f636]) ).
cnf(s114,plain,
( ~ spl0_22
| ~ spl0_93 ),
inference(sat_conversion,[],[f640]) ).
cnf(s115,plain,
( ~ spl0_22
| spl0_94 ),
inference(sat_conversion,[],[f644]) ).
cnf(s117,plain,
( ~ spl0_15
| ~ spl0_95 ),
inference(sat_conversion,[],[f650]) ).
cnf(s118,plain,
( ~ spl0_15
| ~ spl0_96 ),
inference(sat_conversion,[],[f654]) ).
cnf(s119,plain,
( ~ spl0_15
| spl0_97 ),
inference(sat_conversion,[],[f658]) ).
cnf(s121,plain,
( ~ spl0_39
| ~ spl0_98 ),
inference(sat_conversion,[],[f664]) ).
cnf(s122,plain,
( ~ spl0_39
| ~ spl0_99 ),
inference(sat_conversion,[],[f668]) ).
cnf(s123,plain,
( ~ spl0_39
| ~ spl0_100 ),
inference(sat_conversion,[],[f672]) ).
cnf(s137,plain,
( ~ spl0_25
| ~ spl0_110 ),
inference(sat_conversion,[],[f720]) ).
cnf(s138,plain,
( ~ spl0_25
| ~ spl0_111 ),
inference(sat_conversion,[],[f724]) ).
cnf(s139,plain,
( ~ spl0_25
| spl0_112 ),
inference(sat_conversion,[],[f728]) ).
cnf(s141,plain,
( ~ spl0_27
| ~ spl0_113 ),
inference(sat_conversion,[],[f734]) ).
cnf(s142,plain,
( ~ spl0_27
| ~ spl0_114 ),
inference(sat_conversion,[],[f738]) ).
cnf(s143,plain,
( ~ spl0_27
| spl0_115 ),
inference(sat_conversion,[],[f742]) ).
cnf(s145,plain,
( ~ spl0_34
| ~ spl0_116 ),
inference(sat_conversion,[],[f748]) ).
cnf(s146,plain,
( ~ spl0_34
| spl0_117 ),
inference(sat_conversion,[],[f752]) ).
cnf(s147,plain,
( ~ spl0_34
| spl0_118 ),
inference(sat_conversion,[],[f756]) ).
cnf(s149,plain,
( ~ spl0_1
| ~ spl0_119 ),
inference(sat_conversion,[],[f762]) ).
cnf(s150,plain,
( ~ spl0_1
| ~ spl0_120 ),
inference(sat_conversion,[],[f766]) ).
cnf(s151,plain,
( ~ spl0_1
| spl0_121 ),
inference(sat_conversion,[],[f770]) ).
cnf(s152,plain,
( ~ spl0_1
| spl0_17 ),
inference(sat_conversion,[],[f771]) ).
cnf(s153,plain,
( ~ spl0_4
| ~ spl0_122 ),
inference(sat_conversion,[],[f776]) ).
cnf(s154,plain,
( ~ spl0_4
| ~ spl0_123 ),
inference(sat_conversion,[],[f780]) ).
cnf(s155,plain,
( ~ spl0_4
| ~ spl0_124 ),
inference(sat_conversion,[],[f784]) ).
cnf(s157,plain,
( ~ spl0_14
| ~ spl0_125 ),
inference(sat_conversion,[],[f790]) ).
cnf(s158,plain,
( ~ spl0_14
| spl0_126 ),
inference(sat_conversion,[],[f794]) ).
cnf(s159,plain,
( ~ spl0_14
| spl0_127 ),
inference(sat_conversion,[],[f798]) ).
cnf(s161,plain,
( ~ spl0_5
| ~ spl0_128 ),
inference(sat_conversion,[],[f804]) ).
cnf(s162,plain,
( ~ spl0_5
| ~ spl0_129 ),
inference(sat_conversion,[],[f808]) ).
cnf(s163,plain,
( ~ spl0_5
| spl0_130 ),
inference(sat_conversion,[],[f812]) ).
cnf(s165,plain,
( ~ spl0_58
| ~ spl0_131 ),
inference(sat_conversion,[],[f818]) ).
cnf(s166,plain,
( ~ spl0_58
| spl0_132 ),
inference(sat_conversion,[],[f822]) ).
cnf(s167,plain,
( ~ spl0_58
| spl0_133 ),
inference(sat_conversion,[],[f826]) ).
cnf(s170,plain,
( ~ spl0_52
| ~ spl0_135 ),
inference(sat_conversion,[],[f836]) ).
cnf(s171,plain,
( ~ spl0_52
| spl0_136 ),
inference(sat_conversion,[],[f840]) ).
cnf(s173,plain,
( ~ spl0_7
| ~ spl0_137 ),
inference(sat_conversion,[],[f846]) ).
cnf(s174,plain,
( ~ spl0_7
| ~ spl0_138 ),
inference(sat_conversion,[],[f850]) ).
cnf(s175,plain,
( ~ spl0_7
| spl0_139 ),
inference(sat_conversion,[],[f854]) ).
cnf(s177,plain,
( ~ spl0_9
| ~ spl0_140 ),
inference(sat_conversion,[],[f860]) ).
cnf(s178,plain,
( ~ spl0_9
| spl0_141 ),
inference(sat_conversion,[],[f864]) ).
cnf(s179,plain,
( ~ spl0_9
| spl0_142 ),
inference(sat_conversion,[],[f868]) ).
cnf(s181,plain,
( ~ spl0_13
| ~ spl0_143 ),
inference(sat_conversion,[],[f874]) ).
cnf(s182,plain,
( ~ spl0_13
| spl0_144 ),
inference(sat_conversion,[],[f878]) ).
cnf(s183,plain,
( ~ spl0_13
| spl0_145 ),
inference(sat_conversion,[],[f882]) ).
cnf(s189,plain,
( ~ spl0_2
| ~ spl0_149 ),
inference(sat_conversion,[],[f902]) ).
cnf(s190,plain,
( ~ spl0_2
| ~ spl0_150 ),
inference(sat_conversion,[],[f906]) ).
cnf(s191,plain,
( ~ spl0_2
| spl0_151 ),
inference(sat_conversion,[],[f910]) ).
cnf(s192,plain,
( ~ spl0_2
| spl0_17 ),
inference(sat_conversion,[],[f911]) ).
cnf(s205,plain,
( ~ spl0_18
| spl0_24
| ~ spl0_30 ),
inference(sat_conversion,[],[f977]) ).
cnf(s208,plain,
( ~ spl0_26
| spl0_95
| ~ spl0_97
| ~ spl0_160 ),
inference(sat_conversion,[],[f991]) ).
cnf(s211,plain,
( ~ spl0_32
| spl0_122
| spl0_123
| ~ spl0_161 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s215,plain,
( ~ spl0_30
| ~ spl0_35
| spl0_50 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s221,plain,
( ~ spl0_41
| spl0_99
| spl0_100
| ~ spl0_163 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s222,plain,
( ~ spl0_44
| spl0_98
| spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f1094]) ).
cnf(s224,plain,
( ~ spl0_44
| spl0_122
| spl0_123
| spl0_161 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s253,plain,
( ~ spl0_24
| ~ spl0_66
| ~ spl0_67
| ~ spl0_169 ),
inference(sat_conversion,[],[f1227]) ).
cnf(s261,plain,
( ~ spl0_45
| ~ spl0_46
| spl0_48 ),
inference(sat_conversion,[],[f1253]) ).
cnf(s262,plain,
( ~ spl0_45
| spl0_48
| ~ spl0_49 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s285,plain,
( ~ spl0_31
| spl0_129
| ~ spl0_130
| ~ spl0_166 ),
inference(sat_conversion,[],[f1331]) ).
cnf(s287,plain,
( ~ spl0_32
| spl0_128
| spl0_129
| ~ spl0_130 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s288,plain,
( ~ spl0_32
| ~ spl0_49
| spl0_53 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s299,plain,
( ~ spl0_26
| spl0_29
| ~ spl0_31 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s300,plain,
( ~ spl0_26
| spl0_143
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f1395]) ).
cnf(s301,plain,
( ~ spl0_26
| spl0_29
| ~ spl0_32 ),
inference(sat_conversion,[],[f1396]) ).
cnf(s334,plain,
( ~ spl0_46
| spl0_135
| ~ spl0_136
| ~ spl0_174 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s335,plain,
( ~ spl0_26
| ~ spl0_65
| ~ spl0_67
| spl0_169 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s361,plain,
( ~ spl0_21
| ~ spl0_41
| spl0_50 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s365,plain,
( ~ spl0_54
| spl0_149
| spl0_150
| ~ spl0_151 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s366,plain,
( ~ spl0_54
| spl0_119
| ~ spl0_121
| spl0_165 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s377,plain,
( ~ spl0_32
| spl0_92
| ~ spl0_94
| spl0_159 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s394,plain,
( ~ spl0_29
| spl0_77
| ~ spl0_79
| ~ spl0_158 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s395,plain,
( ~ spl0_29
| spl0_125
| ~ spl0_126
| ~ spl0_127 ),
inference(sat_conversion,[],[f1604]) ).
cnf(s396,plain,
( ~ spl0_29
| ~ spl0_66
| ~ spl0_67
| spl0_169 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s419,plain,
( ~ spl0_47
| ~ spl0_65
| ~ spl0_66
| ~ spl0_67 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s423,plain,
( spl0_29
| ~ spl0_32
| ~ spl0_47 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s434,plain,
( ~ spl0_50
| spl0_120
| ~ spl0_121
| ~ spl0_165 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s435,plain,
( ~ spl0_50
| spl0_140
| ~ spl0_141
| ~ spl0_142 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s443,plain,
( ~ spl0_53
| spl0_113
| spl0_114
| ~ spl0_115 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s446,plain,
( ~ spl0_54
| spl0_92
| spl0_93
| ~ spl0_159 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s448,plain,
( ~ spl0_35
| ~ spl0_54
| spl0_57 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s459,plain,
( ~ spl0_51
| spl0_74
| spl0_75
| ~ spl0_76 ),
inference(sat_conversion,[],[f1751]) ).
cnf(s463,plain,
( ~ spl0_46
| spl0_74
| ~ spl0_75
| ~ spl0_76 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s465,plain,
( ~ spl0_46
| spl0_116
| ~ spl0_117
| ~ spl0_173 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s466,plain,
( ~ spl0_49
| ~ spl0_69
| ~ spl0_70
| spl0_157 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s468,plain,
( ~ spl0_49
| ~ spl0_78
| ~ spl0_79
| spl0_158 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s469,plain,
( ~ spl0_49
| spl0_116
| ~ spl0_117
| ~ spl0_118 ),
inference(sat_conversion,[],[f1792]) ).
cnf(s472,plain,
( ~ spl0_55
| spl0_77
| ~ spl0_78
| ~ spl0_79 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s475,plain,
( spl0_29
| ~ spl0_31
| ~ spl0_55 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s484,plain,
( ~ spl0_57
| spl0_137
| spl0_138
| ~ spl0_139 ),
inference(sat_conversion,[],[f1858]) ).
cnf(s488,plain,
( ~ spl0_38
| ~ spl0_74
| spl0_75
| spl0_155 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s498,plain,
( ~ spl0_48
| spl0_86
| ~ spl0_87
| ~ spl0_88 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s499,plain,
( ~ spl0_48
| spl0_93
| ~ spl0_94
| ~ spl0_159 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s505,plain,
( ~ spl0_37
| spl0_143
| ~ spl0_144
| spl0_171 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s513,plain,
( ~ spl0_38
| spl0_95
| spl0_96
| ~ spl0_160 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s515,plain,
( ~ spl0_38
| spl0_111
| ~ spl0_112
| spl0_168 ),
inference(sat_conversion,[],[f1920]) ).
cnf(s520,plain,
( ~ spl0_40
| spl0_119
| spl0_120
| ~ spl0_121 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s522,plain,
( ~ spl0_40
| ~ spl0_46
| spl0_57 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s523,plain,
( ~ spl0_45
| spl0_131
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s530,plain,
( ~ spl0_18
| spl0_24
| ~ spl0_31 ),
inference(sat_conversion,[],[f1962]) ).
cnf(s547,plain,
( ~ spl0_21
| ~ spl0_74
| ~ spl0_75
| ~ spl0_76 ),
inference(sat_conversion,[],[f1978]) ).
cnf(s552,plain,
( ~ spl0_21
| spl0_24
| ~ spl0_31 ),
inference(sat_conversion,[],[f1983]) ).
cnf(s566,plain,
( ~ spl0_24
| ~ spl0_68
| ~ spl0_70
| ~ spl0_157 ),
inference(sat_conversion,[],[f1997]) ).
cnf(s581,plain,
( ~ spl0_53
| spl0_93
| ~ spl0_94
| spl0_159 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s582,plain,
( ~ spl0_51
| spl0_95
| ~ spl0_97
| spl0_160 ),
inference(sat_conversion,[],[f2016]) ).
cnf(s584,plain,
( ~ spl0_18
| ~ spl0_68
| ~ spl0_69
| ~ spl0_70 ),
inference(sat_conversion,[],[f2028]) ).
cnf(s589,plain,
( ~ spl0_21
| ~ spl0_65
| ~ spl0_67
| ~ spl0_169 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s590,plain,
( ~ spl0_21
| ~ spl0_68
| ~ spl0_69
| ~ spl0_157 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s591,plain,
( ~ spl0_21
| ~ spl0_71
| ~ spl0_72
| ~ spl0_73 ),
inference(sat_conversion,[],[f2044]) ).
cnf(s594,plain,
( ~ spl0_24
| ~ spl0_62
| ~ spl0_63
| ~ spl0_64 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s595,plain,
( ~ spl0_24
| ~ spl0_66
| ~ spl0_67
| ~ spl0_169 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s599,plain,
( ~ spl0_31
| spl0_89
| ~ spl0_91
| ~ spl0_170 ),
inference(sat_conversion,[],[f2077]) ).
cnf(s602,plain,
( ~ spl0_40
| spl0_89
| ~ spl0_90
| spl0_170 ),
inference(sat_conversion,[],[f2107]) ).
cnf(s607,plain,
( ~ spl0_21
| ~ spl0_40
| spl0_50 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s624,plain,
( ~ spl0_55
| spl0_75
| ~ spl0_76
| ~ spl0_155 ),
inference(sat_conversion,[],[f2128]) ).
cnf(s629,plain,
( ~ spl0_56
| spl0_92
| spl0_93
| spl0_159 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s639,plain,
( ~ spl0_53
| spl0_128
| ~ spl0_130
| spl0_166 ),
inference(sat_conversion,[],[f2145]) ).
cnf(s640,plain,
( ~ spl0_51
| spl0_135
| ~ spl0_136
| spl0_174 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s642,plain,
( ~ spl0_30
| spl0_89
| ~ spl0_90
| ~ spl0_91 ),
inference(sat_conversion,[],[f2164]) ).
cnf(s643,plain,
( ~ spl0_30
| spl0_110
| ~ spl0_112
| ~ spl0_168 ),
inference(sat_conversion,[],[f2165]) ).
cnf(s644,plain,
( ~ spl0_30
| spl0_119
| ~ spl0_121
| ~ spl0_165 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s647,plain,
( ~ spl0_41
| spl0_89
| ~ spl0_91
| spl0_170 ),
inference(sat_conversion,[],[f2181]) ).
cnf(s648,plain,
( ~ spl0_41
| spl0_110
| spl0_111
| ~ spl0_112 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s649,plain,
( ~ spl0_41
| spl0_119
| spl0_120
| ~ spl0_165 ),
inference(sat_conversion,[],[f2183]) ).
cnf(s651,plain,
( ~ spl0_55
| ~ spl0_65
| ~ spl0_66
| spl0_169 ),
inference(sat_conversion,[],[f2197]) ).
cnf(s652,plain,
( ~ spl0_55
| ~ spl0_117
| ~ spl0_118
| spl0_173 ),
inference(sat_conversion,[],[f2198]) ).
cnf(s653,plain,
( ~ spl0_55
| spl0_143
| ~ spl0_144
| ~ spl0_171 ),
inference(sat_conversion,[],[f2199]) ).
cnf(s654,plain,
( ~ spl0_56
| spl0_98
| spl0_99
| spl0_163 ),
inference(sat_conversion,[],[f2217]) ).
cnf(s655,plain,
( ~ spl0_56
| spl0_122
| spl0_123
| spl0_124 ),
inference(sat_conversion,[],[f2218]) ).
cnf(s656,plain,
( ~ spl0_56
| spl0_128
| spl0_129
| spl0_166 ),
inference(sat_conversion,[],[f2219]) ).
cnf(s658,plain,
( spl0_50
| spl0_49
| spl0_30
| ~ spl0_54
| ~ spl0_17
| spl0_2 ),
inference(rat,[],[s300,s181,s182,s183,s50,s26,s377,s446,s113,s114,s115,s31,s443,s648,s141,s142,s143,s137,s138,s139,s42,s43]) ).
cnf(s659,plain,
( ~ spl0_9
| ~ spl0_50 ),
inference(rat,[],[s435,s177,s178,s179]) ).
cnf(s662,plain,
( ~ spl0_25
| ~ spl0_41 ),
inference(rat,[],[s648,s137,s138,s139]) ).
cnf(s663,plain,
( spl0_22
| spl0_30
| spl0_48
| ~ spl0_17
| spl0_2 ),
inference(rat,[],[s654,s221,s121,s122,s123,s38,s662,s60,s395,s157,s158,s159,s31,s19]) ).
cnf(s664,plain,
( spl0_56
| spl0_4
| ~ spl0_3 ),
inference(rat,[],[s395,s157,s158,s159,s58,s60,s108,s498,s105,s106,s107]) ).
cnf(s665,plain,
( ~ spl0_41
| ~ spl0_56
| ~ spl0_3 ),
inference(rat,[],[s654,s221,s121,s122,s123,s38,s662,s108,s498,s105,s106,s107]) ).
cnf(s666,plain,
( spl0_4
| ~ spl0_3
| spl0_2 ),
inference(rat,[],[s629,s446,s113,s114,s31,s665,s664,s52,s108]) ).
cnf(s667,plain,
( ~ spl0_11
| ~ spl0_30 ),
inference(rat,[],[s642,s109,s110,s111]) ).
cnf(s668,plain,
( ~ spl0_42
| ~ spl0_24
| ~ spl0_29 ),
inference(rat,[],[s253,s396,s78,s79]) ).
cnf(s669,plain,
( ~ spl0_14
| ~ spl0_29 ),
inference(rat,[],[s395,s157,s158,s159]) ).
cnf(s670,plain,
( ~ spl0_76
| spl0_74
| ~ spl0_46
| ~ spl0_51 ),
inference(rat,[],[s463,s459]) ).
cnf(s671,plain,
( ~ spl0_7
| ~ spl0_57 ),
inference(rat,[],[s484,s173,s174,s175]) ).
cnf(s672,plain,
( spl0_8
| spl0_7
| ~ spl0_40
| ~ spl0_17
| spl0_1 ),
inference(rat,[],[s659,s607,s3,s11]) ).
cnf(s673,plain,
( spl0_22
| spl0_2
| spl0_1 ),
inference(rat,[],[s670,s89,s91,s672,s671,s522,s59,s513,s582,s117,s118,s119,s34,s261,s36,s668,s205,s8,s667,s222,s121,s122,s123,s48,s38,s662,s663,s31,s669,s60,s655,s153,s154,s155,s666,s108,s498,s105,s106,s107,s1]) ).
cnf(s674,plain,
( spl0_159
| spl0_2
| spl0_1 ),
inference(rat,[],[s670,s89,s91,s672,s671,s522,s59,s513,s582,s117,s118,s119,s34,s222,s121,s122,s123,s48,s38,s261,s662,s36,s32,s668,s205,s8,s667,s26,s300,s181,s182,s183,s50,s377,s581,s669,s60,s655,s153,s154,s155,s666,s108,s498,s105,s106,s107,s1,s115,s114,s113,s673]) ).
cnf(s675,plain,
( spl0_46
| ~ spl0_29
| ~ spl0_17 ),
inference(rat,[],[s37,s419,s668,s77,s78,s79,s36,s669]) ).
cnf(s676,plain,
( ~ spl0_34
| ~ spl0_46
| ~ spl0_55 ),
inference(rat,[],[s465,s652,s145,s146,s147]) ).
cnf(s677,plain,
( ~ spl0_76
| spl0_2
| spl0_1 ),
inference(rat,[],[s671,s672,s522,s59,s488,s624,s547,s11,s89,s670,s56,s676,s675,s60,s655,s153,s154,s155,s666,s54,s498,s105,s106,s107,s446,s674,s114,s113,s673,s108,s1]) ).
cnf(s679,plain,
( spl0_41
| spl0_42
| spl0_122
| spl0_123
| ~ spl0_17 ),
inference(rat,[],[s224,s211,s35,s32]) ).
cnf(s680,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s671,s3,s65,s659,s361,s679,s505,s653,s668,s181,s182,s552,s6,s11,s91,s677,s53,s54,s446,s674,s113,s114,s673,s669,s60,s655,s153,s154,s155,s666,s498,s105,s106,s107,s108,s1]) ).
cnf(s681,plain,
( ~ spl0_42
| spl0_46
| ~ spl0_55
| ~ spl0_17 ),
inference(rat,[],[s37,s595,s419,s651,s77,s78,s79]) ).
cnf(s682,plain,
( ~ spl0_5
| ~ spl0_32 ),
inference(rat,[],[s287,s161,s162,s163]) ).
cnf(s685,plain,
( ~ spl0_6
| ~ spl0_49
| ~ spl0_24 ),
inference(rat,[],[s566,s466,s81,s82,s83]) ).
cnf(s686,plain,
( spl0_46
| spl0_29
| spl0_48
| spl0_41
| ~ spl0_2 ),
inference(rat,[],[s659,s215,s20,s21,s685,s40,s682,s55,s37,s301,s423,s32,s681,s475,s54,s192,s365,s189,s190,s191]) ).
cnf(s687,plain,
( ~ spl0_42
| ~ spl0_21
| ~ spl0_55 ),
inference(rat,[],[s589,s651,s77,s78,s79]) ).
cnf(s688,plain,
( spl0_6
| ~ spl0_35
| spl0_31
| ~ spl0_17 ),
inference(rat,[],[s659,s215,s20,s21]) ).
cnf(s689,plain,
( spl0_29
| ~ spl0_76
| spl0_48
| spl0_41
| spl0_1 ),
inference(rat,[],[s590,s466,s81,s82,s83,s688,s40,s55,s682,s301,s32,s687,s11,s89,s670,s47,s261,s686,s475,s54,s192,s365,s189,s190,s191,s680]) ).
cnf(s690,plain,
( ~ spl0_4
| ~ spl0_56 ),
inference(rat,[],[s655,s153,s154,s155]) ).
cnf(s691,plain,
( spl0_29
| spl0_48
| spl0_41
| spl0_4
| spl0_1 ),
inference(rat,[],[s590,s466,s81,s82,s83,s2,s55,s682,s301,s32,s687,s11,s91,s689,s54,s192,s365,s189,s190,s191,s680]) ).
cnf(s692,plain,
( spl0_8
| spl0_14
| ~ spl0_55
| spl0_41
| spl0_4
| spl0_1 ),
inference(rat,[],[s685,s2,s55,s682,s300,s32,s181,s182,s183,s687,s552,s6,s11,s53,s192,s365,s189,s190,s191,s680]) ).
cnf(s693,plain,
( ~ spl0_3
| ~ spl0_56
| spl0_1 ),
inference(rat,[],[s670,s89,s91,s692,s56,s676,s675,s669,s691,s54,s498,s665,s105,s106,s107,s192,s365,s189,s190,s191,s680,s690]) ).
cnf(s694,plain,
( ~ spl0_41
| spl0_48
| ~ spl0_56
| ~ spl0_17 ),
inference(rat,[],[s654,s221,s121,s122,s123,s38,s662]) ).
cnf(s695,plain,
( spl0_48
| ~ spl0_56
| spl0_1 ),
inference(rat,[],[s670,s56,s89,s91,s676,s692,s675,s669,s691,s694,s54,s192,s365,s189,s190,s191,s680,s690]) ).
cnf(s696,plain,
( ~ spl0_32
| ~ spl0_24
| spl0_29
| spl0_4
| ~ spl0_2 ),
inference(rat,[],[s685,s2,s55,s682,s301,s192,s365,s189,s190,s191]) ).
cnf(s697,plain,
( spl0_49
| spl0_32
| spl0_29
| ~ spl0_2 ),
inference(rat,[],[s299,s55,s41,s192,s365,s189,s190,s191]) ).
cnf(s698,plain,
( ~ spl0_16
| ~ spl0_24 ),
inference(rat,[],[s594,s73,s74,s75]) ).
cnf(s699,plain,
( ~ spl0_22
| ~ spl0_48
| ~ spl0_53 ),
inference(rat,[],[s581,s499,s114,s115]) ).
cnf(s700,plain,
( ~ spl0_41
| spl0_29
| spl0_22
| spl0_3
| ~ spl0_56
| ~ spl0_2 ),
inference(rat,[],[s285,s656,s20,s161,s162,s163,s659,s2,s361,s685,s12,s697,s698,s696,s14,s662,s192,s690]) ).
cnf(s701,plain,
( ~ spl0_24
| spl0_41
| spl0_29
| spl0_22
| spl0_4
| ~ spl0_2 ),
inference(rat,[],[s591,s85,s86,s87,s5,s667,s26,s335,s253,s685,s77,s78,s79,s12,s697,s32,s698,s696,s192]) ).
cnf(s702,plain,
( ~ spl0_32
| spl0_24
| spl0_29
| spl0_4
| spl0_1 ),
inference(rat,[],[s463,s89,s90,s91,s11,s590,s466,s81,s82,s83,s2,s55,s37,s682,s301,s423,s192,s365,s189,s190,s191,s680]) ).
cnf(s703,plain,
( spl0_29
| ~ spl0_56
| spl0_1 ),
inference(rat,[],[s469,s145,s146,s147,s697,s25,s702,s701,s700,s690,s693,s699,s695,s57,s365,s189,s190,s191,s192,s680]) ).
cnf(s704,plain,
( ~ spl0_6
| ~ spl0_18 ),
inference(rat,[],[s584,s81,s82,s83]) ).
cnf(s705,plain,
( ~ spl0_56
| spl0_1 ),
inference(rat,[],[s656,s285,s161,s162,s163,s2,s704,s8,s667,s19,s53,s669,s703,s699,s695,s690,s57,s365,s189,s190,s191,s192,s680]) ).
cnf(s706,plain,
( ~ spl0_41
| spl0_4
| spl0_29
| spl0_1 ),
inference(rat,[],[s639,s285,s20,s161,s162,s163,s659,s2,s361,s685,s12,s697,s698,s696,s14,s662,s699,s60,s57,s365,s189,s190,s191,s192,s680,s664,s705]) ).
cnf(s707,plain,
( spl0_4
| spl0_29
| spl0_1 ),
inference(rat,[],[s469,s145,s146,s147,s697,s25,s702,s701,s706,s699,s60,s705,s57,s365,s189,s190,s191,s192,s680]) ).
cnf(s708,plain,
( ~ spl0_3
| ~ spl0_48 ),
inference(rat,[],[s498,s105,s106,s107]) ).
cnf(s709,plain,
( ~ spl0_11
| ~ spl0_31
| ~ spl0_41 ),
inference(rat,[],[s599,s647,s109,s111]) ).
cnf(s710,plain,
( ~ spl0_12
| ~ spl0_21 ),
inference(rat,[],[s591,s85,s86,s87]) ).
cnf(s711,plain,
( spl0_49
| spl0_29
| ~ spl0_2 ),
inference(rat,[],[s301,s697,s55,s192,s365,s189,s190,s191]) ).
cnf(s712,plain,
( ~ spl0_41
| ~ spl0_49
| spl0_3
| spl0_22
| ~ spl0_17 ),
inference(rat,[],[s709,s5,s20,s685,s710,s659,s361,s12,s698,s14,s662]) ).
cnf(s713,plain,
( ~ spl0_34
| ~ spl0_49 ),
inference(rat,[],[s469,s145,s146,s147]) ).
cnf(s714,plain,
( ~ spl0_24
| spl0_29
| spl0_1 ),
inference(rat,[],[s602,s599,s59,s21,s513,s667,s109,s110,s111,s582,s5,s117,s118,s119,s710,s7,s12,s685,s698,s699,s60,s705,s57,s56,s713,s711,s365,s189,s190,s191,s192,s680]) ).
cnf(s715,plain,
( ~ spl0_8
| ~ spl0_46
| ~ spl0_51 ),
inference(rat,[],[s670,s89,s91]) ).
cnf(s716,plain,
( spl0_29
| spl0_1 ),
inference(rat,[],[s590,s466,s81,s82,s83,s21,s552,s11,s715,s643,s515,s137,s138,s139,s37,s14,s29,s714,s56,s713,s419,s77,s78,s79,s679,s712,s711,s708,s153,s154,s707,s699,s60,s57,s365,s189,s190,s191,s192,s680,s705]) ).
cnf(s717,plain,
( ~ spl0_24
| ~ spl0_26
| spl0_1 ),
inference(rat,[],[s48,s699,s582,s12,s208,s710,s117,s119,s5,s7,s704,s8,s709,s662,s679,s698,s668,s57,s53,s365,s189,s190,s191,s154,s153,s58,s669,s716,s192,s680,s705]) ).
cnf(s718,plain,
( ~ spl0_8
| ~ spl0_46 ),
inference(rat,[],[s463,s89,s90,s91]) ).
cnf(s719,plain,
spl0_1,
inference(rat,[],[s5,s685,s709,s55,s679,s717,s668,s710,s552,s11,s718,s153,s154,s53,s58,s675,s669,s716,s705,s365,s189,s190,s191,s192,s680]) ).
cnf(s720,plain,
spl0_17,
inference(rat,[],[s152,s719]) ).
cnf(s721,plain,
spl0_121,
inference(rat,[],[s151,s719]) ).
cnf(s722,plain,
~ spl0_120,
inference(rat,[],[s150,s719]) ).
cnf(s723,plain,
~ spl0_119,
inference(rat,[],[s149,s719]) ).
cnf(s724,plain,
~ spl0_40,
inference(rat,[],[s520,s721,s722,s723]) ).
cnf(s725,plain,
( ~ spl0_54
| spl0_49
| spl0_2 ),
inference(rat,[],[s658,s644,s434,s366,s720,s721,s723,s722]) ).
cnf(s726,plain,
( spl0_49
| spl0_29
| spl0_2 ),
inference(rat,[],[s41,s299,s301,s55,s725,s720]) ).
cnf(s727,plain,
( ~ spl0_54
| spl0_6
| spl0_29
| spl0_2 ),
inference(rat,[],[s377,s26,s446,s299,s113,s114,s115,s21,s31,s644,s649,s366,s720,s721,s723,s722]) ).
cnf(s728,plain,
( ~ spl0_24
| spl0_29
| spl0_2 ),
inference(rat,[],[s513,s59,s582,s690,s56,s52,s727,s117,s118,s119,s7,s685,s698,s713,s726,s720,s724]) ).
cnf(s729,plain,
( ~ spl0_54
| spl0_29
| spl0_2 ),
inference(rat,[],[s699,s31,s40,s649,s448,s366,s288,s682,s671,s17,s301,s25,s713,s726,s728,s720,s722,s723,s721]) ).
cnf(s730,plain,
( spl0_29
| spl0_2 ),
inference(rat,[],[s712,s31,s708,s699,s54,s729,s472,s93,s94,s95,s288,s13,s25,s728,s713,s726,s720]) ).
cnf(s731,plain,
( spl0_49
| spl0_2 ),
inference(rat,[],[s55,s725,s300,s181,s182,s183,s6,s718,s675,s669,s730,s720]) ).
cnf(s732,plain,
( ~ spl0_54
| spl0_2 ),
inference(rat,[],[s446,s377,s113,s114,s115,s26,s31,s644,s649,s366,s300,s181,s182,s183,s6,s718,s675,s669,s730,s720,s721,s723,s722]) ).
cnf(s733,plain,
( ~ spl0_15
| spl0_2 ),
inference(rat,[],[s513,s582,s117,s118,s119,s56,s713,s731,s59,s690,s52,s732,s724,s720]) ).
cnf(s734,plain,
( ~ spl0_24
| spl0_2 ),
inference(rat,[],[s7,s685,s698,s731,s733]) ).
cnf(s735,plain,
spl0_2,
inference(rat,[],[s394,s468,s93,s94,s95,s13,s734,s731,s730,s720]) ).
cnf(s736,plain,
spl0_151,
inference(rat,[],[s191,s735]) ).
cnf(s737,plain,
~ spl0_150,
inference(rat,[],[s190,s735]) ).
cnf(s738,plain,
~ spl0_149,
inference(rat,[],[s189,s735]) ).
cnf(s739,plain,
~ spl0_54,
inference(rat,[],[s365,s736,s737,s738]) ).
cnf(s740,plain,
spl0_49,
inference(rat,[],[s300,s181,s182,s183,s6,s718,s675,s669,s55,s711,s720,s739,s735]) ).
cnf(s741,plain,
~ spl0_34,
inference(rat,[],[s713,s740]) ).
cnf(s742,plain,
spl0_51,
inference(rat,[],[s56,s720,s739,s741]) ).
cnf(s743,plain,
( ~ spl0_24
| spl0_29 ),
inference(rat,[],[s651,s253,s54,s77,s78,s79,s699,s35,s221,s51,s222,s654,s12,s688,s121,s122,s123,s710,s285,s30,s5,s656,s667,s161,s162,s163,s26,s2,s696,s690,s59,s208,s513,s582,s117,s118,s119,s7,s685,s698,s720,s739,s724,s735,s742,s740]) ).
cnf(s745,plain,
( ~ spl0_52
| ~ spl0_46 ),
inference(rat,[],[s334,s640,s170,s171,s742]) ).
cnf(s746,plain,
( ~ spl0_58
| ~ spl0_45 ),
inference(rat,[],[s523,s165,s166,s167]) ).
cnf(s747,plain,
spl0_29,
inference(rat,[],[s21,s704,s530,s62,s746,s643,s515,s137,s138,s139,s14,s29,s708,s262,s63,s745,s671,s17,s37,s301,s423,s25,s743,s720,s740,s741]) ).
cnf(s748,plain,
~ spl0_14,
inference(rat,[],[s669,s747]) ).
cnf(s749,plain,
spl0_46,
inference(rat,[],[s675,s720,s747]) ).
cnf(s750,plain,
spl0_31,
inference(rat,[],[s53,s739,s720,s748]) ).
cnf(s751,plain,
~ spl0_8,
inference(rat,[],[s718,s749]) ).
cnf(s752,plain,
~ spl0_52,
inference(rat,[],[s745,s749]) ).
cnf(s753,plain,
spl0_13,
inference(rat,[],[s6,s748,s751]) ).
cnf(s754,plain,
spl0_145,
inference(rat,[],[s183,s753]) ).
cnf(s755,plain,
spl0_144,
inference(rat,[],[s182,s753]) ).
cnf(s756,plain,
~ spl0_143,
inference(rat,[],[s181,s753]) ).
cnf(s757,plain,
~ spl0_26,
inference(rat,[],[s300,s754,s755,s756]) ).
cnf(s758,plain,
( spl0_6
| spl0_16 ),
inference(rat,[],[s656,s285,s161,s162,s163,s2,s690,s59,s513,s582,s117,s118,s119,s7,s742,s724,s720,s750]) ).
cnf(s759,plain,
~ spl0_24,
inference(rat,[],[s758,s685,s698,s740]) ).
cnf(s762,plain,
~ spl0_18,
inference(rat,[],[s530,s750,s759]) ).
cnf(s763,plain,
spl0_7,
inference(rat,[],[s17,s757,s720,s759]) ).
cnf(s769,plain,
~ spl0_57,
inference(rat,[],[s671,s763]) ).
cnf(s771,plain,
spl0_45,
inference(rat,[],[s63,s752,s720,s769]) ).
cnf(s772,plain,
spl0_58,
inference(rat,[],[s62,s762,s720,s769]) ).
cnf(s779,plain,
$false,
inference(rat,[],[s746,s771,s772]) ).
fof(f2220,plain,
$false,
inference(avatar_sat_refutation,[],[s779]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN473+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n015.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 16:14:47 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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.58/1.17 % (2752808)Detected formulas, will run a generic FOF schedule.
% 3.58/1.17 % (2752817)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3038053984:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.58/1.17 % (2752817)Instruction limit reached!
% 3.58/1.17 % (2752817)------------------------------
% 3.58/1.17 % (2752817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.58/1.17 % (2752817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.58/1.17 % (2752817)CaDiCaL version: 2.1.3
% 3.58/1.17 % (2752817)Termination reason: Instruction limit
% 3.58/1.17 % (2752817)Termination phase: Saturation
% 3.58/1.17 % (2752817)Time elapsed: 0.030 s
% 3.58/1.17 % (2752817)Peak memory usage: 88 MB
% 3.58/1.17 % (2752817)Instructions burned: 120 (million)
% 3.58/1.17 % (2752816)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1720548880:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.58/1.17 % (2752813)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=3613007999:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.58/1.17 % (2752814)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=550247402:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.58/1.17 % (2752815)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=3222426027:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.58/1.17 % (2752818)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2839908268:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.58/1.17 % (2752819)dis-21_1_sil=8000:lcm=predicate:random_seed=335314548: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.58/1.17 % (2752819)First to succeed.
% 3.58/1.17 % (2752818)Also succeeded, but the first one will report.
% 3.58/1.17 % (2752819)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2752808"
% 3.58/1.17 % (2752816)Also succeeded, but the first one will report.
% 3.58/1.17 % (2752821)lrs+10_1_sil=8000:sp=occurrence:random_seed=2708051385:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.58/1.17 % (2752821)Also succeeded, but the first one will report.
% 3.58/1.17 % (2752819)Refutation found. Thanks to Tanya!
% 3.58/1.17 % SZS status Theorem for theBenchmark
% 3.58/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 4.01/1.37 % (2752819)------------------------------
% 4.01/1.37 % (2752819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.37 % (2752819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.37 % (2752819)CaDiCaL version: 2.1.3
% 4.01/1.37 % (2752819)Termination reason: Refutation
% 4.01/1.37 % (2752819)Time elapsed: 0.039 s
% 4.01/1.37 % (2752819)Peak memory usage: 90 MB
% 4.01/1.37 % (2752819)Instructions burned: 63 (million)
% 4.01/1.37 % (2752819)------------------------------
% 4.01/1.37 % (2752819)------------------------------
% 4.01/1.37 % (2752808)Success in time 0.484 s
% 4.01/1.37 % Vampire exiting
%------------------------------------------------------------------------------