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

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

quot#(s(x), s(y))quot#(minus(s(x), s(y)), s(y))

Rewrite Rules

minus(x, 0)xminus(s(x), s(y))minus(x, y)
le(0, y)truele(s(x), 0)false
le(s(x), s(y))le(x, y)quot(0, s(y))0
quot(s(x), s(y))s(quot(minus(s(x), s(y)), s(y)))

Original Signature

Termination of terms over the following signature is verified: 0, minus, le, s, false, true, quot


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

le#(s(x), s(y))le#(x, y)quot#(s(x), s(y))minus#(s(x), s(y))
minus#(s(x), s(y))minus#(x, y)quot#(s(x), s(y))quot#(minus(s(x), s(y)), s(y))

Rewrite Rules

minus(x, 0)xminus(s(x), s(y))minus(x, y)
le(0, y)truele(s(x), 0)false
le(s(x), s(y))le(x, y)quot(0, s(y))0
quot(s(x), s(y))s(quot(minus(s(x), s(y)), s(y)))

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, le, true, false, quot

Strategy


The following SCCs where found

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

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

quot#(s(x), s(y)) → quot#(minus(s(x), s(y)), s(y))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

minus#(s(x), s(y))minus#(x, y)

Rewrite Rules

minus(x, 0)xminus(s(x), s(y))minus(x, y)
le(0, y)truele(s(x), 0)false
le(s(x), s(y))le(x, y)quot(0, s(y))0
quot(s(x), s(y))s(quot(minus(s(x), s(y)), s(y)))

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, le, true, false, quot

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

minus#(s(x), s(y))minus#(x, y)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

le#(s(x), s(y))le#(x, y)

Rewrite Rules

minus(x, 0)xminus(s(x), s(y))minus(x, y)
le(0, y)truele(s(x), 0)false
le(s(x), s(y))le(x, y)quot(0, s(y))0
quot(s(x), s(y))s(quot(minus(s(x), s(y)), s(y)))

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, le, true, false, quot

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

le#(s(x), s(y))le#(x, y)