%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN510+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:16:40 PM UTC 2026
% Result : Theorem 33.00s 4.56s
% Output : CNFRefutation 33.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 1
% Syntax : Number of formulae : 628 ( 10 unt; 0 def)
% Number of atoms : 5652 ( 0 equ)
% Maximal formula atoms : 720 ( 9 avg)
% Number of connectives : 8082 (3058 ~;3982 |; 828 &)
% ( 0 <=>; 214 =>; 0 <=; 0 <~>)
% Maximal formula depth : 116 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 34 prp; 0-1 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 636 ( 636 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( hskp23
| hskp22
| hskp21 )
& ( hskp2
| hskp9
| hskp24 )
& ( hskp2
| hskp6
| hskp26 )
& ( hskp22
| hskp7
| hskp26 )
& ( hskp18
| hskp24
| hskp3 )
& ( hskp22
| hskp25
| hskp13 )
& ( hskp6
| hskp14
| hskp13 )
& ( hskp6
| hskp24
| hskp13 )
& ( hskp4
| hskp7
| hskp12 )
& ( hskp14
| hskp10
| hskp5 )
& ( hskp25
| hskp27
| hskp5 )
& ( hskp22
| hskp20
| hskp31 )
& ( hskp16
| hskp10
| hskp31 )
& ( hskp14
| hskp12
| hskp31 )
& ( hskp23
| hskp15
| hskp28 )
& ( hskp14
| hskp20
| ! [X101] :
( ndr1_0
=> ( ~ c3_1(X101)
| ~ c2_1(X101)
| ~ c1_1(X101) ) ) )
& ( hskp14
| hskp10
| ! [X100] :
( ndr1_0
=> ( ~ c3_1(X100)
| ~ c2_1(X100)
| ~ c0_1(X100) ) ) )
& ( hskp4
| hskp26
| ! [X99] :
( ndr1_0
=> ( ~ c3_1(X99)
| ~ c2_1(X99)
| ~ c0_1(X99) ) ) )
& ( hskp26
| hskp27
| ! [X98] :
( ndr1_0
=> ( ~ c3_1(X98)
| ~ c1_1(X98)
| ~ c0_1(X98) ) ) )
& ( hskp14
| ! [X97] :
( ndr1_0
=> ( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c0_1(X97) ) )
| ! [X96] :
( ndr1_0
=> ( ~ c3_1(X96)
| ~ c1_1(X96)
| ~ c0_1(X96) ) ) )
& ( hskp14
| hskp26
| ! [X95] :
( ndr1_0
=> ( ~ c2_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95) ) ) )
& ( hskp4
| hskp5
| ! [X94] :
( ndr1_0
=> ( ~ c2_1(X94)
| ~ c1_1(X94)
| c3_1(X94) ) ) )
& ( hskp9
| hskp25
| ! [X93] :
( ndr1_0
=> ( ~ c2_1(X93)
| ~ c0_1(X93)
| c3_1(X93) ) ) )
& ( hskp21
| hskp14
| ! [X92] :
( ndr1_0
=> ( ~ c2_1(X92)
| ~ c0_1(X92)
| c3_1(X92) ) ) )
& ( hskp24
| hskp26
| ! [X91] :
( ndr1_0
=> ( ~ c2_1(X91)
| ~ c0_1(X91)
| c3_1(X91) ) ) )
& ( hskp7
| hskp30
| ! [X90] :
( ndr1_0
=> ( ~ c2_1(X90)
| ~ c0_1(X90)
| c3_1(X90) ) ) )
& ( hskp21
| hskp12
| ! [X89] :
( ndr1_0
=> ( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89) ) ) )
& ( hskp6
| hskp3
| ! [X88] :
( ndr1_0
=> ( ~ c3_1(X88)
| ~ c1_1(X88)
| c2_1(X88) ) ) )
& ( hskp0
| hskp15
| ! [X87] :
( ndr1_0
=> ( ~ c3_1(X87)
| ~ c0_1(X87)
| c2_1(X87) ) ) )
& ( hskp4
| hskp25
| ! [X86] :
( ndr1_0
=> ( ~ c1_1(X86)
| c3_1(X86)
| c2_1(X86) ) ) )
& ( hskp6
| hskp3
| ! [X85] :
( ndr1_0
=> ( ~ c1_1(X85)
| c3_1(X85)
| c2_1(X85) ) ) )
& ( hskp14
| ! [X84] :
( ndr1_0
=> ( ~ c3_1(X84)
| ~ c2_1(X84)
| ~ c0_1(X84) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c1_1(X83)
| c3_1(X83)
| c2_1(X83) ) ) )
& ( hskp24
| ! [X82] :
( ndr1_0
=> ( ~ c3_1(X82)
| ~ c1_1(X82)
| ~ c0_1(X82) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81) ) ) )
& ( hskp22
| hskp21
| ! [X80] :
( ndr1_0
=> ( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80) ) ) )
& ( ! [X79] :
( ndr1_0
=> ( ~ c3_1(X79)
| ~ c2_1(X79)
| ~ c0_1(X79) ) )
| ! [X78] :
( ndr1_0
=> ( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( ~ c2_1(X77)
| ~ c0_1(X77)
| c3_1(X77) ) )
| ! [X76] :
( ndr1_0
=> ( ~ c3_1(X76)
| ~ c0_1(X76)
| c2_1(X76) ) )
| ! [X75] :
( ndr1_0
=> ( ~ c3_1(X75)
| ~ c0_1(X75)
| c1_1(X75) ) ) )
& ( hskp23
| ! [X74] :
( ndr1_0
=> ( ~ c2_1(X74)
| ~ c1_1(X74)
| ~ c0_1(X74) ) )
| ! [X73] :
( ndr1_0
=> ( ~ c2_1(X73)
| ~ c0_1(X73)
| c1_1(X73) ) ) )
& ( hskp3
| ! [X72] :
( ndr1_0
=> ( ~ c3_1(X72)
| ~ c1_1(X72)
| c2_1(X72) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71) ) ) )
& ( hskp7
| ! [X70] :
( ndr1_0
=> ( ~ c1_1(X70)
| ~ c0_1(X70)
| c2_1(X70) ) )
| ! [X69] :
( ndr1_0
=> ( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69) ) ) )
& ( hskp22
| ! [X68] :
( ndr1_0
=> ( ~ c1_1(X68)
| c3_1(X68)
| c2_1(X68) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c2_1(X67)
| ~ c0_1(X67)
| c1_1(X67) ) ) )
& ( hskp19
| ! [X66] :
( ndr1_0
=> ( ~ c3_1(X66)
| ~ c2_1(X66)
| c1_1(X66) ) )
| ! [X65] :
( ndr1_0
=> ( ~ c2_1(X65)
| ~ c0_1(X65)
| c1_1(X65) ) ) )
& ( hskp21
| hskp29
| ! [X64] :
( ndr1_0
=> ( ~ c2_1(X64)
| c3_1(X64)
| c1_1(X64) ) ) )
& ( hskp20
| hskp13
| ! [X63] :
( ndr1_0
=> ( ~ c0_1(X63)
| c3_1(X63)
| c1_1(X63) ) ) )
& ( hskp13
| ! [X62] :
( ndr1_0
=> ( ~ c2_1(X62)
| ~ c1_1(X62)
| ~ c0_1(X62) ) )
| ! [X61] :
( ndr1_0
=> ( ~ c0_1(X61)
| c3_1(X61)
| c1_1(X61) ) ) )
& ( hskp9
| hskp19
| ! [X60] :
( ndr1_0
=> ( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60) ) ) )
& ( hskp11
| hskp12
| ! [X59] :
( ndr1_0
=> ( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59) ) ) )
& ( hskp18
| ! [X58] :
( ndr1_0
=> ( ~ c2_1(X58)
| ~ c1_1(X58)
| c3_1(X58) ) )
| ! [X57] :
( ndr1_0
=> ( ~ c0_1(X57)
| c2_1(X57)
| c1_1(X57) ) ) )
& ( hskp12
| ! [X56] :
( ndr1_0
=> ( ~ c1_1(X56)
| ~ c0_1(X56)
| c3_1(X56) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c0_1(X55)
| c2_1(X55)
| c1_1(X55) ) ) )
& ( hskp17
| ! [X54] :
( ndr1_0
=> ( ~ c1_1(X54)
| ~ c0_1(X54)
| c2_1(X54) ) )
| ! [X53] :
( ndr1_0
=> ( ~ c0_1(X53)
| c2_1(X53)
| c1_1(X53) ) ) )
& ( hskp16
| hskp3
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| c2_1(X52)
| c1_1(X52) ) ) )
& ( hskp2
| hskp15
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| c2_1(X51)
| c1_1(X51) ) ) )
& ( hskp14
| hskp13
| ! [X50] :
( ndr1_0
=> ( ~ c3_1(X50)
| ~ c2_1(X50)
| c0_1(X50) ) ) )
& ( hskp12
| ! [X49] :
( ndr1_0
=> ( ~ c2_1(X49)
| ~ c1_1(X49)
| ~ c0_1(X49) ) )
| ! [X48] :
( ndr1_0
=> ( ~ c3_1(X48)
| ~ c2_1(X48)
| c0_1(X48) ) ) )
& ( hskp31
| ! [X47] :
( ndr1_0
=> ( ~ c2_1(X47)
| ~ c0_1(X47)
| c1_1(X47) ) )
| ! [X46] :
( ndr1_0
=> ( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( ~ c3_1(X45)
| ~ c0_1(X45)
| c2_1(X45) ) )
| ! [X44] :
( ndr1_0
=> ( ~ c2_1(X44)
| c3_1(X44)
| c1_1(X44) ) )
| ! [X43] :
( ndr1_0
=> ( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43) ) ) )
& ( hskp30
| hskp0
| ! [X42] :
( ndr1_0
=> ( ~ c3_1(X42)
| ~ c1_1(X42)
| c0_1(X42) ) ) )
& ( hskp6
| ! [X41] :
( ndr1_0
=> ( ~ c1_1(X41)
| ~ c0_1(X41)
| c2_1(X41) ) )
| ! [X40] :
( ndr1_0
=> ( ~ c3_1(X40)
| ~ c1_1(X40)
| c0_1(X40) ) ) )
& ( hskp9
| hskp10
| ! [X39] :
( ndr1_0
=> ( ~ c2_1(X39)
| ~ c1_1(X39)
| c0_1(X39) ) ) )
& ( hskp0
| ! [X38] :
( ndr1_0
=> ( ~ c3_1(X38)
| ~ c2_1(X38)
| ~ c0_1(X38) ) )
| ! [X37] :
( ndr1_0
=> ( ~ c2_1(X37)
| c3_1(X37)
| c0_1(X37) ) ) )
& ( hskp9
| hskp11
| ! [X36] :
( ndr1_0
=> ( ~ c1_1(X36)
| c3_1(X36)
| c0_1(X36) ) ) )
& ( ! [X35] :
( ndr1_0
=> ( ~ c3_1(X35)
| ~ c2_1(X35)
| ~ c0_1(X35) ) )
| ! [X34] :
( ndr1_0
=> ( ~ c3_1(X34)
| ~ c1_1(X34)
| ~ c0_1(X34) ) )
| ! [X33] :
( ndr1_0
=> ( ~ c1_1(X33)
| c3_1(X33)
| c0_1(X33) ) ) )
& ( hskp11
| ! [X32] :
( ndr1_0
=> ( ~ c2_1(X32)
| ~ c1_1(X32)
| ~ c0_1(X32) ) )
| ! [X31] :
( ndr1_0
=> ( ~ c1_1(X31)
| c3_1(X31)
| c0_1(X31) ) ) )
& ( hskp11
| hskp29
| ! [X30] :
( ndr1_0
=> ( ~ c3_1(X30)
| c2_1(X30)
| c0_1(X30) ) ) )
& ( hskp10
| hskp8
| ! [X29] :
( ndr1_0
=> ( ~ c1_1(X29)
| c2_1(X29)
| c0_1(X29) ) ) )
& ( ! [X28] :
( ndr1_0
=> ( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X27] :
( ndr1_0
=> ( ~ c3_1(X27)
| ~ c2_1(X27)
| c0_1(X27) ) )
| ! [X26] :
( ndr1_0
=> ( ~ c1_1(X26)
| c2_1(X26)
| c0_1(X26) ) ) )
& ( ! [X25] :
( ndr1_0
=> ( ~ c0_1(X25)
| c3_1(X25)
| c1_1(X25) ) )
| ! [X24] :
( ndr1_0
=> ( ~ c3_1(X24)
| c2_1(X24)
| c0_1(X24) ) )
| ! [X23] :
( ndr1_0
=> ( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) ) ) )
& ( hskp9
| hskp8
| ! [X22] :
( ndr1_0
=> ( c3_1(X22)
| c2_1(X22)
| c0_1(X22) ) ) )
& ( hskp7
| ! [X21] :
( ndr1_0
=> ( ~ c3_1(X21)
| ~ c0_1(X21)
| c2_1(X21) ) )
| ! [X20] :
( ndr1_0
=> ( c3_1(X20)
| c2_1(X20)
| c0_1(X20) ) ) )
& ( ! [X19] :
( ndr1_0
=> ( ~ c3_1(X19)
| ~ c1_1(X19)
| ~ c0_1(X19) ) )
| ! [X18] :
( ndr1_0
=> ( ~ c1_1(X18)
| ~ c0_1(X18)
| c2_1(X18) ) )
| ! [X17] :
( ndr1_0
=> ( c3_1(X17)
| c2_1(X17)
| c0_1(X17) ) ) )
& ( hskp6
| ! [X16] :
( ndr1_0
=> ( ~ c2_1(X16)
| ~ c0_1(X16)
| c1_1(X16) ) )
| ! [X15] :
( ndr1_0
=> ( c3_1(X15)
| c2_1(X15)
| c0_1(X15) ) ) )
& ( hskp2
| hskp5
| ! [X14] :
( ndr1_0
=> ( ~ c3_1(X14)
| c1_1(X14)
| c0_1(X14) ) ) )
& ( hskp1
| ! [X13] :
( ndr1_0
=> ( ~ c2_1(X13)
| ~ c1_1(X13)
| ~ c0_1(X13) ) )
| ! [X12] :
( ndr1_0
=> ( ~ c3_1(X12)
| c1_1(X12)
| c0_1(X12) ) ) )
& ( ! [X11] :
( ndr1_0
=> ( ~ c3_1(X11)
| ~ c2_1(X11)
| c0_1(X11) ) )
| ! [X10] :
( ndr1_0
=> ( ~ c3_1(X10)
| c1_1(X10)
| c0_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( ~ c2_1(X9)
| c1_1(X9)
| c0_1(X9) ) ) )
& ( hskp2
| hskp28
| ! [X8] :
( ndr1_0
=> ( c3_1(X8)
| c1_1(X8)
| c0_1(X8) ) ) )
& ( hskp4
| ! [X7] :
( ndr1_0
=> ( ~ c3_1(X7)
| ~ c0_1(X7)
| c2_1(X7) ) )
| ! [X6] :
( ndr1_0
=> ( c3_1(X6)
| c1_1(X6)
| c0_1(X6) ) ) )
& ( ! [X5] :
( ndr1_0
=> ( ~ c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) ) )
| ! [X4] :
( ndr1_0
=> ( ~ c0_1(X4)
| c3_1(X4)
| c1_1(X4) ) )
| ! [X3] :
( ndr1_0
=> ( c3_1(X3)
| c1_1(X3)
| c0_1(X3) ) ) )
& ( hskp3
| ! [X2] :
( ndr1_0
=> ( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) )
| ! [X1] :
( ndr1_0
=> ( c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ) )
& ( hskp2
| ! [Z] :
( ndr1_0
=> ( ~ c2_1(Z)
| ~ c1_1(Z)
| ~ c0_1(Z) ) )
| ! [Y] :
( ndr1_0
=> ( c2_1(Y)
| c1_1(Y)
| c0_1(Y) ) ) )
& ( hskp1
| ! [X] :
( ndr1_0
=> ( ~ c3_1(X)
| ~ c0_1(X)
| c1_1(X) ) )
| ! [W] :
( ndr1_0
=> ( c2_1(W)
| c1_1(W)
| c0_1(W) ) ) )
& ( hskp0
| ! [V] :
( ndr1_0
=> ( ~ c3_1(V)
| c1_1(V)
| c0_1(V) ) )
| ! [U] :
( ndr1_0
=> ( c2_1(U)
| c1_1(U)
| c0_1(U) ) ) )
& ( ( c3_1(a563)
& c1_1(a563)
& c0_1(a563)
& ndr1_0 )
| ~ hskp31 )
& ( ( c3_1(a562)
& c2_1(a562)
& c1_1(a562)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a552)
& c2_1(a552)
& c0_1(a552)
& ndr1_0 )
| ~ hskp29 )
& ( ( c2_1(a541)
& c1_1(a541)
& c0_1(a541)
& ndr1_0 )
| ~ hskp28 )
& ( ( ~ c1_1(a615)
& c2_1(a615)
& c0_1(a615)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a604)
& c2_1(a604)
& c1_1(a604)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c1_1(a594)
& ~ c0_1(a594)
& c2_1(a594)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c2_1(a590)
& ~ c0_1(a590)
& c1_1(a590)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a587)
& ~ c2_1(a587)
& ~ c0_1(a587)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c2_1(a584)
& ~ c0_1(a584)
& c3_1(a584)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c1_1(a582)
& c3_1(a582)
& c2_1(a582)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c3_1(a580)
& ~ c0_1(a580)
& c1_1(a580)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c3_1(a576)
& ~ c1_1(a576)
& c0_1(a576)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c3_1(a573)
& ~ c1_1(a573)
& ~ c0_1(a573)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c2_1(a571)
& ~ c1_1(a571)
& c0_1(a571)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a570)
& ~ c2_1(a570)
& c1_1(a570)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c2_1(a567)
& c1_1(a567)
& c0_1(a567)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c0_1(a566)
& c3_1(a566)
& c2_1(a566)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c2_1(a565)
& c3_1(a565)
& c0_1(a565)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c1_1(a564)
& c3_1(a564)
& c0_1(a564)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c2_1(a553)
& c3_1(a553)
& c1_1(a553)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c0_1(a551)
& c3_1(a551)
& c1_1(a551)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c2_1(a549)
& ~ c1_1(a549)
& ~ c0_1(a549)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c0_1(a548)
& c2_1(a548)
& c1_1(a548)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a547)
& ~ c0_1(a547)
& c2_1(a547)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a546)
& ~ c0_1(a546)
& c3_1(a546)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a544)
& c1_1(a544)
& c0_1(a544)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c2_1(a540)
& ~ c1_1(a540)
& c3_1(a540)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c3_1(a539)
& ~ c2_1(a539)
& c0_1(a539)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c3_1(a538)
& ~ c2_1(a538)
& ~ c1_1(a538)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c3_1(a537)
& ~ c1_1(a537)
& c2_1(a537)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c3_1(a536)
& c2_1(a536)
& c0_1(a536)
& ndr1_0 )
| ~ hskp0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ( ( hskp23
| hskp22
| hskp21 )
& ( hskp2
| hskp9
| hskp24 )
& ( hskp2
| hskp6
| hskp26 )
& ( hskp22
| hskp7
| hskp26 )
& ( hskp18
| hskp24
| hskp3 )
& ( hskp22
| hskp25
| hskp13 )
& ( hskp6
| hskp14
| hskp13 )
& ( hskp6
| hskp24
| hskp13 )
& ( hskp4
| hskp7
| hskp12 )
& ( hskp14
| hskp10
| hskp5 )
& ( hskp25
| hskp27
| hskp5 )
& ( hskp22
| hskp20
| hskp31 )
& ( hskp16
| hskp10
| hskp31 )
& ( hskp14
| hskp12
| hskp31 )
& ( hskp23
| hskp15
| hskp28 )
& ( hskp14
| hskp20
| ! [X101] :
( ndr1_0
=> ( ~ c3_1(X101)
| ~ c2_1(X101)
| ~ c1_1(X101) ) ) )
& ( hskp14
| hskp10
| ! [X100] :
( ndr1_0
=> ( ~ c3_1(X100)
| ~ c2_1(X100)
| ~ c0_1(X100) ) ) )
& ( hskp4
| hskp26
| ! [X99] :
( ndr1_0
=> ( ~ c3_1(X99)
| ~ c2_1(X99)
| ~ c0_1(X99) ) ) )
& ( hskp26
| hskp27
| ! [X98] :
( ndr1_0
=> ( ~ c3_1(X98)
| ~ c1_1(X98)
| ~ c0_1(X98) ) ) )
& ( hskp14
| ! [X97] :
( ndr1_0
=> ( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c0_1(X97) ) )
| ! [X96] :
( ndr1_0
=> ( ~ c3_1(X96)
| ~ c1_1(X96)
| ~ c0_1(X96) ) ) )
& ( hskp14
| hskp26
| ! [X95] :
( ndr1_0
=> ( ~ c2_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95) ) ) )
& ( hskp4
| hskp5
| ! [X94] :
( ndr1_0
=> ( ~ c2_1(X94)
| ~ c1_1(X94)
| c3_1(X94) ) ) )
& ( hskp9
| hskp25
| ! [X93] :
( ndr1_0
=> ( ~ c2_1(X93)
| ~ c0_1(X93)
| c3_1(X93) ) ) )
& ( hskp21
| hskp14
| ! [X92] :
( ndr1_0
=> ( ~ c2_1(X92)
| ~ c0_1(X92)
| c3_1(X92) ) ) )
& ( hskp24
| hskp26
| ! [X91] :
( ndr1_0
=> ( ~ c2_1(X91)
| ~ c0_1(X91)
| c3_1(X91) ) ) )
& ( hskp7
| hskp30
| ! [X90] :
( ndr1_0
=> ( ~ c2_1(X90)
| ~ c0_1(X90)
| c3_1(X90) ) ) )
& ( hskp21
| hskp12
| ! [X89] :
( ndr1_0
=> ( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89) ) ) )
& ( hskp6
| hskp3
| ! [X88] :
( ndr1_0
=> ( ~ c3_1(X88)
| ~ c1_1(X88)
| c2_1(X88) ) ) )
& ( hskp0
| hskp15
| ! [X87] :
( ndr1_0
=> ( ~ c3_1(X87)
| ~ c0_1(X87)
| c2_1(X87) ) ) )
& ( hskp4
| hskp25
| ! [X86] :
( ndr1_0
=> ( ~ c1_1(X86)
| c3_1(X86)
| c2_1(X86) ) ) )
& ( hskp6
| hskp3
| ! [X85] :
( ndr1_0
=> ( ~ c1_1(X85)
| c3_1(X85)
| c2_1(X85) ) ) )
& ( hskp14
| ! [X84] :
( ndr1_0
=> ( ~ c3_1(X84)
| ~ c2_1(X84)
| ~ c0_1(X84) ) )
| ! [X83] :
( ndr1_0
=> ( ~ c1_1(X83)
| c3_1(X83)
| c2_1(X83) ) ) )
& ( hskp24
| ! [X82] :
( ndr1_0
=> ( ~ c3_1(X82)
| ~ c1_1(X82)
| ~ c0_1(X82) ) )
| ! [X81] :
( ndr1_0
=> ( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81) ) ) )
& ( hskp22
| hskp21
| ! [X80] :
( ndr1_0
=> ( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80) ) ) )
& ( ! [X79] :
( ndr1_0
=> ( ~ c3_1(X79)
| ~ c2_1(X79)
| ~ c0_1(X79) ) )
| ! [X78] :
( ndr1_0
=> ( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( ~ c2_1(X77)
| ~ c0_1(X77)
| c3_1(X77) ) )
| ! [X76] :
( ndr1_0
=> ( ~ c3_1(X76)
| ~ c0_1(X76)
| c2_1(X76) ) )
| ! [X75] :
( ndr1_0
=> ( ~ c3_1(X75)
| ~ c0_1(X75)
| c1_1(X75) ) ) )
& ( hskp23
| ! [X74] :
( ndr1_0
=> ( ~ c2_1(X74)
| ~ c1_1(X74)
| ~ c0_1(X74) ) )
| ! [X73] :
( ndr1_0
=> ( ~ c2_1(X73)
| ~ c0_1(X73)
| c1_1(X73) ) ) )
& ( hskp3
| ! [X72] :
( ndr1_0
=> ( ~ c3_1(X72)
| ~ c1_1(X72)
| c2_1(X72) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71) ) ) )
& ( hskp7
| ! [X70] :
( ndr1_0
=> ( ~ c1_1(X70)
| ~ c0_1(X70)
| c2_1(X70) ) )
| ! [X69] :
( ndr1_0
=> ( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69) ) ) )
& ( hskp22
| ! [X68] :
( ndr1_0
=> ( ~ c1_1(X68)
| c3_1(X68)
| c2_1(X68) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c2_1(X67)
| ~ c0_1(X67)
| c1_1(X67) ) ) )
& ( hskp19
| ! [X66] :
( ndr1_0
=> ( ~ c3_1(X66)
| ~ c2_1(X66)
| c1_1(X66) ) )
| ! [X65] :
( ndr1_0
=> ( ~ c2_1(X65)
| ~ c0_1(X65)
| c1_1(X65) ) ) )
& ( hskp21
| hskp29
| ! [X64] :
( ndr1_0
=> ( ~ c2_1(X64)
| c3_1(X64)
| c1_1(X64) ) ) )
& ( hskp20
| hskp13
| ! [X63] :
( ndr1_0
=> ( ~ c0_1(X63)
| c3_1(X63)
| c1_1(X63) ) ) )
& ( hskp13
| ! [X62] :
( ndr1_0
=> ( ~ c2_1(X62)
| ~ c1_1(X62)
| ~ c0_1(X62) ) )
| ! [X61] :
( ndr1_0
=> ( ~ c0_1(X61)
| c3_1(X61)
| c1_1(X61) ) ) )
& ( hskp9
| hskp19
| ! [X60] :
( ndr1_0
=> ( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60) ) ) )
& ( hskp11
| hskp12
| ! [X59] :
( ndr1_0
=> ( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59) ) ) )
& ( hskp18
| ! [X58] :
( ndr1_0
=> ( ~ c2_1(X58)
| ~ c1_1(X58)
| c3_1(X58) ) )
| ! [X57] :
( ndr1_0
=> ( ~ c0_1(X57)
| c2_1(X57)
| c1_1(X57) ) ) )
& ( hskp12
| ! [X56] :
( ndr1_0
=> ( ~ c1_1(X56)
| ~ c0_1(X56)
| c3_1(X56) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c0_1(X55)
| c2_1(X55)
| c1_1(X55) ) ) )
& ( hskp17
| ! [X54] :
( ndr1_0
=> ( ~ c1_1(X54)
| ~ c0_1(X54)
| c2_1(X54) ) )
| ! [X53] :
( ndr1_0
=> ( ~ c0_1(X53)
| c2_1(X53)
| c1_1(X53) ) ) )
& ( hskp16
| hskp3
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| c2_1(X52)
| c1_1(X52) ) ) )
& ( hskp2
| hskp15
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| c2_1(X51)
| c1_1(X51) ) ) )
& ( hskp14
| hskp13
| ! [X50] :
( ndr1_0
=> ( ~ c3_1(X50)
| ~ c2_1(X50)
| c0_1(X50) ) ) )
& ( hskp12
| ! [X49] :
( ndr1_0
=> ( ~ c2_1(X49)
| ~ c1_1(X49)
| ~ c0_1(X49) ) )
| ! [X48] :
( ndr1_0
=> ( ~ c3_1(X48)
| ~ c2_1(X48)
| c0_1(X48) ) ) )
& ( hskp31
| ! [X47] :
( ndr1_0
=> ( ~ c2_1(X47)
| ~ c0_1(X47)
| c1_1(X47) ) )
| ! [X46] :
( ndr1_0
=> ( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( ~ c3_1(X45)
| ~ c0_1(X45)
| c2_1(X45) ) )
| ! [X44] :
( ndr1_0
=> ( ~ c2_1(X44)
| c3_1(X44)
| c1_1(X44) ) )
| ! [X43] :
( ndr1_0
=> ( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43) ) ) )
& ( hskp30
| hskp0
| ! [X42] :
( ndr1_0
=> ( ~ c3_1(X42)
| ~ c1_1(X42)
| c0_1(X42) ) ) )
& ( hskp6
| ! [X41] :
( ndr1_0
=> ( ~ c1_1(X41)
| ~ c0_1(X41)
| c2_1(X41) ) )
| ! [X40] :
( ndr1_0
=> ( ~ c3_1(X40)
| ~ c1_1(X40)
| c0_1(X40) ) ) )
& ( hskp9
| hskp10
| ! [X39] :
( ndr1_0
=> ( ~ c2_1(X39)
| ~ c1_1(X39)
| c0_1(X39) ) ) )
& ( hskp0
| ! [X38] :
( ndr1_0
=> ( ~ c3_1(X38)
| ~ c2_1(X38)
| ~ c0_1(X38) ) )
| ! [X37] :
( ndr1_0
=> ( ~ c2_1(X37)
| c3_1(X37)
| c0_1(X37) ) ) )
& ( hskp9
| hskp11
| ! [X36] :
( ndr1_0
=> ( ~ c1_1(X36)
| c3_1(X36)
| c0_1(X36) ) ) )
& ( ! [X35] :
( ndr1_0
=> ( ~ c3_1(X35)
| ~ c2_1(X35)
| ~ c0_1(X35) ) )
| ! [X34] :
( ndr1_0
=> ( ~ c3_1(X34)
| ~ c1_1(X34)
| ~ c0_1(X34) ) )
| ! [X33] :
( ndr1_0
=> ( ~ c1_1(X33)
| c3_1(X33)
| c0_1(X33) ) ) )
& ( hskp11
| ! [X32] :
( ndr1_0
=> ( ~ c2_1(X32)
| ~ c1_1(X32)
| ~ c0_1(X32) ) )
| ! [X31] :
( ndr1_0
=> ( ~ c1_1(X31)
| c3_1(X31)
| c0_1(X31) ) ) )
& ( hskp11
| hskp29
| ! [X30] :
( ndr1_0
=> ( ~ c3_1(X30)
| c2_1(X30)
| c0_1(X30) ) ) )
& ( hskp10
| hskp8
| ! [X29] :
( ndr1_0
=> ( ~ c1_1(X29)
| c2_1(X29)
| c0_1(X29) ) ) )
& ( ! [X28] :
( ndr1_0
=> ( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X27] :
( ndr1_0
=> ( ~ c3_1(X27)
| ~ c2_1(X27)
| c0_1(X27) ) )
| ! [X26] :
( ndr1_0
=> ( ~ c1_1(X26)
| c2_1(X26)
| c0_1(X26) ) ) )
& ( ! [X25] :
( ndr1_0
=> ( ~ c0_1(X25)
| c3_1(X25)
| c1_1(X25) ) )
| ! [X24] :
( ndr1_0
=> ( ~ c3_1(X24)
| c2_1(X24)
| c0_1(X24) ) )
| ! [X23] :
( ndr1_0
=> ( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) ) ) )
& ( hskp9
| hskp8
| ! [X22] :
( ndr1_0
=> ( c3_1(X22)
| c2_1(X22)
| c0_1(X22) ) ) )
& ( hskp7
| ! [X21] :
( ndr1_0
=> ( ~ c3_1(X21)
| ~ c0_1(X21)
| c2_1(X21) ) )
| ! [X20] :
( ndr1_0
=> ( c3_1(X20)
| c2_1(X20)
| c0_1(X20) ) ) )
& ( ! [X19] :
( ndr1_0
=> ( ~ c3_1(X19)
| ~ c1_1(X19)
| ~ c0_1(X19) ) )
| ! [X18] :
( ndr1_0
=> ( ~ c1_1(X18)
| ~ c0_1(X18)
| c2_1(X18) ) )
| ! [X17] :
( ndr1_0
=> ( c3_1(X17)
| c2_1(X17)
| c0_1(X17) ) ) )
& ( hskp6
| ! [X16] :
( ndr1_0
=> ( ~ c2_1(X16)
| ~ c0_1(X16)
| c1_1(X16) ) )
| ! [X15] :
( ndr1_0
=> ( c3_1(X15)
| c2_1(X15)
| c0_1(X15) ) ) )
& ( hskp2
| hskp5
| ! [X14] :
( ndr1_0
=> ( ~ c3_1(X14)
| c1_1(X14)
| c0_1(X14) ) ) )
& ( hskp1
| ! [X13] :
( ndr1_0
=> ( ~ c2_1(X13)
| ~ c1_1(X13)
| ~ c0_1(X13) ) )
| ! [X12] :
( ndr1_0
=> ( ~ c3_1(X12)
| c1_1(X12)
| c0_1(X12) ) ) )
& ( ! [X11] :
( ndr1_0
=> ( ~ c3_1(X11)
| ~ c2_1(X11)
| c0_1(X11) ) )
| ! [X10] :
( ndr1_0
=> ( ~ c3_1(X10)
| c1_1(X10)
| c0_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( ~ c2_1(X9)
| c1_1(X9)
| c0_1(X9) ) ) )
& ( hskp2
| hskp28
| ! [X8] :
( ndr1_0
=> ( c3_1(X8)
| c1_1(X8)
| c0_1(X8) ) ) )
& ( hskp4
| ! [X7] :
( ndr1_0
=> ( ~ c3_1(X7)
| ~ c0_1(X7)
| c2_1(X7) ) )
| ! [X6] :
( ndr1_0
=> ( c3_1(X6)
| c1_1(X6)
| c0_1(X6) ) ) )
& ( ! [X5] :
( ndr1_0
=> ( ~ c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) ) )
| ! [X4] :
( ndr1_0
=> ( ~ c0_1(X4)
| c3_1(X4)
| c1_1(X4) ) )
| ! [X3] :
( ndr1_0
=> ( c3_1(X3)
| c1_1(X3)
| c0_1(X3) ) ) )
& ( hskp3
| ! [X2] :
( ndr1_0
=> ( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) )
| ! [X1] :
( ndr1_0
=> ( c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ) )
& ( hskp2
| ! [Z] :
( ndr1_0
=> ( ~ c2_1(Z)
| ~ c1_1(Z)
| ~ c0_1(Z) ) )
| ! [Y] :
( ndr1_0
=> ( c2_1(Y)
| c1_1(Y)
| c0_1(Y) ) ) )
& ( hskp1
| ! [X] :
( ndr1_0
=> ( ~ c3_1(X)
| ~ c0_1(X)
| c1_1(X) ) )
| ! [W] :
( ndr1_0
=> ( c2_1(W)
| c1_1(W)
| c0_1(W) ) ) )
& ( hskp0
| ! [V] :
( ndr1_0
=> ( ~ c3_1(V)
| c1_1(V)
| c0_1(V) ) )
| ! [U] :
( ndr1_0
=> ( c2_1(U)
| c1_1(U)
| c0_1(U) ) ) )
& ( ( c3_1(a563)
& c1_1(a563)
& c0_1(a563)
& ndr1_0 )
| ~ hskp31 )
& ( ( c3_1(a562)
& c2_1(a562)
& c1_1(a562)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a552)
& c2_1(a552)
& c0_1(a552)
& ndr1_0 )
| ~ hskp29 )
& ( ( c2_1(a541)
& c1_1(a541)
& c0_1(a541)
& ndr1_0 )
| ~ hskp28 )
& ( ( ~ c1_1(a615)
& c2_1(a615)
& c0_1(a615)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a604)
& c2_1(a604)
& c1_1(a604)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c1_1(a594)
& ~ c0_1(a594)
& c2_1(a594)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c2_1(a590)
& ~ c0_1(a590)
& c1_1(a590)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a587)
& ~ c2_1(a587)
& ~ c0_1(a587)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c2_1(a584)
& ~ c0_1(a584)
& c3_1(a584)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c1_1(a582)
& c3_1(a582)
& c2_1(a582)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c3_1(a580)
& ~ c0_1(a580)
& c1_1(a580)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c3_1(a576)
& ~ c1_1(a576)
& c0_1(a576)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c3_1(a573)
& ~ c1_1(a573)
& ~ c0_1(a573)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c2_1(a571)
& ~ c1_1(a571)
& c0_1(a571)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a570)
& ~ c2_1(a570)
& c1_1(a570)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c2_1(a567)
& c1_1(a567)
& c0_1(a567)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c0_1(a566)
& c3_1(a566)
& c2_1(a566)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c2_1(a565)
& c3_1(a565)
& c0_1(a565)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c1_1(a564)
& c3_1(a564)
& c0_1(a564)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c2_1(a553)
& c3_1(a553)
& c1_1(a553)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c0_1(a551)
& c3_1(a551)
& c1_1(a551)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c2_1(a549)
& ~ c1_1(a549)
& ~ c0_1(a549)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c0_1(a548)
& c2_1(a548)
& c1_1(a548)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a547)
& ~ c0_1(a547)
& c2_1(a547)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a546)
& ~ c0_1(a546)
& c3_1(a546)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a544)
& c1_1(a544)
& c0_1(a544)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c2_1(a540)
& ~ c1_1(a540)
& c3_1(a540)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c3_1(a539)
& ~ c2_1(a539)
& c0_1(a539)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c3_1(a538)
& ~ c2_1(a538)
& ~ c1_1(a538)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c3_1(a537)
& ~ c1_1(a537)
& c2_1(a537)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c3_1(a536)
& c2_1(a536)
& c0_1(a536)
& ndr1_0 )
| ~ hskp0 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( hskp23
| hskp22
| hskp21 )
& ( hskp2
| hskp9
| hskp24 )
& ( hskp2
| hskp6
| hskp26 )
& ( hskp22
| hskp7
| hskp26 )
& ( hskp18
| hskp24
| hskp3 )
& ( hskp22
| hskp25
| hskp13 )
& ( hskp6
| hskp14
| hskp13 )
& ( hskp6
| hskp24
| hskp13 )
& ( hskp4
| hskp7
| hskp12 )
& ( hskp14
| hskp10
| hskp5 )
& ( hskp25
| hskp27
| hskp5 )
& ( hskp22
| hskp20
| hskp31 )
& ( hskp16
| hskp10
| hskp31 )
& ( hskp14
| hskp12
| hskp31 )
& ( hskp23
| hskp15
| hskp28 )
& ( hskp14
| hskp20
| ! [X101] :
( ~ c3_1(X101)
| ~ c2_1(X101)
| ~ c1_1(X101)
| ~ ndr1_0 ) )
& ( hskp14
| hskp10
| ! [X100] :
( ~ c3_1(X100)
| ~ c2_1(X100)
| ~ c0_1(X100)
| ~ ndr1_0 ) )
& ( hskp4
| hskp26
| ! [X99] :
( ~ c3_1(X99)
| ~ c2_1(X99)
| ~ c0_1(X99)
| ~ ndr1_0 ) )
& ( hskp26
| hskp27
| ! [X98] :
( ~ c3_1(X98)
| ~ c1_1(X98)
| ~ c0_1(X98)
| ~ ndr1_0 ) )
& ( hskp14
| ! [X97] :
( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c0_1(X97)
| ~ ndr1_0 )
| ! [X96] :
( ~ c3_1(X96)
| ~ c1_1(X96)
| ~ c0_1(X96)
| ~ ndr1_0 ) )
& ( hskp14
| hskp26
| ! [X95] :
( ~ c2_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95)
| ~ ndr1_0 ) )
& ( hskp4
| hskp5
| ! [X94] :
( ~ c2_1(X94)
| ~ c1_1(X94)
| c3_1(X94)
| ~ ndr1_0 ) )
& ( hskp9
| hskp25
| ! [X93] :
( ~ c2_1(X93)
| ~ c0_1(X93)
| c3_1(X93)
| ~ ndr1_0 ) )
& ( hskp21
| hskp14
| ! [X92] :
( ~ c2_1(X92)
| ~ c0_1(X92)
| c3_1(X92)
| ~ ndr1_0 ) )
& ( hskp24
| hskp26
| ! [X91] :
( ~ c2_1(X91)
| ~ c0_1(X91)
| c3_1(X91)
| ~ ndr1_0 ) )
& ( hskp7
| hskp30
| ! [X90] :
( ~ c2_1(X90)
| ~ c0_1(X90)
| c3_1(X90)
| ~ ndr1_0 ) )
& ( hskp21
| hskp12
| ! [X89] :
( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89)
| ~ ndr1_0 ) )
& ( hskp6
| hskp3
| ! [X88] :
( ~ c3_1(X88)
| ~ c1_1(X88)
| c2_1(X88)
| ~ ndr1_0 ) )
& ( hskp0
| hskp15
| ! [X87] :
( ~ c3_1(X87)
| ~ c0_1(X87)
| c2_1(X87)
| ~ ndr1_0 ) )
& ( hskp4
| hskp25
| ! [X86] :
( ~ c1_1(X86)
| c3_1(X86)
| c2_1(X86)
| ~ ndr1_0 ) )
& ( hskp6
| hskp3
| ! [X85] :
( ~ c1_1(X85)
| c3_1(X85)
| c2_1(X85)
| ~ ndr1_0 ) )
& ( hskp14
| ! [X84] :
( ~ c3_1(X84)
| ~ c2_1(X84)
| ~ c0_1(X84)
| ~ ndr1_0 )
| ! [X83] :
( ~ c1_1(X83)
| c3_1(X83)
| c2_1(X83)
| ~ ndr1_0 ) )
& ( hskp24
| ! [X82] :
( ~ c3_1(X82)
| ~ c1_1(X82)
| ~ c0_1(X82)
| ~ ndr1_0 )
| ! [X81] :
( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81)
| ~ ndr1_0 ) )
& ( hskp22
| hskp21
| ! [X80] :
( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80)
| ~ ndr1_0 ) )
& ( ! [X79] :
( ~ c3_1(X79)
| ~ c2_1(X79)
| ~ c0_1(X79)
| ~ ndr1_0 )
| ! [X78] :
( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78)
| ~ ndr1_0 ) )
& ( ! [X77] :
( ~ c2_1(X77)
| ~ c0_1(X77)
| c3_1(X77)
| ~ ndr1_0 )
| ! [X76] :
( ~ c3_1(X76)
| ~ c0_1(X76)
| c2_1(X76)
| ~ ndr1_0 )
| ! [X75] :
( ~ c3_1(X75)
| ~ c0_1(X75)
| c1_1(X75)
| ~ ndr1_0 ) )
& ( hskp23
| ! [X74] :
( ~ c2_1(X74)
| ~ c1_1(X74)
| ~ c0_1(X74)
| ~ ndr1_0 )
| ! [X73] :
( ~ c2_1(X73)
| ~ c0_1(X73)
| c1_1(X73)
| ~ ndr1_0 ) )
& ( hskp3
| ! [X72] :
( ~ c3_1(X72)
| ~ c1_1(X72)
| c2_1(X72)
| ~ ndr1_0 )
| ! [X71] :
( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71)
| ~ ndr1_0 ) )
& ( hskp7
| ! [X70] :
( ~ c1_1(X70)
| ~ c0_1(X70)
| c2_1(X70)
| ~ ndr1_0 )
| ! [X69] :
( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69)
| ~ ndr1_0 ) )
& ( hskp22
| ! [X68] :
( ~ c1_1(X68)
| c3_1(X68)
| c2_1(X68)
| ~ ndr1_0 )
| ! [X67] :
( ~ c2_1(X67)
| ~ c0_1(X67)
| c1_1(X67)
| ~ ndr1_0 ) )
& ( hskp19
| ! [X66] :
( ~ c3_1(X66)
| ~ c2_1(X66)
| c1_1(X66)
| ~ ndr1_0 )
| ! [X65] :
( ~ c2_1(X65)
| ~ c0_1(X65)
| c1_1(X65)
| ~ ndr1_0 ) )
& ( hskp21
| hskp29
| ! [X64] :
( ~ c2_1(X64)
| c3_1(X64)
| c1_1(X64)
| ~ ndr1_0 ) )
& ( hskp20
| hskp13
| ! [X63] :
( ~ c0_1(X63)
| c3_1(X63)
| c1_1(X63)
| ~ ndr1_0 ) )
& ( hskp13
| ! [X62] :
( ~ c2_1(X62)
| ~ c1_1(X62)
| ~ c0_1(X62)
| ~ ndr1_0 )
| ! [X61] :
( ~ c0_1(X61)
| c3_1(X61)
| c1_1(X61)
| ~ ndr1_0 ) )
& ( hskp9
| hskp19
| ! [X60] :
( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60)
| ~ ndr1_0 ) )
& ( hskp11
| hskp12
| ! [X59] :
( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59)
| ~ ndr1_0 ) )
& ( hskp18
| ! [X58] :
( ~ c2_1(X58)
| ~ c1_1(X58)
| c3_1(X58)
| ~ ndr1_0 )
| ! [X57] :
( ~ c0_1(X57)
| c2_1(X57)
| c1_1(X57)
| ~ ndr1_0 ) )
& ( hskp12
| ! [X56] :
( ~ c1_1(X56)
| ~ c0_1(X56)
| c3_1(X56)
| ~ ndr1_0 )
| ! [X55] :
( ~ c0_1(X55)
| c2_1(X55)
| c1_1(X55)
| ~ ndr1_0 ) )
& ( hskp17
| ! [X54] :
( ~ c1_1(X54)
| ~ c0_1(X54)
| c2_1(X54)
| ~ ndr1_0 )
| ! [X53] :
( ~ c0_1(X53)
| c2_1(X53)
| c1_1(X53)
| ~ ndr1_0 ) )
& ( hskp16
| hskp3
| ! [X52] :
( c3_1(X52)
| c2_1(X52)
| c1_1(X52)
| ~ ndr1_0 ) )
& ( hskp2
| hskp15
| ! [X51] :
( c3_1(X51)
| c2_1(X51)
| c1_1(X51)
| ~ ndr1_0 ) )
& ( hskp14
| hskp13
| ! [X50] :
( ~ c3_1(X50)
| ~ c2_1(X50)
| c0_1(X50)
| ~ ndr1_0 ) )
& ( hskp12
| ! [X49] :
( ~ c2_1(X49)
| ~ c1_1(X49)
| ~ c0_1(X49)
| ~ ndr1_0 )
| ! [X48] :
( ~ c3_1(X48)
| ~ c2_1(X48)
| c0_1(X48)
| ~ ndr1_0 ) )
& ( hskp31
| ! [X47] :
( ~ c2_1(X47)
| ~ c0_1(X47)
| c1_1(X47)
| ~ ndr1_0 )
| ! [X46] :
( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46)
| ~ ndr1_0 ) )
& ( ! [X45] :
( ~ c3_1(X45)
| ~ c0_1(X45)
| c2_1(X45)
| ~ ndr1_0 )
| ! [X44] :
( ~ c2_1(X44)
| c3_1(X44)
| c1_1(X44)
| ~ ndr1_0 )
| ! [X43] :
( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43)
| ~ ndr1_0 ) )
& ( hskp30
| hskp0
| ! [X42] :
( ~ c3_1(X42)
| ~ c1_1(X42)
| c0_1(X42)
| ~ ndr1_0 ) )
& ( hskp6
| ! [X41] :
( ~ c1_1(X41)
| ~ c0_1(X41)
| c2_1(X41)
| ~ ndr1_0 )
| ! [X40] :
( ~ c3_1(X40)
| ~ c1_1(X40)
| c0_1(X40)
| ~ ndr1_0 ) )
& ( hskp9
| hskp10
| ! [X39] :
( ~ c2_1(X39)
| ~ c1_1(X39)
| c0_1(X39)
| ~ ndr1_0 ) )
& ( hskp0
| ! [X38] :
( ~ c3_1(X38)
| ~ c2_1(X38)
| ~ c0_1(X38)
| ~ ndr1_0 )
| ! [X37] :
( ~ c2_1(X37)
| c3_1(X37)
| c0_1(X37)
| ~ ndr1_0 ) )
& ( hskp9
| hskp11
| ! [X36] :
( ~ c1_1(X36)
| c3_1(X36)
| c0_1(X36)
| ~ ndr1_0 ) )
& ( ! [X35] :
( ~ c3_1(X35)
| ~ c2_1(X35)
| ~ c0_1(X35)
| ~ ndr1_0 )
| ! [X34] :
( ~ c3_1(X34)
| ~ c1_1(X34)
| ~ c0_1(X34)
| ~ ndr1_0 )
| ! [X33] :
( ~ c1_1(X33)
| c3_1(X33)
| c0_1(X33)
| ~ ndr1_0 ) )
& ( hskp11
| ! [X32] :
( ~ c2_1(X32)
| ~ c1_1(X32)
| ~ c0_1(X32)
| ~ ndr1_0 )
| ! [X31] :
( ~ c1_1(X31)
| c3_1(X31)
| c0_1(X31)
| ~ ndr1_0 ) )
& ( hskp11
| hskp29
| ! [X30] :
( ~ c3_1(X30)
| c2_1(X30)
| c0_1(X30)
| ~ ndr1_0 ) )
& ( hskp10
| hskp8
| ! [X29] :
( ~ c1_1(X29)
| c2_1(X29)
| c0_1(X29)
| ~ ndr1_0 ) )
& ( ! [X28] :
( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X27] :
( ~ c3_1(X27)
| ~ c2_1(X27)
| c0_1(X27)
| ~ ndr1_0 )
| ! [X26] :
( ~ c1_1(X26)
| c2_1(X26)
| c0_1(X26)
| ~ ndr1_0 ) )
& ( ! [X25] :
( ~ c0_1(X25)
| c3_1(X25)
| c1_1(X25)
| ~ ndr1_0 )
| ! [X24] :
( ~ c3_1(X24)
| c2_1(X24)
| c0_1(X24)
| ~ ndr1_0 )
| ! [X23] :
( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23)
| ~ ndr1_0 ) )
& ( hskp9
| hskp8
| ! [X22] :
( c3_1(X22)
| c2_1(X22)
| c0_1(X22)
| ~ ndr1_0 ) )
& ( hskp7
| ! [X21] :
( ~ c3_1(X21)
| ~ c0_1(X21)
| c2_1(X21)
| ~ ndr1_0 )
| ! [X20] :
( c3_1(X20)
| c2_1(X20)
| c0_1(X20)
| ~ ndr1_0 ) )
& ( ! [X19] :
( ~ c3_1(X19)
| ~ c1_1(X19)
| ~ c0_1(X19)
| ~ ndr1_0 )
| ! [X18] :
( ~ c1_1(X18)
| ~ c0_1(X18)
| c2_1(X18)
| ~ ndr1_0 )
| ! [X17] :
( c3_1(X17)
| c2_1(X17)
| c0_1(X17)
| ~ ndr1_0 ) )
& ( hskp6
| ! [X16] :
( ~ c2_1(X16)
| ~ c0_1(X16)
| c1_1(X16)
| ~ ndr1_0 )
| ! [X15] :
( c3_1(X15)
| c2_1(X15)
| c0_1(X15)
| ~ ndr1_0 ) )
& ( hskp2
| hskp5
| ! [X14] :
( ~ c3_1(X14)
| c1_1(X14)
| c0_1(X14)
| ~ ndr1_0 ) )
& ( hskp1
| ! [X13] :
( ~ c2_1(X13)
| ~ c1_1(X13)
| ~ c0_1(X13)
| ~ ndr1_0 )
| ! [X12] :
( ~ c3_1(X12)
| c1_1(X12)
| c0_1(X12)
| ~ ndr1_0 ) )
& ( ! [X11] :
( ~ c3_1(X11)
| ~ c2_1(X11)
| c0_1(X11)
| ~ ndr1_0 )
| ! [X10] :
( ~ c3_1(X10)
| c1_1(X10)
| c0_1(X10)
| ~ ndr1_0 )
| ! [X9] :
( ~ c2_1(X9)
| c1_1(X9)
| c0_1(X9)
| ~ ndr1_0 ) )
& ( hskp2
| hskp28
| ! [X8] :
( c3_1(X8)
| c1_1(X8)
| c0_1(X8)
| ~ ndr1_0 ) )
& ( hskp4
| ! [X7] :
( ~ c3_1(X7)
| ~ c0_1(X7)
| c2_1(X7)
| ~ ndr1_0 )
| ! [X6] :
( c3_1(X6)
| c1_1(X6)
| c0_1(X6)
| ~ ndr1_0 ) )
& ( ! [X5] :
( ~ c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| ! [X4] :
( ~ c0_1(X4)
| c3_1(X4)
| c1_1(X4)
| ~ ndr1_0 )
| ! [X3] :
( c3_1(X3)
| c1_1(X3)
| c0_1(X3)
| ~ ndr1_0 ) )
& ( hskp3
| ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2)
| ~ ndr1_0 )
| ! [X1] :
( c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0 ) )
& ( hskp2
| ! [Z] :
( ~ c2_1(Z)
| ~ c1_1(Z)
| ~ c0_1(Z)
| ~ ndr1_0 )
| ! [Y] :
( c2_1(Y)
| c1_1(Y)
| c0_1(Y)
| ~ ndr1_0 ) )
& ( hskp1
| ! [X] :
( ~ c3_1(X)
| ~ c0_1(X)
| c1_1(X)
| ~ ndr1_0 )
| ! [W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| ~ ndr1_0 ) )
& ( hskp0
| ! [V] :
( ~ c3_1(V)
| c1_1(V)
| c0_1(V)
| ~ ndr1_0 )
| ! [U] :
( c2_1(U)
| c1_1(U)
| c0_1(U)
| ~ ndr1_0 ) )
& ( ( c3_1(a563)
& c1_1(a563)
& c0_1(a563)
& ndr1_0 )
| ~ hskp31 )
& ( ( c3_1(a562)
& c2_1(a562)
& c1_1(a562)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a552)
& c2_1(a552)
& c0_1(a552)
& ndr1_0 )
| ~ hskp29 )
& ( ( c2_1(a541)
& c1_1(a541)
& c0_1(a541)
& ndr1_0 )
| ~ hskp28 )
& ( ( ~ c1_1(a615)
& c2_1(a615)
& c0_1(a615)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a604)
& c2_1(a604)
& c1_1(a604)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c1_1(a594)
& ~ c0_1(a594)
& c2_1(a594)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c2_1(a590)
& ~ c0_1(a590)
& c1_1(a590)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a587)
& ~ c2_1(a587)
& ~ c0_1(a587)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c2_1(a584)
& ~ c0_1(a584)
& c3_1(a584)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c1_1(a582)
& c3_1(a582)
& c2_1(a582)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c3_1(a580)
& ~ c0_1(a580)
& c1_1(a580)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c3_1(a576)
& ~ c1_1(a576)
& c0_1(a576)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c3_1(a573)
& ~ c1_1(a573)
& ~ c0_1(a573)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c2_1(a571)
& ~ c1_1(a571)
& c0_1(a571)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a570)
& ~ c2_1(a570)
& c1_1(a570)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c2_1(a567)
& c1_1(a567)
& c0_1(a567)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c0_1(a566)
& c3_1(a566)
& c2_1(a566)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c2_1(a565)
& c3_1(a565)
& c0_1(a565)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c1_1(a564)
& c3_1(a564)
& c0_1(a564)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c2_1(a553)
& c3_1(a553)
& c1_1(a553)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c0_1(a551)
& c3_1(a551)
& c1_1(a551)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c2_1(a549)
& ~ c1_1(a549)
& ~ c0_1(a549)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c0_1(a548)
& c2_1(a548)
& c1_1(a548)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a547)
& ~ c0_1(a547)
& c2_1(a547)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a546)
& ~ c0_1(a546)
& c3_1(a546)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a544)
& c1_1(a544)
& c0_1(a544)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c2_1(a540)
& ~ c1_1(a540)
& c3_1(a540)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c3_1(a539)
& ~ c2_1(a539)
& c0_1(a539)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c3_1(a538)
& ~ c2_1(a538)
& ~ c1_1(a538)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c3_1(a537)
& ~ c1_1(a537)
& c2_1(a537)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c3_1(a536)
& c2_1(a536)
& c0_1(a536)
& ndr1_0 )
| ~ hskp0 ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,plain,
( ( hskp23
| hskp22
| hskp21 )
& ( hskp2
| hskp9
| hskp24 )
& ( hskp2
| hskp6
| hskp26 )
& ( hskp22
| hskp7
| hskp26 )
& ( hskp18
| hskp24
| hskp3 )
& ( hskp22
| hskp25
| hskp13 )
& ( hskp6
| hskp14
| hskp13 )
& ( hskp6
| hskp24
| hskp13 )
& ( hskp4
| hskp7
| hskp12 )
& ( hskp14
| hskp10
| hskp5 )
& ( hskp25
| hskp27
| hskp5 )
& ( hskp22
| hskp20
| hskp31 )
& ( hskp16
| hskp10
| hskp31 )
& ( hskp14
| hskp12
| hskp31 )
& ( hskp23
| hskp15
| hskp28 )
& ( hskp14
| hskp20
| ! [X101] :
( ~ c3_1(X101)
| ~ c2_1(X101)
| ~ c1_1(X101) )
| ~ ndr1_0 )
& ( hskp14
| hskp10
| ! [X100] :
( ~ c3_1(X100)
| ~ c2_1(X100)
| ~ c0_1(X100) )
| ~ ndr1_0 )
& ( hskp4
| hskp26
| ! [X99] :
( ~ c3_1(X99)
| ~ c2_1(X99)
| ~ c0_1(X99) )
| ~ ndr1_0 )
& ( hskp26
| hskp27
| ! [X98] :
( ~ c3_1(X98)
| ~ c1_1(X98)
| ~ c0_1(X98) )
| ~ ndr1_0 )
& ( hskp14
| ! [X97] :
( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c0_1(X97) )
| ~ ndr1_0
| ! [X96] :
( ~ c3_1(X96)
| ~ c1_1(X96)
| ~ c0_1(X96) )
| ~ ndr1_0 )
& ( hskp14
| hskp26
| ! [X95] :
( ~ c2_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95) )
| ~ ndr1_0 )
& ( hskp4
| hskp5
| ! [X94] :
( ~ c2_1(X94)
| ~ c1_1(X94)
| c3_1(X94) )
| ~ ndr1_0 )
& ( hskp9
| hskp25
| ! [X93] :
( ~ c2_1(X93)
| ~ c0_1(X93)
| c3_1(X93) )
| ~ ndr1_0 )
& ( hskp21
| hskp14
| ! [X92] :
( ~ c2_1(X92)
| ~ c0_1(X92)
| c3_1(X92) )
| ~ ndr1_0 )
& ( hskp24
| hskp26
| ! [X91] :
( ~ c2_1(X91)
| ~ c0_1(X91)
| c3_1(X91) )
| ~ ndr1_0 )
& ( hskp7
| hskp30
| ! [X90] :
( ~ c2_1(X90)
| ~ c0_1(X90)
| c3_1(X90) )
| ~ ndr1_0 )
& ( hskp21
| hskp12
| ! [X89] :
( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89) )
| ~ ndr1_0 )
& ( hskp6
| hskp3
| ! [X88] :
( ~ c3_1(X88)
| ~ c1_1(X88)
| c2_1(X88) )
| ~ ndr1_0 )
& ( hskp0
| hskp15
| ! [X87] :
( ~ c3_1(X87)
| ~ c0_1(X87)
| c2_1(X87) )
| ~ ndr1_0 )
& ( hskp4
| hskp25
| ! [X86] :
( ~ c1_1(X86)
| c3_1(X86)
| c2_1(X86) )
| ~ ndr1_0 )
& ( hskp6
| hskp3
| ! [X85] :
( ~ c1_1(X85)
| c3_1(X85)
| c2_1(X85) )
| ~ ndr1_0 )
& ( hskp14
| ! [X84] :
( ~ c3_1(X84)
| ~ c2_1(X84)
| ~ c0_1(X84) )
| ~ ndr1_0
| ! [X83] :
( ~ c1_1(X83)
| c3_1(X83)
| c2_1(X83) )
| ~ ndr1_0 )
& ( hskp24
| ! [X82] :
( ~ c3_1(X82)
| ~ c1_1(X82)
| ~ c0_1(X82) )
| ~ ndr1_0
| ! [X81] :
( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81) )
| ~ ndr1_0 )
& ( hskp22
| hskp21
| ! [X80] :
( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80) )
| ~ ndr1_0 )
& ( ! [X79] :
( ~ c3_1(X79)
| ~ c2_1(X79)
| ~ c0_1(X79) )
| ~ ndr1_0
| ! [X78] :
( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78) )
| ~ ndr1_0 )
& ( ! [X77] :
( ~ c2_1(X77)
| ~ c0_1(X77)
| c3_1(X77) )
| ~ ndr1_0
| ! [X76] :
( ~ c3_1(X76)
| ~ c0_1(X76)
| c2_1(X76) )
| ~ ndr1_0
| ! [X75] :
( ~ c3_1(X75)
| ~ c0_1(X75)
| c1_1(X75) )
| ~ ndr1_0 )
& ( hskp23
| ! [X74] :
( ~ c2_1(X74)
| ~ c1_1(X74)
| ~ c0_1(X74) )
| ~ ndr1_0
| ! [X73] :
( ~ c2_1(X73)
| ~ c0_1(X73)
| c1_1(X73) )
| ~ ndr1_0 )
& ( hskp3
| ! [X72] :
( ~ c3_1(X72)
| ~ c1_1(X72)
| c2_1(X72) )
| ~ ndr1_0
| ! [X71] :
( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71) )
| ~ ndr1_0 )
& ( hskp7
| ! [X70] :
( ~ c1_1(X70)
| ~ c0_1(X70)
| c2_1(X70) )
| ~ ndr1_0
| ! [X69] :
( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69) )
| ~ ndr1_0 )
& ( hskp22
| ! [X68] :
( ~ c1_1(X68)
| c3_1(X68)
| c2_1(X68) )
| ~ ndr1_0
| ! [X67] :
( ~ c2_1(X67)
| ~ c0_1(X67)
| c1_1(X67) )
| ~ ndr1_0 )
& ( hskp19
| ! [X66] :
( ~ c3_1(X66)
| ~ c2_1(X66)
| c1_1(X66) )
| ~ ndr1_0
| ! [X65] :
( ~ c2_1(X65)
| ~ c0_1(X65)
| c1_1(X65) )
| ~ ndr1_0 )
& ( hskp21
| hskp29
| ! [X64] :
( ~ c2_1(X64)
| c3_1(X64)
| c1_1(X64) )
| ~ ndr1_0 )
& ( hskp20
| hskp13
| ! [X63] :
( ~ c0_1(X63)
| c3_1(X63)
| c1_1(X63) )
| ~ ndr1_0 )
& ( hskp13
| ! [X62] :
( ~ c2_1(X62)
| ~ c1_1(X62)
| ~ c0_1(X62) )
| ~ ndr1_0
| ! [X61] :
( ~ c0_1(X61)
| c3_1(X61)
| c1_1(X61) )
| ~ ndr1_0 )
& ( hskp9
| hskp19
| ! [X60] :
( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60) )
| ~ ndr1_0 )
& ( hskp11
| hskp12
| ! [X59] :
( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59) )
| ~ ndr1_0 )
& ( hskp18
| ! [X58] :
( ~ c2_1(X58)
| ~ c1_1(X58)
| c3_1(X58) )
| ~ ndr1_0
| ! [X57] :
( ~ c0_1(X57)
| c2_1(X57)
| c1_1(X57) )
| ~ ndr1_0 )
& ( hskp12
| ! [X56] :
( ~ c1_1(X56)
| ~ c0_1(X56)
| c3_1(X56) )
| ~ ndr1_0
| ! [X55] :
( ~ c0_1(X55)
| c2_1(X55)
| c1_1(X55) )
| ~ ndr1_0 )
& ( hskp17
| ! [X54] :
( ~ c1_1(X54)
| ~ c0_1(X54)
| c2_1(X54) )
| ~ ndr1_0
| ! [X53] :
( ~ c0_1(X53)
| c2_1(X53)
| c1_1(X53) )
| ~ ndr1_0 )
& ( hskp16
| hskp3
| ! [X52] :
( c3_1(X52)
| c2_1(X52)
| c1_1(X52) )
| ~ ndr1_0 )
& ( hskp2
| hskp15
| ! [X51] :
( c3_1(X51)
| c2_1(X51)
| c1_1(X51) )
| ~ ndr1_0 )
& ( hskp14
| hskp13
| ! [X50] :
( ~ c3_1(X50)
| ~ c2_1(X50)
| c0_1(X50) )
| ~ ndr1_0 )
& ( hskp12
| ! [X49] :
( ~ c2_1(X49)
| ~ c1_1(X49)
| ~ c0_1(X49) )
| ~ ndr1_0
| ! [X48] :
( ~ c3_1(X48)
| ~ c2_1(X48)
| c0_1(X48) )
| ~ ndr1_0 )
& ( hskp31
| ! [X47] :
( ~ c2_1(X47)
| ~ c0_1(X47)
| c1_1(X47) )
| ~ ndr1_0
| ! [X46] :
( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46) )
| ~ ndr1_0 )
& ( ! [X45] :
( ~ c3_1(X45)
| ~ c0_1(X45)
| c2_1(X45) )
| ~ ndr1_0
| ! [X44] :
( ~ c2_1(X44)
| c3_1(X44)
| c1_1(X44) )
| ~ ndr1_0
| ! [X43] :
( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43) )
| ~ ndr1_0 )
& ( hskp30
| hskp0
| ! [X42] :
( ~ c3_1(X42)
| ~ c1_1(X42)
| c0_1(X42) )
| ~ ndr1_0 )
& ( hskp6
| ! [X41] :
( ~ c1_1(X41)
| ~ c0_1(X41)
| c2_1(X41) )
| ~ ndr1_0
| ! [X40] :
( ~ c3_1(X40)
| ~ c1_1(X40)
| c0_1(X40) )
| ~ ndr1_0 )
& ( hskp9
| hskp10
| ! [X39] :
( ~ c2_1(X39)
| ~ c1_1(X39)
| c0_1(X39) )
| ~ ndr1_0 )
& ( hskp0
| ! [X38] :
( ~ c3_1(X38)
| ~ c2_1(X38)
| ~ c0_1(X38) )
| ~ ndr1_0
| ! [X37] :
( ~ c2_1(X37)
| c3_1(X37)
| c0_1(X37) )
| ~ ndr1_0 )
& ( hskp9
| hskp11
| ! [X36] :
( ~ c1_1(X36)
| c3_1(X36)
| c0_1(X36) )
| ~ ndr1_0 )
& ( ! [X35] :
( ~ c3_1(X35)
| ~ c2_1(X35)
| ~ c0_1(X35) )
| ~ ndr1_0
| ! [X34] :
( ~ c3_1(X34)
| ~ c1_1(X34)
| ~ c0_1(X34) )
| ~ ndr1_0
| ! [X33] :
( ~ c1_1(X33)
| c3_1(X33)
| c0_1(X33) )
| ~ ndr1_0 )
& ( hskp11
| ! [X32] :
( ~ c2_1(X32)
| ~ c1_1(X32)
| ~ c0_1(X32) )
| ~ ndr1_0
| ! [X31] :
( ~ c1_1(X31)
| c3_1(X31)
| c0_1(X31) )
| ~ ndr1_0 )
& ( hskp11
| hskp29
| ! [X30] :
( ~ c3_1(X30)
| c2_1(X30)
| c0_1(X30) )
| ~ ndr1_0 )
& ( hskp10
| hskp8
| ! [X29] :
( ~ c1_1(X29)
| c2_1(X29)
| c0_1(X29) )
| ~ ndr1_0 )
& ( ! [X28] :
( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28) )
| ~ ndr1_0
| ! [X27] :
( ~ c3_1(X27)
| ~ c2_1(X27)
| c0_1(X27) )
| ~ ndr1_0
| ! [X26] :
( ~ c1_1(X26)
| c2_1(X26)
| c0_1(X26) )
| ~ ndr1_0 )
& ( ! [X25] :
( ~ c0_1(X25)
| c3_1(X25)
| c1_1(X25) )
| ~ ndr1_0
| ! [X24] :
( ~ c3_1(X24)
| c2_1(X24)
| c0_1(X24) )
| ~ ndr1_0
| ! [X23] :
( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) )
| ~ ndr1_0 )
& ( hskp9
| hskp8
| ! [X22] :
( c3_1(X22)
| c2_1(X22)
| c0_1(X22) )
| ~ ndr1_0 )
& ( hskp7
| ! [X21] :
( ~ c3_1(X21)
| ~ c0_1(X21)
| c2_1(X21) )
| ~ ndr1_0
| ! [X20] :
( c3_1(X20)
| c2_1(X20)
| c0_1(X20) )
| ~ ndr1_0 )
& ( ! [X19] :
( ~ c3_1(X19)
| ~ c1_1(X19)
| ~ c0_1(X19) )
| ~ ndr1_0
| ! [X18] :
( ~ c1_1(X18)
| ~ c0_1(X18)
| c2_1(X18) )
| ~ ndr1_0
| ! [X17] :
( c3_1(X17)
| c2_1(X17)
| c0_1(X17) )
| ~ ndr1_0 )
& ( hskp6
| ! [X16] :
( ~ c2_1(X16)
| ~ c0_1(X16)
| c1_1(X16) )
| ~ ndr1_0
| ! [X15] :
( c3_1(X15)
| c2_1(X15)
| c0_1(X15) )
| ~ ndr1_0 )
& ( hskp2
| hskp5
| ! [X14] :
( ~ c3_1(X14)
| c1_1(X14)
| c0_1(X14) )
| ~ ndr1_0 )
& ( hskp1
| ! [X13] :
( ~ c2_1(X13)
| ~ c1_1(X13)
| ~ c0_1(X13) )
| ~ ndr1_0
| ! [X12] :
( ~ c3_1(X12)
| c1_1(X12)
| c0_1(X12) )
| ~ ndr1_0 )
& ( ! [X11] :
( ~ c3_1(X11)
| ~ c2_1(X11)
| c0_1(X11) )
| ~ ndr1_0
| ! [X10] :
( ~ c3_1(X10)
| c1_1(X10)
| c0_1(X10) )
| ~ ndr1_0
| ! [X9] :
( ~ c2_1(X9)
| c1_1(X9)
| c0_1(X9) )
| ~ ndr1_0 )
& ( hskp2
| hskp28
| ! [X8] :
( c3_1(X8)
| c1_1(X8)
| c0_1(X8) )
| ~ ndr1_0 )
& ( hskp4
| ! [X7] :
( ~ c3_1(X7)
| ~ c0_1(X7)
| c2_1(X7) )
| ~ ndr1_0
| ! [X6] :
( c3_1(X6)
| c1_1(X6)
| c0_1(X6) )
| ~ ndr1_0 )
& ( ! [X5] :
( ~ c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) )
| ~ ndr1_0
| ! [X4] :
( ~ c0_1(X4)
| c3_1(X4)
| c1_1(X4) )
| ~ ndr1_0
| ! [X3] :
( c3_1(X3)
| c1_1(X3)
| c0_1(X3) )
| ~ ndr1_0 )
& ( hskp3
| ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ ndr1_0
| ! [X1] :
( c3_1(X1)
| c1_1(X1)
| c0_1(X1) )
| ~ ndr1_0 )
& ( hskp2
| ! [Z] :
( ~ c2_1(Z)
| ~ c1_1(Z)
| ~ c0_1(Z) )
| ~ ndr1_0
| ! [Y] :
( c2_1(Y)
| c1_1(Y)
| c0_1(Y) )
| ~ ndr1_0 )
& ( hskp1
| ! [X] :
( ~ c3_1(X)
| ~ c0_1(X)
| c1_1(X) )
| ~ ndr1_0
| ! [W] :
( c2_1(W)
| c1_1(W)
| c0_1(W) )
| ~ ndr1_0 )
& ( hskp0
| ! [V] :
( ~ c3_1(V)
| c1_1(V)
| c0_1(V) )
| ~ ndr1_0
| ! [U] :
( c2_1(U)
| c1_1(U)
| c0_1(U) )
| ~ ndr1_0 )
& ( ( c3_1(a563)
& c1_1(a563)
& c0_1(a563)
& ndr1_0 )
| ~ hskp31 )
& ( ( c3_1(a562)
& c2_1(a562)
& c1_1(a562)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a552)
& c2_1(a552)
& c0_1(a552)
& ndr1_0 )
| ~ hskp29 )
& ( ( c2_1(a541)
& c1_1(a541)
& c0_1(a541)
& ndr1_0 )
| ~ hskp28 )
& ( ( ~ c1_1(a615)
& c2_1(a615)
& c0_1(a615)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a604)
& c2_1(a604)
& c1_1(a604)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c1_1(a594)
& ~ c0_1(a594)
& c2_1(a594)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c2_1(a590)
& ~ c0_1(a590)
& c1_1(a590)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a587)
& ~ c2_1(a587)
& ~ c0_1(a587)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c2_1(a584)
& ~ c0_1(a584)
& c3_1(a584)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c1_1(a582)
& c3_1(a582)
& c2_1(a582)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c3_1(a580)
& ~ c0_1(a580)
& c1_1(a580)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c3_1(a576)
& ~ c1_1(a576)
& c0_1(a576)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c3_1(a573)
& ~ c1_1(a573)
& ~ c0_1(a573)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c2_1(a571)
& ~ c1_1(a571)
& c0_1(a571)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a570)
& ~ c2_1(a570)
& c1_1(a570)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c2_1(a567)
& c1_1(a567)
& c0_1(a567)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c0_1(a566)
& c3_1(a566)
& c2_1(a566)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c2_1(a565)
& c3_1(a565)
& c0_1(a565)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c1_1(a564)
& c3_1(a564)
& c0_1(a564)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c2_1(a553)
& c3_1(a553)
& c1_1(a553)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c0_1(a551)
& c3_1(a551)
& c1_1(a551)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c2_1(a549)
& ~ c1_1(a549)
& ~ c0_1(a549)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c0_1(a548)
& c2_1(a548)
& c1_1(a548)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a547)
& ~ c0_1(a547)
& c2_1(a547)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a546)
& ~ c0_1(a546)
& c3_1(a546)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a544)
& c1_1(a544)
& c0_1(a544)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c2_1(a540)
& ~ c1_1(a540)
& c3_1(a540)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c3_1(a539)
& ~ c2_1(a539)
& c0_1(a539)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c3_1(a538)
& ~ c2_1(a538)
& ~ c1_1(a538)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c3_1(a537)
& ~ c1_1(a537)
& c2_1(a537)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c3_1(a536)
& c2_1(a536)
& c0_1(a536)
& ndr1_0 )
| ~ hskp0 ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f5,plain,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f6,plain,
( c0_1(a536)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f7,plain,
( c2_1(a536)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f8,plain,
( ~ c3_1(a536)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f9,plain,
( ndr1_0
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
( c2_1(a537)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f11,plain,
( ~ c1_1(a537)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f12,plain,
( ~ c3_1(a537)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f13,plain,
( ndr1_0
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f14,plain,
( ~ c1_1(a538)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f15,plain,
( ~ c2_1(a538)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f16,plain,
( ~ c3_1(a538)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f17,plain,
( ndr1_0
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f18,plain,
( c0_1(a539)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f19,plain,
( ~ c2_1(a539)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f20,plain,
( ~ c3_1(a539)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f21,plain,
( ndr1_0
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f22,plain,
( c3_1(a540)
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f23,plain,
( ~ c1_1(a540)
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
( ~ c2_1(a540)
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f25,plain,
( ndr1_0
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f26,plain,
( c0_1(a544)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f27,plain,
( c1_1(a544)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f28,plain,
( ~ c3_1(a544)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f29,plain,
( ndr1_0
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f30,plain,
( c3_1(a546)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f31,plain,
( ~ c0_1(a546)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f32,plain,
( ~ c1_1(a546)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f37,plain,
( ndr1_0
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f38,plain,
( c1_1(a548)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f39,plain,
( c2_1(a548)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f40,plain,
( ~ c0_1(a548)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f41,plain,
( ndr1_0
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f42,plain,
( ~ c0_1(a549)
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f43,plain,
( ~ c1_1(a549)
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f44,plain,
( ~ c2_1(a549)
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f45,plain,
( ndr1_0
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f46,plain,
( c1_1(a551)
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f47,plain,
( c3_1(a551)
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f48,plain,
( ~ c0_1(a551)
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f49,plain,
( ndr1_0
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f50,plain,
( c1_1(a553)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f51,plain,
( c3_1(a553)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f52,plain,
( ~ c2_1(a553)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f53,plain,
( ndr1_0
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f54,plain,
( c0_1(a564)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f55,plain,
( c3_1(a564)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f56,plain,
( ~ c1_1(a564)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f58,plain,
( c0_1(a565)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f59,plain,
( c3_1(a565)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f60,plain,
( ~ c2_1(a565)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f61,plain,
( ndr1_0
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f62,plain,
( c2_1(a566)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f63,plain,
( c3_1(a566)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f64,plain,
( ~ c0_1(a566)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f66,plain,
( c0_1(a567)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f67,plain,
( c1_1(a567)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f68,plain,
( ~ c2_1(a567)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f69,plain,
( ndr1_0
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f70,plain,
( c1_1(a570)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f71,plain,
( ~ c2_1(a570)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f72,plain,
( ~ c3_1(a570)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f77,plain,
( ndr1_0
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f78,plain,
( ~ c0_1(a573)
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f79,plain,
( ~ c1_1(a573)
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f80,plain,
( ~ c3_1(a573)
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f81,plain,
( ndr1_0
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f82,plain,
( c0_1(a576)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f83,plain,
( ~ c1_1(a576)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f84,plain,
( ~ c3_1(a576)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f89,plain,
( ndr1_0
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f90,plain,
( c2_1(a582)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f91,plain,
( c3_1(a582)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f92,plain,
( ~ c1_1(a582)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f93,plain,
( ndr1_0
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f94,plain,
( c3_1(a584)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f95,plain,
( ~ c0_1(a584)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f96,plain,
( ~ c2_1(a584)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f101,plain,
( ndr1_0
| ~ hskp24 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f102,plain,
( c1_1(a590)
| ~ hskp24 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f104,plain,
( ~ c2_1(a590)
| ~ hskp24 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f105,plain,
( ndr1_0
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f106,plain,
( c2_1(a594)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f107,plain,
( ~ c0_1(a594)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f108,plain,
( ~ c1_1(a594)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f110,plain,
( c1_1(a604)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f111,plain,
( c2_1(a604)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f112,plain,
( ~ c3_1(a604)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f113,plain,
( ndr1_0
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f114,plain,
( c0_1(a615)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f115,plain,
( c2_1(a615)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f116,plain,
( ~ c1_1(a615)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f122,plain,
( c0_1(a552)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f123,plain,
( c2_1(a552)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f124,plain,
( c3_1(a552)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f130,plain,
( c0_1(a563)
| ~ hskp31 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f131,plain,
( c1_1(a563)
| ~ hskp31 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f132,plain,
( c3_1(a563)
| ~ hskp31 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f133,plain,
! [X0,X1] :
( hskp0
| ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f134,plain,
! [X0,X1] :
( hskp1
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ ndr1_0
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f135,plain,
! [X0,X1] :
( hskp2
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f136,plain,
! [X0,X1] :
( hskp3
| ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f138,plain,
! [X0,X1] :
( hskp4
| ~ c3_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| ~ ndr1_0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f140,plain,
! [X0,X1,X2] :
( ~ c3_1(X2)
| ~ c2_1(X2)
| c0_1(X2)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f141,plain,
! [X0,X1] :
( hskp1
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f142,plain,
! [X0] :
( hskp2
| hskp5
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f149,plain,
! [X0] :
( hskp10
| hskp8
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f150,plain,
! [X0] :
( hskp11
| hskp29
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f155,plain,
! [X0] :
( hskp9
| hskp10
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f156,plain,
! [X0,X1] :
( hskp6
| ~ c1_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f159,plain,
! [X0,X1] :
( hskp31
| ~ c2_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f163,plain,
! [X0] :
( hskp16
| hskp3
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f166,plain,
! [X0,X1] :
( hskp18
| ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f168,plain,
! [X0] :
( hskp9
| hskp19
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f171,plain,
! [X0] :
( hskp21
| hskp29
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f175,plain,
! [X0,X1] :
( hskp3
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f178,plain,
! [X0,X1] :
( ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f179,plain,
! [X0] :
( hskp22
| hskp21
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f182,plain,
! [X0] :
( hskp6
| hskp3
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f183,plain,
! [X0] :
( hskp4
| hskp25
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f184,plain,
! [X0] :
( hskp0
| hskp15
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f185,plain,
! [X0] :
( hskp6
| hskp3
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f186,plain,
! [X0] :
( hskp21
| hskp12
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f189,plain,
! [X0] :
( hskp21
| hskp14
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f190,plain,
! [X0] :
( hskp9
| hskp25
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f194,plain,
! [X0] :
( hskp26
| hskp27
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f202,plain,
( hskp25
| hskp27
| hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f205,plain,
( hskp6
| hskp24
| hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f208,plain,
( hskp18
| hskp24
| hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f213,plain,
! [X0,X1] :
( hskp0
| ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f133]) ).
fof(f214,plain,
! [X0,X1] :
( hskp1
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f134]) ).
fof(f215,plain,
! [X0,X1] :
( hskp2
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f135]) ).
fof(f216,plain,
! [X0,X1] :
( hskp3
| ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f136]) ).
fof(f218,plain,
! [X0,X1] :
( hskp4
| ~ c3_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f138]) ).
fof(f219,plain,
! [X0,X1,X2] :
( ~ c3_1(X2)
| ~ c2_1(X2)
| c0_1(X2)
| ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f140]) ).
fof(f220,plain,
! [X0,X1] :
( hskp1
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f141]) ).
fof(f229,plain,
! [X0,X1] :
( hskp6
| ~ c1_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f156]) ).
fof(f231,plain,
! [X0,X1] :
( hskp31
| ~ c2_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f159]) ).
fof(f235,plain,
! [X0,X1] :
( hskp18
| ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f166]) ).
fof(f240,plain,
! [X0,X1] :
( hskp3
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f175]) ).
fof(f243,plain,
! [X0,X1] :
( ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f178]) ).
fof(f251,plain,
! [X0] :
( ~ hskp18
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a573)
| c0_1(a573)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f213,f79]) ).
fof(f254,plain,
! [X0] :
( ~ hskp9
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a549)
| c0_1(a549)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f213,f43]) ).
fof(f255,plain,
! [X0] :
( ~ hskp6
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a546)
| c0_1(a546)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f213,f32]) ).
fof(f256,plain,
! [X0] :
( ~ hskp4
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a540)
| c0_1(a540)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f213,f23]) ).
fof(f259,plain,
! [X0] :
( ~ hskp18
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a573)
| c0_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f251,f77]) ).
fof(f260,plain,
! [X0] :
( ~ hskp9
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a549)
| c0_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f254,f41]) ).
fof(f261,plain,
! [X0] :
( ~ hskp6
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f255,f29]) ).
fof(f262,plain,
! [X0] :
( ~ hskp4
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a540)
| c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f256,f21]) ).
fof(f284,plain,
! [X0] :
( ~ hskp18
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a573)
| c0_1(a573)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f214,f79]) ).
fof(f287,plain,
! [X0] :
( ~ hskp9
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a549)
| c0_1(a549)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f214,f43]) ).
fof(f288,plain,
! [X0] :
( ~ hskp6
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a546)
| c0_1(a546)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f214,f32]) ).
fof(f292,plain,
! [X0] :
( ~ hskp18
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a573)
| c0_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f284,f77]) ).
fof(f293,plain,
! [X0] :
( ~ hskp9
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a549)
| c0_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f287,f41]) ).
fof(f294,plain,
! [X0] :
( ~ hskp6
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f29]) ).
fof(f305,plain,
! [X0] :
( ~ hskp6
| hskp2
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(a546)
| c0_1(a546)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f215,f32]) ).
fof(f311,plain,
! [X0] :
( ~ hskp6
| hskp2
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f305,f29]) ).
fof(f327,plain,
( ~ hskp6
| hskp2
| hskp5
| ~ c3_1(a546)
| c0_1(a546)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f142,f32]) ).
fof(f334,plain,
( ~ hskp6
| hskp2
| hskp5
| ~ c3_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f327,f29]) ).
fof(f339,plain,
( ~ hskp6
| hskp2
| hskp5
| ~ c3_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f334,f31]) ).
fof(f366,plain,
! [X0] :
( ~ hskp25
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a594)
| c0_1(a594)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f216,f108]) ).
fof(f369,plain,
! [X0] :
( ~ hskp18
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a573)
| c0_1(a573)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f216,f79]) ).
fof(f372,plain,
! [X0] :
( ~ hskp9
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a549)
| c0_1(a549)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f216,f43]) ).
fof(f375,plain,
! [X0] :
( ~ hskp2
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a538)
| c0_1(a538)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f216,f14]) ).
fof(f376,plain,
! [X0] :
( ~ hskp1
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a537)
| c0_1(a537)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f216,f11]) ).
fof(f377,plain,
! [X0] :
( ~ hskp25
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a594)
| c0_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f366,f105]) ).
fof(f378,plain,
! [X0] :
( ~ hskp18
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a573)
| c0_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f369,f77]) ).
fof(f379,plain,
! [X0] :
( ~ hskp9
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a549)
| c0_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f41]) ).
fof(f380,plain,
! [X0] :
( ~ hskp2
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a538)
| c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f375,f13]) ).
fof(f381,plain,
! [X0] :
( ~ hskp1
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a537)
| c0_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f376,f9]) ).
fof(f403,plain,
! [X0] :
( ~ hskp18
| hskp4
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| c3_1(a573)
| c0_1(a573)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f218,f79]) ).
fof(f412,plain,
! [X0] :
( ~ hskp18
| hskp4
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| c3_1(a573)
| c0_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f403,f77]) ).
fof(f423,plain,
( ~ hskp11
| hskp10
| hskp8
| ~ c1_1(a553)
| c0_1(a553)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f149,f52]) ).
fof(f432,plain,
( ~ hskp11
| hskp10
| hskp8
| ~ c1_1(a553)
| c0_1(a553) ),
inference(forward_subsumption_resolution,[status(thm)],[f423,f49]) ).
fof(f437,plain,
( ~ hskp11
| hskp10
| hskp8
| c0_1(a553) ),
inference(forward_subsumption_resolution,[status(thm)],[f432,f50]) ).
fof(f439,plain,
! [X0,X1] :
( ~ hskp25
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a594)
| c0_1(a594)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f219,f108]) ).
fof(f440,plain,
! [X0,X1] :
( ~ hskp21
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a582)
| c0_1(a582)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f219,f92]) ).
fof(f446,plain,
! [X0,X1] :
( ~ hskp6
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a546)
| c0_1(a546)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f219,f32]) ).
fof(f450,plain,
! [X0,X1] :
( ~ hskp25
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a594)
| c0_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f105]) ).
fof(f451,plain,
! [X0,X1] :
( ~ hskp21
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a582)
| c0_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f440,f89]) ).
fof(f453,plain,
! [X0,X1] :
( ~ hskp6
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f446,f29]) ).
fof(f457,plain,
( ~ hskp22
| hskp11
| hskp29
| ~ c3_1(a584)
| c0_1(a584)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f150,f96]) ).
fof(f463,plain,
( ~ hskp9
| hskp11
| hskp29
| ~ c3_1(a549)
| c0_1(a549)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f150,f44]) ).
fof(f468,plain,
( ~ hskp22
| hskp11
| hskp29
| ~ c3_1(a584)
| c0_1(a584) ),
inference(forward_subsumption_resolution,[status(thm)],[f457,f93]) ).
fof(f469,plain,
( ~ hskp9
| hskp11
| hskp29
| ~ c3_1(a549)
| c0_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f41]) ).
fof(f472,plain,
( ~ hskp22
| hskp11
| hskp29
| ~ c3_1(a584) ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f95]) ).
fof(f473,plain,
( ~ hskp9
| hskp11
| hskp29
| ~ c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f469,f42]) ).
fof(f506,plain,
( ~ hskp8
| hskp9
| hskp10
| ~ c2_1(a548)
| ~ c1_1(a548)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f155,f40]) ).
fof(f511,plain,
( ~ hskp8
| hskp9
| hskp10
| ~ c2_1(a548)
| ~ c1_1(a548) ),
inference(forward_subsumption_resolution,[status(thm)],[f506,f37]) ).
fof(f521,plain,
! [X0] :
( ~ hskp6
| hskp1
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a546)
| c0_1(a546)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f220,f32]) ).
fof(f528,plain,
! [X0] :
( ~ hskp6
| hskp1
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f521,f29]) ).
fof(f549,plain,
( ~ hskp8
| hskp9
| hskp10
| ~ c2_1(a548) ),
inference(forward_subsumption_resolution,[status(thm)],[f511,f38]) ).
fof(f674,plain,
( ~ hskp2
| hskp16
| hskp3
| c3_1(a538)
| c2_1(a538)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f163,f14]) ).
fof(f680,plain,
( ~ hskp2
| hskp16
| hskp3
| c3_1(a538)
| c2_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f674,f13]) ).
fof(f702,plain,
( ~ hskp2
| hskp16
| hskp3
| c3_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f680,f15]) ).
fof(f703,plain,
( ~ hskp2
| ~ hskp2
| hskp16
| hskp3 ),
inference(resolution,[status(thm)],[f702,f16]) ).
fof(f704,plain,
( ~ hskp2
| hskp16
| hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f703]) ).
fof(f731,plain,
( ~ hskp12
| hskp9
| hskp19
| ~ c3_1(a564)
| c2_1(a564)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f168,f56]) ).
fof(f738,plain,
( ~ hskp12
| hskp9
| hskp19
| ~ c3_1(a564)
| c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f53]) ).
fof(f742,plain,
( ~ hskp12
| hskp9
| hskp19
| c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f738,f55]) ).
fof(f801,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ c2_1(a615)
| c3_1(a615)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f171,f116]) ).
fof(f802,plain,
( ~ hskp25
| hskp21
| hskp29
| ~ c2_1(a594)
| c3_1(a594)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f171,f108]) ).
fof(f804,plain,
( ~ hskp19
| hskp21
| hskp29
| ~ c2_1(a576)
| c3_1(a576)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f171,f83]) ).
fof(f805,plain,
( ~ hskp18
| hskp21
| hskp29
| ~ c2_1(a573)
| c3_1(a573)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f171,f79]) ).
fof(f812,plain,
( ~ hskp1
| hskp21
| hskp29
| ~ c2_1(a537)
| c3_1(a537)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f171,f11]) ).
fof(f813,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ c2_1(a615)
| c3_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f801,f113]) ).
fof(f814,plain,
( ~ hskp25
| hskp21
| hskp29
| ~ c2_1(a594)
| c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f105]) ).
fof(f815,plain,
( ~ hskp19
| hskp21
| hskp29
| ~ c2_1(a576)
| c3_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f804,f81]) ).
fof(f816,plain,
( ~ hskp18
| hskp21
| hskp29
| ~ c2_1(a573)
| c3_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f805,f77]) ).
fof(f817,plain,
( ~ hskp1
| hskp21
| hskp29
| ~ c2_1(a537)
| c3_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f812,f9]) ).
fof(f818,plain,
( ~ hskp27
| hskp21
| hskp29
| c3_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f813,f115]) ).
fof(f819,plain,
( ~ hskp25
| hskp21
| hskp29
| c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f814,f106]) ).
fof(f820,plain,
( ~ hskp19
| hskp21
| hskp29
| ~ c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f815,f84]) ).
fof(f821,plain,
( ~ hskp18
| hskp21
| hskp29
| ~ c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f816,f80]) ).
fof(f822,plain,
( ~ hskp1
| hskp21
| hskp29
| ~ c2_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f817,f12]) ).
fof(f831,plain,
( ~ hskp3
| hskp22
| hskp21
| ~ c0_1(a539)
| c2_1(a539)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f179,f20]) ).
fof(f838,plain,
( ~ hskp3
| hskp22
| hskp21
| ~ c0_1(a539)
| c2_1(a539) ),
inference(forward_subsumption_resolution,[status(thm)],[f831,f17]) ).
fof(f843,plain,
( ~ hskp3
| hskp22
| hskp21
| ~ c0_1(a539) ),
inference(forward_subsumption_resolution,[status(thm)],[f838,f19]) ).
fof(f868,plain,
! [X0] :
( ~ hskp10
| hskp6
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(a551)
| ~ c1_1(a551)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f229,f48]) ).
fof(f876,plain,
! [X0] :
( ~ hskp10
| hskp6
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(a551)
| ~ c1_1(a551) ),
inference(forward_subsumption_resolution,[status(thm)],[f868,f45]) ).
fof(f922,plain,
! [X0] :
( ~ hskp14
| hskp31
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a566)
| ~ c2_1(a566)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f231,f64]) ).
fof(f929,plain,
! [X0] :
( ~ hskp14
| hskp31
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a566)
| ~ c2_1(a566) ),
inference(forward_subsumption_resolution,[status(thm)],[f922,f61]) ).
fof(f938,plain,
( ~ hskp16
| hskp4
| hskp25
| ~ c1_1(a570)
| c2_1(a570)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f183,f72]) ).
fof(f940,plain,
( ~ hskp5
| hskp4
| hskp25
| ~ c1_1(a544)
| c2_1(a544)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f183,f28]) ).
fof(f947,plain,
( ~ hskp16
| hskp4
| hskp25
| ~ c1_1(a570)
| c2_1(a570) ),
inference(forward_subsumption_resolution,[status(thm)],[f938,f69]) ).
fof(f948,plain,
( ~ hskp5
| hskp4
| hskp25
| ~ c1_1(a544)
| c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f940,f25]) ).
fof(f952,plain,
( ~ hskp16
| hskp4
| hskp25
| ~ c1_1(a570) ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f71]) ).
fof(f953,plain,
( ~ hskp5
| hskp4
| hskp25
| c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f948,f27]) ).
fof(f964,plain,
( ~ hskp4
| hskp0
| hskp15
| ~ c3_1(a540)
| ~ c0_1(a540)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f184,f24]) ).
fof(f970,plain,
( ~ hskp4
| hskp0
| hskp15
| ~ c3_1(a540)
| ~ c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f964,f21]) ).
fof(f974,plain,
( ~ hskp4
| hskp0
| hskp15
| ~ c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f970,f22]) ).
fof(f975,plain,
! [X0] :
( hskp6
| hskp3
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f185,f182]) ).
fof(f976,plain,
( ~ hskp24
| hskp6
| hskp3
| ~ c1_1(a590)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f975,f104]) ).
fof(f988,plain,
( ~ hskp24
| hskp6
| hskp3
| ~ c1_1(a590) ),
inference(forward_subsumption_resolution,[status(thm)],[f976,f101]) ).
fof(f1026,plain,
( ~ hskp24
| hskp6
| hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f988,f102]) ).
fof(f1036,plain,
( ~ hskp5
| hskp21
| hskp12
| ~ c2_1(a544)
| ~ c0_1(a544)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f186,f28]) ).
fof(f1040,plain,
( ~ hskp0
| hskp21
| hskp12
| ~ c2_1(a536)
| ~ c0_1(a536)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f186,f8]) ).
fof(f1043,plain,
( ~ hskp5
| hskp21
| hskp12
| ~ c2_1(a544)
| ~ c0_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f1036,f25]) ).
fof(f1045,plain,
( ~ hskp0
| hskp21
| hskp12
| ~ c2_1(a536)
| ~ c0_1(a536) ),
inference(forward_subsumption_resolution,[status(thm)],[f1040,f5]) ).
fof(f1048,plain,
( ~ hskp5
| hskp21
| hskp12
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f1043,f26]) ).
fof(f1050,plain,
( ~ hskp0
| hskp21
| hskp12
| ~ c2_1(a536) ),
inference(forward_subsumption_resolution,[status(thm)],[f1045,f6]) ).
fof(f1108,plain,
! [X0] :
( ~ hskp19
| hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(a576)
| c2_1(a576)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f235,f83]) ).
fof(f1114,plain,
! [X0] :
( ~ hskp4
| hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(a540)
| c2_1(a540)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f235,f23]) ).
fof(f1117,plain,
! [X0] :
( ~ hskp19
| hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(a576)
| c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f1108,f81]) ).
fof(f1120,plain,
! [X0] :
( ~ hskp4
| hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(a540)
| c2_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f21]) ).
fof(f1192,plain,
( ~ hskp0
| hskp9
| hskp25
| ~ c2_1(a536)
| ~ c0_1(a536)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f190,f8]) ).
fof(f1197,plain,
( ~ hskp0
| hskp9
| hskp25
| ~ c2_1(a536)
| ~ c0_1(a536) ),
inference(forward_subsumption_resolution,[status(thm)],[f1192,f5]) ).
fof(f1202,plain,
( ~ hskp0
| hskp9
| hskp25
| ~ c2_1(a536) ),
inference(forward_subsumption_resolution,[status(thm)],[f1197,f6]) ).
fof(f1264,plain,
! [X0] :
( ~ hskp5
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a544)
| c2_1(a544)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f243,f28]) ).
fof(f1265,plain,
! [X0] :
( ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a539)
| c2_1(a539)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f243,f20]) ).
fof(f1266,plain,
! [X0] :
( ~ hskp2
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a538)
| c2_1(a538)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f243,f16]) ).
fof(f1271,plain,
! [X0] :
( ~ hskp5
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a544)
| c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f1264,f25]) ).
fof(f1272,plain,
! [X0] :
( ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a539)
| c2_1(a539) ),
inference(forward_subsumption_resolution,[status(thm)],[f1265,f17]) ).
fof(f1273,plain,
! [X0] :
( ~ hskp2
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a538)
| c2_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f1266,f13]) ).
fof(f1393,plain,
! [X0] :
( ~ hskp1
| hskp3
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c2_1(a537)
| ~ c0_1(a537)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f240,f11]) ).
fof(f1398,plain,
! [X0] :
( ~ hskp1
| hskp3
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c2_1(a537)
| ~ c0_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f1393,f9]) ).
fof(f1463,plain,
! [X0] :
( ~ hskp5
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f1271,f26]) ).
fof(f1464,plain,
! [X0] :
( ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a539) ),
inference(forward_subsumption_resolution,[status(thm)],[f1272,f19]) ).
fof(f1465,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ hskp3
| ~ c2_1(a615)
| ~ c0_1(a615)
| ~ c0_1(a539) ),
inference(resolution,[status(thm)],[f1464,f818]) ).
fof(f1477,plain,
( ~ hskp29
| ~ hskp3
| ~ c2_1(a552)
| ~ c0_1(a552)
| ~ c0_1(a539) ),
inference(resolution,[status(thm)],[f1464,f124]) ).
fof(f1479,plain,
( ~ hskp21
| ~ hskp3
| ~ c2_1(a582)
| ~ c0_1(a582)
| ~ c0_1(a539) ),
inference(resolution,[status(thm)],[f1464,f91]) ).
fof(f1482,plain,
( ~ hskp12
| ~ hskp3
| ~ c2_1(a564)
| ~ c0_1(a564)
| ~ c0_1(a539) ),
inference(resolution,[status(thm)],[f1464,f55]) ).
fof(f1491,plain,
! [X0] :
( hskp21
| hskp14
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a539) ),
inference(resolution,[status(thm)],[f1464,f189]) ).
fof(f1494,plain,
! [X0] :
( hskp21
| hskp12
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a539) ),
inference(resolution,[status(thm)],[f1464,f186]) ).
fof(f1505,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ hskp3
| ~ c2_1(a615)
| ~ c0_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f1465,f18]) ).
fof(f1509,plain,
( ~ hskp29
| ~ hskp3
| ~ c2_1(a552)
| ~ c0_1(a552) ),
inference(forward_subsumption_resolution,[status(thm)],[f1477,f18]) ).
fof(f1510,plain,
( ~ hskp21
| ~ hskp3
| ~ c2_1(a582)
| ~ c0_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f1479,f18]) ).
fof(f1511,plain,
( ~ hskp12
| ~ hskp3
| ~ c2_1(a564)
| ~ c0_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1482,f18]) ).
fof(f1516,plain,
! [X0] :
( hskp21
| hskp14
| ~ ndr1_0
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a539) ),
inference(duplicate_literals_removal,[status(thm)],[f1491]) ).
fof(f1517,plain,
! [X0] :
( hskp21
| hskp14
| ~ ndr1_0
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1516,f18]) ).
fof(f1522,plain,
! [X0] :
( hskp21
| hskp12
| ~ ndr1_0
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a539) ),
inference(duplicate_literals_removal,[status(thm)],[f1494]) ).
fof(f1523,plain,
! [X0] :
( hskp21
| hskp12
| ~ ndr1_0
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1522,f18]) ).
fof(f1546,plain,
( ~ hskp29
| ~ hskp3
| ~ c2_1(a552) ),
inference(forward_subsumption_resolution,[status(thm)],[f1509,f122]) ).
fof(f1547,plain,
( ~ hskp29
| ~ hskp29
| ~ hskp3 ),
inference(resolution,[status(thm)],[f1546,f123]) ).
fof(f1554,plain,
( ~ hskp29
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f1547]) ).
fof(f1557,plain,
( ~ hskp1
| hskp21
| ~ c2_1(a537)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f1554,f822]) ).
fof(f1558,plain,
( ~ hskp18
| hskp21
| ~ c2_1(a573)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f1554,f821]) ).
fof(f1559,plain,
( ~ hskp19
| hskp21
| ~ c2_1(a576)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f1554,f820]) ).
fof(f1561,plain,
( ~ hskp22
| hskp11
| ~ c3_1(a584)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f1554,f472]) ).
fof(f1563,plain,
( ~ hskp1
| hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f1557,f10]) ).
fof(f1564,plain,
( ~ hskp22
| hskp11
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f1561,f94]) ).
fof(f1583,plain,
( ~ hskp21
| ~ hskp3
| ~ c0_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f1510,f90]) ).
fof(f1597,plain,
( ~ hskp12
| ~ hskp3
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1511,f54]) ).
fof(f1598,plain,
( ~ hskp12
| hskp9
| hskp19
| ~ hskp12
| ~ hskp3 ),
inference(resolution,[status(thm)],[f1597,f742]) ).
fof(f1605,plain,
( hskp9
| hskp19
| ~ hskp12
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f1598]) ).
fof(f1608,plain,
! [X0] :
( hskp21
| hskp14
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1517,f17]) ).
fof(f1611,plain,
! [X0] :
( hskp21
| hskp12
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1523,f17]) ).
fof(f1612,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ hskp3
| ~ c2_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f1505,f114]) ).
fof(f1613,plain,
( ~ hskp3
| ~ hskp27
| hskp21
| ~ hskp3
| ~ c2_1(a615) ),
inference(resolution,[status(thm)],[f1612,f1554]) ).
fof(f1614,plain,
( ~ hskp27
| hskp21
| ~ hskp3
| ~ c2_1(a615) ),
inference(duplicate_literals_removal,[status(thm)],[f1613]) ).
fof(f1615,plain,
( ~ hskp27
| hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f1614,f115]) ).
fof(f1617,plain,
! [X0] :
( ~ hskp18
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f259,f78]) ).
fof(f1626,plain,
( ~ hskp6
| ~ hskp18
| hskp0
| ~ c3_1(a546)
| c0_1(a546)
| c2_1(a573) ),
inference(resolution,[status(thm)],[f1617,f32]) ).
fof(f1634,plain,
( ~ hskp6
| ~ hskp18
| hskp0
| ~ c3_1(a546)
| c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f1626,f31]) ).
fof(f1636,plain,
! [X0] :
( ~ hskp9
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f260,f42]) ).
fof(f1638,plain,
( ~ hskp25
| ~ hskp9
| hskp0
| ~ c3_1(a594)
| c0_1(a594)
| c2_1(a549) ),
inference(resolution,[status(thm)],[f1636,f108]) ).
fof(f1645,plain,
( ~ hskp6
| ~ hskp9
| hskp0
| ~ c3_1(a546)
| c0_1(a546)
| c2_1(a549) ),
inference(resolution,[status(thm)],[f1636,f32]) ).
fof(f1649,plain,
( ~ hskp25
| ~ hskp9
| hskp0
| ~ c3_1(a594)
| c0_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f1638,f44]) ).
fof(f1653,plain,
( ~ hskp6
| ~ hskp9
| hskp0
| ~ c3_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1645,f44]) ).
fof(f1655,plain,
! [X0] :
( ~ hskp6
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f261,f31]) ).
fof(f1664,plain,
( ~ hskp6
| ~ hskp6
| hskp0
| ~ c3_1(a546)
| c0_1(a546)
| c2_1(a546) ),
inference(resolution,[status(thm)],[f1655,f32]) ).
fof(f1671,plain,
( ~ hskp6
| hskp0
| ~ c3_1(a546)
| c0_1(a546)
| c2_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f1664]) ).
fof(f1672,plain,
( ~ hskp6
| hskp0
| ~ c3_1(a546)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1671,f31]) ).
fof(f1675,plain,
( ~ hskp6
| hskp0
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1672,f30]) ).
fof(f1676,plain,
( ~ hskp6
| ~ hskp18
| hskp0
| c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f1634,f30]) ).
fof(f1677,plain,
! [X0] :
( ~ hskp4
| hskp0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f262,f24]) ).
fof(f1687,plain,
( ~ hskp4
| ~ hskp4
| hskp0
| ~ c3_1(a540)
| c0_1(a540)
| c0_1(a540) ),
inference(resolution,[status(thm)],[f1677,f23]) ).
fof(f1693,plain,
( ~ hskp4
| hskp0
| ~ c3_1(a540)
| c0_1(a540) ),
inference(duplicate_literals_removal,[status(thm)],[f1687]) ).
fof(f1694,plain,
( ~ hskp4
| hskp0
| c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f1693,f22]) ).
fof(f1695,plain,
( ~ hskp4
| hskp0
| hskp15 ),
inference(backward_subsumption_resolution,[status(thm)],[f974,f1694]) ).
fof(f1696,plain,
( ~ hskp25
| ~ hskp9
| hskp0
| ~ c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f1649,f107]) ).
fof(f1702,plain,
( ~ hskp6
| ~ hskp9
| hskp0
| ~ c3_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1653,f31]) ).
fof(f1720,plain,
! [X0] :
( ~ hskp18
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f292,f78]) ).
fof(f1727,plain,
( ~ hskp12
| ~ hskp18
| hskp1
| ~ c3_1(a564)
| ~ c0_1(a564)
| c2_1(a573) ),
inference(resolution,[status(thm)],[f1720,f56]) ).
fof(f1730,plain,
( ~ hskp4
| ~ hskp18
| hskp1
| ~ c3_1(a540)
| ~ c0_1(a540)
| c2_1(a573) ),
inference(resolution,[status(thm)],[f1720,f23]) ).
fof(f1737,plain,
( ~ hskp12
| ~ hskp18
| hskp1
| ~ c3_1(a564)
| c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f1727,f54]) ).
fof(f1738,plain,
( ~ hskp4
| ~ hskp18
| hskp1
| ~ c0_1(a540)
| c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f1730,f22]) ).
fof(f1744,plain,
( ~ hskp12
| ~ hskp18
| hskp1
| c2_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f1737,f55]) ).
fof(f1749,plain,
! [X0] :
( ~ hskp9
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f293,f42]) ).
fof(f1756,plain,
( ~ hskp12
| ~ hskp9
| hskp1
| ~ c3_1(a564)
| ~ c0_1(a564)
| c2_1(a549) ),
inference(resolution,[status(thm)],[f1749,f56]) ).
fof(f1759,plain,
( ~ hskp4
| ~ hskp9
| hskp1
| ~ c3_1(a540)
| ~ c0_1(a540)
| c2_1(a549) ),
inference(resolution,[status(thm)],[f1749,f23]) ).
fof(f1765,plain,
( ~ hskp12
| ~ hskp9
| hskp1
| ~ c3_1(a564)
| ~ c0_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1756,f44]) ).
fof(f1767,plain,
( ~ hskp4
| ~ hskp9
| hskp1
| ~ c3_1(a540)
| ~ c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f1759,f44]) ).
fof(f1768,plain,
! [X0] :
( ~ hskp6
| hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f294,f31]) ).
fof(f1775,plain,
( ~ hskp12
| ~ hskp6
| hskp1
| ~ c3_1(a564)
| ~ c0_1(a564)
| c2_1(a546) ),
inference(resolution,[status(thm)],[f1768,f56]) ).
fof(f1784,plain,
( ~ hskp12
| ~ hskp6
| hskp1
| ~ c3_1(a564)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1775,f54]) ).
fof(f1807,plain,
( ~ hskp12
| ~ hskp9
| hskp1
| ~ c3_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1765,f54]) ).
fof(f1808,plain,
( ~ hskp4
| ~ hskp9
| hskp1
| ~ c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f1767,f22]) ).
fof(f1827,plain,
( ~ hskp12
| ~ hskp6
| hskp1
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1784,f55]) ).
fof(f1836,plain,
! [X0] :
( ~ hskp2
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f1273,f15]) ).
fof(f1849,plain,
( ~ hskp29
| ~ hskp2
| ~ c2_1(a552)
| ~ c0_1(a552)
| ~ c0_1(a538) ),
inference(resolution,[status(thm)],[f1836,f124]) ).
fof(f1851,plain,
( ~ hskp21
| ~ hskp2
| ~ c2_1(a582)
| ~ c0_1(a582)
| ~ c0_1(a538) ),
inference(resolution,[status(thm)],[f1836,f91]) ).
fof(f1881,plain,
( ~ hskp29
| ~ hskp2
| ~ c2_1(a552)
| ~ c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f1849,f122]) ).
fof(f1882,plain,
( ~ hskp21
| ~ hskp2
| ~ c0_1(a582)
| ~ c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f1851,f90]) ).
fof(f1917,plain,
( ~ hskp29
| ~ hskp2
| ~ c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f1881,f123]) ).
fof(f1970,plain,
! [X0] :
( ~ hskp6
| hskp2
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f311,f31]) ).
fof(f1972,plain,
! [X0] :
( ~ hskp25
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f377,f107]) ).
fof(f1996,plain,
! [X0] :
( ~ hskp18
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f378,f78]) ).
fof(f2005,plain,
( ~ hskp6
| ~ hskp18
| hskp3
| ~ c3_1(a546)
| c2_1(a546)
| c3_1(a573) ),
inference(resolution,[status(thm)],[f1996,f32]) ).
fof(f2006,plain,
( ~ hskp4
| ~ hskp18
| hskp3
| ~ c3_1(a540)
| c2_1(a540)
| c3_1(a573) ),
inference(resolution,[status(thm)],[f1996,f23]) ).
fof(f2012,plain,
( ~ hskp6
| ~ hskp18
| hskp3
| ~ c3_1(a546)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2005,f80]) ).
fof(f2013,plain,
( ~ hskp4
| ~ hskp18
| hskp3
| ~ c3_1(a540)
| c2_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f2006,f80]) ).
fof(f2032,plain,
( ~ hskp6
| ~ hskp18
| hskp3
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2012,f30]) ).
fof(f2033,plain,
( ~ hskp4
| ~ hskp18
| hskp3
| ~ c3_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f2013,f24]) ).
fof(f2036,plain,
! [X0] :
( ~ hskp9
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f379,f42]) ).
fof(f2045,plain,
( ~ hskp6
| ~ hskp9
| hskp3
| ~ c3_1(a546)
| c2_1(a546)
| c3_1(a549) ),
inference(resolution,[status(thm)],[f2036,f32]) ).
fof(f2051,plain,
( ~ hskp6
| ~ hskp9
| hskp3
| c2_1(a546)
| c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f2045,f30]) ).
fof(f2053,plain,
! [X0] :
( ~ hskp2
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f380,f16]) ).
fof(f2063,plain,
( ~ hskp4
| ~ hskp2
| hskp3
| ~ c3_1(a540)
| c2_1(a540)
| c0_1(a538) ),
inference(resolution,[status(thm)],[f2053,f23]) ).
fof(f2070,plain,
( ~ hskp4
| ~ hskp2
| hskp3
| ~ c3_1(a540)
| c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f2063,f24]) ).
fof(f2177,plain,
( ~ hskp4
| ~ hskp2
| hskp3
| c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f2070,f22]) ).
fof(f2178,plain,
( ~ hskp29
| ~ hskp2
| ~ hskp4
| ~ hskp2
| hskp3 ),
inference(resolution,[status(thm)],[f2177,f1917]) ).
fof(f2179,plain,
( ~ hskp29
| ~ hskp4
| ~ hskp2
| hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2178]) ).
fof(f2180,plain,
( ~ hskp29
| ~ hskp4
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f2179,f1554]) ).
fof(f2181,plain,
! [X0] :
( ~ hskp1
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c0_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f381,f12]) ).
fof(f2190,plain,
( ~ hskp6
| ~ hskp1
| hskp3
| ~ c3_1(a546)
| c2_1(a546)
| c0_1(a537) ),
inference(resolution,[status(thm)],[f2181,f32]) ).
fof(f2197,plain,
( ~ hskp6
| ~ hskp1
| hskp3
| c2_1(a546)
| c0_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f2190,f30]) ).
fof(f2240,plain,
( ~ hskp1
| hskp21
| ~ c2_1(a537)
| ~ hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f2180,f822]) ).
fof(f2247,plain,
( ~ hskp1
| hskp21
| ~ hskp4
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f2240,f10]) ).
fof(f2336,plain,
! [X0] :
( ~ hskp18
| hskp4
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| c3_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f412,f78]) ).
fof(f2337,plain,
! [X0] :
( ~ hskp18
| ~ hskp18
| hskp4
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) ),
inference(resolution,[status(thm)],[f2336,f80]) ).
fof(f2341,plain,
! [X0] :
( ~ hskp18
| hskp4
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2337]) ).
fof(f2361,plain,
( ~ hskp13
| ~ hskp18
| hskp4
| ~ c3_1(a565)
| ~ c0_1(a565) ),
inference(resolution,[status(thm)],[f2341,f60]) ).
fof(f2375,plain,
( ~ hskp13
| ~ hskp18
| hskp4
| ~ c3_1(a565) ),
inference(forward_subsumption_resolution,[status(thm)],[f2361,f58]) ).
fof(f2377,plain,
( ~ hskp13
| ~ hskp18
| hskp4 ),
inference(forward_subsumption_resolution,[status(thm)],[f2375,f59]) ).
fof(f2482,plain,
! [X0,X1] :
( ~ hskp25
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f450,f107]) ).
fof(f2484,plain,
! [X0] :
( ~ hskp25
| ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a594)
| c0_1(a594)
| ~ c2_1(a594) ),
inference(resolution,[status(thm)],[f2482,f108]) ).
fof(f2491,plain,
! [X0] :
( ~ hskp6
| ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a546)
| c0_1(a546)
| ~ c2_1(a594) ),
inference(resolution,[status(thm)],[f2482,f32]) ).
fof(f2495,plain,
! [X0] :
( ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a594)
| c0_1(a594)
| ~ c2_1(a594) ),
inference(duplicate_literals_removal,[status(thm)],[f2484]) ).
fof(f2496,plain,
! [X0] :
( ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a594)
| c0_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f2495,f106]) ).
fof(f2499,plain,
! [X0] :
( ~ hskp6
| ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a546)
| c0_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2491,f106]) ).
fof(f2548,plain,
! [X0,X1] :
( ~ hskp21
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f451,f90]) ).
fof(f2551,plain,
! [X0] :
( ~ hskp21
| ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a582)
| c0_1(a582)
| c0_1(a582) ),
inference(resolution,[status(thm)],[f2548,f92]) ).
fof(f2562,plain,
! [X0] :
( ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a582)
| c0_1(a582) ),
inference(duplicate_literals_removal,[status(thm)],[f2551]) ).
fof(f2563,plain,
! [X0] :
( ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c0_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f2562,f91]) ).
fof(f2586,plain,
! [X0,X1] :
( ~ hskp6
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f453,f31]) ).
fof(f2595,plain,
! [X0] :
( ~ hskp6
| ~ hskp6
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a546)
| c0_1(a546)
| ~ c2_1(a546) ),
inference(resolution,[status(thm)],[f2586,f32]) ).
fof(f2602,plain,
! [X0] :
( ~ hskp6
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a546)
| c0_1(a546)
| ~ c2_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f2595]) ).
fof(f2603,plain,
! [X0] :
( ~ hskp6
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a546)
| ~ c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2602,f31]) ).
fof(f2605,plain,
! [X0] :
( ~ hskp21
| ~ hskp2
| ~ c0_1(a538)
| ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(resolution,[status(thm)],[f2563,f1882]) ).
fof(f2606,plain,
! [X0] :
( ~ hskp21
| ~ hskp3
| ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(resolution,[status(thm)],[f2563,f1583]) ).
fof(f2608,plain,
! [X0] :
( ~ hskp2
| ~ c0_1(a538)
| ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2605]) ).
fof(f2609,plain,
! [X0] :
( ~ hskp2
| ~ c0_1(a538)
| ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2608,f1836]) ).
fof(f2610,plain,
! [X0] :
( ~ hskp3
| ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2606]) ).
fof(f2616,plain,
( ~ hskp21
| ~ hskp3
| ~ hskp3
| ~ hskp21
| ~ c3_1(a582)
| ~ c2_1(a582) ),
inference(resolution,[status(thm)],[f2610,f1583]) ).
fof(f2637,plain,
( ~ hskp3
| ~ hskp21
| ~ c3_1(a582)
| ~ c2_1(a582) ),
inference(duplicate_literals_removal,[status(thm)],[f2616]) ).
fof(f2638,plain,
( ~ hskp3
| ~ hskp21
| ~ c3_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f2637,f90]) ).
fof(f2650,plain,
( ~ hskp27
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1615,f2657]) ).
fof(f2651,plain,
! [X0] :
( hskp12
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1611,f2657]) ).
fof(f2652,plain,
! [X0] :
( hskp14
| ~ hskp3
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1608,f2657]) ).
fof(f2653,plain,
( ~ hskp19
| ~ c2_1(a576)
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1559,f2657]) ).
fof(f2654,plain,
( ~ hskp18
| ~ c2_1(a573)
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1558,f2657]) ).
fof(f2655,plain,
( ~ hskp1
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1563,f2657]) ).
fof(f2656,plain,
( ~ hskp3
| hskp22
| ~ c0_1(a539) ),
inference(backward_subsumption_resolution,[status(thm)],[f843,f2657]) ).
fof(f2657,plain,
( ~ hskp3
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f2638,f91]) ).
fof(f2678,plain,
( ~ hskp0
| hskp12
| ~ c2_1(a536)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2657,f1050]) ).
fof(f2680,plain,
( ~ hskp5
| hskp12
| ~ c2_1(a544)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2657,f1048]) ).
fof(f2685,plain,
( ~ hskp3
| hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f2656,f18]) ).
fof(f2687,plain,
( ~ hskp0
| hskp12
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2678,f7]) ).
fof(f2688,plain,
! [X0] :
( hskp26
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2650,f194]) ).
fof(f2689,plain,
( hskp25
| hskp5
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2650,f202]) ).
fof(f2690,plain,
! [X0] :
( hskp26
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2688,f17]) ).
fof(f2694,plain,
( ~ hskp6
| ~ hskp1
| c2_1(a546)
| c0_1(a537) ),
inference(backward_subsumption_resolution,[status(thm)],[f2197,f2655]) ).
fof(f2702,plain,
( ~ hskp4
| ~ hskp9
| ~ c0_1(a540)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2655,f1808]) ).
fof(f2703,plain,
( ~ hskp12
| ~ hskp9
| ~ c3_1(a564)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2655,f1807]) ).
fof(f2707,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2703,f55]) ).
fof(f2708,plain,
( hskp11
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1564,f2685]) ).
fof(f2728,plain,
( hskp19
| ~ hskp12
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1605,f2707]) ).
fof(f2729,plain,
( ~ hskp0
| ~ hskp3
| ~ hskp9
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2707,f2687]) ).
fof(f2730,plain,
( ~ hskp0
| ~ hskp9
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2729]) ).
fof(f2734,plain,
( ~ hskp6
| ~ hskp9
| ~ c3_1(a546)
| ~ hskp9
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2730,f1702]) ).
fof(f2736,plain,
( ~ hskp25
| ~ hskp9
| ~ c3_1(a594)
| ~ hskp9
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2730,f1696]) ).
fof(f2739,plain,
( ~ hskp6
| ~ c3_1(a546)
| ~ hskp9
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2734]) ).
fof(f2740,plain,
( ~ hskp6
| ~ hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2739,f30]) ).
fof(f2742,plain,
( ~ hskp25
| ~ c3_1(a594)
| ~ hskp9
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2736]) ).
fof(f2744,plain,
( ~ hskp6
| ~ hskp9
| c2_1(a546)
| c3_1(a549) ),
inference(backward_subsumption_resolution,[status(thm)],[f2051,f2740]) ).
fof(f2765,plain,
( ~ hskp4
| ~ hskp18
| hskp1
| ~ c0_1(a540)
| ~ hskp18
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2654,f1738]) ).
fof(f2766,plain,
( ~ hskp12
| ~ hskp18
| hskp1
| ~ hskp18
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2654,f1744]) ).
fof(f2770,plain,
( ~ hskp6
| ~ hskp18
| hskp0
| ~ hskp18
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2654,f1676]) ).
fof(f2787,plain,
( ~ hskp4
| hskp1
| ~ c0_1(a540)
| ~ hskp18
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2765]) ).
fof(f2788,plain,
( ~ hskp4
| ~ c0_1(a540)
| ~ hskp18
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2787,f2655]) ).
fof(f2789,plain,
( ~ hskp12
| hskp1
| ~ hskp18
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2766]) ).
fof(f2790,plain,
( ~ hskp12
| ~ hskp18
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2789,f2655]) ).
fof(f2795,plain,
( ~ hskp6
| hskp0
| ~ hskp18
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2770]) ).
fof(f2895,plain,
! [X0] :
( ~ hskp6
| hskp1
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f528,f31]) ).
fof(f2896,plain,
! [X0] :
( ~ hskp3
| ~ hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a546) ),
inference(resolution,[status(thm)],[f2895,f2655]) ).
fof(f2897,plain,
! [X0] :
( ~ hskp3
| ~ hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2896,f30]) ).
fof(f2919,plain,
( ~ hskp9
| ~ hskp3
| ~ hskp5
| ~ c2_1(a544)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2680,f2707]) ).
fof(f2920,plain,
( ~ hskp9
| ~ hskp5
| ~ c2_1(a544)
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2919]) ).
fof(f2929,plain,
( ~ hskp4
| hskp0
| ~ hskp4
| ~ hskp9
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2702,f1694]) ).
fof(f2946,plain,
( hskp0
| ~ hskp4
| ~ hskp9
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f2929]) ).
fof(f2947,plain,
( ~ hskp4
| ~ hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2946,f2730]) ).
fof(f3048,plain,
( ~ hskp25
| hskp21
| hskp29
| ~ hskp25
| ~ hskp9
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2742,f819]) ).
fof(f3071,plain,
( hskp21
| hskp29
| ~ hskp25
| ~ hskp9
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f3048]) ).
fof(f3072,plain,
( hskp21
| ~ hskp25
| ~ hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f3071,f1554]) ).
fof(f3075,plain,
( ~ hskp25
| ~ hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f3072,f2657]) ).
fof(f3076,plain,
( hskp5
| ~ hskp3
| ~ hskp9
| ~ hskp3 ),
inference(resolution,[status(thm)],[f3075,f2689]) ).
fof(f3089,plain,
( hskp5
| ~ hskp9
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f3076]) ).
fof(f3165,plain,
( ~ hskp4
| hskp0
| ~ hskp4
| ~ hskp18
| ~ hskp3 ),
inference(resolution,[status(thm)],[f2788,f1694]) ).
fof(f3183,plain,
( hskp0
| ~ hskp4
| ~ hskp18
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f3165]) ).
fof(f3395,plain,
( ~ hskp9
| ~ c2_1(a544)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f2920,f3089]) ).
fof(f3397,plain,
( ~ hskp5
| hskp4
| hskp25
| ~ hskp9
| ~ hskp3 ),
inference(resolution,[status(thm)],[f3395,f953]) ).
fof(f3409,plain,
( ~ hskp5
| hskp4
| ~ hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f3397,f3075]) ).
fof(f3417,plain,
( ~ hskp9
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f3089,f3418]) ).
fof(f3418,plain,
( ~ hskp5
| ~ hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f3409,f2947]) ).
fof(f3985,plain,
( ~ hskp21
| ~ hskp2
| ~ c0_1(a538)
| ~ hskp21
| ~ c2_1(a582) ),
inference(resolution,[status(thm)],[f2609,f91]) ).
fof(f4019,plain,
( ~ hskp2
| ~ c0_1(a538)
| ~ hskp21
| ~ c2_1(a582) ),
inference(duplicate_literals_removal,[status(thm)],[f3985]) ).
fof(f4020,plain,
( ~ hskp2
| ~ c0_1(a538)
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f4019,f90]) ).
fof(f4046,plain,
( ~ hskp4
| ~ hskp2
| hskp3
| ~ hskp2
| ~ hskp21 ),
inference(resolution,[status(thm)],[f4020,f2177]) ).
fof(f4072,plain,
( ~ hskp4
| hskp3
| ~ hskp2
| ~ hskp21 ),
inference(duplicate_literals_removal,[status(thm)],[f4046]) ).
fof(f4073,plain,
( ~ hskp4
| ~ hskp2
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f4072,f2657]) ).
fof(f4086,plain,
( ~ hskp1
| ~ hskp4
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f2247,f4073]) ).
fof(f4099,plain,
( ~ hskp0
| hskp12
| ~ c2_1(a536)
| ~ hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f4073,f1050]) ).
fof(f4113,plain,
( ~ hskp0
| hskp12
| ~ hskp4
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4099,f7]) ).
fof(f4124,plain,
( ~ hskp12
| ~ hskp9
| ~ c3_1(a564)
| ~ hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f4086,f1807]) ).
fof(f4135,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp4
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4124,f55]) ).
fof(f6502,plain,
! [X0] :
( ~ hskp10
| hskp6
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(a551) ),
inference(forward_subsumption_resolution,[status(thm)],[f876,f46]) ).
fof(f6521,plain,
( ~ hskp15
| ~ hskp10
| hskp6
| ~ c1_1(a567)
| ~ c0_1(a567)
| ~ c3_1(a551) ),
inference(resolution,[status(thm)],[f6502,f68]) ).
fof(f6532,plain,
( ~ hskp15
| ~ hskp10
| hskp6
| ~ c1_1(a567)
| ~ c0_1(a567) ),
inference(forward_subsumption_resolution,[status(thm)],[f6521,f47]) ).
fof(f6957,plain,
! [X0] :
( ~ hskp14
| hskp31
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a566) ),
inference(forward_subsumption_resolution,[status(thm)],[f929,f62]) ).
fof(f6986,plain,
! [X0] :
( ~ hskp3
| ~ hskp6
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp14
| hskp31
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a566) ),
inference(resolution,[status(thm)],[f6957,f2897]) ).
fof(f7008,plain,
! [X0] :
( ~ hskp3
| ~ hskp6
| ~ hskp14
| hskp31
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a566) ),
inference(duplicate_literals_removal,[status(thm)],[f6986]) ).
fof(f7009,plain,
! [X0] :
( ~ hskp3
| ~ hskp6
| ~ hskp14
| hskp31
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7008,f63]) ).
fof(f7223,plain,
( ~ hskp15
| ~ hskp10
| hskp6
| ~ c1_1(a567) ),
inference(forward_subsumption_resolution,[status(thm)],[f6532,f66]) ).
fof(f7286,plain,
! [X0] :
( ~ hskp3
| ~ hskp6
| hskp31
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7009,f2652]) ).
fof(f7563,plain,
! [X0] :
( ~ hskp19
| hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f1117,f82]) ).
fof(f7578,plain,
( ~ hskp26
| ~ hskp19
| hskp18
| ~ c2_1(a604)
| ~ c1_1(a604)
| c2_1(a576) ),
inference(resolution,[status(thm)],[f7563,f112]) ).
fof(f7585,plain,
( ~ hskp5
| ~ hskp19
| hskp18
| ~ c2_1(a544)
| ~ c1_1(a544)
| c2_1(a576) ),
inference(resolution,[status(thm)],[f7563,f28]) ).
fof(f7598,plain,
( ~ hskp26
| ~ hskp19
| hskp18
| ~ c2_1(a604)
| c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f7578,f110]) ).
fof(f7601,plain,
( ~ hskp5
| ~ hskp19
| hskp18
| ~ c2_1(a544)
| c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f7585,f27]) ).
fof(f7762,plain,
! [X0] :
( ~ hskp4
| hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f1120,f24]) ).
fof(f7777,plain,
( ~ hskp26
| ~ hskp4
| hskp18
| ~ c2_1(a604)
| ~ c1_1(a604)
| ~ c0_1(a540) ),
inference(resolution,[status(thm)],[f7762,f112]) ).
fof(f7798,plain,
( ~ hskp26
| ~ hskp4
| hskp18
| ~ c2_1(a604)
| ~ c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f7777,f110]) ).
fof(f7884,plain,
( ~ hskp26
| ~ hskp19
| hskp18
| c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f7598,f111]) ).
fof(f7887,plain,
( ~ hskp19
| ~ hskp3
| ~ hskp26
| ~ hskp19
| hskp18 ),
inference(resolution,[status(thm)],[f7884,f2653]) ).
fof(f7890,plain,
( ~ hskp3
| ~ hskp26
| ~ hskp19
| hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f7887]) ).
fof(f7894,plain,
( ~ hskp12
| ~ hskp3
| ~ hskp3
| ~ hskp26
| ~ hskp19 ),
inference(resolution,[status(thm)],[f7890,f2790]) ).
fof(f7897,plain,
( ~ hskp12
| ~ hskp3
| ~ hskp26
| ~ hskp19 ),
inference(duplicate_literals_removal,[status(thm)],[f7894]) ).
fof(f7898,plain,
( ~ hskp12
| ~ hskp3
| ~ hskp26 ),
inference(forward_subsumption_resolution,[status(thm)],[f7897,f2728]) ).
fof(f7900,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp3
| ~ hskp12
| ~ hskp3 ),
inference(resolution,[status(thm)],[f7898,f2690]) ).
fof(f7903,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp12
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f7900]) ).
fof(f8185,plain,
( ~ hskp31
| ~ c3_1(a563)
| ~ c0_1(a563)
| ~ hskp12
| ~ hskp3 ),
inference(resolution,[status(thm)],[f7903,f131]) ).
fof(f8259,plain,
( ~ hskp31
| ~ c3_1(a563)
| ~ hskp12
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f8185,f130]) ).
fof(f8300,plain,
( ~ hskp31
| ~ hskp12
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f8259,f132]) ).
fof(f8316,plain,
! [X0] :
( ~ hskp3
| ~ hskp6
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp12
| ~ hskp3 ),
inference(resolution,[status(thm)],[f8300,f7286]) ).
fof(f8331,plain,
! [X0] :
( ~ hskp6
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp12
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f8316]) ).
fof(f8332,plain,
! [X0] :
( ~ hskp6
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f8331,f2651]) ).
fof(f8502,plain,
( ~ hskp0
| ~ hskp6
| ~ c0_1(a536)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f8332,f7]) ).
fof(f8545,plain,
( ~ hskp0
| ~ hskp6
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f8502,f6]) ).
fof(f8558,plain,
( ~ hskp6
| ~ hskp18
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f2795,f8545]) ).
fof(f8590,plain,
( ~ hskp6
| ~ hskp18
| c2_1(a546) ),
inference(backward_subsumption_resolution,[status(thm)],[f2032,f8558]) ).
fof(f9236,plain,
( ~ hskp19
| ~ hskp3
| ~ hskp5
| ~ hskp19
| hskp18
| ~ c2_1(a544) ),
inference(resolution,[status(thm)],[f7601,f2653]) ).
fof(f9240,plain,
( ~ hskp3
| ~ hskp5
| ~ hskp19
| hskp18
| ~ c2_1(a544) ),
inference(duplicate_literals_removal,[status(thm)],[f9236]) ).
fof(f9245,plain,
( ~ hskp12
| ~ hskp3
| ~ hskp3
| ~ hskp5
| ~ hskp19
| ~ c2_1(a544) ),
inference(resolution,[status(thm)],[f9240,f2790]) ).
fof(f9249,plain,
( ~ hskp12
| ~ hskp3
| ~ hskp5
| ~ hskp19
| ~ c2_1(a544) ),
inference(duplicate_literals_removal,[status(thm)],[f9245]) ).
fof(f9250,plain,
( ~ hskp12
| ~ hskp3
| ~ hskp5
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f9249,f2728]) ).
fof(f9251,plain,
( ~ hskp3
| ~ hskp5
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f9250,f2680]) ).
fof(f9253,plain,
( ~ hskp5
| hskp4
| hskp25
| ~ hskp3
| ~ hskp5 ),
inference(resolution,[status(thm)],[f9251,f953]) ).
fof(f9283,plain,
( hskp4
| hskp25
| ~ hskp3
| ~ hskp5 ),
inference(duplicate_literals_removal,[status(thm)],[f9253]) ).
fof(f9284,plain,
( hskp4
| hskp25
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f9283,f2689]) ).
fof(f11130,plain,
! [X0] :
( ~ hskp1
| hskp3
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c0_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f1398,f10]) ).
fof(f11159,plain,
( ~ hskp11
| ~ hskp1
| hskp3
| ~ c3_1(a553)
| ~ c1_1(a553)
| ~ c0_1(a537) ),
inference(resolution,[status(thm)],[f11130,f52]) ).
fof(f11171,plain,
( ~ hskp11
| ~ hskp1
| hskp3
| ~ c3_1(a553)
| ~ c0_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f11159,f50]) ).
fof(f11267,plain,
( ~ hskp26
| ~ hskp4
| hskp18
| ~ c0_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f7798,f111]) ).
fof(f15342,plain,
( ~ hskp11
| ~ hskp1
| hskp3
| ~ c0_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f11171,f51]) ).
fof(f17666,plain,
! [X0] :
( ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f2496,f107]) ).
fof(f17704,plain,
( ~ hskp25
| ~ hskp25
| ~ c3_1(a594)
| ~ c2_1(a594)
| ~ c3_1(a594) ),
inference(resolution,[status(thm)],[f17666,f107]) ).
fof(f17720,plain,
( ~ hskp25
| ~ c2_1(a594)
| ~ c3_1(a594) ),
inference(duplicate_literals_removal,[status(thm)],[f17704]) ).
fof(f17721,plain,
( ~ hskp25
| ~ c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f17720,f106]) ).
fof(f17728,plain,
! [X0] :
( ~ hskp25
| hskp3
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1972,f17721]) ).
fof(f17739,plain,
( ~ hskp25
| hskp21
| hskp29 ),
inference(backward_subsumption_resolution,[status(thm)],[f819,f17721]) ).
fof(f17777,plain,
( ~ hskp3
| ~ hskp25
| hskp21 ),
inference(resolution,[status(thm)],[f17739,f1554]) ).
fof(f17780,plain,
( ~ hskp3
| ~ hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f17777,f2657]) ).
fof(f17781,plain,
( hskp4
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f9284,f17780]) ).
fof(f17794,plain,
( ~ hskp0
| hskp9
| ~ c2_1(a536)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f17780,f1202]) ).
fof(f17804,plain,
( ~ hskp0
| hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f17794,f7]) ).
fof(f17809,plain,
( hskp0
| ~ hskp18
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f3183,f17781]) ).
fof(f17863,plain,
( ~ hskp0
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f17804,f3417]) ).
fof(f17953,plain,
! [X0] :
( ~ hskp25
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f17728,f17780]) ).
fof(f18002,plain,
( ~ hskp6
| ~ hskp25
| ~ c3_1(a546)
| c2_1(a546) ),
inference(resolution,[status(thm)],[f17953,f32]) ).
fof(f18030,plain,
( ~ hskp6
| ~ hskp25
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f18002,f30]) ).
fof(f18045,plain,
( ~ hskp4
| ~ hskp18
| ~ c3_1(a540) ),
inference(backward_subsumption_resolution,[status(thm)],[f2033,f18049]) ).
fof(f18049,plain,
( ~ hskp18
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f17809,f17863]) ).
fof(f18061,plain,
( ~ hskp26
| ~ hskp4
| ~ c0_1(a540)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f18049,f11267]) ).
fof(f18071,plain,
( ~ hskp4
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f18045,f22]) ).
fof(f18077,plain,
( ~ hskp26
| ~ c0_1(a540)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f18061,f17781]) ).
fof(f18094,plain,
( ~ hskp13
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f2377,f18071]) ).
fof(f18120,plain,
( hskp24
| hskp3
| ~ hskp13 ),
inference(resolution,[status(thm)],[f18094,f208]) ).
fof(f19020,plain,
( ~ hskp4
| hskp0
| ~ hskp26
| ~ hskp3 ),
inference(resolution,[status(thm)],[f18077,f1694]) ).
fof(f19032,plain,
( ~ hskp4
| ~ hskp26
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f19020,f17863]) ).
fof(f19040,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f2690,f19041]) ).
fof(f19041,plain,
( ~ hskp26
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f19032,f17781]) ).
fof(f21434,plain,
! [X0] :
( ~ hskp6
| ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2499,f31]) ).
fof(f21481,plain,
( ~ hskp6
| ~ hskp6
| ~ hskp25
| ~ c3_1(a546)
| ~ c2_1(a546)
| ~ c3_1(a546) ),
inference(resolution,[status(thm)],[f21434,f31]) ).
fof(f21496,plain,
( ~ hskp6
| ~ hskp25
| ~ c2_1(a546)
| ~ c3_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f21481]) ).
fof(f21497,plain,
( ~ hskp6
| ~ hskp25
| ~ c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f21496,f30]) ).
fof(f21499,plain,
( ~ hskp6
| ~ hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f21497,f18030]) ).
fof(f21504,plain,
( ~ hskp0
| hskp9
| ~ c2_1(a536)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f21499,f1202]) ).
fof(f21509,plain,
( ~ hskp16
| hskp4
| ~ c1_1(a570)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f21499,f952]) ).
fof(f21512,plain,
( ~ hskp0
| hskp9
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f21504,f7]) ).
fof(f21513,plain,
( ~ hskp16
| hskp4
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f21509,f70]) ).
fof(f21516,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp2
| ~ hskp16
| ~ hskp6 ),
inference(resolution,[status(thm)],[f21513,f4135]) ).
fof(f21727,plain,
( ~ hskp2
| hskp3
| ~ hskp12
| ~ hskp9
| ~ hskp2
| ~ hskp6 ),
inference(resolution,[status(thm)],[f21516,f704]) ).
fof(f21736,plain,
( hskp3
| ~ hskp12
| ~ hskp9
| ~ hskp2
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f21727]) ).
fof(f21737,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp2
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f21736,f3417]) ).
fof(f21762,plain,
( ~ hskp0
| ~ hskp4
| ~ hskp2
| ~ hskp9
| ~ hskp2
| ~ hskp6 ),
inference(resolution,[status(thm)],[f21737,f4113]) ).
fof(f21780,plain,
( ~ hskp0
| ~ hskp4
| ~ hskp9
| ~ hskp2
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f21762]) ).
fof(f21781,plain,
( ~ hskp0
| ~ hskp4
| ~ hskp2
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f21780,f21512]) ).
fof(f21924,plain,
! [X0] :
( ~ hskp6
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2603,f30]) ).
fof(f21973,plain,
( ~ hskp6
| ~ hskp6
| ~ c3_1(a546)
| ~ c2_1(a546)
| ~ c2_1(a546) ),
inference(resolution,[status(thm)],[f21924,f31]) ).
fof(f21982,plain,
( ~ hskp6
| ~ c3_1(a546)
| ~ c2_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f21973]) ).
fof(f21983,plain,
( ~ hskp6
| ~ c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f21982,f30]) ).
fof(f21984,plain,
( ~ hskp6
| ~ hskp9
| c3_1(a549) ),
inference(backward_subsumption_resolution,[status(thm)],[f2744,f21983]) ).
fof(f21986,plain,
( ~ hskp6
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f8590,f21983]) ).
fof(f21989,plain,
( ~ hskp6
| ~ hskp1
| c0_1(a537) ),
inference(backward_subsumption_resolution,[status(thm)],[f2694,f21983]) ).
fof(f21992,plain,
! [X0] :
( ~ hskp6
| hskp2
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1970,f21983]) ).
fof(f21994,plain,
( ~ hskp12
| ~ hskp6
| hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f1827,f21983]) ).
fof(f21998,plain,
( ~ hskp6
| hskp0 ),
inference(backward_subsumption_resolution,[status(thm)],[f1675,f21983]) ).
fof(f22081,plain,
( hskp24
| hskp3
| ~ hskp6 ),
inference(resolution,[status(thm)],[f21986,f208]) ).
fof(f22083,plain,
( hskp9
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f21512,f21998]) ).
fof(f22084,plain,
( ~ hskp4
| ~ hskp2
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f21781,f21998]) ).
fof(f22086,plain,
( ~ hskp3
| ~ hskp6 ),
inference(resolution,[status(thm)],[f21998,f17863]) ).
fof(f22104,plain,
( ~ hskp11
| ~ hskp1
| ~ c0_1(a537)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f22086,f15342]) ).
fof(f22221,plain,
( hskp24
| hskp13 ),
inference(backward_subsumption_resolution,[status(thm)],[f205,f22222]) ).
fof(f22222,plain,
( hskp24
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f22081,f22086]) ).
fof(f22223,plain,
( hskp24
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f18120,f22221]) ).
fof(f22227,plain,
( hskp6
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1026,f22223]) ).
fof(f22234,plain,
( ~ hskp16
| ~ hskp6
| ~ hskp2
| ~ hskp6 ),
inference(resolution,[status(thm)],[f22084,f21513]) ).
fof(f22242,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f22234]) ).
fof(f22438,plain,
( ~ hskp2
| hskp3
| ~ hskp2
| ~ hskp6 ),
inference(resolution,[status(thm)],[f22242,f704]) ).
fof(f22448,plain,
( hskp3
| ~ hskp2
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f22438]) ).
fof(f22449,plain,
( hskp3
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f22448,f22227]) ).
fof(f22450,plain,
( ~ hskp6
| ~ hskp2 ),
inference(resolution,[status(thm)],[f22449,f22086]) ).
fof(f22451,plain,
( ~ hskp6
| hskp5
| ~ c3_1(a546) ),
inference(backward_subsumption_resolution,[status(thm)],[f339,f22450]) ).
fof(f22452,plain,
! [X0] :
( ~ hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f21992,f22450]) ).
fof(f22466,plain,
( ~ hskp6
| hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f22451,f30]) ).
fof(f22477,plain,
( ~ hskp6
| c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f21984,f22083]) ).
fof(f22504,plain,
( ~ hskp5
| ~ hskp6
| ~ c2_1(a544)
| ~ c0_1(a544) ),
inference(resolution,[status(thm)],[f22452,f27]) ).
fof(f22567,plain,
( ~ hskp5
| ~ hskp6
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f22504,f26]) ).
fof(f23045,plain,
( ~ hskp6
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f22567,f22466]) ).
fof(f23052,plain,
! [X0] :
( ~ hskp5
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f23045,f1463]) ).
fof(f23116,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f23052,f22466]) ).
fof(f23802,plain,
( ~ hskp11
| ~ hskp1
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f22104,f21989]) ).
fof(f23807,plain,
( ~ hskp12
| ~ hskp6
| ~ hskp11
| ~ hskp6 ),
inference(resolution,[status(thm)],[f23802,f21994]) ).
fof(f23821,plain,
( ~ hskp12
| ~ hskp11
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f23807]) ).
fof(f26932,plain,
( ~ hskp11
| ~ c3_1(a553)
| ~ c0_1(a553)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f19040,f50]) ).
fof(f27008,plain,
( ~ hskp11
| ~ c0_1(a553)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f26932,f51]) ).
fof(f27096,plain,
( ~ c0_1(a553)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f27008,f2708]) ).
fof(f27098,plain,
( ~ hskp11
| hskp10
| hskp8
| ~ hskp3 ),
inference(resolution,[status(thm)],[f27096,f437]) ).
fof(f27110,plain,
( hskp10
| hskp8
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f27098,f2708]) ).
fof(f27215,plain,
( ~ hskp29
| ~ c2_1(a552)
| ~ c0_1(a552)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f23116,f124]) ).
fof(f27217,plain,
( ~ hskp21
| ~ c2_1(a582)
| ~ c0_1(a582)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f23116,f91]) ).
fof(f27256,plain,
( ~ hskp29
| ~ c2_1(a552)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f27215,f122]) ).
fof(f27257,plain,
( ~ hskp21
| ~ c0_1(a582)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f27217,f90]) ).
fof(f27280,plain,
( ~ hskp29
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f27256,f123]) ).
fof(f27287,plain,
( ~ hskp9
| hskp11
| ~ c3_1(a549)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f27280,f473]) ).
fof(f27292,plain,
( ~ hskp9
| hskp11
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f27287,f22477]) ).
fof(f27309,plain,
( ~ hskp12
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f23821,f27310]) ).
fof(f27310,plain,
( hskp11
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f27292,f22083]) ).
fof(f27845,plain,
! [X0] :
( ~ hskp21
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ hskp21
| ~ hskp6 ),
inference(resolution,[status(thm)],[f27257,f2563]) ).
fof(f27859,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ hskp21
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f27845]) ).
fof(f27860,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp21
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f27859,f23116]) ).
fof(f31879,plain,
( ~ hskp21
| ~ c2_1(a582)
| ~ hskp21
| ~ hskp6 ),
inference(resolution,[status(thm)],[f27860,f91]) ).
fof(f31917,plain,
( ~ c2_1(a582)
| ~ hskp21
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f31879]) ).
fof(f31918,plain,
( ~ hskp21
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f31917,f90]) ).
fof(f31945,plain,
( ~ hskp0
| hskp12
| ~ c2_1(a536)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f31918,f1050]) ).
fof(f31951,plain,
( ~ hskp0
| hskp12
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f31945,f7]) ).
fof(f32286,plain,
~ hskp6,
inference(backward_subsumption_resolution,[status(thm)],[f21998,f32287]) ).
fof(f32287,plain,
( ~ hskp0
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f31951,f27309]) ).
fof(f32303,plain,
hskp3,
inference(backward_subsumption_resolution,[status(thm)],[f22227,f32286]) ).
fof(f32321,plain,
( ~ hskp15
| ~ hskp10
| ~ c1_1(a567) ),
inference(backward_subsumption_resolution,[status(thm)],[f7223,f32286]) ).
fof(f32338,plain,
( ~ hskp15
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f32321,f67]) ).
fof(f32339,plain,
( hskp10
| hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f27110,f32303]) ).
fof(f32363,plain,
~ hskp0,
inference(backward_subsumption_resolution,[status(thm)],[f17863,f32303]) ).
fof(f32365,plain,
hskp4,
inference(backward_subsumption_resolution,[status(thm)],[f17781,f32303]) ).
fof(f32373,plain,
~ hskp9,
inference(backward_subsumption_resolution,[status(thm)],[f3417,f32303]) ).
fof(f32622,plain,
( ~ hskp4
| hskp15 ),
inference(backward_subsumption_resolution,[status(thm)],[f1695,f32363]) ).
fof(f32748,plain,
( ~ hskp8
| hskp10
| ~ c2_1(a548) ),
inference(backward_subsumption_resolution,[status(thm)],[f549,f32373]) ).
fof(f32764,plain,
( ~ hskp8
| hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f32748,f39]) ).
fof(f32962,plain,
~ hskp10,
inference(backward_subsumption_resolution,[status(thm)],[f32338,f32963]) ).
fof(f32963,plain,
hskp15,
inference(forward_subsumption_resolution,[status(thm)],[f32622,f32365]) ).
fof(f32965,plain,
hskp8,
inference(backward_subsumption_resolution,[status(thm)],[f32339,f32962]) ).
fof(f33044,plain,
~ hskp8,
inference(forward_subsumption_resolution,[status(thm)],[f32764,f32962]) ).
fof(f33045,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f32965,f33044]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN510+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 11:04:06 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 33.00/4.56 % Refutation found
% 33.00/4.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 33.00/4.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 33.00/4.57 % Elapsed time: 4.275105 seconds
% 33.00/4.57 % CPU time: 33.641095 seconds
% 33.00/4.57 % Total memory used: 84.569 MB
% 33.00/4.57 % Net memory used: 79.574 MB
%------------------------------------------------------------------------------