TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (47ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (513ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (6406ms), DependencyGraph (1ms), ReductionPairSAT (623ms), DependencyGraph (1ms), SizeChangePrinciple (2655ms), ForwardNarrowing (2ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 6 was processed with processor DependencyGraph (1ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (0ms).

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

reverse#(cons(x, xs)) → reverse#(del(last(cons(x, xs)), cons(x, xs)))

Rewrite Rules

last(nil) → 0last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))eq(0, 0) → true
eq(0, s(y)) → falseeq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))

Original Signature

Termination of terms over the following signature is verified: reverse, 0, s, last, if, false, true, del, eq, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

last#(cons(x, cons(y, xs))) → last#(cons(y, xs))del#(x, cons(y, xs)) → if#(eq(x, y), x, y, xs)
reverse#(cons(x, xs)) → del#(last(cons(x, xs)), cons(x, xs))reverse#(cons(x, xs)) → last#(cons(x, xs))
del#(x, cons(y, xs)) → eq#(x, y)eq#(s(x), s(y)) → eq#(x, y)
reverse#(cons(x, xs)) → reverse#(del(last(cons(x, xs)), cons(x, xs)))if#(false, x, y, xs) → del#(x, xs)

Rewrite Rules

last(nil) → 0last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))eq(0, 0) → true
eq(0, s(y)) → falseeq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))

Original Signature

Termination of terms over the following signature is verified: reverse, 0, last, s, if, true, false, del, nil, cons, eq

Strategy

The following SCCs where found

last#(cons(x, cons(y, xs))) → last#(cons(y, xs))
del#(x, cons(y, xs)) → if#(eq(x, y), x, y, xs)if#(false, x, y, xs) → del#(x, xs)
eq#(s(x), s(y)) → eq#(x, y)
reverse#(cons(x, xs)) → reverse#(del(last(cons(x, xs)), cons(x, xs)))

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

del#(x, cons(y, xs)) → if#(eq(x, y), x, y, xs)if#(false, x, y, xs) → del#(x, xs)

Rewrite Rules

last(nil) → 0last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))eq(0, 0) → true
eq(0, s(y)) → falseeq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))

Original Signature

Termination of terms over the following signature is verified: reverse, 0, last, s, if, true, false, del, nil, cons, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

del#(x, cons(y, xs)) → if#(eq(x, y), x, y, xs)

Problem 6: DependencyGraph

Dependency Pair Problem

Dependency Pairs

if#(false, x, y, xs) → del#(x, xs)

Rewrite Rules

last(nil) → 0last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))eq(0, 0) → true
eq(0, s(y)) → falseeq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))

Original Signature

Termination of terms over the following signature is verified: reverse, 0, s, last, if, false, true, del, eq, cons, nil

Strategy

There are no SCCs!

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

eq#(s(x), s(y)) → eq#(x, y)

Rewrite Rules

last(nil) → 0last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))eq(0, 0) → true
eq(0, s(y)) → falseeq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))

Original Signature

Termination of terms over the following signature is verified: reverse, 0, last, s, if, true, false, del, nil, cons, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

eq#(s(x), s(y)) → eq#(x, y)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

last#(cons(x, cons(y, xs))) → last#(cons(y, xs))

Rewrite Rules

last(nil) → 0last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))eq(0, 0) → true
eq(0, s(y)) → falseeq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))

Original Signature

Termination of terms over the following signature is verified: reverse, 0, last, s, if, true, false, del, nil, cons, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

last#(cons(x, cons(y, xs))) → last#(cons(y, xs))