YES

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

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (3ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark^#(c)	→	a__c^#		mark^#(f(X))	→	a__f^#(X)
a__c^#	→	a__f^#(g(c))

Rewrite Rules

a__c	→	a__f(g(c))		a__f(g(X))	→	g(X)
mark(c)	→	a__c		mark(f(X))	→	a__f(X)
mark(g(X))	→	g(X)		a__c	→	c
a__f(X)	→	f(X)

Original Signature

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

Strategy

There are no SCCs!