(VAR x)
(HORN-CLAUSES
  S(a)
  S(b)
  S(c)
  S(f(x)) | S(x)
)
(RULES
  a -> f(b)
  b -> d
  c -> a
  c -> f(d)
)
(COMMENT
  Figure 3 left, Lucas PROLE'26

)