(format LCTRS :logic QF_NIA)

(fun f 1 :sort (Int Int))

(rule (f x) z :guard (= x (* z z)))