NO

Problem 1:

(VAR vu95NonEmpty x y)
(RULES
a -> d
b -> d
e -> e
f(x,y) -> g(x) | a ->* d
f(x,y) -> h(x) | b ->* d
g(s(x)) -> x
h(s(x)) -> x
)

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

Problem 1:
-> Pairs:
 E -> E
 F(x,y) -> G(x) | a ->* d
 F(x,y) -> H(x) | b ->* d
-> QPairs:
 Empty
-> Rules:
 a -> d
 b -> d
 e -> e
 f(x,y) -> g(x) | a ->* d
 f(x,y) -> h(x) | b ->* d
 g(s(x)) -> x
 h(s(x)) -> x

Problem 1:

SCC Processor:
-> Pairs:
 E -> E
 F(x,y) -> G(x) | a ->* d
 F(x,y) -> H(x) | b ->* d
-> QPairs:
 Empty
-> Rules:
 a -> d
 b -> d
 e -> e
 f(x,y) -> g(x) | a ->* d
 f(x,y) -> h(x) | b ->* d
 g(s(x)) -> x
 h(s(x)) -> x
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 E -> E
-> QPairs:
 Empty
->->-> Rules:
 a -> d
 b -> d
 e -> e
 f(x,y) -> g(x) | a ->* d
 f(x,y) -> h(x) | b ->* d
 g(s(x)) -> x
 h(s(x)) -> x

Problem 1:

Infiniteness Processor:
-> Pairs:
 E -> E
-> QPairs:
 Empty
-> Rules:
 a -> d
 b -> d
 e -> e
 f(x,y) -> g(x) | a ->* d
 f(x,y) -> h(x) | b ->* d
 g(s(x)) -> x
 h(s(x)) -> x
-> Pairs in cycle:
 E -> E

The problem is infinite.
29.82user 0.39system 0:30.93elapsed 97%CPU (0avgtext+0avgdata 89500maxresident)k
26320inputs+120outputs (117major+23754minor)pagefaults 0swaps