MAYBE (format LCTRS :logic QF_LIA) (fun a 0 :sort (Int)) (fun f 1 :sort (Int Int)) (fun g 1 :sort (Int Int)) (rule (f x_0) z_1 :guard (= z_1 3) :vars ((x_0 Int) (z_1 Int))) (rule (g (f x_2)) a :vars ((x_2 Int))) (rule (g z_3) a :guard (= z_3 3) :vars ((z_3 Int))) Confluence could not be determined. Elapsed Time: 8.84 ms