YES

The TRS could be proven terminating. The proof took 2707 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (176ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (1182ms).
 |    | – Problem 3 was processed with processor DependencyGraph (13ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (422ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (293ms).
 |    |    |    |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (381ms).
 |    |    |    |    |    | – Problem 7 was processed with processor DependencyGraph (2ms).
 |    |    |    |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (149ms).
 |    |    |    |    |    |    |    | – Problem 9 was processed with processor DependencyGraph (0ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(first(X1, X2))mark#(X2)mark#(if(X1, X2, X3))a__if#(mark(X1), X2, X3)
mark#(first(X1, X2))a__first#(mark(X1), mark(X2))mark#(from(X))a__from#(X)
a__and#(true, X)mark#(X)a__if#(true, X, Y)mark#(X)
a__add#(0, X)mark#(X)mark#(and(X1, X2))mark#(X1)
mark#(and(X1, X2))a__and#(mark(X1), X2)mark#(add(X1, X2))a__add#(mark(X1), X2)
a__if#(false, X, Y)mark#(Y)mark#(first(X1, X2))mark#(X1)
mark#(if(X1, X2, X3))mark#(X1)mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, first, a__first, a__from, cons, nil

Strategy


The following SCCs where found

mark#(and(X1, X2)) → mark#(X1)mark#(first(X1, X2)) → mark#(X2)
mark#(if(X1, X2, X3)) → a__if#(mark(X1), X2, X3)mark#(add(X1, X2)) → a__add#(mark(X1), X2)
mark#(and(X1, X2)) → a__and#(mark(X1), X2)a__if#(false, X, Y) → mark#(Y)
mark#(first(X1, X2)) → mark#(X1)mark#(if(X1, X2, X3)) → mark#(X1)
a__and#(true, X) → mark#(X)a__if#(true, X, Y) → mark#(X)
mark#(add(X1, X2)) → mark#(X1)a__add#(0, X) → mark#(X)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(and(X1, X2))mark#(X1)mark#(first(X1, X2))mark#(X2)
mark#(add(X1, X2))a__add#(mark(X1), X2)mark#(and(X1, X2))a__and#(mark(X1), X2)
mark#(if(X1, X2, X3))a__if#(mark(X1), X2, X3)a__if#(false, X, Y)mark#(Y)
mark#(first(X1, X2))mark#(X1)mark#(if(X1, X2, X3))mark#(X1)
a__and#(true, X)mark#(X)a__if#(true, X, Y)mark#(X)
mark#(add(X1, X2))mark#(X1)a__add#(0, X)mark#(X)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, first, a__first, a__from, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

a__first(X1, X2)first(X1, X2)a__from(X)cons(X, from(s(X)))
a__from(X)from(X)a__and(true, X)mark(X)
a__if(X1, X2, X3)if(X1, X2, X3)a__first(0, X)nil
a__add(X1, X2)add(X1, X2)a__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
mark(nil)nila__add(0, X)mark(X)
a__and(false, Y)falsemark(s(X))s(X)
mark(0)0mark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(false, X, Y)mark(Y)
mark(false)falsemark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(true)true
mark(from(X))a__from(X)mark(and(X1, X2))a__and(mark(X1), X2)
a__add(s(X), Y)s(add(X, Y))a__if(true, X, Y)mark(X)
mark(add(X1, X2))a__add(mark(X1), X2)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark#(if(X1, X2, X3))a__if#(mark(X1), X2, X3)

Problem 3: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(and(X1, X2))mark#(X1)mark#(first(X1, X2))mark#(X2)
mark#(and(X1, X2))a__and#(mark(X1), X2)mark#(add(X1, X2))a__add#(mark(X1), X2)
a__if#(false, X, Y)mark#(Y)mark#(first(X1, X2))mark#(X1)
a__and#(true, X)mark#(X)mark#(if(X1, X2, X3))mark#(X1)
a__if#(true, X, Y)mark#(X)a__add#(0, X)mark#(X)
mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, a__first, first, a__from, nil, cons

Strategy


The following SCCs where found

mark#(and(X1, X2)) → mark#(X1)mark#(first(X1, X2)) → mark#(X2)
mark#(add(X1, X2)) → a__add#(mark(X1), X2)mark#(and(X1, X2)) → a__and#(mark(X1), X2)
mark#(first(X1, X2)) → mark#(X1)mark#(if(X1, X2, X3)) → mark#(X1)
a__and#(true, X) → mark#(X)mark#(add(X1, X2)) → mark#(X1)
a__add#(0, X) → mark#(X)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(and(X1, X2))mark#(X1)mark#(first(X1, X2))mark#(X2)
mark#(add(X1, X2))a__add#(mark(X1), X2)mark#(and(X1, X2))a__and#(mark(X1), X2)
mark#(first(X1, X2))mark#(X1)mark#(if(X1, X2, X3))mark#(X1)
a__and#(true, X)mark#(X)mark#(add(X1, X2))mark#(X1)
a__add#(0, X)mark#(X)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, a__first, first, a__from, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark#(first(X1, X2))mark#(X2)mark#(first(X1, X2))mark#(X1)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(and(X1, X2))mark#(X1)mark#(and(X1, X2))a__and#(mark(X1), X2)
mark#(add(X1, X2))a__add#(mark(X1), X2)a__and#(true, X)mark#(X)
mark#(if(X1, X2, X3))mark#(X1)a__add#(0, X)mark#(X)
mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, first, a__first, a__from, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark#(if(X1, X2, X3))mark#(X1)

Problem 6: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(and(X1, X2))mark#(X1)mark#(add(X1, X2))a__add#(mark(X1), X2)
mark#(and(X1, X2))a__and#(mark(X1), X2)a__and#(true, X)mark#(X)
mark#(add(X1, X2))mark#(X1)a__add#(0, X)mark#(X)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, a__first, first, a__from, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

a__first(X1, X2)first(X1, X2)a__from(X)cons(X, from(s(X)))
a__from(X)from(X)a__and(true, X)mark(X)
a__if(X1, X2, X3)if(X1, X2, X3)a__first(0, X)nil
a__add(X1, X2)add(X1, X2)a__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
mark(nil)nila__add(0, X)mark(X)
a__and(false, Y)falsemark(s(X))s(X)
mark(0)0mark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(false, X, Y)mark(Y)
mark(false)falsemark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(true)true
mark(from(X))a__from(X)mark(and(X1, X2))a__and(mark(X1), X2)
a__add(s(X), Y)s(add(X, Y))a__if(true, X, Y)mark(X)
mark(add(X1, X2))a__add(mark(X1), X2)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

a__and#(true, X)mark#(X)

Problem 7: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(and(X1, X2))mark#(X1)mark#(and(X1, X2))a__and#(mark(X1), X2)
mark#(add(X1, X2))a__add#(mark(X1), X2)a__add#(0, X)mark#(X)
mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, first, a__first, a__from, cons, nil

Strategy


The following SCCs where found

mark#(and(X1, X2)) → mark#(X1)mark#(add(X1, X2)) → a__add#(mark(X1), X2)
a__add#(0, X) → mark#(X)mark#(add(X1, X2)) → mark#(X1)

Problem 8: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(and(X1, X2))mark#(X1)mark#(add(X1, X2))a__add#(mark(X1), X2)
a__add#(0, X)mark#(X)mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, first, a__first, a__from, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark#(and(X1, X2))mark#(X1)mark#(add(X1, X2))a__add#(mark(X1), X2)
mark#(add(X1, X2))mark#(X1)

Problem 9: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__add#(0, X)mark#(X)

Rewrite Rules

a__and(true, X)mark(X)a__and(false, Y)false
a__if(true, X, Y)mark(X)a__if(false, X, Y)mark(Y)
a__add(0, X)mark(X)a__add(s(X), Y)s(add(X, Y))
a__first(0, X)nila__first(s(X), cons(Y, Z))cons(Y, first(X, Z))
a__from(X)cons(X, from(s(X)))mark(and(X1, X2))a__and(mark(X1), X2)
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(add(X1, X2))a__add(mark(X1), X2)
mark(first(X1, X2))a__first(mark(X1), mark(X2))mark(from(X))a__from(X)
mark(true)truemark(false)false
mark(0)0mark(s(X))s(X)
mark(nil)nilmark(cons(X1, X2))cons(X1, X2)
a__and(X1, X2)and(X1, X2)a__if(X1, X2, X3)if(X1, X2, X3)
a__add(X1, X2)add(X1, X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: true, mark, from, a__add, add, and, a__and, 0, a__if, s, if, false, a__first, first, a__from, nil, cons

Strategy


There are no SCCs!