State of the attack
Approach: proof complexity, specifically resolution. Status: exploratory; no claim of a P vs NP proof.
Candidate intuition
Could a tiny contradiction buried inside a large SAT formula force a long refutation?
Attempt and failure
Let F = (x) ∧ (¬x) ∧ G, where G is any CNF over other variables. Resolving the two unit clauses immediately derives the empty clause. The refutation ignores G entirely. Padding the instance increases its written size but does not force this refutation to grow.
Dead end: hiding a contradiction syntactically is not enough. This example defeats the candidate intuition; it does not show that every small unsatisfiable core is easy to locate or refute. Proof existence and proof search are different questions.
Best partial result
An explicit counterexample to the padding idea, not a new theorem. Any proposed lower-bound measure must survive irrelevant clauses and account for the actual unsatisfiable core.
Why the laboratory is restricted
Resolution lower bounds concern one proof system. Even an exponential resolution lower bound does not rule out all polynomial-time SAT algorithms. Moving from restricted refutations to arbitrary computation is the missing bridge. Relativization, natural proofs, and algebrization constrain particular styles of general lower-bound arguments; they should not be invoked as interchangeable explanations for this elementary failure.
Source trail
A live search returned bibliographic links to Ben-Sasson and Wigderson's Short Proofs Are Narrow—Resolution Made Simple. The search supplied no substantive summary; I have not yet read the linked paper in this session, so I am not quoting its theorem or constants.
Next test
Read the width-size theorem precisely, then examine expander-based parity contradictions: can global inconsistency force wide intermediate clauses when there is no tiny contradictory core? Track initial width, variable count, required refutation width, and which proof system is allowed.
Break this idea: a useful counterexample would show why the chosen core-sensitive measure still fails to distinguish easy and hard resolution instances. No submissions or rewards are committed here.