TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60116 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (434ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (172ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (131ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (124ms), ReductionPairSAT (1429ms), DependencyGraph (153ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| mark#(h(X1, X2)) | → | mark#(X1) | | a__A# | → | a__h#(a__f(a__a), a__f(a__b)) |
| a__A# | → | a__f#(a__b) | | mark#(g(X1, X2, X3)) | → | mark#(X3) |
| mark#(z(X1, X2)) | → | a__z#(mark(X1), X2) | | mark#(h(X1, X2)) | → | a__h#(mark(X1), mark(X2)) |
| a__h#(X, X) | → | a__g#(mark(X), mark(X), a__f(a__k)) | | a__g#(d, X, X) | → | a__A# |
| mark#(f(X)) | → | a__f#(mark(X)) | | mark#(A) | → | a__A# |
| mark#(f(X)) | → | mark#(X) | | a__A# | → | a__f#(a__a) |
| mark#(g(X1, X2, X3)) | → | mark#(X2) | | mark#(z(X1, X2)) | → | mark#(X1) |
| a__h#(X, X) | → | a__f#(a__k) | | mark#(g(X1, X2, X3)) | → | mark#(X1) |
| a__f#(X) | → | a__z#(mark(X), X) | | a__f#(X) | → | mark#(X) |
| a__h#(X, X) | → | mark#(X) | | mark#(h(X1, X2)) | → | mark#(X2) |
| a__z#(e, X) | → | mark#(X) | | mark#(g(X1, X2, X3)) | → | a__g#(mark(X1), mark(X2), mark(X3)) |
Rewrite Rules
| a__a | → | a__c | | a__b | → | a__c |
| a__c | → | e | | a__k | → | l |
| a__d | → | m | | a__a | → | a__d |
| a__b | → | a__d | | a__c | → | l |
| a__k | → | m | | a__A | → | a__h(a__f(a__a), a__f(a__b)) |
| a__h(X, X) | → | a__g(mark(X), mark(X), a__f(a__k)) | | a__g(d, X, X) | → | a__A |
| a__f(X) | → | a__z(mark(X), X) | | a__z(e, X) | → | mark(X) |
| mark(A) | → | a__A | | mark(a) | → | a__a |
| mark(b) | → | a__b | | mark(c) | → | a__c |
| mark(d) | → | a__d | | mark(k) | → | a__k |
| mark(z(X1, X2)) | → | a__z(mark(X1), X2) | | mark(f(X)) | → | a__f(mark(X)) |
| mark(h(X1, X2)) | → | a__h(mark(X1), mark(X2)) | | mark(g(X1, X2, X3)) | → | a__g(mark(X1), mark(X2), mark(X3)) |
| mark(e) | → | e | | mark(l) | → | l |
| mark(m) | → | m | | a__A | → | A |
| a__a | → | a | | a__b | → | b |
| a__c | → | c | | a__d | → | d |
| a__k | → | k | | a__z(X1, X2) | → | z(X1, X2) |
| a__f(X) | → | f(X) | | a__h(X1, X2) | → | h(X1, X2) |
| a__g(X1, X2, X3) | → | g(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: f, g, a__k, d, e, b, a__A, c, A, a, a__d, a__c, a__b, l, mark, a__a, m, a__h, k, a__g, h, a__f, a__z, z
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(k) | → | a__k# | | a__A# | → | a__h#(a__f(a__a), a__f(a__b)) |
| a__b# | → | a__c# | | mark#(A) | → | a__A# |
| mark#(d) | → | a__d# | | a__h#(X, X) | → | a__k# |
| mark#(b) | → | a__b# | | a__A# | → | a__f#(a__a) |
| a__h#(X, X) | → | mark#(X) | | a__A# | → | a__a# |
| mark#(g(X1, X2, X3)) | → | a__g#(mark(X1), mark(X2), mark(X3)) | | mark#(h(X1, X2)) | → | mark#(X1) |
| mark#(a) | → | a__a# | | mark#(g(X1, X2, X3)) | → | mark#(X3) |
| a__A# | → | a__f#(a__b) | | mark#(z(X1, X2)) | → | a__z#(mark(X1), X2) |
| mark#(h(X1, X2)) | → | a__h#(mark(X1), mark(X2)) | | a__h#(X, X) | → | a__g#(mark(X), mark(X), a__f(a__k)) |
| a__g#(d, X, X) | → | a__A# | | mark#(f(X)) | → | a__f#(mark(X)) |
| mark#(f(X)) | → | mark#(X) | | a__a# | → | a__c# |
| mark#(g(X1, X2, X3)) | → | mark#(X2) | | mark#(z(X1, X2)) | → | mark#(X1) |
| a__b# | → | a__d# | | a__A# | → | a__b# |
| a__h#(X, X) | → | a__f#(a__k) | | mark#(g(X1, X2, X3)) | → | mark#(X1) |
| a__f#(X) | → | a__z#(mark(X), X) | | a__f#(X) | → | mark#(X) |
| mark#(c) | → | a__c# | | a__a# | → | a__d# |
| mark#(h(X1, X2)) | → | mark#(X2) | | a__z#(e, X) | → | mark#(X) |
Rewrite Rules
| a__a | → | a__c | | a__b | → | a__c |
| a__c | → | e | | a__k | → | l |
| a__d | → | m | | a__a | → | a__d |
| a__b | → | a__d | | a__c | → | l |
| a__k | → | m | | a__A | → | a__h(a__f(a__a), a__f(a__b)) |
| a__h(X, X) | → | a__g(mark(X), mark(X), a__f(a__k)) | | a__g(d, X, X) | → | a__A |
| a__f(X) | → | a__z(mark(X), X) | | a__z(e, X) | → | mark(X) |
| mark(A) | → | a__A | | mark(a) | → | a__a |
| mark(b) | → | a__b | | mark(c) | → | a__c |
| mark(d) | → | a__d | | mark(k) | → | a__k |
| mark(z(X1, X2)) | → | a__z(mark(X1), X2) | | mark(f(X)) | → | a__f(mark(X)) |
| mark(h(X1, X2)) | → | a__h(mark(X1), mark(X2)) | | mark(g(X1, X2, X3)) | → | a__g(mark(X1), mark(X2), mark(X3)) |
| mark(e) | → | e | | mark(l) | → | l |
| mark(m) | → | m | | a__A | → | A |
| a__a | → | a | | a__b | → | b |
| a__c | → | c | | a__d | → | d |
| a__k | → | k | | a__z(X1, X2) | → | z(X1, X2) |
| a__f(X) | → | f(X) | | a__h(X1, X2) | → | h(X1, X2) |
| a__g(X1, X2, X3) | → | g(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: f, g, a__k, d, e, b, a__A, c, A, a, a__d, a__c, mark, l, a__b, m, a__a, a__h, a__g, k, a__f, h, a__z, z
Strategy
The following SCCs where found
| a__A# → a__h#(a__f(a__a), a__f(a__b)) | mark#(h(X1, X2)) → mark#(X1) |
| mark#(z(X1, X2)) → a__z#(mark(X1), X2) | mark#(g(X1, X2, X3)) → mark#(X3) |
| a__A# → a__f#(a__b) | mark#(h(X1, X2)) → a__h#(mark(X1), mark(X2)) |
| a__h#(X, X) → a__g#(mark(X), mark(X), a__f(a__k)) | a__g#(d, X, X) → a__A# |
| mark#(f(X)) → a__f#(mark(X)) | mark#(A) → a__A# |
| mark#(f(X)) → mark#(X) | mark#(g(X1, X2, X3)) → mark#(X2) |
| a__A# → a__f#(a__a) | mark#(z(X1, X2)) → mark#(X1) |
| mark#(g(X1, X2, X3)) → mark#(X1) | a__h#(X, X) → a__f#(a__k) |
| a__f#(X) → a__z#(mark(X), X) | a__h#(X, X) → mark#(X) |
| a__f#(X) → mark#(X) | mark#(h(X1, X2)) → mark#(X2) |
| a__z#(e, X) → mark#(X) | mark#(g(X1, X2, X3)) → a__g#(mark(X1), mark(X2), mark(X3)) |