TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (268ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (10ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (9ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (9ms), ReductionPairSAT (timeout)].
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (18ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (37ms), DependencyGraph (4ms)].
 | – Problem 5 was processed with processor SubtermCriterion (0ms).

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

sum#(plus(cons(0, x), cons(y, l))) → sum#(cons(s(x), cons(y, l)))sum#(cons(x, cons(y, l))) → sum#(cons(plus(x, y), l))
sum#(app(l, cons(x, cons(y, k)))) → sum#(app(l, sum(cons(x, cons(y, k)))))sum#(app(l, cons(x, cons(y, k)))) → sum#(cons(x, cons(y, k)))

Rewrite Rules

app(nil, k) → kapp(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))pred(cons(s(x), nil)) → cons(x, nil)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → yplus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → xif(true, x, y) → x
if(false, x, y) → ynot(x) → if(x, false, true)
gt(s(x), zero) → truegt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: app, plus, true, sum, zero, id, not, 0, s, if, false, gt, pred, nil, cons

Open Dependency Pair Problem 4

Dependency Pairs

plus#(id(x), s(y)) → plus#(x, if(gt(s(y), y), y, s(y)))plus#(s(x), s(y)) → plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
plus#(s(x), x) → plus#(if(gt(x, x), id(x), id(x)), s(x))

Rewrite Rules

app(nil, k) → kapp(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))pred(cons(s(x), nil)) → cons(x, nil)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → yplus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → xif(true, x, y) → x
if(false, x, y) → ynot(x) → if(x, false, true)
gt(s(x), zero) → truegt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: app, plus, true, sum, zero, id, not, 0, s, if, false, gt, pred, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

plus#(s(x), x) → id#(x)plus#(id(x), s(y)) → plus#(x, if(gt(s(y), y), y, s(y)))
sum#(plus(cons(0, x), cons(y, l))) → pred#(sum(cons(s(x), cons(y, l))))sum#(cons(x, cons(y, l))) → sum#(cons(plus(x, y), l))
plus#(id(x), s(y)) → gt#(s(y), y)plus#(s(x), s(y)) → gt#(x, y)
plus#(s(x), x) → plus#(if(gt(x, x), id(x), id(x)), s(x))plus#(s(x), s(y)) → if#(gt(x, y), x, y)
plus#(s(x), x) → gt#(x, x)plus#(id(x), s(y)) → if#(gt(s(y), y), y, s(y))
plus#(s(x), x) → if#(gt(x, x), id(x), id(x))plus#(s(x), s(y)) → id#(x)
sum#(plus(cons(0, x), cons(y, l))) → sum#(cons(s(x), cons(y, l)))sum#(app(l, cons(x, cons(y, k)))) → app#(l, sum(cons(x, cons(y, k))))
plus#(s(x), s(y)) → plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))sum#(cons(x, cons(y, l))) → plus#(x, y)
plus#(s(x), s(y)) → if#(not(gt(x, y)), id(x), id(y))sum#(app(l, cons(x, cons(y, k)))) → sum#(cons(x, cons(y, k)))
sum#(app(l, cons(x, cons(y, k)))) → sum#(app(l, sum(cons(x, cons(y, k)))))gt#(s(x), s(y)) → gt#(x, y)
not#(x) → if#(x, false, true)plus#(s(x), s(y)) → not#(gt(x, y))
plus#(s(x), s(y)) → id#(y)app#(cons(x, l), k) → app#(l, k)

Rewrite Rules

app(nil, k) → kapp(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))pred(cons(s(x), nil)) → cons(x, nil)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → yplus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → xif(true, x, y) → x
if(false, x, y) → ynot(x) → if(x, false, true)
gt(s(x), zero) → truegt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: app, plus, true, sum, zero, id, not, 0, s, if, false, gt, pred, cons, nil

Strategy

The following SCCs where found

plus#(id(x), s(y)) → plus#(x, if(gt(s(y), y), y, s(y)))plus#(s(x), s(y)) → plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
plus#(s(x), x) → plus#(if(gt(x, x), id(x), id(x)), s(x))
sum#(plus(cons(0, x), cons(y, l))) → sum#(cons(s(x), cons(y, l)))sum#(cons(x, cons(y, l))) → sum#(cons(plus(x, y), l))
sum#(app(l, cons(x, cons(y, k)))) → sum#(cons(x, cons(y, k)))sum#(app(l, cons(x, cons(y, k)))) → sum#(app(l, sum(cons(x, cons(y, k)))))
gt#(s(x), s(y)) → gt#(x, y)
app#(cons(x, l), k) → app#(l, k)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

app#(cons(x, l), k) → app#(l, k)

Rewrite Rules

app(nil, k) → kapp(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))pred(cons(s(x), nil)) → cons(x, nil)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → yplus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → xif(true, x, y) → x
if(false, x, y) → ynot(x) → if(x, false, true)
gt(s(x), zero) → truegt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: app, plus, true, sum, zero, id, not, 0, s, if, false, gt, pred, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

app#(cons(x, l), k) → app#(l, k)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

app(nil, k) → kapp(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))pred(cons(s(x), nil)) → cons(x, nil)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → yplus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → xif(true, x, y) → x
if(false, x, y) → ynot(x) → if(x, false, true)
gt(s(x), zero) → truegt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: app, plus, true, sum, zero, id, not, 0, s, if, false, gt, pred, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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