TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (73ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (323ms).
 | – Problem 3 was processed with processor PolynomialLinearRange8NegiUR (5559ms).
 |    | – Problem 4 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange8NegiUR (9429ms), DependencyGraph (3ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 4

Dependency Pairs

h#(c(s(x), c(s(0), y)), z, t(x)) → h#(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))h#(x, c(y, z), t(w)) → h#(c(s(y), x), z, t(c(t(w), w)))

Rewrite Rules

h(c(x, y), c(s(z), z), t(w)) → h(z, c(y, x), t(t(c(x, c(y, t(w))))))h(x, c(y, z), t(w)) → h(c(s(y), x), z, t(c(t(w), w)))
h(c(s(x), c(s(0), y)), z, t(x)) → h(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))t(t(x)) → t(c(t(x), x))
t(x) → xt(x) → c(0, c(0, c(0, c(0, c(0, x)))))

Original Signature

Termination of terms over the following signature is verified: t, 0, s, c, h

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

t#(t(x)) → t#(x)h#(c(x, y), c(s(z), z), t(w)) → h#(z, c(y, x), t(t(c(x, c(y, t(w))))))
h#(x, c(y, z), t(w)) → t#(w)h#(c(s(x), c(s(0), y)), z, t(x)) → t#(c(x, s(x)))
h#(c(s(x), c(s(0), y)), z, t(x)) → h#(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))h#(c(x, y), c(s(z), z), t(w)) → t#(t(c(x, c(y, t(w)))))
h#(c(x, y), c(s(z), z), t(w)) → t#(c(x, c(y, t(w))))h#(x, c(y, z), t(w)) → t#(c(t(w), w))
t#(t(x)) → t#(c(t(x), x))h#(c(x, y), c(s(z), z), t(w)) → t#(w)
h#(c(s(x), c(s(0), y)), z, t(x)) → t#(t(c(x, s(x))))h#(x, c(y, z), t(w)) → h#(c(s(y), x), z, t(c(t(w), w)))

Rewrite Rules

h(c(x, y), c(s(z), z), t(w)) → h(z, c(y, x), t(t(c(x, c(y, t(w))))))h(x, c(y, z), t(w)) → h(c(s(y), x), z, t(c(t(w), w)))
h(c(s(x), c(s(0), y)), z, t(x)) → h(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))t(t(x)) → t(c(t(x), x))
t(x) → xt(x) → c(0, c(0, c(0, c(0, c(0, x)))))

Original Signature

Termination of terms over the following signature is verified: t, 0, s, c, h

Strategy

The following SCCs where found

h#(c(x, y), c(s(z), z), t(w)) → h#(z, c(y, x), t(t(c(x, c(y, t(w))))))h#(c(s(x), c(s(0), y)), z, t(x)) → h#(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))
h#(x, c(y, z), t(w)) → h#(c(s(y), x), z, t(c(t(w), w)))
t#(t(x)) → t#(x)t#(t(x)) → t#(c(t(x), x))

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

t#(t(x)) → t#(x)t#(t(x)) → t#(c(t(x), x))

Rewrite Rules

h(c(x, y), c(s(z), z), t(w)) → h(z, c(y, x), t(t(c(x, c(y, t(w))))))h(x, c(y, z), t(w)) → h(c(s(y), x), z, t(c(t(w), w)))
h(c(s(x), c(s(0), y)), z, t(x)) → h(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))t(t(x)) → t(c(t(x), x))
t(x) → xt(x) → c(0, c(0, c(0, c(0, c(0, x)))))

Original Signature

Termination of terms over the following signature is verified: t, 0, s, c, h

Strategy

Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

t#(t(x)) → t#(x)t#(t(x)) → t#(c(t(x), x))

Problem 3: PolynomialLinearRange8NegiUR

Dependency Pair Problem

Dependency Pairs

h#(c(x, y), c(s(z), z), t(w)) → h#(z, c(y, x), t(t(c(x, c(y, t(w))))))h#(c(s(x), c(s(0), y)), z, t(x)) → h#(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))
h#(x, c(y, z), t(w)) → h#(c(s(y), x), z, t(c(t(w), w)))

Rewrite Rules

h(c(x, y), c(s(z), z), t(w)) → h(z, c(y, x), t(t(c(x, c(y, t(w))))))h(x, c(y, z), t(w)) → h(c(s(y), x), z, t(c(t(w), w)))
h(c(s(x), c(s(0), y)), z, t(x)) → h(y, c(s(0), c(x, z)), t(t(c(x, s(x)))))t(t(x)) → t(c(t(x), x))
t(x) → xt(x) → c(0, c(0, c(0, c(0, c(0, x)))))

Original Signature

Termination of terms over the following signature is verified: t, 0, s, c, h

Strategy

Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

h#(c(x, y), c(s(z), z), t(w)) → h#(z, c(y, x), t(t(c(x, c(y, t(w))))))