Algorithm for extensional equality in combinator calculus
Equality of terms in the combinator calculus is undecidable. We can encode the natural numbers as Church numerals and then show that every recursive function is represented, see for instance section 1.3.1 of Jaap van Oosten's book. I don't have any other books with me right now, but am sure almost any book on this topic will have the result, Barendregt's book surely does.

For your purposes it might be useful enough to apply a simple heuristic that will cover sufficiently many cases. You could do exactly what you suggest: see if two terms applied to a variable reduce to the same term (but you need to give up after a while).