The TRS could be proven non-terminating. The proof took 436 ms.

The following reduction sequence is a witness for non-termination:

f#(__x, __x) →* f#(__x, __x)

The following DP Processors were used


Caught Exception: class java.lang.ThreadDeath
Problem 1 was processed with processor BackwardInstantiation (4ms).
null
 | – Problem 2 was processed with processor ForwardInstantiation (6ms).
 |    | – Problem 3 was processed with processor BackwardInstantiation (6ms).
 |    |    | – Problem 4 was processed with processor ForwardInstantiation (13ms).
 |    |    |    | – Problem 5 was processed with processor BackwardInstantiation (11ms).
 |    |    |    |    | – Problem 6 was processed with processor ForwardInstantiation (13ms).
 |    |    |    |    |    | – Problem 7 remains open; application of the following processors failed [Propagation (52ms)].

Problem 1: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(x, y)f#(x, x)f#(s(x), y)f#(y, x)

Rewrite Rules

f(x, y)f(x, x)f(s(x), y)f(y, x)

Original Signature

Termination of terms over the following signature is verified: f, s

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(x, y) → f#(x, x) on dependency pair chains it holds that: Thus, f#(x, y) → f#(x, x) is replaced by instances determined through the above matching. These instances are:
f#(_x, _x) → f#(_x, _x)f#(_y, _x) → f#(_y, _y)

Problem 2: ForwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(_x, _x)f#(_x, _x)f#(_y, _x)f#(_y, _y)
f#(s(x), y)f#(y, x)

Rewrite Rules

f(x, y)f(x, x)f(s(x), y)f(y, x)

Original Signature

Termination of terms over the following signature is verified: f, s

Strategy


Instantiation

For all potential successors l → r of the rule f#(s(x), y) → f#(y, x) on dependency pair chains it holds that: Thus, f#(s(x), y) → f#(y, x) is replaced by instances determined through the above matching. These instances are:
f#(s(x), s(_x)) → f#(s(_x), x)f#(s(x), y) → f#(y, x)
f#(s(x), x) → f#(x, x)

Problem 3: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(_x, _x)f#(_x, _x)f#(_y, _x)f#(_y, _y)
f#(s(x), s(_x))f#(s(_x), x)f#(s(x), y)f#(y, x)
f#(s(x), x)f#(x, x)

Rewrite Rules

f(x, y)f(x, x)f(s(x), y)f(y, x)

Original Signature

Termination of terms over the following signature is verified: f, s

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(_y, _x) → f#(_y, _y) on dependency pair chains it holds that: Thus, f#(_y, _x) → f#(_y, _y) is replaced by instances determined through the above matching. These instances are:
f#(__x, __x) → f#(__x, __x)f#(__y, __y) → f#(__y, __y)
f#(y, x) → f#(y, y)f#(x, x) → f#(x, x)
f#(s(___x), __x) → f#(s(___x), s(___x))

Problem 4: ForwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(_x, _x)f#(_x, _x)f#(__x, __x)f#(__x, __x)
f#(__y, __y)f#(__y, __y)f#(s(x), s(_x))f#(s(_x), x)
f#(y, x)f#(y, y)f#(x, x)f#(x, x)
f#(s(___x), __x)f#(s(___x), s(___x))f#(s(x), x)f#(x, x)
f#(s(x), y)f#(y, x)

Rewrite Rules

f(x, y)f(x, x)f(s(x), y)f(y, x)

Original Signature

Termination of terms over the following signature is verified: f, s

Strategy


Instantiation

For all potential successors l → r of the rule f#(s(x), y) → f#(y, x) on dependency pair chains it holds that: Thus, f#(s(x), y) → f#(y, x) is replaced by instances determined through the above matching. These instances are:
f#(s(x), s(x)) → f#(s(x), x)f#(s(x), s(___x)) → f#(s(___x), x)
f#(s(x), s(_x)) → f#(s(_x), x)f#(s(s(__x)), s(_x)) → f#(s(_x), s(__x))
f#(s(x), y) → f#(y, x)f#(s(x), x) → f#(x, x)

Problem 5: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(s(x), s(x))f#(s(x), x)f#(_x, _x)f#(_x, _x)
f#(s(x), s(___x))f#(s(___x), x)f#(__x, __x)f#(__x, __x)
f#(__y, __y)f#(__y, __y)f#(s(x), s(_x))f#(s(_x), x)
f#(y, x)f#(y, y)f#(s(___x), __x)f#(s(___x), s(___x))
f#(x, x)f#(x, x)f#(s(s(__x)), s(_x))f#(s(_x), s(__x))
f#(s(x), x)f#(x, x)f#(s(x), y)f#(y, x)

Rewrite Rules

f(x, y)f(x, x)f(s(x), y)f(y, x)

Original Signature

Termination of terms over the following signature is verified: f, s

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(y, x) → f#(y, y) on dependency pair chains it holds that: Thus, f#(y, x) → f#(y, y) is replaced by instances determined through the above matching. These instances are:
f#(s(_x), _x) → f#(s(_x), s(_x))f#(s(___x), s(___x)) → f#(s(___x), s(___x))
f#(s(__x), _x) → f#(s(__x), s(__x))f#(_x, _x) → f#(_x, _x)
f#(_y, _x) → f#(_y, _y)f#(s(_x), s(__x)) → f#(s(_x), s(_x))
f#(__x, __x) → f#(__x, __x)f#(__y, __y) → f#(__y, __y)
f#(s(____x), _x) → f#(s(____x), s(____x))f#(_y, _y) → f#(_y, _y)

Problem 6: ForwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(s(__x), _x)f#(s(__x), s(__x))f#(__x, __x)f#(__x, __x)
f#(s(s(__x)), s(_x))f#(s(_x), s(__x))f#(s(___x), __x)f#(s(___x), s(___x))
f#(_y, _y)f#(_y, _y)f#(s(x), y)f#(y, x)
f#(s(x), s(x))f#(s(x), x)f#(s(_x), _x)f#(s(_x), s(_x))
f#(s(___x), s(___x))f#(s(___x), s(___x))f#(s(x), s(___x))f#(s(___x), x)
f#(_x, _x)f#(_x, _x)f#(s(_x), s(__x))f#(s(_x), s(_x))
f#(_y, _x)f#(_y, _y)f#(__y, __y)f#(__y, __y)
f#(s(x), s(_x))f#(s(_x), x)f#(x, x)f#(x, x)
f#(s(____x), _x)f#(s(____x), s(____x))f#(s(x), x)f#(x, x)

Rewrite Rules

f(x, y)f(x, x)f(s(x), y)f(y, x)

Original Signature

Termination of terms over the following signature is verified: f, s

Strategy


Instantiation

For all potential successors l → r of the rule f#(s(x), y) → f#(y, x) on dependency pair chains it holds that: Thus, f#(s(x), y) → f#(y, x) is replaced by instances determined through the above matching. These instances are:
f#(s(x), s(x)) → f#(s(x), x)f#(s(s(_x)), s(_x)) → f#(s(_x), s(_x))
f#(s(x), s(__x)) → f#(s(__x), x)f#(s(s(___x)), s(___x)) → f#(s(___x), s(___x))
f#(s(x), s(___x)) → f#(s(___x), x)f#(s(x), s(____x)) → f#(s(____x), x)
f#(s(x), s(_x)) → f#(s(_x), x)f#(s(s(__x)), s(_x)) → f#(s(_x), s(__x))
f#(s(s(____x)), s(_x)) → f#(s(_x), s(____x))f#(s(s(_x)), s(s(__x))) → f#(s(s(__x)), s(_x))
f#(s(x), y) → f#(y, x)f#(s(x), x) → f#(x, x)