The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (204ms), SubtermCriterion (0ms), DependencyGraph (167ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (129ms), PolynomialLinearRange8NegiUR (30000ms), ReductionPairSAT (5601ms), DependencyGraph (152ms), SizeChangePrinciple (timeout)].
| mark#(diff(X1, X2)) | → | mark#(X1) | mark#(leq(X1, X2)) | → | mark#(X1) | |
| mark#(if(X1, X2, X3)) | → | a__if#(mark(X1), X2, X3) | mark#(p(X)) | → | a__p#(mark(X)) | |
| mark#(leq(X1, X2)) | → | mark#(X2) | a__if#(true, X, Y) | → | mark#(X) | |
| mark#(diff(X1, X2)) | → | mark#(X2) | a__diff#(X, Y) | → | mark#(Y) | |
| mark#(diff(X1, X2)) | → | a__diff#(mark(X1), mark(X2)) | a__leq#(s(X), s(Y)) | → | mark#(X) | |
| mark#(p(X)) | → | mark#(X) | a__if#(false, X, Y) | → | mark#(Y) | |
| mark#(leq(X1, X2)) | → | a__leq#(mark(X1), mark(X2)) | mark#(if(X1, X2, X3)) | → | mark#(X1) | |
| a__diff#(X, Y) | → | mark#(X) | mark#(s(X)) | → | mark#(X) | |
| a__leq#(s(X), s(Y)) | → | mark#(Y) | a__diff#(X, Y) | → | a__leq#(mark(X), mark(Y)) | |
| a__p#(s(X)) | → | mark#(X) | a__leq#(s(X), s(Y)) | → | a__leq#(mark(X), mark(Y)) | |
| a__diff#(X, Y) | → | a__if#(a__leq(mark(X), mark(Y)), 0, s(diff(p(X), Y))) |
| a__p(0) | → | 0 | a__p(s(X)) | → | mark(X) | |
| a__leq(0, Y) | → | true | a__leq(s(X), 0) | → | false | |
| a__leq(s(X), s(Y)) | → | a__leq(mark(X), mark(Y)) | a__if(true, X, Y) | → | mark(X) | |
| a__if(false, X, Y) | → | mark(Y) | a__diff(X, Y) | → | a__if(a__leq(mark(X), mark(Y)), 0, s(diff(p(X), Y))) | |
| mark(p(X)) | → | a__p(mark(X)) | mark(leq(X1, X2)) | → | a__leq(mark(X1), mark(X2)) | |
| mark(if(X1, X2, X3)) | → | a__if(mark(X1), X2, X3) | mark(diff(X1, X2)) | → | a__diff(mark(X1), mark(X2)) | |
| mark(0) | → | 0 | mark(s(X)) | → | s(mark(X)) | |
| mark(true) | → | true | mark(false) | → | false | |
| a__p(X) | → | p(X) | a__leq(X1, X2) | → | leq(X1, X2) | |
| a__if(X1, X2, X3) | → | if(X1, X2, X3) | a__diff(X1, X2) | → | diff(X1, X2) |
Termination of terms over the following signature is verified: a__p, diff, leq, true, mark, a__diff, 0, s, a__leq, a__if, if, p, false