TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (23ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (74ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (192ms), DependencyGraph (1ms), ReductionPairSAT (279ms), DependencyGraph (3ms), SizeChangePrinciple (4ms), ForwardNarrowing (0ms), BackwardInstantiation (0ms), ForwardInstantiation (1ms), Propagation (1ms)].
 | – Problem 3 was processed with processor SubtermCriterion (0ms).

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

a__f#(b, X, c)a__f#(X, a__c, X)

Rewrite Rules

a__f(b, X, c)a__f(X, a__c, X)a__cb
mark(f(X1, X2, X3))a__f(X1, mark(X2), X3)mark(c)a__c
mark(b)ba__f(X1, X2, X3)f(X1, X2, X3)
a__cc

Original Signature

Termination of terms over the following signature is verified: f, b, c, a__c, mark, a__f


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__f#(b, X, c)a__c#a__f#(b, X, c)a__f#(X, a__c, X)
mark#(f(X1, X2, X3))a__f#(X1, mark(X2), X3)mark#(c)a__c#
mark#(f(X1, X2, X3))mark#(X2)

Rewrite Rules

a__f(b, X, c)a__f(X, a__c, X)a__cb
mark(f(X1, X2, X3))a__f(X1, mark(X2), X3)mark(c)a__c
mark(b)ba__f(X1, X2, X3)f(X1, X2, X3)
a__cc

Original Signature

Termination of terms over the following signature is verified: f, b, c, a__c, mark, a__f

Strategy


The following SCCs where found

a__f#(b, X, c) → a__f#(X, a__c, X)

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

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

a__f(b, X, c)a__f(X, a__c, X)a__cb
mark(f(X1, X2, X3))a__f(X1, mark(X2), X3)mark(c)a__c
mark(b)ba__f(X1, X2, X3)f(X1, X2, X3)
a__cc

Original Signature

Termination of terms over the following signature is verified: f, b, c, a__c, mark, a__f

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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