(VAR q r x y)
(REPLACEMENT-MAP
  (s )
)
(HORN-CLAUSES
  x >= 0
  s(x) >= s(y) | x >= y
  peven(x) | x ->* s(s(0))
  odd(x) | x ->* s(0)
  zero(x) | x ->* 0
)
(RULES
  s(s(x)) -> x | x >= s(0)
)
(COMMENT
  Example 1, Lucas IWC'24-GTRS
  https://www.trs.css.i.nagoya-u.ac.jp/event/iwc2024/IWC2024_proceedings.pdf
)