YES (format LCTRS :logic QF_LIA) (fun f 1 :sort (Int Unit)) (rule (f x_0) (f (- 0 x_0)) :guard (> x_0 0) :vars ((x_0 Int))) Confluent by Weak Orthogonality with proof: no critical pairs Elapsed Time: 12.45 ms