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

  Signature: F :: (a -> a) -> a -> a -> a
             G :: (a -> a) -> a -> a

  Rules: F(F(Z, U), U) -> F(G(F(Z, U)), Z(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.