TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (393ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (60ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (41ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (40ms), ReductionPairSAT (3627ms), DependencyGraph (40ms), ReductionPairSAT (3477ms), DependencyGraph (42ms), SizeChangePrinciple (timeout)].
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor ReductionPairSAT (218ms).
 |    | – Problem 6 remains open; application of the following processors failed [DependencyGraph (2ms), ReductionPairSAT (98ms), DependencyGraph (2ms)].
 | – Problem 5 was processed with processor SubtermCriterion (1ms).

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

divides#(y, x)div#(x, y)if#(false, x, y)pr#(x, y)
div#(div(x, y), z)zero#(y)pr#(x, s(s(y)))divides#(s(s(y)), x)
zero#(s(x))if#(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))quot#(x, 0, s(z))div#(x, s(z))
div#(x, y)quot#(x, y, y)pr#(x, s(s(y)))if#(divides(s(s(y)), x), x, s(y))
quot#(s(x), s(y), z)quot#(x, y, z)div#(div(x, y), z)div#(x, times(zero(y), z))

Rewrite Rules

p(0)0p(s(x))x
plus(x, 0)xplus(0, y)y
plus(s(x), y)s(plus(x, y))plus(s(x), y)s(plus(p(s(x)), y))
plus(x, s(y))s(plus(x, p(s(y))))times(0, y)0
times(s(0), y)ytimes(s(x), y)plus(y, times(x, y))
div(0, y)0div(x, y)quot(x, y, y)
quot(zero(y), s(y), z)0quot(s(x), s(y), z)quot(x, y, z)
quot(x, 0, s(z))s(div(x, s(z)))div(div(x, y), z)div(x, times(zero(y), z))
eq(0, 0)trueeq(s(x), 0)false
eq(0, s(y))falseeq(s(x), s(y))eq(x, y)
divides(y, x)eq(x, times(div(x, y), y))prime(s(s(x)))pr(s(s(x)), s(x))
pr(x, s(0))truepr(x, s(s(y)))if(divides(s(s(y)), x), x, s(y))
if(true, x, y)falseif(false, x, y)pr(x, y)
zero(div(x, x))xzero(divides(x, x))x
zero(times(x, x))xzero(quot(x, x, x))x
zero(s(x))if(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))

Original Signature

Termination of terms over the following signature is verified: plus, div, true, divides, zero, prime, 0, s, times, if, p, false, quot, pr, eq




Open Dependency Pair Problem 6

Dependency Pairs

plus#(s(x), y)plus#(p(s(x)), y)plus#(x, s(y))plus#(x, p(s(y)))

Rewrite Rules

p(0)0p(s(x))x
plus(x, 0)xplus(0, y)y
plus(s(x), y)s(plus(x, y))plus(s(x), y)s(plus(p(s(x)), y))
plus(x, s(y))s(plus(x, p(s(y))))times(0, y)0
times(s(0), y)ytimes(s(x), y)plus(y, times(x, y))
div(0, y)0div(x, y)quot(x, y, y)
quot(zero(y), s(y), z)0quot(s(x), s(y), z)quot(x, y, z)
quot(x, 0, s(z))s(div(x, s(z)))div(div(x, y), z)div(x, times(zero(y), z))
eq(0, 0)trueeq(s(x), 0)false
eq(0, s(y))falseeq(s(x), s(y))eq(x, y)
divides(y, x)eq(x, times(div(x, y), y))prime(s(s(x)))pr(s(s(x)), s(x))
pr(x, s(0))truepr(x, s(s(y)))if(divides(s(s(y)), x), x, s(y))
if(true, x, y)falseif(false, x, y)pr(x, y)
zero(div(x, x))xzero(divides(x, x))x
zero(times(x, x))xzero(quot(x, x, x))x
zero(s(x))if(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))

Original Signature

Termination of terms over the following signature is verified: plus, div, true, divides, zero, prime, 0, s, times, if, p, false, quot, pr, eq


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

zero#(s(x))plus#(0, zero(0))pr#(x, s(s(y)))divides#(s(s(y)), x)
zero#(s(x))if#(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))pr#(x, s(s(y)))if#(divides(s(s(y)), x), x, s(y))
divides#(y, x)eq#(x, times(div(x, y), y))if#(false, x, y)pr#(x, y)
plus#(s(x), y)plus#(x, y)plus#(s(x), y)plus#(p(s(x)), y)
prime#(s(s(x)))pr#(s(s(x)), s(x))eq#(s(x), s(y))eq#(x, y)
plus#(x, s(y))p#(s(y))divides#(y, x)div#(x, y)
div#(div(x, y), z)zero#(y)zero#(s(x))plus#(zero(0), 0)
times#(s(x), y)times#(x, y)zero#(s(x))eq#(x, s(0))
div#(div(x, y), z)times#(zero(y), z)div#(div(x, y), z)div#(x, times(zero(y), z))
quot#(s(x), s(y), z)quot#(x, y, z)times#(s(x), y)plus#(y, times(x, y))
quot#(x, 0, s(z))div#(x, s(z))divides#(y, x)times#(div(x, y), y)
div#(x, y)quot#(x, y, y)zero#(s(x))zero#(0)
plus#(s(x), y)p#(s(x))plus#(x, s(y))plus#(x, p(s(y)))

Rewrite Rules

p(0)0p(s(x))x
plus(x, 0)xplus(0, y)y
plus(s(x), y)s(plus(x, y))plus(s(x), y)s(plus(p(s(x)), y))
plus(x, s(y))s(plus(x, p(s(y))))times(0, y)0
times(s(0), y)ytimes(s(x), y)plus(y, times(x, y))
div(0, y)0div(x, y)quot(x, y, y)
quot(zero(y), s(y), z)0quot(s(x), s(y), z)quot(x, y, z)
quot(x, 0, s(z))s(div(x, s(z)))div(div(x, y), z)div(x, times(zero(y), z))
eq(0, 0)trueeq(s(x), 0)false
eq(0, s(y))falseeq(s(x), s(y))eq(x, y)
divides(y, x)eq(x, times(div(x, y), y))prime(s(s(x)))pr(s(s(x)), s(x))
pr(x, s(0))truepr(x, s(s(y)))if(divides(s(s(y)), x), x, s(y))
if(true, x, y)falseif(false, x, y)pr(x, y)
zero(div(x, x))xzero(divides(x, x))x
zero(times(x, x))xzero(quot(x, x, x))x
zero(s(x))if(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))

Original Signature

Termination of terms over the following signature is verified: plus, div, true, divides, zero, prime, 0, s, times, if, p, false, quot, pr, eq

Strategy


The following SCCs where found

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

plus#(s(x), y) → plus#(x, y)plus#(s(x), y) → plus#(p(s(x)), y)
plus#(x, s(y)) → plus#(x, p(s(y)))

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

divides#(y, x) → div#(x, y)div#(div(x, y), z) → zero#(y)
if#(false, x, y) → pr#(x, y)pr#(x, s(s(y))) → divides#(s(s(y)), x)
zero#(s(x)) → if#(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))quot#(x, 0, s(z)) → div#(x, s(z))
pr#(x, s(s(y))) → if#(divides(s(s(y)), x), x, s(y))div#(x, y) → quot#(x, y, y)
div#(div(x, y), z) → div#(x, times(zero(y), z))quot#(s(x), s(y), z) → quot#(x, y, z)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

times#(s(x), y)times#(x, y)

Rewrite Rules

p(0)0p(s(x))x
plus(x, 0)xplus(0, y)y
plus(s(x), y)s(plus(x, y))plus(s(x), y)s(plus(p(s(x)), y))
plus(x, s(y))s(plus(x, p(s(y))))times(0, y)0
times(s(0), y)ytimes(s(x), y)plus(y, times(x, y))
div(0, y)0div(x, y)quot(x, y, y)
quot(zero(y), s(y), z)0quot(s(x), s(y), z)quot(x, y, z)
quot(x, 0, s(z))s(div(x, s(z)))div(div(x, y), z)div(x, times(zero(y), z))
eq(0, 0)trueeq(s(x), 0)false
eq(0, s(y))falseeq(s(x), s(y))eq(x, y)
divides(y, x)eq(x, times(div(x, y), y))prime(s(s(x)))pr(s(s(x)), s(x))
pr(x, s(0))truepr(x, s(s(y)))if(divides(s(s(y)), x), x, s(y))
if(true, x, y)falseif(false, x, y)pr(x, y)
zero(div(x, x))xzero(divides(x, x))x
zero(times(x, x))xzero(quot(x, x, x))x
zero(s(x))if(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))

Original Signature

Termination of terms over the following signature is verified: plus, div, true, divides, zero, prime, 0, s, times, if, p, false, quot, pr, eq

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

times#(s(x), y)times#(x, y)

Problem 4: ReductionPairSAT



Dependency Pair Problem

Dependency Pairs

plus#(s(x), y)plus#(x, y)plus#(s(x), y)plus#(p(s(x)), y)
plus#(x, s(y))plus#(x, p(s(y)))

Rewrite Rules

p(0)0p(s(x))x
plus(x, 0)xplus(0, y)y
plus(s(x), y)s(plus(x, y))plus(s(x), y)s(plus(p(s(x)), y))
plus(x, s(y))s(plus(x, p(s(y))))times(0, y)0
times(s(0), y)ytimes(s(x), y)plus(y, times(x, y))
div(0, y)0div(x, y)quot(x, y, y)
quot(zero(y), s(y), z)0quot(s(x), s(y), z)quot(x, y, z)
quot(x, 0, s(z))s(div(x, s(z)))div(div(x, y), z)div(x, times(zero(y), z))
eq(0, 0)trueeq(s(x), 0)false
eq(0, s(y))falseeq(s(x), s(y))eq(x, y)
divides(y, x)eq(x, times(div(x, y), y))prime(s(s(x)))pr(s(s(x)), s(x))
pr(x, s(0))truepr(x, s(s(y)))if(divides(s(s(y)), x), x, s(y))
if(true, x, y)falseif(false, x, y)pr(x, y)
zero(div(x, x))xzero(divides(x, x))x
zero(times(x, x))xzero(quot(x, x, x))x
zero(s(x))if(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))

Original Signature

Termination of terms over the following signature is verified: plus, div, true, divides, zero, prime, 0, s, times, if, p, false, quot, pr, eq

Strategy


Function Precedence

p < plus = div = true = divides = zero = prime = 0 = s = times = if = false = plus# = quot = pr = eq

Argument Filtering

plus: 1 2
div: all arguments are removed from div
true: all arguments are removed from true
divides: 1 2
zero: 1
prime: all arguments are removed from prime
0: all arguments are removed from 0
s: 1
times: 1 2
if: all arguments are removed from if
p: collapses to 1
false: all arguments are removed from false
plus#: collapses to 1
quot: all arguments are removed from quot
pr: collapses to 2
eq: collapses to 2

Status

plus: lexicographic with permutation 1 → 2 2 → 1
div: multiset
true: multiset
divides: lexicographic with permutation 1 → 2 2 → 1
zero: lexicographic with permutation 1 → 1
prime: multiset
0: multiset
s: multiset
times: lexicographic with permutation 1 → 2 2 → 1
if: multiset
false: multiset
quot: multiset

Usable Rules

p(s(x)) → xp(0) → 0

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

p(0)0p(s(x))x
plus(x, 0)xplus(0, y)y
plus(s(x), y)s(plus(x, y))plus(s(x), y)s(plus(p(s(x)), y))
plus(x, s(y))s(plus(x, p(s(y))))times(0, y)0
times(s(0), y)ytimes(s(x), y)plus(y, times(x, y))
div(0, y)0div(x, y)quot(x, y, y)
quot(zero(y), s(y), z)0quot(s(x), s(y), z)quot(x, y, z)
quot(x, 0, s(z))s(div(x, s(z)))div(div(x, y), z)div(x, times(zero(y), z))
eq(0, 0)trueeq(s(x), 0)false
eq(0, s(y))falseeq(s(x), s(y))eq(x, y)
divides(y, x)eq(x, times(div(x, y), y))prime(s(s(x)))pr(s(s(x)), s(x))
pr(x, s(0))truepr(x, s(s(y)))if(divides(s(s(y)), x), x, s(y))
if(true, x, y)falseif(false, x, y)pr(x, y)
zero(div(x, x))xzero(divides(x, x))x
zero(times(x, x))xzero(quot(x, x, x))x
zero(s(x))if(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))

Original Signature

Termination of terms over the following signature is verified: plus, div, true, divides, zero, prime, 0, s, times, if, p, false, quot, pr, eq

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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