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 (8ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (141ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (295ms), DependencyGraph (2ms), ReductionPairSAT (507ms), DependencyGraph (2ms), SizeChangePrinciple (5ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (0ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

f#(0, 1, x)f#(h(x), h(x), x)

Rewrite Rules

f(0, 1, x)f(h(x), h(x), x)h(0)0
h(g(x, y))y

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, h


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(0, 1, x)h#(x)f#(0, 1, x)f#(h(x), h(x), x)

Rewrite Rules

f(0, 1, x)f(h(x), h(x), x)h(0)0
h(g(x, y))y

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, h

Strategy


The following SCCs where found

f#(0, 1, x) → f#(h(x), h(x), x)