YES

Problem 1:

(VAR x y z)
(STRATEGY CONTEXTSENSITIVE
 (a)
 (b)
 (c)
 (d)
 (f 1)
 (g 1 2 3)
 (h 1 2)
 (i 1)
)
(RULES
 f(x) -> g(x,y,z) | h(a,x) -> i(y), h(a,y) -> i(z)
 h(a,a) -> i(b)
 h(a,b) -> i(c)
 h(b,b) -> i(d)
)


Problem 1:

Dependency Pair Processor:
-> Rules:
 f(x) -> g(x,y,z) | h(a,x) -> i(y), h(a,y) -> i(z)
 h(a,a) -> i(b)
 h(a,b) -> i(c)
 h(b,b) -> i(d)
-> Infeasible Rules:
 Empty.
-> Equations:
 Empty.
-> Horn Clauses:
 f(x20) |>= x19 | x20 |>= x19
 h(x22,x23) |>= x21 | x22 |>= x21
 h(x25,x26) |>= x24 | x26 |>= x24
 F(x28) |>= x27 | x28 |>= x27
 H(x30,x31) |>= x29 | x30 |>= x29
 H(x33,x34) |>= x32 | x34 |>= x32
 x17 |>= x17
 Mk(f(x35),F(x35))
 Mk(h(x36,x37),H(x36,x37))
 F(x) ->h x39 | h(a,x) -> i(y), h(a,y) -> i(z), y |>= x38, Mk(x38,x39)
 F(x) ->h x39 | h(a,x) -> i(y), h(a,y) -> i(z), z |>= x38, Mk(x38,x39)

Problem 1:

SCC Processor:
-> Rules:
 f(x) -> g(x,y,z) | h(a,x) -> i(y), h(a,y) -> i(z)
 h(a,a) -> i(b)
 h(a,b) -> i(c)
 h(b,b) -> i(d)
-> Infeasible Rules:
 Empty.
-> Equations:
 Empty.
->Strongly Connected Components:
 There is no strongly connected component

The problem is finite.
19.82user 0.47system 0:20.86elapsed 97%CPU (0avgtext+0avgdata 9732maxresident)k
13064inputs+160outputs (63major+5559minor)pagefaults 0swaps