Lee's algorithm for synthesis of ranking functions in size-change termination proofs
The complexity is acceptable in current verifiers, and has been implemented in at least the AProVE termination analysis tool for term rewrite systems.

They describe their implementation in Lazy Abstraction for Size-Change Termination, by Codish, Fuhs, Giesl &amp; Schneider-Kamp, basing their implementation on the papers you refer to. Performance is good both from an expressiveness point of view and a run-time perspective.

The additional (clever!) trick is to pre-process the search for an appropriate abstraction and ranking function into a SAT problem (along with other search procedures for termination analysis) and having a SAT solver try to simultaneously find an instance. This trick is common in the termination analysis community.