Help needed for last puzzle in Session 6

[luckylone]

Hello, I've been stuck on this one fo quite a while and can't seem to find a solution using no custom blocks.
I would like some help or hints to point me in the right direction.
I think I understand the blocks and the underlying logic well enough but I wouldn't be against a formal explanation as there is little to no clear documentation on the subject. I am not so informed when it comes to predicate logic.
I've joined my latest attempt at a proof, it seems I can't unify P(c) to P(y) or vice versa.
Thanks in advance !

[nomeata]

Hint: the or-elimination block in the middle does a case distinction, breaking the proof into two. You placed your existential introduction block behind it, meaning that you have to find the same value for x in both cases. IIRC that will not work.

Try to attach the or-elimination block directly to your goal, and then put two introduction blocks for the existential inside. You may have to put them even further inside other blocks, e.g. inside the implication-elimination.

[luckylone]

Ok taking your advice into account here is a second proof attempt. Again I can't seem to find a method to prove the second case for P(c).

[luckylone]

Here is yet another proof attempt. Although I am over the minimum blocks, I don't understand why this proof doesn't work.

[nomeata]

Hmm, I can’t quite tell if the proof is really not good, or if The Incredible Proof Machine has trouble with the higher order unification needed.

And I must admit I can’t build the proof right away myself.

BTW, Did you do the second-to-last puzzle of session 6? You might be able to build on top of that, if A is False (and if A is true it is simple anyways)

[thaumasiotes]

That most recent proof is definitely correct; The Incredible Proof Machine will accept it with no changes if you add an appropriate annotation block.

In the outer disjunction, the automatic top case is ?x.P(y(x)) -> False, but it should be ?x.P(x) -> False.

I agree that The Incredible Proof Machine would be much better if there were documentation on the requirements of the quantifier-instantiation and quantifier-generalization blocks. They do not work in an intuitive way. It's better to be allowed to read the documentation than to be forced to guess what valid logical operations might be prohibited for technical reasons.