TIMEOUT

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (22ms), SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (203ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (914ms), DependencyGraph (6ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

r#(xs, cons(y, ys), nil, cons(w, ws)) → r#(xs, xs, cons(succ(zero), nil), ws)r#(xs, nil, zs, cons(w, ws)) → r#(xs, xs, cons(succ(zero), zs), ws)
r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) → r#(ys, cons(y, ys), zs, cons(succ(zero), cons(w, ws)))

Rewrite Rules

r(xs, ys, zs, nil) → xsr(xs, nil, zs, cons(w, ws)) → r(xs, xs, cons(succ(zero), zs), ws)
r(xs, cons(y, ys), nil, cons(w, ws)) → r(xs, xs, cons(succ(zero), nil), ws)r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) → r(ys, cons(y, ys), zs, cons(succ(zero), cons(w, ws)))

Original Signature

Termination of terms over the following signature is verified: succ, r, zero, cons, nil