One of the secrets to mathematical problem solving is that one needs to place a high value on partial progress, as being a crucial stepping stone to fully solving the problem.
(Terrence Tao, https://plus.google.com/u/0/114134834346472219368/posts/Xdm8eiPLWZp)
It's extremely applicable to my recent wrestling with the particular kind of focal encoding problems I've been playing with lately. On a given day of working on them for a few hours, I can easily come up with a dozen half-baked ideas, none of which actually work, but a few of which fail in interesting ways. And often as not, I make real progress by combining ideas that half-fail and half-succeed in complementary ways.
Like literally just this morning, I thought I had finally succeeded in extracting out the context-clearing effect of the Pfenning-Davies-esque box-like modalities in adjoint logic, and encoding it as a family of universal quantifiers --- and then I noticed I had totally failed to do this, and the resulting logic that I had in front of me was actually [Alex] Simpson-style. So this looked like an utter failure, until I pulled out a tool from my bag of obscure technical tricks that had previously succeeded in turning a Simpson-style modal logic into a Pfenning-Davies-style one, turned the crank, and lo and behold, it appears to have fixed the problem.