I always puzzled why the two steps are so different in complexity: almost for any proof checking the basis assertion is simple mechanical procedure, while most of the work deferred to proving inductive step. What if we divorce the basis and inductive step? The assertions where basis is true while the inductive step fails are plentiful and easy to come by (e.g. "All natural numbers are odd").
The case where inductive step is valid but basis fails seems to be more subtle. Assertion involving total order on natural numbers are one example ("All natural numbers are greater than 5"). I'm looking for little more sophisticated assertion where we can't bluntly leverage transitivity of the order relation. Any equality where inductive step is valid but basis fails?
The standard lattice technique of converting inequality to equality ( $x \preceq y \Leftrightarrow GCD(x,y)=x $ is one example which hints that equalities where inductive step is valid but basis fails must be common, but I would like to see analytic closed form expression, e.g polynomial.
Edit: Little reflection upon Tomasz comment prompts that the question must be constrained to satisfiable formulas. Then, there exists $N$ such that the assertion is true, and induction step proves that the statement is valid for all numbers greater than $N$. It becomes evident that no polynomial equality fits this requirement.