; @author Jonas Schöpf
; @author Aart Middeldorp
; secret problem 2025
; category: LCTRS
(format LCTRS :smtlib 2.6)

(theory Ints)

(fun f (-> Int Int Int))
(fun d (-> Int Int Int))

(rule (f x y) (+ x y) :guard (> x 0))
(rule (f x y) (f y x) :guard (<= x 0))
(rule (f x y) (d x y) :guard (and (> y 0) (= x (* 2 y))) :var ((x Int)))
(rule (d x y) (+ y x))