We present the implementation of cTI, a system for
universal left-termination inference of logic programs,
which heavily
relies on static analysis techniques.
Termination inference generalizes
termination analysis/checking.
Traditionally, a termination analyzer tries to prove that a given class
of queries terminates. This class must be provided to the system,
requiring user annotations. With termination
inference such annotations are no longer necessary.
Instead, all provably terminating classes to all related
predicates are inferred at once.
The architecture of cTI is described
and some optimizations are discussed.
Running times for classical examples from
the termination literature in LP
and for some middle-sized logic programs are given.