NO

Problem 1:

(VAR vu95NonEmpty x)
(RULES
a -> b
b -> a
f(x,x) -> a
g(x) -> a | g(x) ->* b
)

Problem 1:
Valid CTRS Processor:
-> Rules:
 a -> b
 b -> a
 f(x,x) -> a
 g(x) -> a | g(x) ->* b
-> The system is a 2-CTRS.

Problem 1:
-> Pairs:
 A -> B
 B -> A
 F(x,x) -> A
 G(x) -> A | g(x) ->* b
-> QPairs:
 Empty
-> Rules:
 a -> b
 b -> a
 f(x,x) -> a
 g(x) -> a | g(x) ->* b

Problem 1:

SCC Processor:
-> Pairs:
 A -> B
 B -> A
 F(x,x) -> A
 G(x) -> A | g(x) ->* b
-> QPairs:
 Empty
-> Rules:
 a -> b
 b -> a
 f(x,x) -> a
 g(x) -> a | g(x) ->* b
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 A -> B
 B -> A
-> QPairs:
 Empty
->->-> Rules:
 a -> b
 b -> a
 f(x,x) -> a
 g(x) -> a | g(x) ->* b

Problem 1:

Infiniteness Processor:
-> Pairs:
 A -> B
 B -> A
-> QPairs:
 Empty
-> Rules:
 a -> b
 b -> a
 f(x,x) -> a
 g(x) -> a | g(x) ->* b
-> Pairs in cycle:
 A -> B
 B -> A

The problem is infinite.
30.06user 0.22system 0:31.05elapsed 97%CPU (0avgtext+0avgdata 59152maxresident)k
51936inputs+216outputs (229major+19875minor)pagefaults 0swaps