How to show that $\vdash\neg(\square \neg p\land p\land\diamond(p\land\square p\land \diamond p) )$ in the logic K?
First of all, does this proof work? Assume the converse (i.e. that $\vdash\square \neg p\land p\land\diamond(p\land\square p\land \diamond p) $). Then by soundness, $\models\square \neg p\land p\land\diamond(p\land\square p\land \diamond p) $. But this cannot be true. Indeed, consider a model and a point in it. If it satisfies $\square \neg p$, then it cannot possibly sayisfy $\diamond(p\land\square p\land \diamond p)$ because there would be a point accessible from the point we are considering where $p$ is true, contrary to the fact that $\square \neg p$ is true at that point.
And how to derive the proof using the Necessitation Rule and the Distribution Axiom (if they are needed)?
EDIT: as pointed out in the comments here, my 'solution' is wrong.
I'm guessing the error you're referring to based on the comments of the other post is that when you say "assume the converse..." you presumably meant 'assume the negation' and what follows is not actually the negation. But despite this inauspicious start, the bulk of your reasoning is correct. The fact is that $\square\lnot p$ and $\lozenge(p\land \square p\land \lozenge p)$ cannot both be true at a point in a frame for the reasons you say, and this implies that $\square \neg p\land p\land\lozenge(p\land\square p\land \lozenge p)$ is false at every point in every frame, and hence that $\lnot (\square \neg p\land p\land\lozenge(p\land\square p\land \lozenge p))$ is true at every point in every frame, hence valid in K. Thus completeness says that it is provable in the various deductive systems for K.
If we actually want to produce the syntactic proof, in this case it's not hard to follow the intuition of the semantic argument above. If we can prove that $\square\lnot p$ and $\lozenge(p\land \square p\land \lozenge p)$ lead to a contradiction, then the rest is just propositional logic. We want to show that $\lozenge(p\land \square p\land \lozenge p)$ implies $\lozenge p,$ which is a special case of $\lozenge(A\land B)$ implies $\lozenge A.$ Then we're done since $\lozenge p$ is just an abbreviation for $\lnot\square \lnot p$ (if your system doesn't work this way the necessary modifications should be minor).
Putting everything in terms of $\square,$ and using a little more propositional logic, we reduce things to showing $\square \lnot A$ implies $\square (\lnot A\lor \lnot B)$ and so since $A$ and $B$ were arbitrary, we can rephrase this as showing $ \square A$ implies $\square(A\lor B).$ We can of course do this by proving $\square A\to \square(A\lor B),$ and at long last we get to do a tiny bit of modal proof: $(A\to A\lor B)$ is provable by propositional logic, and then $\square(A\to A\lor B)$ follows from necessitation, and then $\square A\to \square(A\lor B)$ follows from distribution axiom and modus ponens.