YES

Problem 1:

(VAR x z)
(STRATEGY CONTEXTSENSITIVE
 (a)
 (c)
 (d)
 (f 1)
 (k)
 (s 1)
 (t 1)
)
(RULES
 a -> c
 a -> d
 f(x) -> z | s(x) -> t(z)
 s(c) -> t(k)
)


Problem 1:

Dependency Pair Processor:
-> Rules:
 a -> c
 a -> d
 f(x) -> z | s(x) -> t(z)
 s(c) -> t(k)
-> Infeasible Rules:
 Empty.
-> Equations:
 Empty.
-> Horn Clauses:
 f(x19) |>= x18 | x19 |>= x18
 s(x21) |>= x20 | x21 |>= x20
 F(x23) |>= x22 | x23 |>= x22
 S(x25) |>= x24 | x25 |>= x24
 x16 |>= x16
 Mk(a,A)
 Mk(f(x26),F(x26))
 Mk(s(x27),S(x27))
 F(x) ->h x33 | s(x) -> t(z), z |>= x32, Mk(x32,x33)

Problem 1:

SCC Processor:
-> Rules:
 a -> c
 a -> d
 f(x) -> z | s(x) -> t(z)
 s(c) -> t(k)
-> Infeasible Rules:
 Empty.
-> Equations:
 Empty.
->Strongly Connected Components:
 There is no strongly connected component

The problem is finite.
19.34user 0.81system 0:20.41elapsed 98%CPU (0avgtext+0avgdata 9032maxresident)k
10792inputs+56outputs (48major+3043minor)pagefaults 0swaps