%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN445+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Sun Sep 27 09:38:04 AM UTC 2026
% Result : Theorem 198.71s 31.68s
% Output : CNFRefutation 198.71s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
~ ( ( hskp25
| hskp12
| hskp20 )
& ( hskp16
| hskp26 )
& ( hskp12
| hskp11
| hskp26 )
& ( hskp23
| hskp15
| hskp6 )
& ( hskp24
| hskp5
| hskp17 )
& ( hskp10
| hskp1
| hskp7 )
& ( hskp10
| hskp27
| hskp29 )
& ( hskp28
| ! [X88] :
( ndr1_0
=> ( ~ c3_1(X88)
| ~ c2_1(X88)
| ~ c1_1(X88) ) ) )
& ( hskp21
| hskp17
| ! [X87] :
( ndr1_0
=> ( ~ c3_1(X87)
| ~ c1_1(X87)
| ~ c0_1(X87) ) ) )
& ( hskp23
| hskp26
| ! [X86] :
( ndr1_0
=> ( ~ c2_1(X86)
| ~ c1_1(X86)
| ~ c0_1(X86) ) ) )
& ( hskp8
| hskp6
| ! [X85] :
( ndr1_0
=> ( ~ c2_1(X85)
| ~ c1_1(X85)
| ~ c0_1(X85) ) ) )
& ( hskp25
| hskp15
| ! [X84] :
( ndr1_0
=> ( ~ c2_1(X84)
| ~ c1_1(X84)
| c3_1(X84) ) ) )
& ( hskp4
| ! [X83] :
( ndr1_0
=> ( ~ c3_1(X83)
| ~ c2_1(X83)
| ~ c1_1(X83) ) )
| ! [X82] :
( ndr1_0
=> ( ~ c2_1(X82)
| ~ c1_1(X82)
| c3_1(X82) ) ) )
& ( hskp11
| ! [X81] :
( ndr1_0
=> ( ~ c3_1(X81)
| ~ c2_1(X81)
| ~ c0_1(X81) ) )
| ! [X80] :
( ndr1_0
=> ( ~ c2_1(X80)
| ~ c0_1(X80)
| c3_1(X80) ) ) )
& ( hskp24
| hskp23
| ! [X79] :
( ndr1_0
=> ( ~ c1_1(X79)
| ~ c0_1(X79)
| c3_1(X79) ) ) )
& ( hskp4
| hskp17
| ! [X78] :
( ndr1_0
=> ( ~ c1_1(X78)
| ~ c0_1(X78)
| c3_1(X78) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( ~ c3_1(X77)
| ~ c2_1(X77)
| ~ c0_1(X77) ) )
| ! [X76] :
( ndr1_0
=> ( ~ c3_1(X76)
| ~ c1_1(X76)
| c2_1(X76) ) ) )
& ( hskp22
| ! [X75] :
( ndr1_0
=> ( ~ c1_1(X75)
| c3_1(X75)
| c2_1(X75) ) ) )
& ( hskp17
| ! [X74] :
( ndr1_0
=> ( ~ c3_1(X74)
| ~ c1_1(X74)
| ~ c0_1(X74) ) )
| ! [X73] :
( ndr1_0
=> ( ~ c1_1(X73)
| c3_1(X73)
| c2_1(X73) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( ~ c3_1(X72)
| ~ c1_1(X72)
| ~ c0_1(X72) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c3_1(X71)
| ~ c1_1(X71)
| c2_1(X71) ) )
| ! [X70] :
( ndr1_0
=> ( ~ c1_1(X70)
| c3_1(X70)
| c2_1(X70) ) ) )
& ( hskp21
| ! [X69] :
( ndr1_0
=> ( ~ c0_1(X69)
| c3_1(X69)
| c2_1(X69) ) ) )
& ( hskp3
| hskp27
| ! [X68] :
( ndr1_0
=> ( ~ c3_1(X68)
| ~ c2_1(X68)
| c1_1(X68) ) ) )
& ( hskp20
| hskp11
| ! [X67] :
( ndr1_0
=> ( ~ c2_1(X67)
| ~ c0_1(X67)
| c1_1(X67) ) ) )
& ( hskp12
| hskp19
| ! [X66] :
( ndr1_0
=> ( ~ c2_1(X66)
| ~ c0_1(X66)
| c1_1(X66) ) ) )
& ( hskp18
| hskp17
| ! [X65] :
( ndr1_0
=> ( ~ c2_1(X65)
| ~ c0_1(X65)
| c1_1(X65) ) ) )
& ( hskp4
| ! [X64] :
( ndr1_0
=> ( ~ c3_1(X64)
| ~ c0_1(X64)
| c1_1(X64) ) )
| ! [X63] :
( ndr1_0
=> ( ~ c2_1(X63)
| ~ c0_1(X63)
| c1_1(X63) ) ) )
& ( hskp16
| hskp11
| ! [X62] :
( ndr1_0
=> ( ~ c2_1(X62)
| c3_1(X62)
| c1_1(X62) ) ) )
& ( hskp5
| ! [X61] :
( ndr1_0
=> ( ~ c1_1(X61)
| c3_1(X61)
| c2_1(X61) ) )
| ! [X60] :
( ndr1_0
=> ( ~ c2_1(X60)
| c3_1(X60)
| c1_1(X60) ) ) )
& ( hskp17
| ! [X59] :
( ndr1_0
=> ( ~ c1_1(X59)
| c3_1(X59)
| c2_1(X59) ) )
| ! [X58] :
( ndr1_0
=> ( ~ c0_1(X58)
| c3_1(X58)
| c1_1(X58) ) ) )
& ( hskp13
| ! [X57] :
( ndr1_0
=> ( ~ c2_1(X57)
| c3_1(X57)
| c1_1(X57) ) )
| ! [X56] :
( ndr1_0
=> ( ~ c0_1(X56)
| c3_1(X56)
| c1_1(X56) ) ) )
& ( hskp16
| ! [X55] :
( ndr1_0
=> ( ~ c3_1(X55)
| c2_1(X55)
| c1_1(X55) ) ) )
& ( hskp15
| hskp6
| ! [X54] :
( ndr1_0
=> ( ~ c3_1(X54)
| c2_1(X54)
| c1_1(X54) ) ) )
& ( hskp7
| ! [X53] :
( ndr1_0
=> ( ~ c1_1(X53)
| ~ c0_1(X53)
| c2_1(X53) ) )
| ! [X52] :
( ndr1_0
=> ( ~ c3_1(X52)
| c2_1(X52)
| c1_1(X52) ) ) )
& ( hskp14
| ! [X51] :
( ndr1_0
=> ( ~ c3_1(X51)
| ~ c1_1(X51)
| c2_1(X51) ) )
| ! [X50] :
( ndr1_0
=> ( ~ c0_1(X50)
| c2_1(X50)
| c1_1(X50) ) ) )
& ( hskp0
| hskp14
| ! [X49] :
( ndr1_0
=> ( ~ c3_1(X49)
| ~ c2_1(X49)
| c0_1(X49) ) ) )
& ( hskp3
| ! [X48] :
( ndr1_0
=> ( ~ c1_1(X48)
| c3_1(X48)
| c2_1(X48) ) )
| ! [X47] :
( ndr1_0
=> ( ~ c3_1(X47)
| ~ c2_1(X47)
| c0_1(X47) ) ) )
& ( hskp13
| ! [X46] :
( ndr1_0
=> ( ~ c1_1(X46)
| ~ c0_1(X46)
| c3_1(X46) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c2_1(X45)
| ~ c1_1(X45)
| c0_1(X45) ) ) )
& ( hskp12
| ! [X44] :
( ndr1_0
=> ( ~ c0_1(X44)
| c3_1(X44)
| c2_1(X44) ) )
| ! [X43] :
( ndr1_0
=> ( ~ c2_1(X43)
| ~ c1_1(X43)
| c0_1(X43) ) ) )
& ( hskp8
| ! [X42] :
( ndr1_0
=> ( ~ c2_1(X42)
| ~ c1_1(X42)
| c3_1(X42) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c2_1(X41)
| c3_1(X41)
| c0_1(X41) ) ) )
& ( hskp12
| ! [X40] :
( ndr1_0
=> ( ~ c3_1(X40)
| ~ c1_1(X40)
| c2_1(X40) ) )
| ! [X39] :
( ndr1_0
=> ( ~ c1_1(X39)
| c3_1(X39)
| c0_1(X39) ) ) )
& ( hskp11
| hskp10
| ! [X38] :
( ndr1_0
=> ( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38) ) ) )
& ( hskp9
| ! [X37] :
( ndr1_0
=> ( ~ c2_1(X37)
| ~ c0_1(X37)
| c3_1(X37) ) )
| ! [X36] :
( ndr1_0
=> ( ~ c3_1(X36)
| c2_1(X36)
| c0_1(X36) ) ) )
& ( hskp5
| hskp8
| ! [X35] :
( ndr1_0
=> ( ~ c1_1(X35)
| c2_1(X35)
| c0_1(X35) ) ) )
& ( hskp4
| hskp7
| ! [X34] :
( ndr1_0
=> ( ~ c1_1(X34)
| c2_1(X34)
| c0_1(X34) ) ) )
& ( hskp6
| ! [X33] :
( ndr1_0
=> ( ~ c1_1(X33)
| ~ c0_1(X33)
| c3_1(X33) ) )
| ! [X32] :
( ndr1_0
=> ( ~ c1_1(X32)
| c2_1(X32)
| c0_1(X32) ) ) )
& ( hskp5
| ! [X31] :
( ndr1_0
=> ( ~ c3_1(X31)
| ~ c0_1(X31)
| c1_1(X31) ) )
| ! [X30] :
( ndr1_0
=> ( ~ c1_1(X30)
| c2_1(X30)
| c0_1(X30) ) ) )
& ( hskp4
| ! [X29] :
( ndr1_0
=> ( ~ c2_1(X29)
| ~ c0_1(X29)
| c1_1(X29) ) )
| ! [X28] :
( ndr1_0
=> ( ~ c1_1(X28)
| c2_1(X28)
| c0_1(X28) ) ) )
& ( hskp3
| ! [X27] :
( ndr1_0
=> ( ~ c1_1(X27)
| c3_1(X27)
| c0_1(X27) ) )
| ! [X26] :
( ndr1_0
=> ( ~ c1_1(X26)
| c2_1(X26)
| c0_1(X26) ) ) )
& ( ! [X25] :
( ndr1_0
=> ( ~ c3_1(X25)
| ~ c1_1(X25)
| c0_1(X25) ) )
| ! [X24] :
( ndr1_0
=> ( ~ c1_1(X24)
| c3_1(X24)
| c0_1(X24) ) )
| ! [X23] :
( ndr1_0
=> ( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) ) ) )
& ( ! [X22] :
( ndr1_0
=> ( ~ c3_1(X22)
| ~ c2_1(X22)
| c1_1(X22) ) )
| ! [X21] :
( ndr1_0
=> ( ~ c1_1(X21)
| c2_1(X21)
| c0_1(X21) ) )
| ! [X20] :
( ndr1_0
=> ( c3_1(X20)
| c2_1(X20)
| c0_1(X20) ) ) )
& ( hskp0
| hskp2
| ! [X19] :
( ndr1_0
=> ( ~ c3_1(X19)
| c1_1(X19)
| c0_1(X19) ) ) )
& ( hskp0
| ! [X18] :
( ndr1_0
=> ( ~ c3_1(X18)
| ~ c1_1(X18)
| c2_1(X18) ) )
| ! [X17] :
( ndr1_0
=> ( ~ c3_1(X17)
| c1_1(X17)
| c0_1(X17) ) ) )
& ( hskp1
| ! [X16] :
( ndr1_0
=> ( ~ c3_1(X16)
| ~ c2_1(X16)
| c1_1(X16) ) )
| ! [X15] :
( ndr1_0
=> ( ~ c2_1(X15)
| c1_1(X15)
| c0_1(X15) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( ~ c2_1(X14)
| ~ c1_1(X14)
| c3_1(X14) ) )
| ! [X13] :
( ndr1_0
=> ( ~ c1_1(X13)
| c2_1(X13)
| c0_1(X13) ) )
| ! [X12] :
( ndr1_0
=> ( ~ c2_1(X12)
| c1_1(X12)
| c0_1(X12) ) ) )
& ( ! [X11] :
( ndr1_0
=> ( ~ c2_1(X11)
| ~ c0_1(X11)
| c3_1(X11) ) )
| ! [X10] :
( ndr1_0
=> ( ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( c3_1(X9)
| c1_1(X9)
| c0_1(X9) ) ) )
& ( ! [X8] :
( ndr1_0
=> ( ~ c3_1(X8)
| ~ c2_1(X8)
| c0_1(X8) ) )
| ! [X7] :
( ndr1_0
=> ( c3_1(X7)
| c2_1(X7)
| c0_1(X7) ) )
| ! [X6] :
( ndr1_0
=> ( c3_1(X6)
| c1_1(X6)
| c0_1(X6) ) ) )
& ( hskp0
| ! [X5] :
( ndr1_0
=> ( ~ c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) ) )
| ! [X4] :
( ndr1_0
=> ( c2_1(X4)
| c1_1(X4)
| c0_1(X4) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( ~ c3_1(X3)
| ~ c1_1(X3)
| ~ c0_1(X3) ) )
| ! [X2] :
( ndr1_0
=> ( ~ c2_1(X2)
| ~ c0_1(X2)
| c1_1(X2) ) )
| ! [X1] :
( ndr1_0
=> ( c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ) )
& ( ! [Z] :
( ndr1_0
=> ( ~ c3_1(Z)
| ~ c1_1(Z)
| c2_1(Z) ) )
| ! [Y] :
( ndr1_0
=> ( c3_1(Y)
| c2_1(Y)
| c1_1(Y) ) )
| ! [X] :
( ndr1_0
=> ( c2_1(X)
| c1_1(X)
| c0_1(X) ) ) )
& ( ! [W] :
( ndr1_0
=> ( ~ c2_1(W)
| ~ c1_1(W)
| c0_1(W) ) )
| ! [V] :
( ndr1_0
=> ( c3_1(V)
| c2_1(V)
| c0_1(V) ) )
| ! [U] :
( ndr1_0
=> ( c2_1(U)
| c1_1(U)
| c0_1(U) ) ) )
& ( ( c2_1(a354)
& c1_1(a354)
& c0_1(a354)
& ndr1_0 )
| ~ hskp29 )
& ( ( c3_1(a353)
& c2_1(a353)
& c1_1(a353)
& ndr1_0 )
| ~ hskp28 )
& ( ( c3_1(a334)
& c2_1(a334)
& c0_1(a334)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a349)
& ~ c2_1(a349)
& c0_1(a349)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c3_1(a346)
& ~ c1_1(a346)
& ~ c0_1(a346)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c2_1(a342)
& ~ c1_1(a342)
& c3_1(a342)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c0_1(a341)
& c3_1(a341)
& c2_1(a341)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c3_1(a338)
& ~ c2_1(a338)
& ~ c1_1(a338)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c1_1(a336)
& ~ c0_1(a336)
& c3_1(a336)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c3_1(a333)
& ~ c2_1(a333)
& c1_1(a333)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c3_1(a330)
& c2_1(a330)
& c1_1(a330)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c3_1(a329)
& ~ c0_1(a329)
& c2_1(a329)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c3_1(a323)
& c2_1(a323)
& c0_1(a323)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c1_1(a321)
& c3_1(a321)
& c2_1(a321)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c2_1(a320)
& ~ c0_1(a320)
& c1_1(a320)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c0_1(a315)
& c2_1(a315)
& c1_1(a315)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c1_1(a313)
& c3_1(a313)
& c0_1(a313)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c2_1(a310)
& ~ c0_1(a310)
& c3_1(a310)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c2_1(a309)
& c3_1(a309)
& c1_1(a309)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c0_1(a308)
& c3_1(a308)
& c1_1(a308)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c3_1(a307)
& ~ c1_1(a307)
& c0_1(a307)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c1_1(a305)
& ~ c0_1(a305)
& c2_1(a305)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c2_1(a303)
& c1_1(a303)
& c0_1(a303)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c2_1(a302)
& ~ c1_1(a302)
& c0_1(a302)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a301)
& ~ c1_1(a301)
& c2_1(a301)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c2_1(a300)
& ~ c1_1(a300)
& ~ c0_1(a300)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c2_1(a299)
& c3_1(a299)
& c0_1(a299)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c3_1(a297)
& ~ c0_1(a297)
& c1_1(a297)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c1_1(a295)
& c2_1(a295)
& c0_1(a295)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c3_1(a294)
& ~ c2_1(a294)
& ~ c0_1(a294)
& ndr1_0 )
| ~ hskp0 ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( hskp25
| hskp12
| hskp20 )
& ( hskp16
| hskp26 )
& ( hskp12
| hskp11
| hskp26 )
& ( hskp23
| hskp15
| hskp6 )
& ( hskp24
| hskp5
| hskp17 )
& ( hskp10
| hskp1
| hskp7 )
& ( hskp10
| hskp27
| hskp29 )
& ( hskp28
| ! [X88] :
( ndr1_0
=> ( ~ c3_1(X88)
| ~ c2_1(X88)
| ~ c1_1(X88) ) ) )
& ( hskp21
| hskp17
| ! [X87] :
( ndr1_0
=> ( ~ c3_1(X87)
| ~ c1_1(X87)
| ~ c0_1(X87) ) ) )
& ( hskp23
| hskp26
| ! [X86] :
( ndr1_0
=> ( ~ c2_1(X86)
| ~ c1_1(X86)
| ~ c0_1(X86) ) ) )
& ( hskp8
| hskp6
| ! [X85] :
( ndr1_0
=> ( ~ c2_1(X85)
| ~ c1_1(X85)
| ~ c0_1(X85) ) ) )
& ( hskp25
| hskp15
| ! [X84] :
( ndr1_0
=> ( ~ c2_1(X84)
| ~ c1_1(X84)
| c3_1(X84) ) ) )
& ( hskp4
| ! [X83] :
( ndr1_0
=> ( ~ c3_1(X83)
| ~ c2_1(X83)
| ~ c1_1(X83) ) )
| ! [X82] :
( ndr1_0
=> ( ~ c2_1(X82)
| ~ c1_1(X82)
| c3_1(X82) ) ) )
& ( hskp11
| ! [X81] :
( ndr1_0
=> ( ~ c3_1(X81)
| ~ c2_1(X81)
| ~ c0_1(X81) ) )
| ! [X80] :
( ndr1_0
=> ( ~ c2_1(X80)
| ~ c0_1(X80)
| c3_1(X80) ) ) )
& ( hskp24
| hskp23
| ! [X79] :
( ndr1_0
=> ( ~ c1_1(X79)
| ~ c0_1(X79)
| c3_1(X79) ) ) )
& ( hskp4
| hskp17
| ! [X78] :
( ndr1_0
=> ( ~ c1_1(X78)
| ~ c0_1(X78)
| c3_1(X78) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( ~ c3_1(X77)
| ~ c2_1(X77)
| ~ c0_1(X77) ) )
| ! [X76] :
( ndr1_0
=> ( ~ c3_1(X76)
| ~ c1_1(X76)
| c2_1(X76) ) ) )
& ( hskp22
| ! [X75] :
( ndr1_0
=> ( ~ c1_1(X75)
| c3_1(X75)
| c2_1(X75) ) ) )
& ( hskp17
| ! [X74] :
( ndr1_0
=> ( ~ c3_1(X74)
| ~ c1_1(X74)
| ~ c0_1(X74) ) )
| ! [X73] :
( ndr1_0
=> ( ~ c1_1(X73)
| c3_1(X73)
| c2_1(X73) ) ) )
& ( ! [X72] :
( ndr1_0
=> ( ~ c3_1(X72)
| ~ c1_1(X72)
| ~ c0_1(X72) ) )
| ! [X71] :
( ndr1_0
=> ( ~ c3_1(X71)
| ~ c1_1(X71)
| c2_1(X71) ) )
| ! [X70] :
( ndr1_0
=> ( ~ c1_1(X70)
| c3_1(X70)
| c2_1(X70) ) ) )
& ( hskp21
| ! [X69] :
( ndr1_0
=> ( ~ c0_1(X69)
| c3_1(X69)
| c2_1(X69) ) ) )
& ( hskp3
| hskp27
| ! [X68] :
( ndr1_0
=> ( ~ c3_1(X68)
| ~ c2_1(X68)
| c1_1(X68) ) ) )
& ( hskp20
| hskp11
| ! [X67] :
( ndr1_0
=> ( ~ c2_1(X67)
| ~ c0_1(X67)
| c1_1(X67) ) ) )
& ( hskp12
| hskp19
| ! [X66] :
( ndr1_0
=> ( ~ c2_1(X66)
| ~ c0_1(X66)
| c1_1(X66) ) ) )
& ( hskp18
| hskp17
| ! [X65] :
( ndr1_0
=> ( ~ c2_1(X65)
| ~ c0_1(X65)
| c1_1(X65) ) ) )
& ( hskp4
| ! [X64] :
( ndr1_0
=> ( ~ c3_1(X64)
| ~ c0_1(X64)
| c1_1(X64) ) )
| ! [X63] :
( ndr1_0
=> ( ~ c2_1(X63)
| ~ c0_1(X63)
| c1_1(X63) ) ) )
& ( hskp16
| hskp11
| ! [X62] :
( ndr1_0
=> ( ~ c2_1(X62)
| c3_1(X62)
| c1_1(X62) ) ) )
& ( hskp5
| ! [X61] :
( ndr1_0
=> ( ~ c1_1(X61)
| c3_1(X61)
| c2_1(X61) ) )
| ! [X60] :
( ndr1_0
=> ( ~ c2_1(X60)
| c3_1(X60)
| c1_1(X60) ) ) )
& ( hskp17
| ! [X59] :
( ndr1_0
=> ( ~ c1_1(X59)
| c3_1(X59)
| c2_1(X59) ) )
| ! [X58] :
( ndr1_0
=> ( ~ c0_1(X58)
| c3_1(X58)
| c1_1(X58) ) ) )
& ( hskp13
| ! [X57] :
( ndr1_0
=> ( ~ c2_1(X57)
| c3_1(X57)
| c1_1(X57) ) )
| ! [X56] :
( ndr1_0
=> ( ~ c0_1(X56)
| c3_1(X56)
| c1_1(X56) ) ) )
& ( hskp16
| ! [X55] :
( ndr1_0
=> ( ~ c3_1(X55)
| c2_1(X55)
| c1_1(X55) ) ) )
& ( hskp15
| hskp6
| ! [X54] :
( ndr1_0
=> ( ~ c3_1(X54)
| c2_1(X54)
| c1_1(X54) ) ) )
& ( hskp7
| ! [X53] :
( ndr1_0
=> ( ~ c1_1(X53)
| ~ c0_1(X53)
| c2_1(X53) ) )
| ! [X52] :
( ndr1_0
=> ( ~ c3_1(X52)
| c2_1(X52)
| c1_1(X52) ) ) )
& ( hskp14
| ! [X51] :
( ndr1_0
=> ( ~ c3_1(X51)
| ~ c1_1(X51)
| c2_1(X51) ) )
| ! [X50] :
( ndr1_0
=> ( ~ c0_1(X50)
| c2_1(X50)
| c1_1(X50) ) ) )
& ( hskp0
| hskp14
| ! [X49] :
( ndr1_0
=> ( ~ c3_1(X49)
| ~ c2_1(X49)
| c0_1(X49) ) ) )
& ( hskp3
| ! [X48] :
( ndr1_0
=> ( ~ c1_1(X48)
| c3_1(X48)
| c2_1(X48) ) )
| ! [X47] :
( ndr1_0
=> ( ~ c3_1(X47)
| ~ c2_1(X47)
| c0_1(X47) ) ) )
& ( hskp13
| ! [X46] :
( ndr1_0
=> ( ~ c1_1(X46)
| ~ c0_1(X46)
| c3_1(X46) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c2_1(X45)
| ~ c1_1(X45)
| c0_1(X45) ) ) )
& ( hskp12
| ! [X44] :
( ndr1_0
=> ( ~ c0_1(X44)
| c3_1(X44)
| c2_1(X44) ) )
| ! [X43] :
( ndr1_0
=> ( ~ c2_1(X43)
| ~ c1_1(X43)
| c0_1(X43) ) ) )
& ( hskp8
| ! [X42] :
( ndr1_0
=> ( ~ c2_1(X42)
| ~ c1_1(X42)
| c3_1(X42) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c2_1(X41)
| c3_1(X41)
| c0_1(X41) ) ) )
& ( hskp12
| ! [X40] :
( ndr1_0
=> ( ~ c3_1(X40)
| ~ c1_1(X40)
| c2_1(X40) ) )
| ! [X39] :
( ndr1_0
=> ( ~ c1_1(X39)
| c3_1(X39)
| c0_1(X39) ) ) )
& ( hskp11
| hskp10
| ! [X38] :
( ndr1_0
=> ( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38) ) ) )
& ( hskp9
| ! [X37] :
( ndr1_0
=> ( ~ c2_1(X37)
| ~ c0_1(X37)
| c3_1(X37) ) )
| ! [X36] :
( ndr1_0
=> ( ~ c3_1(X36)
| c2_1(X36)
| c0_1(X36) ) ) )
& ( hskp5
| hskp8
| ! [X35] :
( ndr1_0
=> ( ~ c1_1(X35)
| c2_1(X35)
| c0_1(X35) ) ) )
& ( hskp4
| hskp7
| ! [X34] :
( ndr1_0
=> ( ~ c1_1(X34)
| c2_1(X34)
| c0_1(X34) ) ) )
& ( hskp6
| ! [X33] :
( ndr1_0
=> ( ~ c1_1(X33)
| ~ c0_1(X33)
| c3_1(X33) ) )
| ! [X32] :
( ndr1_0
=> ( ~ c1_1(X32)
| c2_1(X32)
| c0_1(X32) ) ) )
& ( hskp5
| ! [X31] :
( ndr1_0
=> ( ~ c3_1(X31)
| ~ c0_1(X31)
| c1_1(X31) ) )
| ! [X30] :
( ndr1_0
=> ( ~ c1_1(X30)
| c2_1(X30)
| c0_1(X30) ) ) )
& ( hskp4
| ! [X29] :
( ndr1_0
=> ( ~ c2_1(X29)
| ~ c0_1(X29)
| c1_1(X29) ) )
| ! [X28] :
( ndr1_0
=> ( ~ c1_1(X28)
| c2_1(X28)
| c0_1(X28) ) ) )
& ( hskp3
| ! [X27] :
( ndr1_0
=> ( ~ c1_1(X27)
| c3_1(X27)
| c0_1(X27) ) )
| ! [X26] :
( ndr1_0
=> ( ~ c1_1(X26)
| c2_1(X26)
| c0_1(X26) ) ) )
& ( ! [X25] :
( ndr1_0
=> ( ~ c3_1(X25)
| ~ c1_1(X25)
| c0_1(X25) ) )
| ! [X24] :
( ndr1_0
=> ( ~ c1_1(X24)
| c3_1(X24)
| c0_1(X24) ) )
| ! [X23] :
( ndr1_0
=> ( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) ) ) )
& ( ! [X22] :
( ndr1_0
=> ( ~ c3_1(X22)
| ~ c2_1(X22)
| c1_1(X22) ) )
| ! [X21] :
( ndr1_0
=> ( ~ c1_1(X21)
| c2_1(X21)
| c0_1(X21) ) )
| ! [X20] :
( ndr1_0
=> ( c3_1(X20)
| c2_1(X20)
| c0_1(X20) ) ) )
& ( hskp0
| hskp2
| ! [X19] :
( ndr1_0
=> ( ~ c3_1(X19)
| c1_1(X19)
| c0_1(X19) ) ) )
& ( hskp0
| ! [X18] :
( ndr1_0
=> ( ~ c3_1(X18)
| ~ c1_1(X18)
| c2_1(X18) ) )
| ! [X17] :
( ndr1_0
=> ( ~ c3_1(X17)
| c1_1(X17)
| c0_1(X17) ) ) )
& ( hskp1
| ! [X16] :
( ndr1_0
=> ( ~ c3_1(X16)
| ~ c2_1(X16)
| c1_1(X16) ) )
| ! [X15] :
( ndr1_0
=> ( ~ c2_1(X15)
| c1_1(X15)
| c0_1(X15) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( ~ c2_1(X14)
| ~ c1_1(X14)
| c3_1(X14) ) )
| ! [X13] :
( ndr1_0
=> ( ~ c1_1(X13)
| c2_1(X13)
| c0_1(X13) ) )
| ! [X12] :
( ndr1_0
=> ( ~ c2_1(X12)
| c1_1(X12)
| c0_1(X12) ) ) )
& ( ! [X11] :
( ndr1_0
=> ( ~ c2_1(X11)
| ~ c0_1(X11)
| c3_1(X11) ) )
| ! [X10] :
( ndr1_0
=> ( ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( c3_1(X9)
| c1_1(X9)
| c0_1(X9) ) ) )
& ( ! [X8] :
( ndr1_0
=> ( ~ c3_1(X8)
| ~ c2_1(X8)
| c0_1(X8) ) )
| ! [X7] :
( ndr1_0
=> ( c3_1(X7)
| c2_1(X7)
| c0_1(X7) ) )
| ! [X6] :
( ndr1_0
=> ( c3_1(X6)
| c1_1(X6)
| c0_1(X6) ) ) )
& ( hskp0
| ! [X5] :
( ndr1_0
=> ( ~ c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) ) )
| ! [X4] :
( ndr1_0
=> ( c2_1(X4)
| c1_1(X4)
| c0_1(X4) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( ~ c3_1(X3)
| ~ c1_1(X3)
| ~ c0_1(X3) ) )
| ! [X2] :
( ndr1_0
=> ( ~ c2_1(X2)
| ~ c0_1(X2)
| c1_1(X2) ) )
| ! [X1] :
( ndr1_0
=> ( c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ) )
& ( ! [Z] :
( ndr1_0
=> ( ~ c3_1(Z)
| ~ c1_1(Z)
| c2_1(Z) ) )
| ! [Y] :
( ndr1_0
=> ( c3_1(Y)
| c2_1(Y)
| c1_1(Y) ) )
| ! [X] :
( ndr1_0
=> ( c2_1(X)
| c1_1(X)
| c0_1(X) ) ) )
& ( ! [W] :
( ndr1_0
=> ( ~ c2_1(W)
| ~ c1_1(W)
| c0_1(W) ) )
| ! [V] :
( ndr1_0
=> ( c3_1(V)
| c2_1(V)
| c0_1(V) ) )
| ! [U] :
( ndr1_0
=> ( c2_1(U)
| c1_1(U)
| c0_1(U) ) ) )
& ( ( c2_1(a354)
& c1_1(a354)
& c0_1(a354)
& ndr1_0 )
| ~ hskp29 )
& ( ( c3_1(a353)
& c2_1(a353)
& c1_1(a353)
& ndr1_0 )
| ~ hskp28 )
& ( ( c3_1(a334)
& c2_1(a334)
& c0_1(a334)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a349)
& ~ c2_1(a349)
& c0_1(a349)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c3_1(a346)
& ~ c1_1(a346)
& ~ c0_1(a346)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c2_1(a342)
& ~ c1_1(a342)
& c3_1(a342)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c0_1(a341)
& c3_1(a341)
& c2_1(a341)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c3_1(a338)
& ~ c2_1(a338)
& ~ c1_1(a338)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c1_1(a336)
& ~ c0_1(a336)
& c3_1(a336)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c3_1(a333)
& ~ c2_1(a333)
& c1_1(a333)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c3_1(a330)
& c2_1(a330)
& c1_1(a330)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c3_1(a329)
& ~ c0_1(a329)
& c2_1(a329)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c3_1(a323)
& c2_1(a323)
& c0_1(a323)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c1_1(a321)
& c3_1(a321)
& c2_1(a321)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c2_1(a320)
& ~ c0_1(a320)
& c1_1(a320)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c0_1(a315)
& c2_1(a315)
& c1_1(a315)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c1_1(a313)
& c3_1(a313)
& c0_1(a313)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c2_1(a310)
& ~ c0_1(a310)
& c3_1(a310)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c2_1(a309)
& c3_1(a309)
& c1_1(a309)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c0_1(a308)
& c3_1(a308)
& c1_1(a308)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c3_1(a307)
& ~ c1_1(a307)
& c0_1(a307)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c1_1(a305)
& ~ c0_1(a305)
& c2_1(a305)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c2_1(a303)
& c1_1(a303)
& c0_1(a303)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c2_1(a302)
& ~ c1_1(a302)
& c0_1(a302)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a301)
& ~ c1_1(a301)
& c2_1(a301)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c2_1(a300)
& ~ c1_1(a300)
& ~ c0_1(a300)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c2_1(a299)
& c3_1(a299)
& c0_1(a299)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c3_1(a297)
& ~ c0_1(a297)
& c1_1(a297)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c1_1(a295)
& c2_1(a295)
& c0_1(a295)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c3_1(a294)
& ~ c2_1(a294)
& ~ c0_1(a294)
& ndr1_0 )
| ~ hskp0 ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_3,negated_conjecture,
( ~ c0_1(a294)
| ~ hskp0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_4,negated_conjecture,
( ~ c2_1(a294)
| ~ hskp0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_5,negated_conjecture,
( ~ c3_1(a294)
| ~ hskp0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_7,negated_conjecture,
( c0_1(a295)
| ~ hskp1 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_8,negated_conjecture,
( c2_1(a295)
| ~ hskp1 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_9,negated_conjecture,
( ~ c1_1(a295)
| ~ hskp1 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_11,negated_conjecture,
( c1_1(a297)
| ~ hskp2 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_12,negated_conjecture,
( ~ c0_1(a297)
| ~ hskp2 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_13,negated_conjecture,
( ~ c3_1(a297)
| ~ hskp2 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_19,negated_conjecture,
( ~ c0_1(a300)
| ~ hskp4 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_20,negated_conjecture,
( ~ c1_1(a300)
| ~ hskp4 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_21,negated_conjecture,
( ~ c2_1(a300)
| ~ hskp4 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_35,negated_conjecture,
( c2_1(a305)
| ~ hskp8 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_36,negated_conjecture,
( ~ c0_1(a305)
| ~ hskp8 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_37,negated_conjecture,
( ~ c1_1(a305)
| ~ hskp8 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_43,negated_conjecture,
( c1_1(a308)
| ~ hskp10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_44,negated_conjecture,
( c3_1(a308)
| ~ hskp10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_45,negated_conjecture,
( ~ c0_1(a308)
| ~ hskp10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_47,negated_conjecture,
( c1_1(a309)
| ~ hskp11 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_48,negated_conjecture,
( c3_1(a309)
| ~ hskp11 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_49,negated_conjecture,
( ~ c2_1(a309)
| ~ hskp11 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_51,negated_conjecture,
( c3_1(a310)
| ~ hskp12 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_52,negated_conjecture,
( ~ c0_1(a310)
| ~ hskp12 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_53,negated_conjecture,
( ~ c2_1(a310)
| ~ hskp12 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_55,negated_conjecture,
( c0_1(a313)
| ~ hskp13 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_56,negated_conjecture,
( c3_1(a313)
| ~ hskp13 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_57,negated_conjecture,
( ~ c1_1(a313)
| ~ hskp13 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_59,negated_conjecture,
( c1_1(a315)
| ~ hskp14 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_60,negated_conjecture,
( c2_1(a315)
| ~ hskp14 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_61,negated_conjecture,
( ~ c0_1(a315)
| ~ hskp14 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_66,negated_conjecture,
( ndr1_0
| ~ hskp16 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_67,negated_conjecture,
( c2_1(a321)
| ~ hskp16 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_68,negated_conjecture,
( c3_1(a321)
| ~ hskp16 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_69,negated_conjecture,
( ~ c1_1(a321)
| ~ hskp16 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_79,negated_conjecture,
( c1_1(a330)
| ~ hskp19 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_80,negated_conjecture,
( c2_1(a330)
| ~ hskp19 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_81,negated_conjecture,
( ~ c3_1(a330)
| ~ hskp19 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_83,negated_conjecture,
( c1_1(a333)
| ~ hskp20 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_84,negated_conjecture,
( ~ c2_1(a333)
| ~ hskp20 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_85,negated_conjecture,
( ~ c3_1(a333)
| ~ hskp20 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_87,negated_conjecture,
( c3_1(a336)
| ~ hskp21 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_88,negated_conjecture,
( ~ c0_1(a336)
| ~ hskp21 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_89,negated_conjecture,
( ~ c1_1(a336)
| ~ hskp21 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_106,negated_conjecture,
( ndr1_0
| ~ hskp26 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_107,negated_conjecture,
( c0_1(a349)
| ~ hskp26 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_108,negated_conjecture,
( ~ c2_1(a349)
| ~ hskp26 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_109,negated_conjecture,
( ~ c3_1(a349)
| ~ hskp26 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_115,negated_conjecture,
( c1_1(a353)
| ~ hskp28 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_116,negated_conjecture,
( c2_1(a353)
| ~ hskp28 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_117,negated_conjecture,
( c3_1(a353)
| ~ hskp28 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_125,negated_conjecture,
( hskp0
| ~ c1_1(B)
| ~ c0_1(B)
| c2_1(B)
| c2_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_126,negated_conjecture,
( ~ c3_1(C)
| ~ c2_1(C)
| c0_1(C)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_129,negated_conjecture,
( hskp1
| ~ c3_1(B)
| ~ c2_1(B)
| c1_1(B)
| ~ c2_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_130,negated_conjecture,
( hskp0
| ~ c3_1(B)
| ~ c1_1(B)
| c2_1(B)
| ~ c3_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_131,negated_conjecture,
( hskp0
| hskp2
| ~ c3_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_132,negated_conjecture,
( ~ c3_1(C)
| ~ c2_1(C)
| c1_1(C)
| ~ c1_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_141,negated_conjecture,
( hskp11
| hskp10
| ~ c3_1(A)
| c2_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_143,negated_conjecture,
( hskp8
| ~ c2_1(B)
| ~ c1_1(B)
| c3_1(B)
| ~ c2_1(A)
| c3_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_144,negated_conjecture,
( hskp12
| ~ c0_1(B)
| c3_1(B)
| c2_1(B)
| ~ c2_1(A)
| ~ c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_147,negated_conjecture,
( hskp0
| hskp14
| ~ c3_1(A)
| ~ c2_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_151,negated_conjecture,
( hskp16
| ~ c3_1(A)
| c2_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_152,negated_conjecture,
( hskp13
| ~ c2_1(B)
| c3_1(B)
| c1_1(B)
| ~ c0_1(A)
| c3_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_156,negated_conjecture,
( hskp4
| ~ c3_1(B)
| ~ c0_1(B)
| c1_1(B)
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_158,negated_conjecture,
( hskp12
| hskp19
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_159,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_161,negated_conjecture,
( hskp21
| ~ c0_1(A)
| c3_1(A)
| c2_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_165,negated_conjecture,
( ~ c3_1(B)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ c3_1(A)
| ~ c1_1(A)
| c2_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_168,negated_conjecture,
( hskp11
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ c2_1(A)
| ~ c0_1(A)
| c3_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_174,negated_conjecture,
( hskp28
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_179,negated_conjecture,
( hskp12
| hskp11
| hskp26 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_180,negated_conjecture,
( hskp16
| hskp26 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_38095,plain,
( ~ c3_1(B)
| ~ c2_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(factor,[status(thm)],[c_126]) ).
cnf(c_184,plain,
( ~ c3_1(B)
| ~ c2_1(B)
| c0_1(B)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(copy,[status(thm)],[c_38095]) ).
cnf(c_38096,plain,
( hskp1
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c2_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(factor,[status(thm)],[c_129]) ).
cnf(c_185,plain,
( hskp1
| ~ c3_1(A)
| ~ c2_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(copy,[status(thm)],[c_38096]) ).
cnf(c_38097,plain,
( ~ c3_1(B)
| ~ c2_1(B)
| c1_1(B)
| ~ c1_1(A)
| c2_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(factor,[status(thm)],[c_132]) ).
cnf(c_186,plain,
( ~ c3_1(B)
| ~ c2_1(B)
| c1_1(B)
| ~ c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(copy,[status(thm)],[c_38097]) ).
cnf(c_38098,plain,
( hskp8
| ~ c2_1(A)
| ~ c1_1(A)
| ~ c2_1(A)
| c3_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(factor,[status(thm)],[c_143]) ).
cnf(c_190,plain,
( hskp8
| ~ c1_1(A)
| ~ c2_1(A)
| c3_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(copy,[status(thm)],[c_38098]) ).
cnf(c_38099,plain,
( hskp13
| ~ c2_1(A)
| c3_1(A)
| ~ c0_1(A)
| c3_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(factor,[status(thm)],[c_152]) ).
cnf(c_191,plain,
( hskp13
| ~ c2_1(A)
| ~ c0_1(A)
| c3_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(copy,[status(thm)],[c_38099]) ).
cnf(c_38100,plain,
( hskp4
| ~ c3_1(A)
| ~ c0_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(factor,[status(thm)],[c_156]) ).
cnf(c_192,plain,
( hskp4
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A)
| ~ ndr1_0 ),
inference(copy,[status(thm)],[c_38100]) ).
cnf(c_205,plain,
( c0_1(a349)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_179,c_107]) ).
cnf(c_207,plain,
( c0_1(a349)
| hskp16 ),
inference(resolve,[status(thm)],[c_180,c_107]) ).
cnf(c_208,plain,
( ndr1_0
| hskp16 ),
inference(resolve,[status(thm)],[c_180,c_106]) ).
cnf(c_38101,negated_conjecture,
( ndr1_0
| ndr1_0 ),
inference(resolve,[status(thm)],[c_208,c_66]) ).
cnf(c_215,negated_conjecture,
ndr1_0,
inference(copy,[status(thm)],[c_38101]) ).
cnf(c_220,plain,
( hskp4
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A) ),
inference(resolve,[status(thm)],[c_215,c_192]) ).
cnf(c_221,plain,
( hskp13
| ~ c2_1(A)
| ~ c0_1(A)
| c3_1(A)
| c1_1(A) ),
inference(resolve,[status(thm)],[c_215,c_191]) ).
cnf(c_222,plain,
( hskp8
| ~ c1_1(A)
| ~ c2_1(A)
| c3_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_190]) ).
cnf(c_226,plain,
( ~ c3_1(B)
| ~ c2_1(B)
| c1_1(B)
| ~ c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_186]) ).
cnf(c_227,plain,
( hskp1
| ~ c3_1(A)
| ~ c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_185]) ).
cnf(c_228,plain,
( ~ c3_1(B)
| ~ c2_1(B)
| c0_1(B)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_184]) ).
cnf(c_231,negated_conjecture,
( hskp28
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_215,c_174]) ).
cnf(c_237,negated_conjecture,
( hskp11
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ c2_1(A)
| ~ c0_1(A)
| c3_1(A) ),
inference(resolve,[status(thm)],[c_215,c_168]) ).
cnf(c_240,negated_conjecture,
( ~ c3_1(B)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ c3_1(A)
| ~ c1_1(A)
| c2_1(A) ),
inference(resolve,[status(thm)],[c_215,c_165]) ).
cnf(c_244,negated_conjecture,
( hskp21
| ~ c0_1(A)
| c3_1(A)
| c2_1(A) ),
inference(resolve,[status(thm)],[c_215,c_161]) ).
cnf(c_246,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A) ),
inference(resolve,[status(thm)],[c_215,c_159]) ).
cnf(c_247,negated_conjecture,
( hskp12
| hskp19
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A) ),
inference(resolve,[status(thm)],[c_215,c_158]) ).
cnf(c_249,negated_conjecture,
( hskp4
| ~ c3_1(B)
| ~ c0_1(B)
| c1_1(B)
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A) ),
inference(resolve,[status(thm)],[c_215,c_156]) ).
cnf(c_254,negated_conjecture,
( hskp16
| ~ c3_1(A)
| c2_1(A)
| c1_1(A) ),
inference(resolve,[status(thm)],[c_215,c_151]) ).
cnf(c_258,negated_conjecture,
( hskp0
| hskp14
| ~ c3_1(A)
| ~ c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_147]) ).
cnf(c_261,negated_conjecture,
( hskp12
| ~ c0_1(B)
| c3_1(B)
| c2_1(B)
| ~ c2_1(A)
| ~ c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_144]) ).
cnf(c_264,negated_conjecture,
( hskp11
| hskp10
| ~ c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_141]) ).
cnf(c_273,negated_conjecture,
( ~ c3_1(C)
| ~ c2_1(C)
| c1_1(C)
| ~ c1_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_132]) ).
cnf(c_274,negated_conjecture,
( hskp0
| hskp2
| ~ c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_131]) ).
cnf(c_275,negated_conjecture,
( hskp0
| ~ c3_1(B)
| ~ c1_1(B)
| c2_1(B)
| ~ c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_130]) ).
cnf(c_276,negated_conjecture,
( hskp1
| ~ c3_1(B)
| ~ c2_1(B)
| c1_1(B)
| ~ c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_129]) ).
cnf(c_279,negated_conjecture,
( ~ c3_1(C)
| ~ c2_1(C)
| c0_1(C)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_126]) ).
cnf(c_280,negated_conjecture,
( hskp0
| ~ c1_1(B)
| ~ c0_1(B)
| c2_1(B)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_215,c_125]) ).
cnf(c_286,plain,
( hskp16
| hskp21
| c3_1(a349)
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_244,c_207]) ).
cnf(c_287,plain,
( hskp12
| hskp11
| hskp21
| c3_1(a349)
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_244,c_205]) ).
cnf(c_288,plain,
( ~ hskp26
| hskp16
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_286,c_109]) ).
cnf(c_38102,negated_conjecture,
( hskp16
| hskp16
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_288,c_180]) ).
cnf(c_289,negated_conjecture,
( hskp16
| hskp21
| c2_1(a349) ),
inference(copy,[status(thm)],[c_38102]) ).
cnf(c_290,plain,
( ~ hskp26
| hskp16
| hskp21 ),
inference(resolve,[status(thm)],[c_289,c_108]) ).
cnf(c_38103,negated_conjecture,
( hskp16
| hskp16
| hskp21 ),
inference(resolve,[status(thm)],[c_290,c_180]) ).
cnf(c_291,negated_conjecture,
( hskp16
| hskp21 ),
inference(copy,[status(thm)],[c_38103]) ).
cnf(c_292,plain,
( c3_1(a336)
| hskp16 ),
inference(resolve,[status(thm)],[c_291,c_87]) ).
cnf(c_38104,negated_conjecture,
( hskp16
| hskp16
| c2_1(a336)
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_254,c_292]) ).
cnf(c_294,negated_conjecture,
( hskp16
| c2_1(a336)
| c1_1(a336) ),
inference(copy,[status(thm)],[c_38104]) ).
cnf(c_299,plain,
( ~ hskp26
| hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_287,c_109]) ).
cnf(c_38105,negated_conjecture,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_299,c_179]) ).
cnf(c_38106,negated_conjecture,
( hskp12
| hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(copy,[status(thm)],[c_38105]) ).
cnf(c_303,negated_conjecture,
( hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(copy,[status(thm)],[c_38106]) ).
cnf(c_304,plain,
( ~ hskp26
| hskp12
| hskp11
| hskp21 ),
inference(resolve,[status(thm)],[c_303,c_108]) ).
cnf(c_38107,negated_conjecture,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp21 ),
inference(resolve,[status(thm)],[c_304,c_179]) ).
cnf(c_38108,negated_conjecture,
( hskp12
| hskp12
| hskp11
| hskp21 ),
inference(copy,[status(thm)],[c_38107]) ).
cnf(c_305,negated_conjecture,
( hskp12
| hskp11
| hskp21 ),
inference(copy,[status(thm)],[c_38108]) ).
cnf(c_306,plain,
( c3_1(a336)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_305,c_87]) ).
cnf(c_372,plain,
( hskp16
| hskp1
| ~ c2_1(a336)
| c1_1(a336)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_227,c_292]) ).
cnf(c_377,plain,
( hskp12
| hskp11
| ~ c2_1(a336)
| c0_1(a336)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_228,c_306]) ).
cnf(c_378,plain,
( hskp16
| ~ c2_1(a336)
| c0_1(a336)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_228,c_292]) ).
cnf(c_429,plain,
( hskp12
| hskp11
| hskp0
| hskp14
| ~ c2_1(a336)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_258,c_306]) ).
cnf(c_38109,negated_conjecture,
( hskp12
| hskp11
| hskp11
| hskp10
| c2_1(a336)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_264,c_306]) ).
cnf(c_465,negated_conjecture,
( hskp12
| hskp11
| hskp10
| c2_1(a336)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_38109]) ).
cnf(c_469,plain,
( ~ hskp21
| hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(resolve,[status(thm)],[c_465,c_88]) ).
cnf(c_38110,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(resolve,[status(thm)],[c_469,c_305]) ).
cnf(c_38111,plain,
( hskp12
| hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(copy,[status(thm)],[c_38110]) ).
cnf(c_477,plain,
( hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(copy,[status(thm)],[c_38111]) ).
cnf(c_493,plain,
( hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_274,c_306]) ).
cnf(c_38112,negated_conjecture,
( hskp12
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| ~ c2_1(A)
| ~ c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_261,c_205]) ).
cnf(c_570,negated_conjecture,
( hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| ~ c2_1(A)
| ~ c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38112]) ).
cnf(c_38113,plain,
( hskp16
| c1_1(a336)
| hskp16
| hskp1
| c1_1(a336)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_372,c_294]) ).
cnf(c_38114,plain,
( hskp16
| hskp16
| hskp1
| c1_1(a336)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_38113]) ).
cnf(c_638,plain,
( hskp16
| hskp1
| c1_1(a336)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_38114]) ).
cnf(c_643,plain,
( ~ hskp21
| hskp16
| hskp1
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_638,c_88]) ).
cnf(c_38115,plain,
( hskp16
| hskp16
| hskp1
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_643,c_291]) ).
cnf(c_645,plain,
( hskp16
| hskp1
| c1_1(a336) ),
inference(copy,[status(thm)],[c_38115]) ).
cnf(c_654,plain,
( ~ hskp21
| hskp16
| hskp1 ),
inference(resolve,[status(thm)],[c_645,c_89]) ).
cnf(c_38116,plain,
( hskp16
| hskp16
| hskp1 ),
inference(resolve,[status(thm)],[c_654,c_291]) ).
cnf(c_656,plain,
( hskp16
| hskp1 ),
inference(copy,[status(thm)],[c_38116]) ).
cnf(c_657,plain,
( c2_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_656,c_8]) ).
cnf(c_658,plain,
( c0_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_656,c_7]) ).
cnf(c_678,plain,
( hskp13
| ~ c2_1(a295)
| c3_1(a295)
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_658,c_221]) ).
cnf(c_38117,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_429,c_477]) ).
cnf(c_38118,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14
| c0_1(a336) ),
inference(copy,[status(thm)],[c_38117]) ).
cnf(c_959,plain,
( hskp10
| hskp12
| hskp11
| hskp0
| hskp14
| c0_1(a336) ),
inference(copy,[status(thm)],[c_38118]) ).
cnf(c_966,plain,
( ~ hskp21
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(resolve,[status(thm)],[c_959,c_88]) ).
cnf(c_38119,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(resolve,[status(thm)],[c_966,c_305]) ).
cnf(c_38120,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(copy,[status(thm)],[c_38119]) ).
cnf(c_967,plain,
( hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(copy,[status(thm)],[c_38120]) ).
cnf(c_968,plain,
( c2_1(a315)
| hskp10
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_967,c_60]) ).
cnf(c_1070,plain,
( ~ hskp21
| hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_493,c_88]) ).
cnf(c_38121,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_1070,c_305]) ).
cnf(c_38122,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(copy,[status(thm)],[c_38121]) ).
cnf(c_1071,plain,
( hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(copy,[status(thm)],[c_38122]) ).
cnf(c_1076,plain,
( ~ hskp21
| hskp12
| hskp11
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_1071,c_89]) ).
cnf(c_38123,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_1076,c_305]) ).
cnf(c_38124,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| hskp2 ),
inference(copy,[status(thm)],[c_38123]) ).
cnf(c_1077,plain,
( hskp12
| hskp11
| hskp0
| hskp2 ),
inference(copy,[status(thm)],[c_38124]) ).
cnf(c_1078,plain,
( c1_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_1077,c_11]) ).
cnf(c_38125,plain,
( hskp16
| hskp13
| c3_1(a295)
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_678,c_657]) ).
cnf(c_1193,plain,
( hskp13
| c3_1(a295)
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_38125]) ).
cnf(c_38126,plain,
( hskp4
| ~ c2_1(a295)
| ~ c0_1(a295)
| c1_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_1193,c_220]) ).
cnf(c_1199,plain,
( hskp4
| ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_38126]) ).
cnf(c_38127,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_377,c_477]) ).
cnf(c_38128,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38127]) ).
cnf(c_1410,plain,
( hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38128]) ).
cnf(c_38129,plain,
( hskp16
| c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_378,c_294]) ).
cnf(c_1420,plain,
( c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38129]) ).
cnf(c_38130,plain,
( hskp16
| hskp4
| ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_1199,c_658]) ).
cnf(c_2563,plain,
( hskp4
| ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_38130]) ).
cnf(c_38131,plain,
( hskp16
| hskp4
| hskp13
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_2563,c_657]) ).
cnf(c_2574,plain,
( hskp4
| hskp13
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_38131]) ).
cnf(c_2579,plain,
( ~ hskp1
| hskp4
| hskp13
| hskp16 ),
inference(resolve,[status(thm)],[c_2574,c_9]) ).
cnf(c_38132,plain,
( hskp16
| hskp4
| hskp13
| hskp16 ),
inference(resolve,[status(thm)],[c_2579,c_656]) ).
cnf(c_2580,plain,
( hskp4
| hskp13
| hskp16 ),
inference(copy,[status(thm)],[c_38132]) ).
cnf(c_2581,plain,
( c3_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2580,c_56]) ).
cnf(c_2582,plain,
( c0_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2580,c_55]) ).
cnf(c_38133,negated_conjecture,
( hskp16
| c2_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2581,c_254]) ).
cnf(c_2610,negated_conjecture,
( c2_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38133]) ).
cnf(c_38134,plain,
( hskp4
| ~ c2_1(a313)
| ~ c0_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2581,c_220]) ).
cnf(c_2621,plain,
( ~ c2_1(a313)
| ~ c0_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38134]) ).
cnf(c_38135,plain,
( hskp4
| hskp16
| ~ c2_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2621,c_2582]) ).
cnf(c_38136,plain,
( hskp4
| ~ c2_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38135]) ).
cnf(c_2633,plain,
( ~ c2_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38136]) ).
cnf(c_38137,plain,
( c1_1(a313)
| hskp4
| hskp16
| c1_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2633,c_2610]) ).
cnf(c_38138,plain,
( c1_1(a313)
| hskp4
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38137]) ).
cnf(c_38139,plain,
( c1_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38138]) ).
cnf(c_2634,plain,
( c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38139]) ).
cnf(c_2635,plain,
( ~ hskp13
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2634,c_57]) ).
cnf(c_38140,plain,
( hskp4
| hskp16
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2635,c_2580]) ).
cnf(c_38141,plain,
( hskp4
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38140]) ).
cnf(c_2636,plain,
( hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_38141]) ).
cnf(c_38142,plain,
( hskp10
| hskp12
| hskp11
| hskp0
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a315)
| c0_1(a315) ),
inference(resolve,[status(thm)],[c_570,c_968]) ).
cnf(c_38143,plain,
( hskp10
| hskp12
| hskp0
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a315)
| c0_1(a315) ),
inference(copy,[status(thm)],[c_38142]) ).
cnf(c_3254,plain,
( hskp10
| hskp0
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a315)
| c0_1(a315) ),
inference(copy,[status(thm)],[c_38143]) ).
cnf(c_38144,negated_conjecture,
( hskp11
| hskp10
| c2_1(A)
| c0_1(A)
| hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_1410,c_264]) ).
cnf(c_38145,negated_conjecture,
( hskp11
| hskp10
| c2_1(A)
| hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38144]) ).
cnf(c_38146,negated_conjecture,
( hskp11
| hskp10
| hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38145]) ).
cnf(c_38147,negated_conjecture,
( hskp11
| hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38146]) ).
cnf(c_11459,negated_conjecture,
( hskp10
| hskp12
| hskp11
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38147]) ).
cnf(c_38148,negated_conjecture,
( hskp16
| c2_1(A)
| c1_1(A)
| c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_1420,c_254]) ).
cnf(c_38149,negated_conjecture,
( hskp16
| c2_1(A)
| c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38148]) ).
cnf(c_38150,negated_conjecture,
( hskp16
| c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38149]) ).
cnf(c_11537,negated_conjecture,
( c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38150]) ).
cnf(c_13325,plain,
( ~ hskp21
| hskp10
| hskp12
| hskp11
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_11459,c_88]) ).
cnf(c_38151,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_13325,c_305]) ).
cnf(c_38152,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38151]) ).
cnf(c_13369,plain,
( hskp10
| hskp12
| hskp11
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_38152]) ).
cnf(c_13379,plain,
( ~ hskp0
| hskp10
| hskp12
| hskp11
| c2_1(a294)
| c1_1(a294) ),
inference(resolve,[status(thm)],[c_13369,c_3]) ).
cnf(c_14835,plain,
( ~ hskp4
| c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(a300)
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_11537,c_19]) ).
cnf(c_38153,plain,
( hskp16
| c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(a300)
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_14835,c_2636]) ).
cnf(c_14849,plain,
( c1_1(a336)
| hskp16
| c0_1(a336)
| c2_1(a300)
| c1_1(a300) ),
inference(copy,[status(thm)],[c_38153]) ).
cnf(c_14859,plain,
( ~ hskp21
| c1_1(a336)
| hskp16
| c2_1(a300)
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_14849,c_88]) ).
cnf(c_38154,plain,
( hskp16
| c1_1(a336)
| hskp16
| c2_1(a300)
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_14859,c_291]) ).
cnf(c_14861,plain,
( c1_1(a336)
| hskp16
| c2_1(a300)
| c1_1(a300) ),
inference(copy,[status(thm)],[c_38154]) ).
cnf(c_14886,plain,
( ~ hskp4
| c1_1(a336)
| hskp16
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_14861,c_21]) ).
cnf(c_38155,plain,
( hskp16
| c1_1(a336)
| hskp16
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_14886,c_2636]) ).
cnf(c_14887,plain,
( c1_1(a336)
| hskp16
| c1_1(a300) ),
inference(copy,[status(thm)],[c_38155]) ).
cnf(c_14910,plain,
( ~ hskp4
| c1_1(a336)
| hskp16 ),
inference(resolve,[status(thm)],[c_14887,c_20]) ).
cnf(c_38156,plain,
( hskp16
| c1_1(a336)
| hskp16 ),
inference(resolve,[status(thm)],[c_14910,c_2636]) ).
cnf(c_14911,plain,
( c1_1(a336)
| hskp16 ),
inference(copy,[status(thm)],[c_38156]) ).
cnf(c_14918,plain,
( ~ hskp21
| hskp16 ),
inference(resolve,[status(thm)],[c_14911,c_89]) ).
cnf(c_38157,plain,
( hskp16
| hskp16 ),
inference(resolve,[status(thm)],[c_14918,c_291]) ).
cnf(c_14920,plain,
hskp16,
inference(copy,[status(thm)],[c_38157]) ).
cnf(c_14921,negated_conjecture,
~ c1_1(a321),
inference(resolve,[status(thm)],[c_14920,c_69]) ).
cnf(c_14922,negated_conjecture,
c3_1(a321),
inference(resolve,[status(thm)],[c_14920,c_68]) ).
cnf(c_14923,negated_conjecture,
c2_1(a321),
inference(resolve,[status(thm)],[c_14920,c_67]) ).
cnf(c_38158,negated_conjecture,
( ~ c2_1(a321)
| c0_1(a321)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14922,c_279]) ).
cnf(c_15071,negated_conjecture,
( c0_1(a321)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14923,c_38158]) ).
cnf(c_38159,negated_conjecture,
( hskp1
| ~ c2_1(a321)
| c1_1(a321)
| ~ c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14922,c_276]) ).
cnf(c_38160,negated_conjecture,
( hskp1
| ~ c2_1(a321)
| ~ c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14921,c_38159]) ).
cnf(c_15072,negated_conjecture,
( hskp1
| ~ c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14923,c_38160]) ).
cnf(c_38161,negated_conjecture,
( hskp0
| ~ c3_1(A)
| ~ c1_1(A)
| c2_1(A)
| c1_1(a321)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14922,c_275]) ).
cnf(c_15073,negated_conjecture,
( hskp0
| ~ c3_1(A)
| ~ c1_1(A)
| c2_1(A)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14921,c_38161]) ).
cnf(c_38162,negated_conjecture,
( hskp0
| hskp2
| c1_1(a321)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14922,c_274]) ).
cnf(c_15074,negated_conjecture,
( hskp0
| hskp2
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14921,c_38162]) ).
cnf(c_38163,negated_conjecture,
( ~ c2_1(a321)
| c1_1(a321)
| ~ c1_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14922,c_273]) ).
cnf(c_38164,negated_conjecture,
( ~ c2_1(a321)
| ~ c1_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14921,c_38163]) ).
cnf(c_15075,negated_conjecture,
( ~ c1_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14923,c_38164]) ).
cnf(c_38165,negated_conjecture,
( ~ c2_1(a321)
| ~ c0_1(a321)
| ~ c3_1(A)
| ~ c1_1(A)
| c2_1(A) ),
inference(resolve,[status(thm)],[c_14922,c_240]) ).
cnf(c_15081,negated_conjecture,
( ~ c0_1(a321)
| ~ c3_1(A)
| ~ c1_1(A)
| c2_1(A) ),
inference(resolve,[status(thm)],[c_14923,c_38165]) ).
cnf(c_38166,negated_conjecture,
( hskp11
| ~ c2_1(a321)
| ~ c0_1(a321)
| ~ c2_1(A)
| ~ c0_1(A)
| c3_1(A) ),
inference(resolve,[status(thm)],[c_14922,c_237]) ).
cnf(c_15082,negated_conjecture,
( hskp11
| ~ c0_1(a321)
| ~ c2_1(A)
| ~ c0_1(A)
| c3_1(A) ),
inference(resolve,[status(thm)],[c_14923,c_38166]) ).
cnf(c_38167,negated_conjecture,
( ~ c2_1(a321)
| c0_1(a321)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14922,c_228]) ).
cnf(c_15083,negated_conjecture,
( c0_1(a321)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14923,c_38167]) ).
cnf(c_38168,negated_conjecture,
( hskp1
| ~ c2_1(a321)
| c1_1(a321)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14922,c_227]) ).
cnf(c_38169,negated_conjecture,
( hskp1
| ~ c2_1(a321)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14921,c_38168]) ).
cnf(c_15084,negated_conjecture,
( hskp1
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14923,c_38169]) ).
cnf(c_38170,negated_conjecture,
( ~ c2_1(a321)
| c1_1(a321)
| ~ c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14922,c_226]) ).
cnf(c_38171,negated_conjecture,
( ~ c2_1(a321)
| ~ c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14921,c_38170]) ).
cnf(c_15085,negated_conjecture,
( ~ c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14923,c_38171]) ).
cnf(c_38172,negated_conjecture,
( hskp4
| ~ c2_1(a321)
| ~ c0_1(a321)
| c1_1(a321) ),
inference(resolve,[status(thm)],[c_14922,c_220]) ).
cnf(c_38173,negated_conjecture,
( hskp4
| ~ c2_1(a321)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14921,c_38172]) ).
cnf(c_15086,negated_conjecture,
( hskp4
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14923,c_38173]) ).
cnf(c_38174,negated_conjecture,
( hskp12
| hskp19
| ~ c2_1(a321)
| c1_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_15084,c_247]) ).
cnf(c_38175,negated_conjecture,
( hskp12
| hskp19
| ~ c2_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_14921,c_38174]) ).
cnf(c_15113,negated_conjecture,
( hskp12
| hskp19
| hskp1 ),
inference(resolve,[status(thm)],[c_14923,c_38175]) ).
cnf(c_38176,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(a321)
| c1_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_15084,c_246]) ).
cnf(c_38177,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_14921,c_38176]) ).
cnf(c_15114,negated_conjecture,
( hskp20
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_14923,c_38177]) ).
cnf(c_15115,plain,
( hskp1
| hskp4 ),
inference(resolve,[status(thm)],[c_15086,c_15084]) ).
cnf(c_15116,plain,
( c2_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15115,c_8]) ).
cnf(c_15117,plain,
( c0_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15115,c_7]) ).
cnf(c_15213,plain,
( c2_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_15113,c_80]) ).
cnf(c_15214,plain,
( c1_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_15113,c_79]) ).
cnf(c_15215,plain,
( c1_1(a333)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15114,c_83]) ).
cnf(c_15268,plain,
( hskp13
| ~ c2_1(a295)
| c3_1(a295)
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15117,c_221]) ).
cnf(c_38178,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(a321)
| c1_1(a321)
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_15074,c_246]) ).
cnf(c_38179,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(a321)
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_14921,c_38178]) ).
cnf(c_15273,negated_conjecture,
( hskp20
| hskp11
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_14923,c_38179]) ).
cnf(c_15320,plain,
( hskp8
| ~ c1_1(a330)
| c3_1(a330)
| c0_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_15213,c_222]) ).
cnf(c_15364,plain,
( c1_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_15273,c_11]) ).
cnf(c_15942,plain,
( hskp20
| hskp11
| hskp0
| c3_1(a297)
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_15085,c_15364]) ).
cnf(c_15946,plain,
( hskp11
| hskp1
| c3_1(a333)
| c2_1(a333)
| c0_1(a333) ),
inference(resolve,[status(thm)],[c_15085,c_15215]) ).
cnf(c_15953,plain,
( hskp12
| hskp11
| hskp0
| c3_1(a297)
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_15085,c_1078]) ).
cnf(c_38180,plain,
( hskp4
| hskp13
| c3_1(a295)
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15268,c_15116]) ).
cnf(c_15958,plain,
( hskp13
| c3_1(a295)
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38180]) ).
cnf(c_38181,plain,
( hskp4
| ~ c2_1(a295)
| ~ c0_1(a295)
| c1_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15958,c_220]) ).
cnf(c_38182,plain,
( hskp4
| ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38181]) ).
cnf(c_15975,plain,
( ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38182]) ).
cnf(c_16757,plain,
( ~ hskp20
| hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(resolve,[status(thm)],[c_15946,c_85]) ).
cnf(c_38183,plain,
( hskp11
| hskp1
| hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(resolve,[status(thm)],[c_16757,c_15114]) ).
cnf(c_38184,plain,
( hskp11
| hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(copy,[status(thm)],[c_38183]) ).
cnf(c_16784,plain,
( hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(copy,[status(thm)],[c_38184]) ).
cnf(c_38185,negated_conjecture,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp1
| c2_1(a333) ),
inference(resolve,[status(thm)],[c_16784,c_244]) ).
cnf(c_16790,negated_conjecture,
( hskp21
| c3_1(a333)
| hskp11
| hskp1
| c2_1(a333) ),
inference(copy,[status(thm)],[c_38185]) ).
cnf(c_16805,plain,
( ~ hskp20
| hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(resolve,[status(thm)],[c_16790,c_85]) ).
cnf(c_38186,plain,
( hskp11
| hskp1
| hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(resolve,[status(thm)],[c_16805,c_15114]) ).
cnf(c_38187,plain,
( hskp11
| hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(copy,[status(thm)],[c_38186]) ).
cnf(c_16807,plain,
( hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(copy,[status(thm)],[c_38187]) ).
cnf(c_16828,plain,
( ~ hskp20
| hskp21
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16807,c_84]) ).
cnf(c_38188,plain,
( hskp11
| hskp1
| hskp21
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16828,c_15114]) ).
cnf(c_38189,plain,
( hskp11
| hskp21
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38188]) ).
cnf(c_16830,plain,
( hskp21
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38189]) ).
cnf(c_16831,plain,
( c3_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16830,c_87]) ).
cnf(c_38190,negated_conjecture,
( hskp11
| hskp10
| c2_1(a336)
| c0_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16831,c_264]) ).
cnf(c_16847,negated_conjecture,
( hskp10
| c2_1(a336)
| c0_1(a336)
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38190]) ).
cnf(c_16864,plain,
( ~ hskp21
| hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16847,c_88]) ).
cnf(c_38191,plain,
( hskp11
| hskp1
| hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16864,c_16830]) ).
cnf(c_38192,plain,
( hskp11
| hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38191]) ).
cnf(c_16865,plain,
( hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38192]) ).
cnf(c_38193,plain,
( hskp1
| c1_1(a336)
| c0_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16865,c_15072]) ).
cnf(c_16866,plain,
( c1_1(a336)
| c0_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38193]) ).
cnf(c_16872,plain,
( ~ hskp21
| c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16866,c_88]) ).
cnf(c_38194,plain,
( hskp11
| hskp1
| c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16872,c_16830]) ).
cnf(c_38195,plain,
( hskp11
| c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38194]) ).
cnf(c_16873,plain,
( c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38195]) ).
cnf(c_16875,plain,
( ~ hskp21
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16873,c_89]) ).
cnf(c_38196,plain,
( hskp11
| hskp1
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16875,c_16830]) ).
cnf(c_38197,plain,
( hskp11
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38196]) ).
cnf(c_16879,plain,
( hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_38197]) ).
cnf(c_16880,plain,
( c2_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16879,c_8]) ).
cnf(c_16881,plain,
( c0_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16879,c_7]) ).
cnf(c_38198,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(a295)
| c1_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16881,c_246]) ).
cnf(c_16891,negated_conjecture,
( hskp20
| ~ c2_1(a295)
| c1_1(a295)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38198]) ).
cnf(c_38199,plain,
( hskp10
| hskp11
| hskp20
| c1_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16891,c_16880]) ).
cnf(c_38200,plain,
( hskp10
| hskp20
| c1_1(a295)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38199]) ).
cnf(c_16896,plain,
( hskp20
| c1_1(a295)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38200]) ).
cnf(c_16897,plain,
( ~ hskp1
| hskp20
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16896,c_9]) ).
cnf(c_38201,plain,
( hskp10
| hskp11
| hskp20
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16897,c_16879]) ).
cnf(c_38202,plain,
( hskp10
| hskp20
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38201]) ).
cnf(c_16898,plain,
( hskp20
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38202]) ).
cnf(c_16902,plain,
( c1_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16898,c_83]) ).
cnf(c_16903,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16902,c_15085]) ).
cnf(c_38203,plain,
( hskp4
| ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15975,c_15117]) ).
cnf(c_16974,plain,
( ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38203]) ).
cnf(c_38204,plain,
( hskp4
| hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_16974,c_15116]) ).
cnf(c_16978,plain,
( hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38204]) ).
cnf(c_16984,plain,
( ~ hskp1
| hskp13
| hskp4 ),
inference(resolve,[status(thm)],[c_16978,c_9]) ).
cnf(c_38205,plain,
( hskp4
| hskp13
| hskp4 ),
inference(resolve,[status(thm)],[c_16984,c_15115]) ).
cnf(c_16988,plain,
( hskp13
| hskp4 ),
inference(copy,[status(thm)],[c_38205]) ).
cnf(c_16994,plain,
( c3_1(a313)
| hskp4 ),
inference(resolve,[status(thm)],[c_16988,c_56]) ).
cnf(c_16995,plain,
( c0_1(a313)
| hskp4 ),
inference(resolve,[status(thm)],[c_16988,c_55]) ).
cnf(c_38206,negated_conjecture,
( hskp4
| ~ c0_1(a313)
| c1_1(a313)
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A)
| hskp4 ),
inference(resolve,[status(thm)],[c_16994,c_249]) ).
cnf(c_17043,negated_conjecture,
( ~ c0_1(a313)
| c1_1(a313)
| ~ c2_1(A)
| ~ c0_1(A)
| c1_1(A)
| hskp4 ),
inference(copy,[status(thm)],[c_38206]) ).
cnf(c_38207,negated_conjecture,
( hskp11
| hskp10
| c2_1(a333)
| c0_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16903,c_264]) ).
cnf(c_38208,negated_conjecture,
( hskp11
| hskp10
| c2_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38207]) ).
cnf(c_38209,negated_conjecture,
( hskp11
| hskp10
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38208]) ).
cnf(c_38210,negated_conjecture,
( hskp11
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38209]) ).
cnf(c_17310,negated_conjecture,
( c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38210]) ).
cnf(c_38211,negated_conjecture,
( hskp21
| c3_1(a333)
| c2_1(a333)
| c2_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17310,c_244]) ).
cnf(c_17316,negated_conjecture,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38211]) ).
cnf(c_17331,plain,
( ~ hskp20
| hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17316,c_85]) ).
cnf(c_38212,plain,
( hskp10
| hskp11
| hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17331,c_16898]) ).
cnf(c_38213,plain,
( hskp10
| hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38212]) ).
cnf(c_17336,plain,
( hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38213]) ).
cnf(c_17350,plain,
( ~ hskp20
| hskp21
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17336,c_84]) ).
cnf(c_38214,plain,
( hskp10
| hskp11
| hskp21
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17350,c_16898]) ).
cnf(c_38215,plain,
( hskp10
| hskp21
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38214]) ).
cnf(c_17351,plain,
( hskp21
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38215]) ).
cnf(c_17352,plain,
( c3_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17351,c_87]) ).
cnf(c_38216,negated_conjecture,
( hskp11
| hskp10
| c2_1(a336)
| c0_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17352,c_264]) ).
cnf(c_38217,negated_conjecture,
( hskp11
| c2_1(a336)
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38216]) ).
cnf(c_17370,negated_conjecture,
( c2_1(a336)
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38217]) ).
cnf(c_17371,plain,
( hskp0
| hskp14
| ~ c2_1(a336)
| c0_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17352,c_258]) ).
cnf(c_17385,plain,
( ~ hskp21
| c2_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17370,c_88]) ).
cnf(c_38218,plain,
( hskp10
| hskp11
| c2_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17385,c_17351]) ).
cnf(c_38219,plain,
( hskp10
| c2_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38218]) ).
cnf(c_17386,plain,
( c2_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38219]) ).
cnf(c_38220,plain,
( hskp10
| hskp11
| hskp0
| hskp14
| c0_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17371,c_17386]) ).
cnf(c_38221,plain,
( hskp10
| hskp0
| hskp14
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38220]) ).
cnf(c_17601,plain,
( hskp0
| hskp14
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38221]) ).
cnf(c_17604,plain,
( ~ hskp21
| hskp0
| hskp14
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17601,c_88]) ).
cnf(c_38222,plain,
( hskp10
| hskp11
| hskp0
| hskp14
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17604,c_17351]) ).
cnf(c_38223,plain,
( hskp10
| hskp0
| hskp14
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38222]) ).
cnf(c_17605,plain,
( hskp0
| hskp14
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38223]) ).
cnf(c_17607,plain,
( c1_1(a315)
| hskp0
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_17605,c_59]) ).
cnf(c_18044,plain,
( hskp1
| hskp11
| ~ c2_1(A)
| ~ c0_1(A)
| c3_1(A) ),
inference(resolve,[status(thm)],[c_15082,c_15084]) ).
cnf(c_38224,plain,
( hskp0
| hskp10
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| c0_1(a315) ),
inference(resolve,[status(thm)],[c_3254,c_17607]) ).
cnf(c_38225,plain,
( hskp0
| hskp10
| hskp10
| hskp0
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| c0_1(a315) ),
inference(copy,[status(thm)],[c_38224]) ).
cnf(c_38226,plain,
( hskp0
| hskp10
| hskp0
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| c0_1(a315) ),
inference(copy,[status(thm)],[c_38225]) ).
cnf(c_18099,plain,
( hskp10
| hskp0
| hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| c0_1(a315) ),
inference(copy,[status(thm)],[c_38226]) ).
cnf(c_38227,plain,
( hskp12
| hskp1
| hskp8
| c3_1(a330)
| c0_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_15320,c_15214]) ).
cnf(c_38228,plain,
( hskp12
| hskp8
| c3_1(a330)
| c0_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38227]) ).
cnf(c_18216,plain,
( hskp8
| c3_1(a330)
| c0_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38228]) ).
cnf(c_18223,plain,
( ~ hskp19
| hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18216,c_81]) ).
cnf(c_38229,plain,
( hskp12
| hskp1
| hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18223,c_15113]) ).
cnf(c_38230,plain,
( hskp12
| hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38229]) ).
cnf(c_18225,plain,
( hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38230]) ).
cnf(c_38231,plain,
( hskp1
| hskp11
| ~ c2_1(a330)
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18225,c_18044]) ).
cnf(c_18227,plain,
( hskp11
| ~ c2_1(a330)
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38231]) ).
cnf(c_38232,plain,
( hskp12
| hskp1
| hskp11
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18227,c_15213]) ).
cnf(c_38233,plain,
( hskp12
| hskp11
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38232]) ).
cnf(c_18237,plain,
( hskp11
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38233]) ).
cnf(c_18242,plain,
( ~ hskp19
| hskp11
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18237,c_81]) ).
cnf(c_38234,plain,
( hskp12
| hskp1
| hskp11
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18242,c_15113]) ).
cnf(c_38235,plain,
( hskp12
| hskp11
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38234]) ).
cnf(c_18244,plain,
( hskp11
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38235]) ).
cnf(c_18246,plain,
( c2_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18244,c_35]) ).
cnf(c_38236,plain,
( hskp1
| c1_1(a305)
| c0_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18246,c_15072]) ).
cnf(c_18247,plain,
( c1_1(a305)
| c0_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38236]) ).
cnf(c_18256,plain,
( ~ hskp8
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18247,c_36]) ).
cnf(c_38237,plain,
( hskp11
| hskp12
| hskp1
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18256,c_18244]) ).
cnf(c_38238,plain,
( hskp11
| hskp12
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38237]) ).
cnf(c_38239,plain,
( hskp11
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38238]) ).
cnf(c_18257,plain,
( c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38239]) ).
cnf(c_18265,plain,
( ~ hskp8
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18257,c_37]) ).
cnf(c_38240,plain,
( hskp11
| hskp12
| hskp1
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_18265,c_18244]) ).
cnf(c_38241,plain,
( hskp11
| hskp12
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38240]) ).
cnf(c_38242,plain,
( hskp11
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38241]) ).
cnf(c_18266,plain,
( hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_38242]) ).
cnf(c_18267,plain,
( c2_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18266,c_8]) ).
cnf(c_18268,plain,
( c0_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18266,c_7]) ).
cnf(c_38243,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(a295)
| c1_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18268,c_246]) ).
cnf(c_18286,negated_conjecture,
( hskp20
| ~ c2_1(a295)
| c1_1(a295)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38243]) ).
cnf(c_38244,plain,
( hskp11
| hskp12
| hskp20
| c1_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18286,c_18267]) ).
cnf(c_38245,plain,
( hskp11
| hskp20
| c1_1(a295)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38244]) ).
cnf(c_18315,plain,
( hskp20
| c1_1(a295)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38245]) ).
cnf(c_18317,plain,
( ~ hskp1
| hskp20
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18315,c_9]) ).
cnf(c_38246,plain,
( hskp11
| hskp12
| hskp20
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18317,c_18266]) ).
cnf(c_38247,plain,
( hskp11
| hskp20
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38246]) ).
cnf(c_18318,plain,
( hskp20
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38247]) ).
cnf(c_18319,plain,
( c1_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18318,c_83]) ).
cnf(c_18320,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18319,c_15085]) ).
cnf(c_18482,plain,
( ~ hskp20
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18320,c_85]) ).
cnf(c_38248,plain,
( hskp11
| hskp12
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18482,c_18318]) ).
cnf(c_38249,plain,
( hskp11
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38248]) ).
cnf(c_18491,plain,
( c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38249]) ).
cnf(c_38250,negated_conjecture,
( hskp12
| c3_1(a333)
| c2_1(a333)
| ~ c2_1(A)
| ~ c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18491,c_261]) ).
cnf(c_38251,negated_conjecture,
( hskp12
| c3_1(a333)
| ~ c2_1(A)
| ~ c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38250]) ).
cnf(c_18495,negated_conjecture,
( c3_1(a333)
| ~ c2_1(A)
| ~ c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38251]) ).
cnf(c_18744,plain,
( ~ hskp2
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_15942,c_13]) ).
cnf(c_38252,plain,
( hskp20
| hskp11
| hskp0
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_18744,c_15273]) ).
cnf(c_38253,plain,
( hskp20
| hskp11
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_38252]) ).
cnf(c_38254,plain,
( hskp20
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_38253]) ).
cnf(c_18745,plain,
( hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_38254]) ).
cnf(c_18751,plain,
( ~ hskp2
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_18745,c_12]) ).
cnf(c_38255,plain,
( hskp20
| hskp11
| hskp0
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_18751,c_15273]) ).
cnf(c_38256,plain,
( hskp20
| hskp11
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_38255]) ).
cnf(c_38257,plain,
( hskp20
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_38256]) ).
cnf(c_18756,plain,
( hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_38257]) ).
cnf(c_18763,plain,
( hskp8
| ~ c1_1(a297)
| c3_1(a297)
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_18756,c_222]) ).
cnf(c_18828,plain,
( ~ hskp2
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_15953,c_13]) ).
cnf(c_38258,plain,
( hskp12
| hskp11
| hskp0
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_18828,c_1077]) ).
cnf(c_38259,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_38258]) ).
cnf(c_38260,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_38259]) ).
cnf(c_18849,plain,
( hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_38260]) ).
cnf(c_18855,plain,
( ~ hskp2
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_18849,c_12]) ).
cnf(c_38261,plain,
( hskp12
| hskp11
| hskp0
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_18855,c_1077]) ).
cnf(c_38262,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_38261]) ).
cnf(c_38263,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_38262]) ).
cnf(c_18857,plain,
( hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_38263]) ).
cnf(c_38264,plain,
( hskp11
| hskp12
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a297)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_18857,c_570]) ).
cnf(c_38265,plain,
( hskp11
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a297)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38264]) ).
cnf(c_18860,plain,
( c3_1(a349)
| c2_1(a349)
| ~ c1_1(a297)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38265]) ).
cnf(c_20632,plain,
( ~ hskp0
| c0_1(a321)
| c2_1(a294)
| c1_1(a294)
| c0_1(a294) ),
inference(resolve,[status(thm)],[c_15083,c_5]) ).
cnf(c_21553,plain,
( ~ hskp26
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349)
| c0_1(a315) ),
inference(resolve,[status(thm)],[c_18099,c_109]) ).
cnf(c_38266,negated_conjecture,
( hskp12
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349)
| c0_1(a315) ),
inference(resolve,[status(thm)],[c_21553,c_179]) ).
cnf(c_38267,negated_conjecture,
( hskp12
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349)
| c0_1(a315) ),
inference(copy,[status(thm)],[c_38266]) ).
cnf(c_21556,negated_conjecture,
( hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349)
| c0_1(a315) ),
inference(copy,[status(thm)],[c_38267]) ).
cnf(c_21563,plain,
( ~ hskp14
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_21556,c_61]) ).
cnf(c_38268,plain,
( hskp0
| hskp10
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_21563,c_17605]) ).
cnf(c_38269,plain,
( hskp0
| hskp10
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(copy,[status(thm)],[c_38268]) ).
cnf(c_38270,plain,
( hskp0
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(copy,[status(thm)],[c_38269]) ).
cnf(c_21565,plain,
( hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(copy,[status(thm)],[c_38270]) ).
cnf(c_21574,plain,
( ~ hskp26
| hskp10
| hskp0
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21565,c_108]) ).
cnf(c_38271,negated_conjecture,
( hskp12
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21574,c_179]) ).
cnf(c_38272,negated_conjecture,
( hskp12
| hskp10
| hskp0
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38271]) ).
cnf(c_21576,negated_conjecture,
( hskp10
| hskp0
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38272]) ).
cnf(c_38273,plain,
( hskp10
| hskp12
| hskp11
| c2_1(a294)
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21576,c_13379]) ).
cnf(c_38274,plain,
( hskp10
| hskp12
| c2_1(a294)
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38273]) ).
cnf(c_38275,plain,
( hskp10
| c2_1(a294)
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38274]) ).
cnf(c_21577,plain,
( c2_1(a294)
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38275]) ).
cnf(c_21589,plain,
( ~ hskp0
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21577,c_4]) ).
cnf(c_38276,plain,
( hskp10
| hskp11
| hskp12
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21589,c_21576]) ).
cnf(c_38277,plain,
( hskp10
| hskp11
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38276]) ).
cnf(c_38278,plain,
( hskp10
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38277]) ).
cnf(c_21591,plain,
( c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38278]) ).
cnf(c_21592,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21591,c_15085]) ).
cnf(c_38279,negated_conjecture,
( hskp11
| hskp10
| c2_1(a294)
| c0_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21592,c_264]) ).
cnf(c_38280,negated_conjecture,
( hskp11
| hskp10
| c2_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38279]) ).
cnf(c_38281,negated_conjecture,
( hskp11
| hskp10
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38280]) ).
cnf(c_38282,negated_conjecture,
( hskp11
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38281]) ).
cnf(c_21627,negated_conjecture,
( c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38282]) ).
cnf(c_21632,plain,
( ~ hskp0
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21627,c_3]) ).
cnf(c_38283,plain,
( hskp10
| hskp11
| hskp12
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21632,c_21576]) ).
cnf(c_38284,plain,
( hskp10
| hskp11
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38283]) ).
cnf(c_38285,plain,
( hskp10
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38284]) ).
cnf(c_21636,plain,
( c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38285]) ).
cnf(c_21652,plain,
( ~ hskp0
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21636,c_4]) ).
cnf(c_38286,plain,
( hskp10
| hskp11
| hskp12
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21652,c_21576]) ).
cnf(c_38287,plain,
( hskp10
| hskp11
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38286]) ).
cnf(c_38288,plain,
( hskp10
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38287]) ).
cnf(c_21653,plain,
( hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38288]) ).
cnf(c_21654,plain,
( c3_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21653,c_44]) ).
cnf(c_21655,plain,
( c1_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21653,c_43]) ).
cnf(c_21663,plain,
( ~ c0_1(a321)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21654,c_15081]) ).
cnf(c_21683,plain,
( ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21654,c_240]) ).
cnf(c_21686,plain,
( hskp28
| ~ c2_1(a308)
| ~ c1_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21654,c_231]) ).
cnf(c_38289,plain,
( hskp20
| hskp11
| hskp0
| hskp8
| c3_1(a297)
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_18763,c_15364]) ).
cnf(c_38290,plain,
( hskp20
| hskp11
| hskp8
| c3_1(a297)
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38289]) ).
cnf(c_38291,plain,
( hskp20
| hskp8
| c3_1(a297)
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38290]) ).
cnf(c_22105,plain,
( hskp8
| c3_1(a297)
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38291]) ).
cnf(c_22111,plain,
( ~ hskp2
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22105,c_13]) ).
cnf(c_38292,plain,
( hskp20
| hskp11
| hskp0
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22111,c_15273]) ).
cnf(c_38293,plain,
( hskp20
| hskp11
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38292]) ).
cnf(c_38294,plain,
( hskp20
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38293]) ).
cnf(c_22112,plain,
( hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38294]) ).
cnf(c_22120,plain,
( ~ hskp2
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22112,c_12]) ).
cnf(c_38295,plain,
( hskp20
| hskp11
| hskp0
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22120,c_15273]) ).
cnf(c_38296,plain,
( hskp20
| hskp11
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38295]) ).
cnf(c_38297,plain,
( hskp20
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38296]) ).
cnf(c_22121,plain,
( hskp8
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38297]) ).
cnf(c_22122,plain,
( c1_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22121,c_83]) ).
cnf(c_22124,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22122,c_15085]) ).
cnf(c_22167,plain,
( ~ hskp20
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22124,c_85]) ).
cnf(c_38298,plain,
( hskp8
| hskp11
| hskp0
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22167,c_22121]) ).
cnf(c_38299,plain,
( hskp8
| hskp11
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38298]) ).
cnf(c_38300,plain,
( hskp8
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38299]) ).
cnf(c_22168,plain,
( c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38300]) ).
cnf(c_38301,negated_conjecture,
( hskp21
| c3_1(a333)
| c2_1(a333)
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22168,c_244]) ).
cnf(c_22172,negated_conjecture,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38301]) ).
cnf(c_22187,plain,
( ~ hskp20
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22172,c_85]) ).
cnf(c_38302,plain,
( hskp8
| hskp11
| hskp0
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22187,c_22121]) ).
cnf(c_38303,plain,
( hskp8
| hskp11
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38302]) ).
cnf(c_38304,plain,
( hskp8
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38303]) ).
cnf(c_22188,plain,
( hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38304]) ).
cnf(c_22196,plain,
( ~ hskp20
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22188,c_84]) ).
cnf(c_38305,plain,
( hskp8
| hskp11
| hskp0
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22196,c_22121]) ).
cnf(c_38306,plain,
( hskp8
| hskp11
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38305]) ).
cnf(c_38307,plain,
( hskp8
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38306]) ).
cnf(c_22197,plain,
( hskp21
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38307]) ).
cnf(c_22203,plain,
( c3_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22197,c_87]) ).
cnf(c_38308,negated_conjecture,
( hskp0
| hskp2
| c1_1(a336)
| c0_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22203,c_274]) ).
cnf(c_22211,negated_conjecture,
( hskp2
| c1_1(a336)
| c0_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38308]) ).
cnf(c_22227,plain,
( ~ hskp21
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22211,c_88]) ).
cnf(c_38309,plain,
( hskp8
| hskp11
| hskp0
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22227,c_22197]) ).
cnf(c_38310,plain,
( hskp8
| hskp11
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38309]) ).
cnf(c_38311,plain,
( hskp8
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38310]) ).
cnf(c_22228,plain,
( hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38311]) ).
cnf(c_22231,plain,
( ~ hskp21
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22228,c_89]) ).
cnf(c_38312,plain,
( hskp8
| hskp11
| hskp0
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22231,c_22197]) ).
cnf(c_38313,plain,
( hskp8
| hskp11
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38312]) ).
cnf(c_38314,plain,
( hskp8
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38313]) ).
cnf(c_22232,plain,
( hskp2
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38314]) ).
cnf(c_22233,plain,
( c1_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22232,c_11]) ).
cnf(c_22234,plain,
( c3_1(a297)
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22233,c_15085]) ).
cnf(c_22268,plain,
( ~ hskp2
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22234,c_13]) ).
cnf(c_38315,plain,
( hskp8
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22268,c_22232]) ).
cnf(c_38316,plain,
( hskp8
| hskp11
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38315]) ).
cnf(c_38317,plain,
( hskp8
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38316]) ).
cnf(c_22273,plain,
( c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38317]) ).
cnf(c_22278,plain,
( ~ hskp2
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22273,c_12]) ).
cnf(c_38318,plain,
( hskp8
| hskp11
| hskp0
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22278,c_22232]) ).
cnf(c_38319,plain,
( hskp8
| hskp11
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38318]) ).
cnf(c_38320,plain,
( hskp8
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38319]) ).
cnf(c_22279,plain,
( c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38320]) ).
cnf(c_38321,plain,
( hskp8
| ~ c1_1(a297)
| c3_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22279,c_222]) ).
cnf(c_22286,plain,
( ~ c1_1(a297)
| c3_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38321]) ).
cnf(c_38322,plain,
( hskp8
| hskp11
| hskp0
| c3_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22286,c_22233]) ).
cnf(c_38323,plain,
( hskp8
| hskp11
| c3_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38322]) ).
cnf(c_38324,plain,
( hskp8
| c3_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38323]) ).
cnf(c_22304,plain,
( c3_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38324]) ).
cnf(c_22311,plain,
( ~ hskp2
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22304,c_13]) ).
cnf(c_38325,plain,
( hskp8
| hskp11
| hskp0
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22311,c_22232]) ).
cnf(c_38326,plain,
( hskp8
| hskp11
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38325]) ).
cnf(c_38327,plain,
( hskp8
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38326]) ).
cnf(c_22312,plain,
( c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38327]) ).
cnf(c_22324,plain,
( ~ hskp2
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22312,c_12]) ).
cnf(c_38328,plain,
( hskp8
| hskp11
| hskp0
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22324,c_22232]) ).
cnf(c_38329,plain,
( hskp8
| hskp11
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38328]) ).
cnf(c_38330,plain,
( hskp8
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38329]) ).
cnf(c_22327,plain,
( hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38330]) ).
cnf(c_22328,plain,
( c2_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22327,c_35]) ).
cnf(c_22329,plain,
( hskp1
| c1_1(a305)
| c0_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22328,c_15072]) ).
cnf(c_22348,plain,
( ~ hskp8
| hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22329,c_36]) ).
cnf(c_38331,plain,
( hskp11
| hskp0
| hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22348,c_22327]) ).
cnf(c_38332,plain,
( hskp11
| hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38331]) ).
cnf(c_22351,plain,
( hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38332]) ).
cnf(c_22353,plain,
( ~ hskp8
| hskp1
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22351,c_37]) ).
cnf(c_38333,plain,
( hskp11
| hskp0
| hskp1
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22353,c_22327]) ).
cnf(c_38334,plain,
( hskp11
| hskp1
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38333]) ).
cnf(c_22354,plain,
( hskp1
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38334]) ).
cnf(c_22355,plain,
( c2_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22354,c_8]) ).
cnf(c_22356,plain,
( c0_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22354,c_7]) ).
cnf(c_38335,negated_conjecture,
( hskp20
| hskp11
| ~ c2_1(a295)
| c1_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22356,c_246]) ).
cnf(c_22370,negated_conjecture,
( hskp20
| ~ c2_1(a295)
| c1_1(a295)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38335]) ).
cnf(c_38336,plain,
( hskp11
| hskp0
| hskp20
| c1_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22370,c_22355]) ).
cnf(c_38337,plain,
( hskp11
| hskp20
| c1_1(a295)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38336]) ).
cnf(c_22387,plain,
( hskp20
| c1_1(a295)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38337]) ).
cnf(c_22388,plain,
( ~ hskp1
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22387,c_9]) ).
cnf(c_38338,plain,
( hskp11
| hskp0
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22388,c_22354]) ).
cnf(c_38339,plain,
( hskp11
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38338]) ).
cnf(c_22399,plain,
( hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38339]) ).
cnf(c_22400,plain,
( c1_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22399,c_83]) ).
cnf(c_22402,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22400,c_15085]) ).
cnf(c_22464,plain,
( ~ hskp20
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22402,c_85]) ).
cnf(c_38340,plain,
( hskp11
| hskp0
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22464,c_22399]) ).
cnf(c_38341,plain,
( hskp11
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38340]) ).
cnf(c_22465,plain,
( c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38341]) ).
cnf(c_38342,negated_conjecture,
( hskp0
| ~ c1_1(a333)
| c2_1(a333)
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22465,c_280]) ).
cnf(c_38343,negated_conjecture,
( hskp0
| ~ c1_1(a333)
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38342]) ).
cnf(c_22466,negated_conjecture,
( ~ c1_1(a333)
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38343]) ).
cnf(c_38344,negated_conjecture,
( hskp21
| c3_1(a333)
| c2_1(a333)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22465,c_244]) ).
cnf(c_22469,negated_conjecture,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38344]) ).
cnf(c_22478,plain,
( ~ hskp20
| hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22469,c_85]) ).
cnf(c_38345,plain,
( hskp11
| hskp0
| hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22478,c_22399]) ).
cnf(c_38346,plain,
( hskp11
| hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38345]) ).
cnf(c_22479,plain,
( hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38346]) ).
cnf(c_22485,plain,
( ~ hskp20
| hskp21
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22479,c_84]) ).
cnf(c_38347,plain,
( hskp11
| hskp0
| hskp21
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22485,c_22399]) ).
cnf(c_38348,plain,
( hskp11
| hskp21
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38347]) ).
cnf(c_22486,plain,
( hskp21
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38348]) ).
cnf(c_22487,plain,
( c3_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22486,c_87]) ).
cnf(c_38349,negated_conjecture,
( hskp0
| hskp2
| c1_1(a336)
| c0_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22487,c_274]) ).
cnf(c_22495,negated_conjecture,
( hskp2
| c1_1(a336)
| c0_1(a336)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38349]) ).
cnf(c_22513,plain,
( ~ hskp21
| hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22495,c_88]) ).
cnf(c_38350,plain,
( hskp11
| hskp0
| hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22513,c_22486]) ).
cnf(c_38351,plain,
( hskp11
| hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38350]) ).
cnf(c_22514,plain,
( hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38351]) ).
cnf(c_22517,plain,
( ~ hskp21
| hskp2
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22514,c_89]) ).
cnf(c_38352,plain,
( hskp11
| hskp0
| hskp2
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22517,c_22486]) ).
cnf(c_38353,plain,
( hskp11
| hskp2
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38352]) ).
cnf(c_22518,plain,
( hskp2
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38353]) ).
cnf(c_22519,plain,
( c1_1(a297)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22518,c_11]) ).
cnf(c_38354,plain,
( hskp4
| ~ c0_1(a313)
| c1_1(a313)
| ~ c2_1(a295)
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_17043,c_15117]) ).
cnf(c_24309,plain,
( ~ c0_1(a313)
| c1_1(a313)
| ~ c2_1(a295)
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38354]) ).
cnf(c_38355,plain,
( hskp4
| c1_1(a313)
| ~ c2_1(a295)
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_24309,c_16995]) ).
cnf(c_24317,plain,
( c1_1(a313)
| ~ c2_1(a295)
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38355]) ).
cnf(c_38356,plain,
( hskp4
| c1_1(a313)
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_24317,c_15116]) ).
cnf(c_24323,plain,
( c1_1(a313)
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38356]) ).
cnf(c_24327,plain,
( ~ hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_24323,c_57]) ).
cnf(c_38357,plain,
( hskp4
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_24327,c_16988]) ).
cnf(c_24328,plain,
( c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_38357]) ).
cnf(c_24342,plain,
( ~ hskp1
| hskp4 ),
inference(resolve,[status(thm)],[c_24328,c_9]) ).
cnf(c_38358,plain,
( hskp4
| hskp4 ),
inference(resolve,[status(thm)],[c_24342,c_15115]) ).
cnf(c_24348,plain,
hskp4,
inference(copy,[status(thm)],[c_38358]) ).
cnf(c_24352,negated_conjecture,
~ c2_1(a300),
inference(resolve,[status(thm)],[c_24348,c_21]) ).
cnf(c_24353,negated_conjecture,
~ c1_1(a300),
inference(resolve,[status(thm)],[c_24348,c_20]) ).
cnf(c_24354,negated_conjecture,
~ c0_1(a300),
inference(resolve,[status(thm)],[c_24348,c_19]) ).
cnf(c_38359,plain,
( hskp11
| hskp0
| c3_1(a349)
| c2_1(a349)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_18860,c_22519]) ).
cnf(c_38360,plain,
( hskp11
| c3_1(a349)
| c2_1(a349)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38359]) ).
cnf(c_25491,plain,
( c3_1(a349)
| c2_1(a349)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38360]) ).
cnf(c_25510,plain,
( ~ hskp26
| c2_1(a349)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_25491,c_109]) ).
cnf(c_38361,negated_conjecture,
( hskp12
| hskp11
| c2_1(a349)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_25510,c_179]) ).
cnf(c_38362,negated_conjecture,
( hskp12
| c2_1(a349)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38361]) ).
cnf(c_25512,negated_conjecture,
( c2_1(a349)
| c0_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38362]) ).
cnf(c_25524,plain,
( ~ hskp2
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_25512,c_12]) ).
cnf(c_38363,plain,
( hskp11
| hskp0
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_25524,c_22518]) ).
cnf(c_38364,plain,
( hskp11
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38363]) ).
cnf(c_25526,plain,
( c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38364]) ).
cnf(c_25535,plain,
( ~ hskp26
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_25526,c_108]) ).
cnf(c_38365,negated_conjecture,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_25535,c_179]) ).
cnf(c_38366,negated_conjecture,
( hskp12
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38365]) ).
cnf(c_25539,negated_conjecture,
( hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38366]) ).
cnf(c_25540,plain,
( c0_1(a321)
| c2_1(a294)
| c1_1(a294)
| c0_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25539,c_20632]) ).
cnf(c_25547,plain,
( ~ hskp0
| c0_1(a321)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25540,c_3]) ).
cnf(c_38367,plain,
( hskp12
| hskp11
| c0_1(a321)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25547,c_25539]) ).
cnf(c_38368,plain,
( hskp12
| c0_1(a321)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38367]) ).
cnf(c_25548,plain,
( c0_1(a321)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38368]) ).
cnf(c_38369,plain,
( ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25548,c_21663]) ).
cnf(c_38370,plain,
( ~ c1_1(a308)
| c2_1(a308)
| hskp11
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38369]) ).
cnf(c_25559,plain,
( ~ c1_1(a308)
| c2_1(a308)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38370]) ).
cnf(c_38371,plain,
( hskp11
| hskp12
| c2_1(a308)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25559,c_21655]) ).
cnf(c_38372,plain,
( hskp11
| c2_1(a308)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38371]) ).
cnf(c_25577,plain,
( c2_1(a308)
| c2_1(a294)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38372]) ).
cnf(c_25584,plain,
( ~ hskp0
| c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25577,c_4]) ).
cnf(c_38373,plain,
( hskp12
| hskp11
| c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25584,c_25539]) ).
cnf(c_38374,plain,
( hskp12
| c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38373]) ).
cnf(c_25588,plain,
( c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38374]) ).
cnf(c_38375,plain,
( hskp28
| ~ c1_1(a308)
| hskp11
| hskp12
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25588,c_21686]) ).
cnf(c_38376,plain,
( hskp28
| ~ c1_1(a308)
| hskp11
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38375]) ).
cnf(c_25589,plain,
( hskp28
| ~ c1_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38376]) ).
cnf(c_38377,plain,
( hskp11
| hskp12
| hskp28
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25589,c_21655]) ).
cnf(c_38378,plain,
( hskp11
| hskp28
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38377]) ).
cnf(c_25596,plain,
( hskp28
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38378]) ).
cnf(c_25598,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25596,c_15085]) ).
cnf(c_25629,plain,
( ~ hskp0
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25598,c_5]) ).
cnf(c_38379,plain,
( hskp12
| hskp11
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25629,c_25539]) ).
cnf(c_38380,plain,
( hskp12
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38379]) ).
cnf(c_25636,plain,
( c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38380]) ).
cnf(c_25640,plain,
( ~ hskp0
| c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25636,c_3]) ).
cnf(c_38381,plain,
( hskp12
| hskp11
| c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25640,c_25539]) ).
cnf(c_38382,plain,
( hskp12
| c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38381]) ).
cnf(c_25641,plain,
( c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38382]) ).
cnf(c_25652,plain,
( ~ hskp0
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25641,c_4]) ).
cnf(c_38383,plain,
( hskp12
| hskp11
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25652,c_25539]) ).
cnf(c_38384,plain,
( hskp12
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38383]) ).
cnf(c_25663,plain,
( hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_38384]) ).
cnf(c_25664,plain,
( c3_1(a353)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25663,c_117]) ).
cnf(c_25665,plain,
( c2_1(a353)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25663,c_116]) ).
cnf(c_25666,plain,
( c1_1(a353)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_25663,c_115]) ).
cnf(c_26731,plain,
( ~ hskp0
| c0_1(a321)
| c2_1(a294)
| c0_1(a294)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_15071,c_5]) ).
cnf(c_38385,plain,
( hskp12
| hskp11
| c3_1(a333)
| ~ c1_1(a353)
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_18495,c_25665]) ).
cnf(c_38386,plain,
( hskp12
| c3_1(a333)
| ~ c1_1(a353)
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38385]) ).
cnf(c_30165,plain,
( c3_1(a333)
| ~ c1_1(a353)
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38386]) ).
cnf(c_38387,plain,
( hskp12
| hskp11
| c3_1(a333)
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30165,c_25666]) ).
cnf(c_38388,plain,
( hskp12
| c3_1(a333)
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38387]) ).
cnf(c_30173,plain,
( c3_1(a333)
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38388]) ).
cnf(c_30192,plain,
( ~ hskp20
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30173,c_85]) ).
cnf(c_38389,plain,
( hskp11
| hskp12
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30192,c_18318]) ).
cnf(c_38390,plain,
( hskp11
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38389]) ).
cnf(c_30195,plain,
( c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38390]) ).
cnf(c_38391,plain,
( hskp12
| hskp11
| ~ c2_1(a353)
| ~ c0_1(a353)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21683,c_25664]) ).
cnf(c_38392,plain,
( hskp12
| ~ c2_1(a353)
| ~ c0_1(a353)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38391]) ).
cnf(c_30704,plain,
( ~ c2_1(a353)
| ~ c0_1(a353)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38392]) ).
cnf(c_38393,plain,
( c2_1(a333)
| hskp11
| hskp12
| ~ c2_1(a353)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30704,c_30195]) ).
cnf(c_38394,plain,
( c2_1(a333)
| hskp11
| ~ c2_1(a353)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38393]) ).
cnf(c_30716,plain,
( c2_1(a333)
| ~ c2_1(a353)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38394]) ).
cnf(c_38395,plain,
( hskp12
| hskp11
| c2_1(a333)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30716,c_25665]) ).
cnf(c_38396,plain,
( hskp12
| c2_1(a333)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38395]) ).
cnf(c_30719,plain,
( c2_1(a333)
| ~ c1_1(a308)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38396]) ).
cnf(c_38397,plain,
( hskp11
| hskp12
| c2_1(a333)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30719,c_21655]) ).
cnf(c_38398,plain,
( hskp11
| c2_1(a333)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38397]) ).
cnf(c_30720,plain,
( c2_1(a333)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38398]) ).
cnf(c_30728,plain,
( ~ hskp20
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30720,c_84]) ).
cnf(c_38399,plain,
( hskp11
| hskp12
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30728,c_18318]) ).
cnf(c_38400,plain,
( hskp11
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38399]) ).
cnf(c_30735,plain,
( c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38400]) ).
cnf(c_38401,plain,
( c3_1(a333)
| ~ c1_1(a308)
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30735,c_18495]) ).
cnf(c_38402,plain,
( c3_1(a333)
| ~ c1_1(a308)
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38401]) ).
cnf(c_30736,plain,
( c3_1(a333)
| ~ c1_1(a308)
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38402]) ).
cnf(c_38403,plain,
( hskp11
| hskp12
| c3_1(a333)
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30736,c_21655]) ).
cnf(c_38404,plain,
( hskp11
| c3_1(a333)
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38403]) ).
cnf(c_30743,plain,
( c3_1(a333)
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38404]) ).
cnf(c_30765,plain,
( ~ hskp20
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30743,c_85]) ).
cnf(c_38405,plain,
( hskp11
| hskp12
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30765,c_18318]) ).
cnf(c_38406,plain,
( hskp11
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38405]) ).
cnf(c_30768,plain,
( c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38406]) ).
cnf(c_30772,plain,
( ~ hskp10
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30768,c_45]) ).
cnf(c_38407,plain,
( hskp11
| hskp12
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30772,c_21653]) ).
cnf(c_38408,plain,
( hskp11
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38407]) ).
cnf(c_30774,plain,
( c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38408]) ).
cnf(c_30790,plain,
( ~ hskp20
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30774,c_84]) ).
cnf(c_38409,plain,
( hskp11
| hskp12
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30790,c_18318]) ).
cnf(c_38410,plain,
( hskp11
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38409]) ).
cnf(c_30793,plain,
( hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_38410]) ).
cnf(c_30794,plain,
( c3_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30793,c_51]) ).
cnf(c_38411,negated_conjecture,
( hskp11
| hskp10
| c2_1(a310)
| c0_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30794,c_264]) ).
cnf(c_30830,negated_conjecture,
( hskp10
| c2_1(a310)
| c0_1(a310)
| hskp11 ),
inference(copy,[status(thm)],[c_38411]) ).
cnf(c_30848,plain,
( ~ hskp12
| hskp10
| c2_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30830,c_52]) ).
cnf(c_38412,plain,
( hskp11
| hskp10
| c2_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30848,c_30793]) ).
cnf(c_30849,plain,
( hskp10
| c2_1(a310)
| hskp11 ),
inference(copy,[status(thm)],[c_38412]) ).
cnf(c_30857,plain,
( ~ hskp12
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_30849,c_53]) ).
cnf(c_38413,plain,
( hskp11
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_30857,c_30793]) ).
cnf(c_30858,plain,
( hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_38413]) ).
cnf(c_30860,plain,
( c3_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30858,c_44]) ).
cnf(c_30861,plain,
( c1_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30858,c_43]) ).
cnf(c_30898,plain,
( ~ c2_1(a308)
| c0_1(a308)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A)
| hskp11 ),
inference(resolve,[status(thm)],[c_30860,c_228]) ).
cnf(c_30914,plain,
( c2_1(a308)
| c0_1(a308)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| hskp11 ),
inference(resolve,[status(thm)],[c_30861,c_15075]) ).
cnf(c_31647,plain,
( ~ hskp0
| c2_1(a308)
| c0_1(a308)
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_30914,c_5]) ).
cnf(c_38414,plain,
( hskp11
| hskp0
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_22466,c_22400]) ).
cnf(c_38415,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38414]) ).
cnf(c_32449,plain,
( c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38415]) ).
cnf(c_38416,negated_conjecture,
( c2_1(a300)
| c1_1(a300)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_32449,c_24354]) ).
cnf(c_38417,negated_conjecture,
( c2_1(a300)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24353,c_38416]) ).
cnf(c_32452,negated_conjecture,
( c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24352,c_38417]) ).
cnf(c_32459,plain,
( ~ hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_32452,c_84]) ).
cnf(c_38418,plain,
( hskp11
| hskp0
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_32459,c_22399]) ).
cnf(c_38419,plain,
( hskp11
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38418]) ).
cnf(c_32461,plain,
( hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_38419]) ).
cnf(c_38420,plain,
( c2_1(a308)
| c0_1(a308)
| c2_1(a294)
| c0_1(a294)
| hskp11
| hskp11 ),
inference(resolve,[status(thm)],[c_32461,c_31647]) ).
cnf(c_32462,plain,
( c2_1(a308)
| c0_1(a308)
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38420]) ).
cnf(c_32475,plain,
( ~ hskp0
| c2_1(a308)
| c0_1(a308)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_32462,c_3]) ).
cnf(c_38421,plain,
( hskp11
| c2_1(a308)
| c0_1(a308)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_32475,c_32461]) ).
cnf(c_32476,plain,
( c2_1(a308)
| c0_1(a308)
| c2_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38421]) ).
cnf(c_32478,plain,
( ~ hskp10
| c2_1(a308)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_32476,c_45]) ).
cnf(c_38422,plain,
( hskp11
| c2_1(a308)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_32478,c_30858]) ).
cnf(c_32479,plain,
( c2_1(a308)
| c2_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38422]) ).
cnf(c_32499,plain,
( ~ hskp0
| c2_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_32479,c_4]) ).
cnf(c_38423,plain,
( hskp11
| c2_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_32499,c_32461]) ).
cnf(c_32506,plain,
( c2_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_38423]) ).
cnf(c_38424,plain,
( hskp11
| c0_1(a308)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A)
| hskp11 ),
inference(resolve,[status(thm)],[c_30898,c_32506]) ).
cnf(c_37711,plain,
( c0_1(a308)
| c2_1(A)
| c3_1(A)
| c1_1(A)
| c0_1(A)
| hskp11 ),
inference(copy,[status(thm)],[c_38424]) ).
cnf(c_37715,plain,
( ~ hskp0
| c0_1(a308)
| c2_1(a294)
| c1_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37711,c_5]) ).
cnf(c_38425,plain,
( hskp11
| c0_1(a308)
| c2_1(a294)
| c1_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37715,c_32461]) ).
cnf(c_37722,plain,
( c0_1(a308)
| c2_1(a294)
| c1_1(a294)
| c0_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38425]) ).
cnf(c_37725,plain,
( ~ hskp0
| c0_1(a308)
| c2_1(a294)
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37722,c_3]) ).
cnf(c_38426,plain,
( hskp11
| c0_1(a308)
| c2_1(a294)
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37725,c_32461]) ).
cnf(c_37726,plain,
( c0_1(a308)
| c2_1(a294)
| c1_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38426]) ).
cnf(c_37729,plain,
( ~ hskp10
| c2_1(a294)
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37726,c_45]) ).
cnf(c_38427,plain,
( hskp11
| c2_1(a294)
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37729,c_30858]) ).
cnf(c_37730,plain,
( c2_1(a294)
| c1_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38427]) ).
cnf(c_37741,plain,
( ~ hskp0
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37730,c_4]) ).
cnf(c_38428,plain,
( hskp11
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37741,c_32461]) ).
cnf(c_37742,plain,
( c1_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38428]) ).
cnf(c_37758,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37742,c_15085]) ).
cnf(c_37812,plain,
( ~ hskp0
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37758,c_5]) ).
cnf(c_38429,plain,
( hskp11
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37812,c_32461]) ).
cnf(c_37813,plain,
( c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38429]) ).
cnf(c_37814,plain,
( ~ hskp0
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37813,c_3]) ).
cnf(c_38430,plain,
( hskp11
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_37814,c_32461]) ).
cnf(c_37815,plain,
( c2_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_38430]) ).
cnf(c_37828,plain,
( ~ hskp0
| hskp11 ),
inference(resolve,[status(thm)],[c_37815,c_4]) ).
cnf(c_38431,plain,
( hskp11
| hskp11 ),
inference(resolve,[status(thm)],[c_37828,c_32461]) ).
cnf(c_37829,plain,
hskp11,
inference(copy,[status(thm)],[c_38431]) ).
cnf(c_37830,negated_conjecture,
~ c2_1(a309),
inference(resolve,[status(thm)],[c_37829,c_49]) ).
cnf(c_37831,negated_conjecture,
c3_1(a309),
inference(resolve,[status(thm)],[c_37829,c_48]) ).
cnf(c_37832,negated_conjecture,
c1_1(a309),
inference(resolve,[status(thm)],[c_37829,c_47]) ).
cnf(c_38432,negated_conjecture,
( ~ c0_1(a321)
| ~ c1_1(a309)
| c2_1(a309) ),
inference(resolve,[status(thm)],[c_37831,c_15081]) ).
cnf(c_38433,negated_conjecture,
( ~ c0_1(a321)
| ~ c1_1(a309) ),
inference(resolve,[status(thm)],[c_37830,c_38432]) ).
cnf(c_37858,negated_conjecture,
~ c0_1(a321),
inference(resolve,[status(thm)],[c_37832,c_38433]) ).
cnf(c_38434,negated_conjecture,
( hskp0
| ~ c1_1(a309)
| c2_1(a309)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_37831,c_15073]) ).
cnf(c_38435,negated_conjecture,
( hskp0
| ~ c1_1(a309)
| c2_1(a309) ),
inference(resolve,[status(thm)],[c_37858,c_38434]) ).
cnf(c_38436,negated_conjecture,
( hskp0
| ~ c1_1(a309) ),
inference(resolve,[status(thm)],[c_37830,c_38435]) ).
cnf(c_37859,negated_conjecture,
hskp0,
inference(resolve,[status(thm)],[c_37832,c_38436]) ).
cnf(c_38437,plain,
( ~ hskp0
| c2_1(a294)
| c0_1(a294)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_37858,c_26731]) ).
cnf(c_38000,plain,
( c2_1(a294)
| c0_1(a294)
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_37859,c_38437]) ).
cnf(c_38027,negated_conjecture,
~ c3_1(a294),
inference(resolve,[status(thm)],[c_37859,c_5]) ).
cnf(c_38028,negated_conjecture,
~ c2_1(a294),
inference(resolve,[status(thm)],[c_37859,c_4]) ).
cnf(c_38029,negated_conjecture,
~ c0_1(a294),
inference(resolve,[status(thm)],[c_37859,c_3]) ).
cnf(c_38438,plain,
( c2_1(a294)
| c3_1(a294)
| c1_1(a294)
| c0_1(a294) ),
inference(factor,[status(thm)],[c_38000]) ).
cnf(c_38439,negated_conjecture,
( c2_1(a294)
| c3_1(a294)
| c1_1(a294) ),
inference(resolve,[status(thm)],[c_38029,c_38438]) ).
cnf(c_38440,negated_conjecture,
( c2_1(a294)
| c1_1(a294) ),
inference(resolve,[status(thm)],[c_38027,c_38439]) ).
cnf(c_38031,negated_conjecture,
c1_1(a294),
inference(resolve,[status(thm)],[c_38028,c_38440]) ).
cnf(c_38441,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294) ),
inference(resolve,[status(thm)],[c_38031,c_15085]) ).
cnf(c_38442,negated_conjecture,
( c3_1(a294)
| c2_1(a294) ),
inference(resolve,[status(thm)],[c_38029,c_38441]) ).
cnf(c_38443,negated_conjecture,
c3_1(a294),
inference(resolve,[status(thm)],[c_38028,c_38442]) ).
cnf(c_38094,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_38027,c_38443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN445+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/5.45 % Computer : n002.cluster.edu
% 0.19/5.45 % Model : x86_64 x86_64
% 0.19/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.45 % Memory : 8046.5625MB
% 0.19/5.45 % OS : Linux 6.8.0-71-generic
% 0.19/5.46 % CPULimit : 300
% 0.19/5.46 % WCLimit : 300
% 0.19/5.46 % DateTime : Sat Sep 26 17:50:15 UTC 2026
% 0.19/5.46 % CPUTime :
% 0.19/5.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/5.46 % Process 2329863 was started by sandbox on n002,
% 0.19/5.46 % Sat Sep 26 17:50:15 2026
% 0.19/5.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.23/5.52
% 0.23/5.52 % From the command line: assign(max_seconds, 300).
% 198.71/31.68
% 198.71/31.68 % given #500 (T,wt=7): 1095 hskp0 | hskp16 | c2_1(a297) | hskp7 | hskp4 | -hskp2. [resolve(512,c,12,b)].
% 198.71/31.68
% 198.71/31.68 % given #1000 (T,wt=5): 3260 hskp16 | hskp12 | hskp8 | hskp23 | hskp24. [resolve(3237,f,715,b),merge(f),merge(g)].
% 198.71/31.68
% 198.71/31.68 % given #1500 (T,wt=7): 5863 hskp6 | hskp17 | hskp5 | hskp4 | hskp2 | hskp0 | -hskp21. [resolve(5853,e,89,b)].
% 198.71/31.68
% 198.71/31.68 % given #2000 (T,wt=7): 8266 c1_1(a349) | c1_1(a329) | hskp13 | hskp16 | hskp17. [resolve(8264,f,696,c),merge(f),merge(g)].
% 198.71/31.68
% 198.71/31.68 % given #2500 (T,wt=11): 5443 hskp11 | hskp7 | hskp10 | hskp4 | hskp0 | c3_1(a297) | -c1_1(a297) | hskp15 | hskp25. [resolve(5433,f,235,c)].
% 198.71/31.68
% 198.71/31.68 % given #3000 (T,wt=8): 13384 c1_1(a346) | c2_1(a346) | hskp11 | hskp12 | hskp10 | hskp15. [resolve(13377,f,2870,e),merge(f),merge(g),merge(h)].
% 198.71/31.68
% 198.71/31.68 % given #3500 (T,wt=6): 15814 hskp0 | hskp4 | c2_1(a297) | hskp22 | -hskp2. [resolve(15384,d,13,b)].
% 198.71/31.68
% 198.71/31.68 % given #4000 (T,wt=5): 18225 hskp1 | hskp12 | c0_1(a330) | hskp8. [resolve(18223,e,15113,b),merge(e),merge(f)].
% 198.71/31.68
% 198.71/31.68 % given #4500 (T,wt=5): 20121 hskp1 | hskp12 | hskp23 | hskp2 | hskp0. [resolve(20120,f,19497,d),merge(f),merge(g),merge(h)].
% 198.71/31.68
% 198.71/31.68 % given #5000 (T,wt=8): 22222 hskp0 | hskp11 | hskp8 | -c1_1(a336) | -c2_1(a336) | hskp28. [resolve(22203,d,231,c)].
% 198.71/31.68
% 198.71/31.68 % given #5500 (T,wt=9): 23893 hskp27 | c2_1(a336) | -c1_1(a336) | -c2_1(a299) | hskp11 | hskp12. [resolve(15154,d,15097,b),merge(g)].
% 198.71/31.68
% 198.71/31.68 % given #6000 (T,wt=8): 26002 hskp0 | hskp27 | hskp6 | c2_1(a320) | c0_1(a321) | -hskp15. [resolve(25994,d,64,b)].
% 198.71/31.68
% 198.71/31.68 % given #6500 (T,wt=11): 26337 hskp12 | hskp11 | c2_1(a299) | -c1_1(a299) | c1_1(a346) | c2_1(a346) | hskp15. [resolve(26313,e,26086,c),merge(g),merge(h)].
% 198.71/31.68
% 198.71/31.68 % given #7000 (T,wt=9): 29880 hskp12 | hskp6 | c2_1(a320) | c0_1(a330) | hskp3 | hskp23 | -hskp15. [resolve(29869,c,64,b)].
% 198.71/31.68
% 198.71/31.68 % given #7500 (T,wt=5): 31755 hskp11 | hskp27 | hskp6 | hskp28 | -hskp0. [resolve(31742,e,4,b)].
% 198.71/31.68
% 198.71/31.68 % given #8000 (T,wt=7): 33621 hskp27 | hskp6 | c0_1(a294) | c2_1(a294) | -hskp0. [resolve(33598,e,5,b)].
% 198.71/31.68
% 198.71/31.68 % given #8500 (T,wt=12): 32766 hskp11 | c0_1(A) | c2_1(A) | -c1_1(A) | c1_1(a336) | -c0_1(a336) | hskp5. [resolve(32754,b,269,f)].
% 198.71/31.68
% 198.71/31.68 % given #9000 (T,wt=12): 36660 hskp23 | c0_1(a330) | c2_1(a302) | hskp12 | hskp27 | hskp10 | -c1_1(a302) | -c0_1(a321). [resolve(36652,d,15081,c),merge(g)].
% 198.71/31.68
% 198.71/31.68 % SZS status Theorem for theBenchmark
% 198.71/31.68
% 198.71/31.68 % Proof 1 at 21.89 (+ 4.11) seconds.
% 198.71/31.68 % Length of proof is 475.
% 198.71/31.68 % Level of proof is 187.
% 198.71/31.68 % Maximum clause weight is 19.000.
% 198.71/31.68 % Given clauses 9260.
% 198.71/31.68
% 198.71/31.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------