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

The following open problems remain:



Open Dependency Pair Problem 3

Dependency Pairs

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

Rewrite Rules

cond(true, x)cond(odd(x), p(p(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

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

Rewrite Rules

cond(true, x)cond(odd(x), p(p(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(p(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(p(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)