We consider termination of the STRS with no additional rule schemes:

  Signature: f :: (d -> d) -> b -> c
             g :: b -> a -> d -> d
             h :: (a -> b -> c) -> b
             i :: c -> c

  Rules: f(g(h(F), Y), U) -> i(F(Y, U))

The system does not satisfy the preconditions to apply static dependency pairs: it is not accessible function passing.

No HORPO proof could be found.