TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60012 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1834ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 8 was processed with processor ReductionPairSAT (104ms).
 |    |    | – Problem 12 was processed with processor ReductionPairSAT (24ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 9 was processed with processor ReductionPairSAT (436ms).
 |    |    | – Problem 13 was processed with processor ReductionPairSAT (283ms).
 |    |    |    | – Problem 16 was processed with processor ReductionPairSAT (177ms).
 |    |    |    |    | – Problem 17 was processed with processor ReductionPairSAT (93ms).
 | – Problem 4 was processed with processor ReductionPairSAT (5048ms).
 |    | – Problem 11 was processed with processor ReductionPairSAT (4916ms).
 |    |    | – Problem 15 was processed with processor ReductionPairSAT (6237ms).
 |    |    |    | – Problem 18 remains open; application of the following processors failed [DependencyGraph (196ms), ReductionPairSAT (17332ms), DependencyGraph (191ms), ReductionPairSAT (11101ms)].
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 10 was processed with processor ReductionPairSAT (70ms).
 |    |    | – Problem 14 was processed with processor ReductionPairSAT (24ms).
 | – Problem 6 was processed with processor SubtermCriterion (0ms).
 | – Problem 7 was processed with processor SubtermCriterion (4ms).

The following open problems remain:

Open Dependency Pair Problem 18

Dependency Pairs

mark#(diff(X1, X2)) → mark#(X1)mark#(leq(X1, X2)) → mark#(X1)
active#(diff(X, Y)) → mark#(if(leq(X, Y), 0, s(diff(p(X), Y))))mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3))
active#(if(false, X, Y)) → mark#(Y)mark#(diff(X1, X2)) → active#(diff(mark(X1), mark(X2)))
mark#(leq(X1, X2)) → active#(leq(mark(X1), mark(X2)))mark#(leq(X1, X2)) → mark#(X2)
mark#(p(X)) → active#(p(mark(X)))mark#(diff(X1, X2)) → mark#(X2)
active#(if(true, X, Y)) → mark#(X)active#(leq(s(X), 0)) → mark#(false)
mark#(p(X)) → mark#(X)active#(p(s(X))) → mark#(X)
active#(p(0)) → mark#(0)mark#(if(X1, X2, X3)) → mark#(X1)
mark#(s(X)) → mark#(X)active#(leq(0, Y)) → mark#(true)
active#(leq(s(X), s(Y))) → mark#(leq(X, Y))

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

active#(diff(X, Y)) → leq#(X, Y)leq#(X1, active(X2)) → leq#(X1, X2)
if#(X1, X2, active(X3)) → if#(X1, X2, X3)mark#(s(X)) → s#(mark(X))
active#(if(true, X, Y)) → mark#(X)mark#(diff(X1, X2)) → diff#(mark(X1), mark(X2))
mark#(s(X)) → mark#(X)active#(leq(s(X), s(Y))) → mark#(leq(X, Y))
active#(diff(X, Y)) → mark#(if(leq(X, Y), 0, s(diff(p(X), Y))))active#(diff(X, Y)) → p#(X)
mark#(true) → active#(true)leq#(X1, mark(X2)) → leq#(X1, X2)
mark#(leq(X1, X2)) → active#(leq(mark(X1), mark(X2)))mark#(p(X)) → active#(p(mark(X)))
active#(leq(s(X), 0)) → mark#(false)if#(X1, mark(X2), X3) → if#(X1, X2, X3)
mark#(p(X)) → mark#(X)if#(X1, X2, mark(X3)) → if#(X1, X2, X3)
active#(p(0)) → mark#(0)if#(mark(X1), X2, X3) → if#(X1, X2, X3)
mark#(if(X1, X2, X3)) → mark#(X1)active#(diff(X, Y)) → if#(leq(X, Y), 0, s(diff(p(X), Y)))
active#(diff(X, Y)) → s#(diff(p(X), Y))mark#(false) → active#(false)
mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3))leq#(mark(X1), X2) → leq#(X1, X2)
active#(if(false, X, Y)) → mark#(Y)if#(X1, active(X2), X3) → if#(X1, X2, X3)
p#(mark(X)) → p#(X)mark#(diff(X1, X2)) → mark#(X2)
active#(leq(s(X), s(Y))) → leq#(X, Y)diff#(X1, active(X2)) → diff#(X1, X2)
active#(leq(0, Y)) → mark#(true)active#(diff(X, Y)) → diff#(p(X), Y)
mark#(if(X1, X2, X3)) → if#(mark(X1), X2, X3)mark#(diff(X1, X2)) → mark#(X1)
mark#(leq(X1, X2)) → mark#(X1)mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))leq#(active(X1), X2) → leq#(X1, X2)
diff#(mark(X1), X2) → diff#(X1, X2)diff#(X1, mark(X2)) → diff#(X1, X2)
mark#(diff(X1, X2)) → active#(diff(mark(X1), mark(X2)))mark#(leq(X1, X2)) → mark#(X2)
if#(active(X1), X2, X3) → if#(X1, X2, X3)s#(mark(X)) → s#(X)
diff#(active(X1), X2) → diff#(X1, X2)mark#(leq(X1, X2)) → leq#(mark(X1), mark(X2))
mark#(p(X)) → p#(mark(X))active#(p(s(X))) → mark#(X)
s#(active(X)) → s#(X)p#(active(X)) → p#(X)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

The following SCCs where found

p#(mark(X)) → p#(X)p#(active(X)) → p#(X)
diff#(active(X1), X2) → diff#(X1, X2)diff#(mark(X1), X2) → diff#(X1, X2)
diff#(X1, mark(X2)) → diff#(X1, X2)diff#(X1, active(X2)) → diff#(X1, X2)
s#(mark(X)) → s#(X)s#(active(X)) → s#(X)
if#(X1, mark(X2), X3) → if#(X1, X2, X3)if#(X1, X2, mark(X3)) → if#(X1, X2, X3)
if#(mark(X1), X2, X3) → if#(X1, X2, X3)if#(X1, active(X2), X3) → if#(X1, X2, X3)
if#(X1, X2, active(X3)) → if#(X1, X2, X3)if#(active(X1), X2, X3) → if#(X1, X2, X3)
leq#(mark(X1), X2) → leq#(X1, X2)leq#(X1, mark(X2)) → leq#(X1, X2)
leq#(active(X1), X2) → leq#(X1, X2)leq#(X1, active(X2)) → leq#(X1, X2)
mark#(diff(X1, X2)) → mark#(X1)mark#(0) → active#(0)
mark#(false) → active#(false)active#(diff(X, Y)) → mark#(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark#(leq(X1, X2)) → mark#(X1)mark#(s(X)) → active#(s(mark(X)))
mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3))active#(if(false, X, Y)) → mark#(Y)
mark#(true) → active#(true)mark#(diff(X1, X2)) → active#(diff(mark(X1), mark(X2)))
mark#(leq(X1, X2)) → mark#(X2)mark#(leq(X1, X2)) → active#(leq(mark(X1), mark(X2)))
mark#(p(X)) → active#(p(mark(X)))mark#(diff(X1, X2)) → mark#(X2)
active#(if(true, X, Y)) → mark#(X)active#(leq(s(X), 0)) → mark#(false)
mark#(p(X)) → mark#(X)active#(p(s(X))) → mark#(X)
active#(p(0)) → mark#(0)mark#(if(X1, X2, X3)) → mark#(X1)
mark#(s(X)) → mark#(X)active#(leq(0, Y)) → mark#(true)
active#(leq(s(X), s(Y))) → mark#(leq(X, Y))

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

diff#(active(X1), X2) → diff#(X1, X2)diff#(mark(X1), X2) → diff#(X1, X2)
diff#(X1, mark(X2)) → diff#(X1, X2)diff#(X1, active(X2)) → diff#(X1, X2)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

diff#(active(X1), X2) → diff#(X1, X2)diff#(mark(X1), X2) → diff#(X1, X2)

Problem 8: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

diff#(X1, mark(X2)) → diff#(X1, X2)diff#(X1, active(X2)) → diff#(X1, X2)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, if, leq, p, false, true, active, mark

Strategy

Function Precedence

mark < active < diff# = 0 = s = diff = if = leq = p = false = true

Argument Filtering

diff#: collapses to 2
0: all arguments are removed from 0
s: all arguments are removed from s
diff: 1 2
if: all arguments are removed from if
leq: all arguments are removed from leq
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: 1
mark: collapses to 1

Status

0: multiset
s: multiset
diff: lexicographic with permutation 1 → 2 2 → 1
if: multiset
leq: multiset
p: multiset
false: multiset
true: multiset
active: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

diff#(X1, active(X2)) → diff#(X1, X2)

Problem 12: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

diff#(X1, mark(X2)) → diff#(X1, X2)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Function Precedence

mark < diff# = 0 = s = diff = if = leq = p = false = true = active

Argument Filtering

diff#: collapses to 2
0: all arguments are removed from 0
s: all arguments are removed from s
diff: all arguments are removed from diff
if: all arguments are removed from if
leq: 1 2
p: collapses to 1
false: all arguments are removed from false
true: all arguments are removed from true
active: all arguments are removed from active
mark: 1

Status

0: multiset
s: multiset
diff: multiset
if: multiset
leq: lexicographic with permutation 1 → 1 2 → 2
false: multiset
true: multiset
active: multiset
mark: lexicographic with permutation 1 → 1

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

diff#(X1, mark(X2)) → diff#(X1, X2)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 9: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, if, leq, p, false, true, active, mark

Strategy

Function Precedence

active = mark < 0 = s = diff = if = leq = p = false = true = if#

Argument Filtering

0: all arguments are removed from 0
s: 1
diff: all arguments are removed from diff
if: 1 2 3
leq: all arguments are removed from leq
p: 1
false: all arguments are removed from false
true: all arguments are removed from true
active: 1
if#: 1 3
mark: collapses to 1

Status

0: multiset
s: lexicographic with permutation 1 → 1
diff: multiset
if: lexicographic with permutation 1 → 1 2 → 2 3 → 3
leq: multiset
p: lexicographic with permutation 1 → 1
false: multiset
true: multiset
active: multiset
if#: lexicographic with permutation 1 → 1 3 → 2

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

if#(X1, X2, active(X3)) → if#(X1, X2, X3)

Problem 13: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Function Precedence

active = mark < 0 = s = diff = if = leq = p = false = true = if#

Argument Filtering

0: all arguments are removed from 0
s: collapses to 1
diff: 1 2
if: 3
leq: all arguments are removed from leq
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: collapses to 1
if#: collapses to 2
mark: 1

Status

0: multiset
diff: lexicographic with permutation 1 → 1 2 → 2
if: lexicographic with permutation 3 → 1
leq: multiset
p: multiset
false: multiset
true: multiset
mark: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 16: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, if, leq, p, false, true, active, mark

Strategy

Function Precedence

mark < 0 = s = diff = if = leq = p = false = true = active = if#

Argument Filtering

0: all arguments are removed from 0
s: all arguments are removed from s
diff: all arguments are removed from diff
if: all arguments are removed from if
leq: all arguments are removed from leq
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: 1
if#: 1 2
mark: collapses to 1

Status

0: multiset
s: multiset
diff: multiset
if: multiset
leq: multiset
p: multiset
false: multiset
true: multiset
active: multiset
if#: lexicographic with permutation 1 → 1 2 → 2

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

if#(X1, active(X2), X3) → if#(X1, X2, X3)

Problem 17: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Function Precedence

mark < 0 = s = diff = if = leq = p = false = true = active = if#

Argument Filtering

0: all arguments are removed from 0
s: all arguments are removed from s
diff: 1 2
if: 2 3
leq: 1 2
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: all arguments are removed from active
if#: collapses to 3
mark: 1

Status

0: multiset
s: multiset
diff: lexicographic with permutation 1 → 2 2 → 1
if: lexicographic with permutation 2 → 1 3 → 2
leq: lexicographic with permutation 1 → 2 2 → 1
p: multiset
false: multiset
true: multiset
active: multiset
mark: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 4: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(diff(X1, X2)) → mark#(X1)mark#(leq(X1, X2)) → mark#(X1)
active#(diff(X, Y)) → mark#(if(leq(X, Y), 0, s(diff(p(X), Y))))mark#(false) → active#(false)
mark#(0) → active#(0)mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3))
mark#(s(X)) → active#(s(mark(X)))mark#(true) → active#(true)
active#(if(false, X, Y)) → mark#(Y)mark#(diff(X1, X2)) → active#(diff(mark(X1), mark(X2)))
mark#(leq(X1, X2)) → active#(leq(mark(X1), mark(X2)))mark#(leq(X1, X2)) → mark#(X2)
mark#(p(X)) → active#(p(mark(X)))mark#(diff(X1, X2)) → mark#(X2)
active#(if(true, X, Y)) → mark#(X)active#(leq(s(X), 0)) → mark#(false)
mark#(p(X)) → mark#(X)active#(p(s(X))) → mark#(X)
active#(p(0)) → mark#(0)mark#(if(X1, X2, X3)) → mark#(X1)
mark#(s(X)) → mark#(X)active#(leq(0, Y)) → mark#(true)
active#(leq(s(X), s(Y))) → mark#(leq(X, Y))

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Function Precedence

active < 0 = s = diff = if = leq = p = false = true = mark = active# = mark#

Argument Filtering

0: all arguments are removed from 0
s: all arguments are removed from s
diff: all arguments are removed from diff
if: all arguments are removed from if
leq: all arguments are removed from leq
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: collapses to 1
mark: all arguments are removed from mark
active#: collapses to 1
mark#: all arguments are removed from mark#

Status

0: multiset
s: multiset
diff: multiset
if: multiset
leq: multiset
p: multiset
false: multiset
true: multiset
mark: multiset
mark#: multiset

Usable Rules

mark(s(X)) → active(s(mark(X)))mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
diff(X1, mark(X2)) → diff(X1, X2)leq(active(X1), X2) → leq(X1, X2)
if(active(X1), X2, X3) → if(X1, X2, X3)active(leq(s(X), 0)) → mark(false)
leq(X1, active(X2)) → leq(X1, X2)mark(true) → active(true)
mark(p(X)) → active(p(mark(X)))active(p(s(X))) → mark(X)
if(X1, X2, active(X3)) → if(X1, X2, X3)diff(mark(X1), X2) → diff(X1, X2)
mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))if(X1, X2, mark(X3)) → if(X1, X2, X3)
s(active(X)) → s(X)mark(0) → active(0)
diff(active(X1), X2) → diff(X1, X2)if(X1, active(X2), X3) → if(X1, X2, X3)
leq(X1, mark(X2)) → leq(X1, X2)if(mark(X1), X2, X3) → if(X1, X2, X3)
active(if(false, X, Y)) → mark(Y)active(p(0)) → mark(0)
leq(mark(X1), X2) → leq(X1, X2)diff(X1, active(X2)) → diff(X1, X2)
mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))if(X1, mark(X2), X3) → if(X1, X2, X3)
p(mark(X)) → p(X)mark(false) → active(false)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))s(mark(X)) → s(X)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(leq(0, Y)) → mark(true)
active(if(true, X, Y)) → mark(X)p(active(X)) → p(X)

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(false) → active#(false)mark#(true) → active#(true)

Problem 11: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(diff(X1, X2)) → mark#(X1)mark#(leq(X1, X2)) → mark#(X1)
active#(diff(X, Y)) → mark#(if(leq(X, Y), 0, s(diff(p(X), Y))))mark#(0) → active#(0)
mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3))mark#(s(X)) → active#(s(mark(X)))
active#(if(false, X, Y)) → mark#(Y)mark#(diff(X1, X2)) → active#(diff(mark(X1), mark(X2)))
mark#(leq(X1, X2)) → active#(leq(mark(X1), mark(X2)))mark#(leq(X1, X2)) → mark#(X2)
mark#(p(X)) → active#(p(mark(X)))mark#(diff(X1, X2)) → mark#(X2)
active#(if(true, X, Y)) → mark#(X)active#(leq(s(X), 0)) → mark#(false)
mark#(p(X)) → mark#(X)active#(p(0)) → mark#(0)
active#(p(s(X))) → mark#(X)mark#(if(X1, X2, X3)) → mark#(X1)
mark#(s(X)) → mark#(X)active#(leq(0, Y)) → mark#(true)
active#(leq(s(X), s(Y))) → mark#(leq(X, Y))

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, if, leq, p, false, true, active, mark

Strategy

Function Precedence

active < 0 = s = diff = if = leq = p = false = true = mark = active# = mark#

Argument Filtering

0: all arguments are removed from 0
s: all arguments are removed from s
diff: all arguments are removed from diff
if: all arguments are removed from if
leq: all arguments are removed from leq
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: collapses to 1
mark: all arguments are removed from mark
active#: collapses to 1
mark#: all arguments are removed from mark#

Status

0: multiset
s: multiset
diff: multiset
if: multiset
leq: multiset
p: multiset
false: multiset
true: multiset
mark: multiset
mark#: multiset

Usable Rules

mark(s(X)) → active(s(mark(X)))mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
diff(X1, mark(X2)) → diff(X1, X2)leq(active(X1), X2) → leq(X1, X2)
if(active(X1), X2, X3) → if(X1, X2, X3)active(leq(s(X), 0)) → mark(false)
leq(X1, active(X2)) → leq(X1, X2)mark(true) → active(true)
mark(p(X)) → active(p(mark(X)))active(p(s(X))) → mark(X)
if(X1, X2, active(X3)) → if(X1, X2, X3)diff(mark(X1), X2) → diff(X1, X2)
mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))if(X1, X2, mark(X3)) → if(X1, X2, X3)
s(active(X)) → s(X)mark(0) → active(0)
diff(active(X1), X2) → diff(X1, X2)if(X1, active(X2), X3) → if(X1, X2, X3)
leq(X1, mark(X2)) → leq(X1, X2)if(mark(X1), X2, X3) → if(X1, X2, X3)
active(if(false, X, Y)) → mark(Y)active(p(0)) → mark(0)
leq(mark(X1), X2) → leq(X1, X2)diff(X1, active(X2)) → diff(X1, X2)
mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))if(X1, mark(X2), X3) → if(X1, X2, X3)
p(mark(X)) → p(X)mark(false) → active(false)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))s(mark(X)) → s(X)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(leq(0, Y)) → mark(true)
active(if(true, X, Y)) → mark(X)p(active(X)) → p(X)

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(0) → active#(0)

Problem 15: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(diff(X1, X2)) → mark#(X1)mark#(leq(X1, X2)) → mark#(X1)
active#(diff(X, Y)) → mark#(if(leq(X, Y), 0, s(diff(p(X), Y))))mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3))
mark#(s(X)) → active#(s(mark(X)))active#(if(false, X, Y)) → mark#(Y)
mark#(diff(X1, X2)) → active#(diff(mark(X1), mark(X2)))mark#(leq(X1, X2)) → active#(leq(mark(X1), mark(X2)))
mark#(leq(X1, X2)) → mark#(X2)mark#(p(X)) → active#(p(mark(X)))
mark#(diff(X1, X2)) → mark#(X2)active#(if(true, X, Y)) → mark#(X)
active#(leq(s(X), 0)) → mark#(false)mark#(p(X)) → mark#(X)
active#(p(s(X))) → mark#(X)active#(p(0)) → mark#(0)
mark#(if(X1, X2, X3)) → mark#(X1)mark#(s(X)) → mark#(X)
active#(leq(0, Y)) → mark#(true)active#(leq(s(X), s(Y))) → mark#(leq(X, Y))

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Function Precedence

0 = diff = if = leq = p = active# = mark# < s = false = true = active = mark

Argument Filtering

0: all arguments are removed from 0
s: all arguments are removed from s
diff: all arguments are removed from diff
if: all arguments are removed from if
leq: all arguments are removed from leq
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: all arguments are removed from active
mark: all arguments are removed from mark
active#: collapses to 1
mark#: all arguments are removed from mark#

Status

0: multiset
s: multiset
diff: multiset
if: multiset
leq: multiset
p: multiset
false: multiset
true: multiset
active: multiset
mark: multiset
mark#: multiset

Usable Rules

mark(s(X)) → active(s(mark(X)))mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
diff(X1, mark(X2)) → diff(X1, X2)leq(active(X1), X2) → leq(X1, X2)
if(active(X1), X2, X3) → if(X1, X2, X3)active(leq(s(X), 0)) → mark(false)
leq(X1, active(X2)) → leq(X1, X2)mark(true) → active(true)
mark(p(X)) → active(p(mark(X)))active(p(s(X))) → mark(X)
if(X1, X2, active(X3)) → if(X1, X2, X3)diff(mark(X1), X2) → diff(X1, X2)
mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))if(X1, X2, mark(X3)) → if(X1, X2, X3)
s(active(X)) → s(X)mark(0) → active(0)
diff(active(X1), X2) → diff(X1, X2)if(X1, active(X2), X3) → if(X1, X2, X3)
leq(X1, mark(X2)) → leq(X1, X2)if(mark(X1), X2, X3) → if(X1, X2, X3)
active(if(false, X, Y)) → mark(Y)active(p(0)) → mark(0)
leq(mark(X1), X2) → leq(X1, X2)diff(X1, active(X2)) → diff(X1, X2)
mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))if(X1, mark(X2), X3) → if(X1, X2, X3)
p(mark(X)) → p(X)mark(false) → active(false)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))s(mark(X)) → s(X)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(leq(0, Y)) → mark(true)
active(if(true, X, Y)) → mark(X)p(active(X)) → p(X)

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(s(X)) → active#(s(mark(X)))

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

leq#(mark(X1), X2) → leq#(X1, X2)leq#(X1, mark(X2)) → leq#(X1, X2)
leq#(active(X1), X2) → leq#(X1, X2)leq#(X1, active(X2)) → leq#(X1, X2)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

leq#(mark(X1), X2) → leq#(X1, X2)leq#(active(X1), X2) → leq#(X1, X2)

Problem 10: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

leq#(X1, mark(X2)) → leq#(X1, X2)leq#(X1, active(X2)) → leq#(X1, X2)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, if, leq, p, false, true, active, mark

Strategy

Function Precedence

active = mark < 0 = s = leq# = diff = if = leq = p = false = true

Argument Filtering

0: all arguments are removed from 0
s: all arguments are removed from s
leq#: collapses to 2
diff: 1
if: 1 3
leq: 1
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: 1
mark: collapses to 1

Status

0: multiset
s: multiset
diff: lexicographic with permutation 1 → 1
if: lexicographic with permutation 1 → 1 3 → 2
leq: lexicographic with permutation 1 → 1
p: multiset
false: multiset
true: multiset
active: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

leq#(X1, active(X2)) → leq#(X1, X2)

Problem 14: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

leq#(X1, mark(X2)) → leq#(X1, X2)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Function Precedence

0 = s = leq# = diff = if = leq = p = false = true = active = mark

Argument Filtering

0: all arguments are removed from 0
s: all arguments are removed from s
leq#: collapses to 2
diff: all arguments are removed from diff
if: all arguments are removed from if
leq: all arguments are removed from leq
p: all arguments are removed from p
false: all arguments are removed from false
true: all arguments are removed from true
active: all arguments are removed from active
mark: 1

Status

0: multiset
s: multiset
diff: multiset
if: multiset
leq: multiset
p: multiset
false: multiset
true: multiset
active: multiset
mark: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

leq#(X1, mark(X2)) → leq#(X1, X2)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

p#(mark(X)) → p#(X)p#(active(X)) → p#(X)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

p#(mark(X)) → p#(X)p#(active(X)) → p#(X)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

s#(mark(X)) → s#(X)s#(active(X)) → s#(X)

Rewrite Rules

active(p(0)) → mark(0)active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)p(active(X)) → p(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)diff(X1, active(X2)) → diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, active, true, false, mark

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X)) → s#(X)s#(active(X)) → s#(X)