Uncurrying for Termination

This page contains experiments.

Additionally, it shows why triangular matrix interpretations of dimension two cannot orient this TRS.

• encode the constraints as a satisfaction problem in non-linear integer arithmetic (orig.smt)
• split into separate assertions (a.smt)
• simplify according to x_2 = 1 and x_7 = 1 (b.smt)
• simplify according to x_4 = 1 and x_9 = 1 (c.smt)
• simplify according to x_8 = 0 (d.smt)
• + is associative (e.smt)
• remove redundand additions (f.smt)
• detect unsatisfiability