Infeasibility Checker for Conditional Rewrite Systems
infChecker is a tool which can be used to
verify infeasibility conditions of variants of Term Rewriting
infChecker is powered by the theorem
prover Prover9 and the model generators
and AGES. AGES is powered by
the SMT solver Barcelogic.
confluence competition (CoCo) in the INF category (see results). Currently, infChecker is the most powerful tool for proving infeasibility and the only tool capable to disprove it, i.e. prove feasibility.