(VAR x y)
(HORN-CLAUSES
  x === y | x ->* y
)
(RULES
  pin(x) -> pout(g(x))
  pin(x) -> pout(f(y)) | pin(x) === pout(g(y))
)
(COMMENT
  Example 49, Lucas FSCD'24
  https://doi.org/10.4230/LIPIcs.FSCD.2024.32
)