Testing "Safe term order" predicate

In a recent question (Safe term order) @false asked for an implementation of the term ordering predicate lt/2, a variant of the ISO builtin (@<)/2.

The truth value of lt(T1,T2) is to be stable w.r.t. arbitrary variable bindings in T1 and T2.

In various answers, different implementations (based on implicit / explicit term traversal) were proposed. Some caveats and hints were raised in comments, so were counterexamples.

So my question: how can candidate implementations be tested? Some brute-force approach? Or something smarter?

In any case, please share your automatic testing machinery for lt/2! It's for the greater good!