Thank you to Git Gud for the pointers! I needed to introduce a subproof assuming Cube(f) within the subproof for SameRow(d,f). The complete proof looks like this:
Goal: ~Cube(f)
1.|SameRow(b,f) v SameRow(c,f) v SameRow(d,f)
2.|~SameRow(c,f)
3.|FrontOf(b,f)
4.|~(SameRow(d,f) ^ Cube(f))
5. |SameRow(b,f)
6. |⊥ Ana Con 3,5
7. |~Cube(f) ⊥Elim 6
(end subproof)
8. |SameRow(c,f)
9. |⊥ ⊥Intro 2,8
10. |~Cube(f) ⊥Elim 9
(end subproof)
11. |SameRow(d,f)
12. |Cube(f)
13. |SameRow(d,f) ^ Cube(f) ^Intro 11, 12
14. |⊥ ⊥Intro 4, 13
15. |~Cube(f) ~Intro 11-14
16.|~Cube(f) VElim 1,5-7,8-10,11-14
It is always a very bad sign when someone has started a bunch of subproofs without indicating what happens at the end of the subproof.
A proof should always have a plan or outline, and subproofs provide the skeleton to do so. But again, you need to indicate what you want to do with the subproof, and that involves indicating what you want as the last line of your subproof. You haven't done that for any of the three subproofs you started, which is exactly why you get in trouble, and get see the forest for the trees.
Now, it is clear that with your first subproof you are hoping to do a proof by contradiction. So, start by creating the proper setup for that:
$A \rightarrow (B \lor C)$
$\quad \neg ((A \rightarrow B) \lor (A \rightarrow C))$
$\quad \text{... skip a bunch of lines ...}$
$\quad \bot$
$\neg \neg ((A \rightarrow B) \lor (A \rightarrow C))$
$(A \rightarrow B) \lor (A \rightarrow C)$
Ok, now that we have set that up properly, let's go back inside the subproof, and see how we can derive the contradiction from the premise and the assumption.
Now, it is at this point that you assume $A$. Why?
Actually, I think I know why, because I have seen it all too often: you are probably thinking "ooh, it would be nice to have $A$, because then I can combine that with the premise! OK, so let's jist assume $A$"
OK, the problem with this kind of thinking is that you end up assuming something that you want ... which is always a bad ide, as that will often lead to a circular proof. Indeed, suppose you were indeed to combone $A$ with the premise, and get $B \lor C$ ... OK .... now what?! Well, one thing you can do is to then close the subproof and conclude $A \rightarrow (B \lor C)$ .... but note that now you just get the very premise, i.e. You are getting nowhere.
Here is some general advice on subproofs, that goes back to my initial point about having a plan: before starting any subproof, you should already know how you are going to use that subproof, and in particular, what the last line of your subproof should be, and what rule you will apply after the subproof is done.
Ok, let's regroup. There is really no good reason to assume $A$. Ok, but what should you do on line 3? Well, again, if you had $A$, you could combine that with the premise, but rather than assuming $A$, you could try and make $A$ your new goal. And, to prove $A$, one thing you could do is to assume $\neg A$, and show that that leads to a contradiction.
However, there is a much more straightforward thing to do. The assumption $\neg ((A \rightarrow B) \lor (A \rightarrow C))$ is a negation of a disjunction, and you are probably aware of how by DeMorgan that is equivalent to the conjunction of the negated disjuncts, i.e. to $\neg (A \rightarrow B) \land \neg (A \rightarrow C)$. Now, I suspect you don't have DeMorgan as an inference rule in your specific system, but think about it this way: apprently you should be able to derive both $\neg (A \rightarrow B)$ as well as $\neg (A \rightarrow C)$ from the Assumption. Now, both of those statements are negations, and you probably know the best strategy to prove negations: Proof bu Contradiction!
OK, so we have another piece of our plan:
$A \rightarrow (B \lor C)$
$\quad \neg ((A \rightarrow B ) \lor (A \rightarrow C))$
$\quad \quad A \rightarrow B$
$\quad \quad \text{skip a few lines...}$
$\quad \quad \bot$
$\quad \neg (A \rightarrow B)$
$\quad \quad (A \rightarrow C)$
$\quad \quad \text{skip a few lines ...}$
$\quad \quad \bot$
$\quad \neg (A\rightarrow C)$
$\quad \text{few lines ...}$
$\quad \bot$
$\neg \neg ((A \rightarrow B) \lor (A \rightarrow C))$
$(A \rightarrow B) \lor (A \rightarrow C)$
OK, see how this is all nicely organized? How you now have an outline, to which you can add details and provide the missing steps at some later point? That is what you are supposed to do! That is how you keep your proof, and your very thinking organized. Indeed, the very point of doing formal logic proofs is to teach you that very skill of careful organization!
Now, I am going to leave those details to you, but leave you with one more hint: what is $\neg (A \rightarrow B)$ equivalent to? .... try and derive that, do the same for $\neg (A \rightarrow C)$, and you're pretty much done! Good luck!
Best Answer
As correctly pointed out by the OP and in the comments here, this argument is provable. It was indeed possible to find a proof.
Here is one possibility using Fitch-style natural deduction system: