  Checking the soundness of cyclic induction reasoning for first-order logic
with inductive definitions (FOLID) is decidable but the standard checking
method is based on an exponential complement operation for B\"uchi automata.
Recently, we introduced a polynomial checking method whose most expensive steps
recall the comparisons done with multiset path orderings. We describe the
implementation of our method in the Cyclist prover. Referred to as E-Cyclist,
it successfully checked all the proofs included in the original distribution of
Cyclist. Heuristics have been devised to automatically define, from the
analysis of the proof derivations, the trace-based ordering measures that
guarantee the soundness property.
