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 (21ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (147ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (468ms), DependencyGraph (1ms), ReductionPairSAT (73ms), DependencyGraph (0ms), SizeChangePrinciple (11ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (1ms)].

The following open problems remain:



Open Dependency Pair Problem 3

Dependency Pairs

cond#(true, x)cond#(odd(x), p(x))

Rewrite Rules

cond(true, x)cond(odd(x), p(x))odd(0)false
odd(s(0))trueodd(s(s(x)))odd(x)
p(0)0p(s(x))x

Original Signature

Termination of terms over the following signature is verified: 0, s, p, false, true, odd, cond


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

odd#(s(s(x)))odd#(x)cond#(true, x)odd#(x)
cond#(true, x)p#(x)cond#(true, x)cond#(odd(x), p(x))

Rewrite Rules

cond(true, x)cond(odd(x), p(x))odd(0)false
odd(s(0))trueodd(s(s(x)))odd(x)
p(0)0p(s(x))x

Original Signature

Termination of terms over the following signature is verified: 0, s, p, true, false, odd, cond

Strategy


The following SCCs where found

odd#(s(s(x))) → odd#(x)

cond#(true, x) → cond#(odd(x), p(x))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

odd#(s(s(x)))odd#(x)

Rewrite Rules

cond(true, x)cond(odd(x), p(x))odd(0)false
odd(s(0))trueodd(s(s(x)))odd(x)
p(0)0p(s(x))x

Original Signature

Termination of terms over the following signature is verified: 0, s, p, true, false, odd, cond

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

odd#(s(s(x)))odd#(x)