The TRS could be proven terminating. The proof took 168 ms.
Problem 1 was processed with processor PolynomialLinearRange4iUR (123ms). | – Problem 2 was processed with processor PolynomialLinearRange4iUR (22ms).
| implies#(x, or(y, z)) | → | implies#(x, z) | implies#(not(x), or(y, z)) | → | implies#(y, or(x, z)) |
| 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)) |
Termination of terms over the following signature is verified: not, or, implies
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) |
| implies#(not(x), or(y, z)) | → | implies#(y, or(x, z)) |
| 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)) |
Termination of terms over the following signature is verified: not, or, implies
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)) |