TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60018 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (2385ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (1612ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (1529ms), PolynomialLinearRange8NegiUR (30037ms), ReductionPairSAT (14326ms)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	te^#(a)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu^#(s)
te^#(msubst(te(a), sortSu(id)))	→	te^#(a)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu^#(circ(sortSu(s), sortSu(t)))		sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	te^#(msubst(te(a), sortSu(t)))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(t)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu^#(t)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	te^#(a)		sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(circ(sortSu(s), sortSu(t)))
sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	te^#(a)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(circ(sortSu(s), sortSu(t)))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(circ(sortSu(s), sortSu(t)))		sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(s)		sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(s)
te^#(subst(te(a), sortSu(id)))	→	te^#(a)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(u)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu^#(circ(sortSu(s), sortSu(t)))		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu^#(t)
sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(s)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu^#(s)
sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(circ(sortSu(t), sortSu(u)))		te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	te^#(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(t)		sortSu^#(circ(sortSu(id), sortSu(s)))	→	sortSu^#(s)
sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(u)		sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(t)
sortSu^#(circ(sortSu(s), sortSu(id)))	→	sortSu^#(s)		sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(t)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(s)

Rewrite Rules

sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))))		sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))		sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
sortSu(circ(sortSu(s), sortSu(id)))	→	sortSu(s)		sortSu(circ(sortSu(id), sortSu(s)))	→	sortSu(s)
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))		te(subst(te(a), sortSu(id)))	→	te(a)
te(msubst(te(a), sortSu(id)))	→	te(a)		te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))

Original Signature

Termination of terms over the following signature is verified: id, circ, subst, lift, te, sop, msubst, cons, sortSu

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu^#(s)		te^#(msubst(te(a), sortSu(id)))	→	te^#(a)
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	te^#(a)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))
sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	te^#(msubst(te(a), sortSu(t)))		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu^#(circ(sortSu(s), sortSu(t)))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(t)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu^#(t)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	te^#(a)		sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(circ(sortSu(s), sortSu(t)))
sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))))		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu^#(cons(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	te^#(a)		te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(circ(sortSu(s), sortSu(t)))
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(circ(sortSu(s), sortSu(t)))		sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(s)		sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(s)
te^#(subst(te(a), sortSu(id)))	→	te^#(a)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu^#(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(u)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu^#(circ(sortSu(s), sortSu(t)))
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu^#(t)		sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(s)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu^#(s)		sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(circ(sortSu(t), sortSu(u)))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	te^#(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))		sortSu^#(circ(sortSu(id), sortSu(s)))	→	sortSu^#(s)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(t)		sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(u)		sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu^#(t)
sortSu^#(circ(sortSu(s), sortSu(id)))	→	sortSu^#(s)		sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu^#(t)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu^#(s)

Rewrite Rules

sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t)))	→	sortSu(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))))		sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t)))))	→	sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t)))))	→	sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))		sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u)))	→	sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
sortSu(circ(sortSu(s), sortSu(id)))	→	sortSu(s)		sortSu(circ(sortSu(id), sortSu(s)))	→	sortSu(s)
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u)))))	→	sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))		te(subst(te(a), sortSu(id)))	→	te(a)
te(msubst(te(a), sortSu(id)))	→	te(a)		te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t)))	→	te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))

Original Signature

Termination of terms over the following signature is verified: id, circ, subst, lift, te, msubst, sop, sortSu, cons

Strategy

The following SCCs where found

te^#(msubst(te(a), sortSu(id))) → te^#(a)	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t))))) → sortSu^#(s)
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → te^#(a)	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu^#(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))
sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → te^#(msubst(te(a), sortSu(t)))	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t))))) → sortSu^#(circ(sortSu(s), sortSu(t)))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → sortSu^#(t)	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t))))) → sortSu^#(t)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) → te^#(a)	sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → sortSu^#(circ(sortSu(s), sortSu(t)))
sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → te^#(a)	te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → sortSu^#(circ(sortSu(s), sortSu(t)))
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu^#(circ(sortSu(s), sortSu(t)))	sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu^#(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → sortSu^#(s)	sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → sortSu^#(s)
te^#(subst(te(a), sortSu(id))) → te^#(a)	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu^#(u)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) → sortSu^#(circ(sortSu(s), sortSu(t)))	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) → sortSu^#(t)
sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu^#(s)	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) → sortSu^#(s)
te^#(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → te^#(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))	sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu^#(circ(sortSu(t), sortSu(u)))
sortSu^#(circ(sortSu(id), sortSu(s))) → sortSu^#(s)	sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu^#(t)
sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu^#(u)	sortSu^#(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → sortSu^#(t)
sortSu^#(circ(sortSu(s), sortSu(id))) → sortSu^#(s)	sortSu^#(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu^#(t)
sortSu^#(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu^#(s)