By Jan Johannsen and Antonina Kolokolova
(based on earlier work by Lennon et. al. [LM68])
You say you work on resolution
Well, you know, we all want a lower bound
You tell me you'd add substitution
Well, you know, first you gotta prove it sound
But if a random restriction doesn't preserve your proofs
All I can tell you is Brother you're going to lose
You say you can prove Pigeonhole
Well, you know, hard examples are hard to find
Though bounds for circuits play a role
Well, you know, this connection isn't well-defined
And with assumptions weaker than that "pigs can fly"
You'll have to wait for a proof by Ajtai
You talk of cut-elimination
Well, you know, not all systems are cut-free
You claim a smaller derivation
Well, you know, I have to ask for the degree
But if what you work on is arithmetical
Even you admit it's too theoretical
But if your work is based on Cook-Reckhow
You ain't gonna get tenure anywhere anyhow...