YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (102ms).
 | – Problem 2 was processed with processor ReductionPairSAT (5717ms).
 |    | – Problem 3 was processed with processor DependencyGraph (5ms).
 |    |    | – Problem 4 was processed with processor ReductionPairSAT (70ms).
 |    |    |    | – Problem 6 was processed with processor ReductionPairSAT (56ms).
 |    |    | – Problem 5 was processed with processor ReductionPairSAT (3142ms).
 |    |    |    | – Problem 7 was processed with processor ReductionPairSAT (3562ms).
 |    |    |    |    | – Problem 8 was processed with processor ReductionPairSAT (11ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)*#(*(i(x), k(y, z)), x) → *#(i(x), z)
*#(*(i(x), k(y, z)), x) → k#(*(*(i(x), y), x), *(*(i(x), z), x))*#(x, *(y, z)) → *#(x, y)
*#(*(i(x), k(y, z)), x) → i#(x)i#(*(x, y)) → i#(x)
i#(*(x, y)) → *#(i(y), i(x))i#(*(x, y)) → i#(y)
*#(x, *(y, z)) → *#(*(x, y), z)*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)
*#(*(i(x), k(y, z)), x) → *#(i(x), y)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

The following SCCs where found

*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)*#(*(i(x), k(y, z)), x) → *#(i(x), z)
*#(x, *(y, z)) → *#(x, y)*#(*(i(x), k(y, z)), x) → i#(x)
i#(*(x, y)) → i#(x)i#(*(x, y)) → *#(i(y), i(x))
i#(*(x, y)) → i#(y)*#(x, *(y, z)) → *#(*(x, y), z)
*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)*#(*(i(x), k(y, z)), x) → *#(i(x), y)

Problem 2: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)*#(*(i(x), k(y, z)), x) → *#(i(x), z)
*#(x, *(y, z)) → *#(x, y)*#(*(i(x), k(y, z)), x) → i#(x)
i#(*(x, y)) → i#(x)i#(*(x, y)) → *#(i(y), i(x))
i#(*(x, y)) → i#(y)*#(x, *(y, z)) → *#(*(x, y), z)
*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)*#(*(i(x), k(y, z)), x) → *#(i(x), y)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

Function Precedence

i# = i < *# = * < 1 = k

Argument Filtering

*#: 1 2
1: all arguments are removed from 1
*: 1 2
k: 1 2
i#: 1
i: 1

Status

*#: lexicographic with permutation 1 → 2 2 → 1
1: multiset
*: lexicographic with permutation 1 → 2 2 → 1
k: multiset
i#: lexicographic with permutation 1 → 1
i: lexicographic with permutation 1 → 1

Usable Rules

*(i(x), x) → 1*(x, i(x)) → 1
*(*(x, y), i(y)) → x*(k(x, y), k(y, x)) → 1
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
*(*(x, i(y)), y) → x*(1, y) → y
k(x, 1) → 1i(1) → 1
*(x, 1) → x*(x, *(y, z)) → *(*(x, y), z)
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))k(*(x, i(y)), *(y, i(x))) → 1
k(x, x) → 1

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.

*#(*(i(x), k(y, z)), x) → i#(x)i#(*(x, y)) → *#(i(y), i(x))

Problem 3: DependencyGraph

Dependency Pair Problem

Dependency Pairs

*#(*(i(x), k(y, z)), x) → *#(i(x), z)*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)
*#(x, *(y, z)) → *#(x, y)i#(*(x, y)) → i#(x)
i#(*(x, y)) → i#(y)*#(x, *(y, z)) → *#(*(x, y), z)
*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)*#(*(i(x), k(y, z)), x) → *#(i(x), y)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

The following SCCs where found

i#(*(x, y)) → i#(x)i#(*(x, y)) → i#(y)
*#(*(i(x), k(y, z)), x) → *#(i(x), z)*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)
*#(x, *(y, z)) → *#(x, y)*#(x, *(y, z)) → *#(*(x, y), z)
*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)*#(*(i(x), k(y, z)), x) → *#(i(x), y)

Problem 4: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

i#(*(x, y)) → i#(x)i#(*(x, y)) → i#(y)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

Function Precedence

* < 1 = k = i# = i

Argument Filtering

1: all arguments are removed from 1
*: 1 2
k: all arguments are removed from k
i#: collapses to 1
i: 1

Status

1: multiset
*: multiset
k: multiset
i: 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.

i#(*(x, y)) → i#(y)

Problem 6: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

i#(*(x, y)) → i#(x)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

Function Precedence

1 = * = k = i# = i

Argument Filtering

1: all arguments are removed from 1
*: 1 2
k: collapses to 1
i#: 1
i: all arguments are removed from i

Status

1: multiset
*: multiset
i#: lexicographic with permutation 1 → 1
i: 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.

i#(*(x, y)) → i#(x)

Problem 5: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

*#(*(i(x), k(y, z)), x) → *#(i(x), z)*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)
*#(x, *(y, z)) → *#(x, y)*#(x, *(y, z)) → *#(*(x, y), z)
*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)*#(*(i(x), k(y, z)), x) → *#(i(x), y)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

Function Precedence

i < *# = * < k < 1

Argument Filtering

*#: 1 2
1: all arguments are removed from 1
*: 1 2
k: 1 2
i: 1

Status

*#: lexicographic with permutation 1 → 2 2 → 1
1: multiset
*: lexicographic with permutation 1 → 2 2 → 1
k: multiset
i: multiset

Usable Rules

*(i(x), x) → 1*(x, i(x)) → 1
*(*(x, y), i(y)) → x*(k(x, y), k(y, x)) → 1
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
*(*(x, i(y)), y) → x*(1, y) → y
k(x, 1) → 1i(1) → 1
*(x, 1) → x*(x, *(y, z)) → *(*(x, y), z)
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))k(*(x, i(y)), *(y, i(x))) → 1
k(x, x) → 1

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.

*#(*(i(x), k(y, z)), x) → *#(i(x), z)*#(x, *(y, z)) → *#(*(x, y), z)
*#(*(i(x), k(y, z)), x) → *#(i(x), y)

Problem 7: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)*#(x, *(y, z)) → *#(x, y)
*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

Function Precedence

*# < i < * < k < 1

Argument Filtering

*#: collapses to 1
1: all arguments are removed from 1
*: 1 2
k: 1 2
i: 1

Status

1: multiset
*: lexicographic with permutation 1 → 2 2 → 1
k: lexicographic with permutation 1 → 1 2 → 2
i: lexicographic with permutation 1 → 1

Usable Rules

*(i(x), x) → 1*(x, i(x)) → 1
*(*(x, y), i(y)) → x*(k(x, y), k(y, x)) → 1
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
*(*(x, i(y)), y) → x*(1, y) → y
k(x, 1) → 1i(1) → 1
*(x, 1) → x*(x, *(y, z)) → *(*(x, y), z)
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))k(*(x, i(y)), *(y, i(x))) → 1
k(x, x) → 1

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.

*#(*(i(x), k(y, z)), x) → *#(*(i(x), z), x)*#(*(i(x), k(y, z)), x) → *#(*(i(x), y), x)

Problem 8: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

*#(x, *(y, z)) → *#(x, y)

Rewrite Rules

*(x, 1) → x*(1, y) → y
*(i(x), x) → 1*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)i(1) → 1
*(*(x, y), i(y)) → x*(*(x, i(y)), y) → x
i(i(x)) → xi(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1k(x, x) → 1
*(k(x, y), k(y, x)) → 1*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1

Original Signature

Termination of terms over the following signature is verified: 1, *, k, i

Strategy

Function Precedence

*# = 1 = * = k = i

Argument Filtering

*#: collapses to 2
1: all arguments are removed from 1
*: 1 2
k: 1 2
i: 1

Status

1: multiset
*: multiset
k: lexicographic with permutation 1 → 2 2 → 1
i: 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.

*#(x, *(y, z)) → *#(x, y)