The TRS could not be proven terminating. The proof attempt took 18232 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (73ms), SubtermCriterion (1ms), DependencyGraph (38ms), PolynomialLinearRange4iUR (1688ms), DependencyGraph (38ms), PolynomialLinearRange8NegiUR (7097ms), DependencyGraph (52ms), ReductionPairSAT (7860ms), DependencyGraph (27ms), SizeChangePrinciple (382ms)].
| circ#(cons(a, s), t) | → | circ#(s, t) | circ#(cons(a, s), t) | → | msubst#(a, t) | |
| msubst#(msubst(a, s), t) | → | circ#(s, t) | circ#(cons(lift, s), circ(cons(lift, t), u)) | → | circ#(cons(lift, circ(s, t)), u) | |
| circ#(cons(lift, s), cons(a, t)) | → | circ#(s, t) | circ#(circ(s, t), u) | → | circ#(t, u) | |
| circ#(cons(lift, s), cons(lift, t)) | → | circ#(s, t) | msubst#(msubst(a, s), t) | → | msubst#(a, circ(s, t)) | |
| circ#(circ(s, t), u) | → | circ#(s, circ(t, u)) | circ#(cons(lift, s), circ(cons(lift, t), u)) | → | circ#(s, t) |
| circ(cons(a, s), t) | → | cons(msubst(a, t), circ(s, t)) | circ(cons(lift, s), cons(a, t)) | → | cons(a, circ(s, t)) | |
| circ(cons(lift, s), cons(lift, t)) | → | cons(lift, circ(s, t)) | circ(circ(s, t), u) | → | circ(s, circ(t, u)) | |
| circ(s, id) | → | s | circ(id, s) | → | s | |
| circ(cons(lift, s), circ(cons(lift, t), u)) | → | circ(cons(lift, circ(s, t)), u) | subst(a, id) | → | a | |
| msubst(a, id) | → | a | msubst(msubst(a, s), t) | → | msubst(a, circ(s, t)) |
Termination of terms over the following signature is verified: id, circ, subst, lift, msubst, cons