TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (219ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (1469ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (5422ms), DependencyGraph (4ms), ReductionPairSAT (1419ms), DependencyGraph (3ms), SizeChangePrinciple (408ms)].
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (3959ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (15025ms), DependencyGraph (5ms), ReductionPairSAT (10330ms), DependencyGraph (7ms), SizeChangePrinciple (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

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

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)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) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))id(x) → x
if(true, x, y) → xif(false, x, y) → y
not(x) → if(x, false, true)gt(s(x), zero) → true
gt(zero, y) → falsegt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: not, id, plus, 0, s, times, if, false, true, gt, zero

Open Dependency Pair Problem 4

Dependency Pairs

times#(x, plus(y, s(z))) → times#(x, plus(y, times(s(z), 0)))times#(x, plus(y, s(z))) → times#(x, s(z))
times#(x, plus(y, s(z))) → times#(s(z), 0)times#(x, s(y)) → times#(x, y)

Rewrite Rules

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)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) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))id(x) → x
if(true, x, y) → xif(false, x, y) → y
not(x) → if(x, false, true)gt(s(x), zero) → true
gt(zero, y) → falsegt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: not, id, plus, 0, s, times, if, false, true, gt, zero

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)))
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))
times#(x, s(y)) → times#(x, y)times#(x, plus(y, s(z))) → plus#(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times#(x, plus(y, s(z))) → times#(x, plus(y, times(s(z), 0)))plus#(s(x), s(y)) → id#(x)
plus#(s(x), x) → if#(gt(x, x), id(x), id(x))times#(x, plus(y, s(z))) → times#(x, s(z))
times#(x, plus(y, s(z))) → plus#(y, times(s(z), 0))plus#(s(x), s(y)) → plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
times#(x, s(y)) → plus#(times(x, y), x)plus#(s(x), s(y)) → if#(not(gt(x, y)), id(x), id(y))
gt#(s(x), s(y)) → gt#(x, y)times#(x, plus(y, s(z))) → times#(s(z), 0)
not#(x) → if#(x, false, true)plus#(s(x), s(y)) → not#(gt(x, y))
plus#(s(x), s(y)) → id#(y)

Rewrite Rules

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)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) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))id(x) → x
if(true, x, y) → xif(false, x, y) → y
not(x) → if(x, false, true)gt(s(x), zero) → true
gt(zero, y) → falsegt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: id, not, plus, 0, s, times, if, true, false, gt, zero

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))
gt#(s(x), s(y)) → gt#(x, y)
times#(x, plus(y, s(z))) → times#(x, plus(y, times(s(z), 0)))times#(x, plus(y, s(z))) → times#(x, s(z))
times#(x, plus(y, s(z))) → times#(s(z), 0)times#(x, s(y)) → times#(x, y)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)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) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))id(x) → x
if(true, x, y) → xif(false, x, y) → y
not(x) → if(x, false, true)gt(s(x), zero) → true
gt(zero, y) → falsegt(s(x), s(y)) → gt(x, y)

Original Signature

Termination of terms over the following signature is verified: id, not, plus, 0, s, times, if, true, false, gt, zero

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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