The TRS could be proven terminating. The proof took 33 ms.
Problem 1 was processed with processor DependencyGraph (24ms).
| or#(x, y) | → | if#(x, true, y) | and#(x, y) | → | if#(x, y, false) | |
| =#(x, y) | → | if#(x, y, not(y)) | implies#(x, y) | → | if#(x, y, true) | |
| =#(x, y) | → | not#(y) | not#(x) | → | if#(x, false, true) | |
| =#(x, y) | → | if#(x, y, if(y, false, true)) | =#(x, y) | → | if#(y, false, true) |
| not(x) | → | if(x, false, true) | and(x, y) | → | if(x, y, false) | |
| or(x, y) | → | if(x, true, y) | implies(x, y) | → | if(x, y, true) | |
| =(x, x) | → | true | =(x, y) | → | if(x, y, not(y)) | |
| if(true, x, y) | → | x | if(false, x, y) | → | y | |
| if(x, x, if(x, false, true)) | → | true | =(x, y) | → | if(x, y, if(y, false, true)) |
Termination of terms over the following signature is verified: not, if, or, implies, false, true, =, and