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 (114ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (4ms), PolynomialLinearRange4 (197ms), DependencyGraph (7ms), ReductionPairSAT (189ms), DependencyGraph (1ms), SizeChangePrinciple (448ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (0ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| U171#(1, x) | → | f#(0) | | f#(x) | → | U171#(implies(implies(x, implies(x, 0)), 0), x) |
Rewrite Rules
| or(0, x) | → | x | | or(x, 0) | → | x |
| or(1, x) | → | 1 | | or(x, 1) | → | 1 |
| or(x, not(x)) | → | 1 | | or(not(x), x) | → | 1 |
| and(0, x) | → | 0 | | and(x, 0) | → | 0 |
| and(1, x) | → | x | | and(x, 1) | → | x |
| and(x, not(x)) | → | 0 | | and(not(x), x) | → | 0 |
| not(1) | → | 0 | | not(0) | → | 1 |
| implies(x, y) | → | U141(not(x), y, x) | | U141(1, y, x) | → | 1 |
| implies(x, y) | → | U151(y, y, x) | | U151(1, y, x) | → | 1 |
| implies(x, y) | → | U161(x, y, x) | | U161(1, y, x) | → | U162(y, y, x) |
| U162(0, y, x) | → | 0 | | f(x) | → | U171(implies(implies(x, implies(x, 0)), 0), x) |
| U171(1, x) | → | f(0) |
Original Signature
Termination of terms over the following signature is verified: f, not, 1, 0, or, implies, and
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| implies#(x, y) | → | not#(x) | | f#(x) | → | implies#(implies(x, implies(x, 0)), 0) |
| f#(x) | → | implies#(x, implies(x, 0)) | | implies#(x, y) | → | U151#(y, y, x) |
| U171#(1, x) | → | f#(0) | | U161#(1, y, x) | → | U162#(y, y, x) |
| U161#(1, y, x) | → | T(y) | | f#(x) | → | implies#(x, 0) |
| implies#(x, y) | → | U141#(not(x), y, x) | | implies#(x, y) | → | U161#(x, y, x) |
| f#(x) | → | U171#(implies(implies(x, implies(x, 0)), 0), x) |
Rewrite Rules
| or(0, x) | → | x | | or(x, 0) | → | x |
| or(1, x) | → | 1 | | or(x, 1) | → | 1 |
| or(x, not(x)) | → | 1 | | or(not(x), x) | → | 1 |
| and(0, x) | → | 0 | | and(x, 0) | → | 0 |
| and(1, x) | → | x | | and(x, 1) | → | x |
| and(x, not(x)) | → | 0 | | and(not(x), x) | → | 0 |
| not(1) | → | 0 | | not(0) | → | 1 |
| implies(x, y) | → | U141(not(x), y, x) | | U141(1, y, x) | → | 1 |
| implies(x, y) | → | U151(y, y, x) | | U151(1, y, x) | → | 1 |
| implies(x, y) | → | U161(x, y, x) | | U161(1, y, x) | → | U162(y, y, x) |
| U162(0, y, x) | → | 0 | | f(x) | → | U171(implies(implies(x, implies(x, 0)), 0), x) |
| U171(1, x) | → | f(0) |
Original Signature
Termination of terms over the following signature is verified: not, f, 1, 0, or, implies, and
Strategy
Context-sensitive strategy:
μ(T) = μ(1) = μ(0) = ∅
μ(f) = μ(U171) = μ(f#) = μ(U151#) = μ(U161) = μ(U162) = μ(U151) = μ(U171#) = μ(not) = μ(U141) = μ(U161#) = μ(U162#) = μ(not#) = μ(U141#) = {1}
μ(or) = μ(implies) = μ(and#) = μ(or#) = μ(implies#) = μ(and) = {1, 2}
The following SCCs where found
| U171#(1, x) → f#(0) | f#(x) → U171#(implies(implies(x, implies(x, 0)), 0), x) |