YES

The TRS could be proven terminating. The proof took 168 ms.

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (123ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (22ms).

Problem 1: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

implies#(x, or(y, z))implies#(x, z)implies#(not(x), or(y, z))implies#(y, or(x, z))

Rewrite Rules

implies(not(x), y)or(x, y)implies(not(x), or(y, z))implies(y, or(x, z))
implies(x, or(y, z))or(y, implies(x, z))

Original Signature

Termination of terms over the following signature is verified: not, or, implies

Strategy


Polynomial Interpretation

There are no usable rules

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

implies#(x, or(y, z))implies#(x, z)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

implies#(not(x), or(y, z))implies#(y, or(x, z))

Rewrite Rules

implies(not(x), y)or(x, y)implies(not(x), or(y, z))implies(y, or(x, z))
implies(x, or(y, z))or(y, implies(x, z))

Original Signature

Termination of terms over the following signature is verified: not, or, implies

Strategy


Polynomial Interpretation

There are no usable rules

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

implies#(not(x), or(y, z))implies#(y, or(x, z))