YES
(VAR x y)
(RULES 
f(x,f(y,a)) -> f(f(f(f(a,a),y),h(a)),x)
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for jwcime2:

-> Dependency pairs:
nF_f(x,f(y,a)) -> nF_f(f(f(f(a,a),y),h(a)),x)
nF_f(x,f(y,a)) -> nF_f(f(f(a,a),y),h(a))
nF_f(x,f(y,a)) -> nF_f(f(a,a),y)
nF_f(x,f(y,a)) -> nF_f(a,a)

-> Proof of termination for jwcime2_1:
-> -> Dependency pairs in cycle:
nF_f(x,f(y,a)) -> nF_f(f(f(f(a,a),y),h(a)),x)
nF_f(x,f(y,a)) -> nF_f(f(a,a),y)

UsableRules:
f(x,f(y,a)) -> f(f(f(f(a,a),y),h(a)),x)

Polynomial Interpretation:

[f](X1,X2) = 2.X1.X2 + 2.X2
[a] = 2
[h](X) = 0
[nF_f](X1,X2) = 1/2.X1.X2 + 2.X2

TIME: 6.966e-3

-> -> Dependency pairs in cycle:
nF_f(x,f(y,a)) -> nF_f(f(f(f(a,a),y),h(a)),x)

UsableRules:
f(x,f(y,a)) -> f(f(f(f(a,a),y),h(a)),x)

Polynomial Interpretation:

[f](X1,X2) = 2.X1.X2 + 2.X2
[a] = 2
[h](X) = 0
[nF_f](X1,X2) = 2.X1.X2 + 2.X2

TIME: 0.519477


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Simple mixed
Coeffs in polynomials: All rationals
Delta: automatic



Termination was proved succesfully.