Is there a systematic method for constructing lambda calculus terms that can distinguish between inputs?
The Böhm-out technique can construct term contexts that can distinguish between terms iff they are distinct in the beta-eta theory (i.e., a term context $C[-]$ so that $C[s]=T$ and $C[t]=F$). See, e.g., http://www.di.unito.it/~dezani/papers/dgp.pdf - it is exceedingly systemtic.

If the terms are closed, as in your example, the context you construct using the Böhm-out technique will be a term M that you apply to the two terms (so $M s = T$, $M t=F$).  Otherwise the term context will include capturing substitutions so that it can work at the sites of the free variables.