YES (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 3) a) Confluent by Almost Parallel Closedness with proof: * CriticalPair Left rule: (f x_0_L) -> z_1_L [(= z_1_L 3)] Right rule: (f x_0_R) -> z_1_R [(= z_1_R 3)] Critical pair: z_1_L ≈ z_1_R [(and (= z_1_L 3) (= z_1_R 3))] which reaches the trivial constrained equation (≈ z_1_L z_1_R) [(and (= z_1_L 3) (= z_1_R 3))] * CriticalPair Left rule: (f x_0_L) -> z_1_L [(= z_1_L 3)] Right rule: (g (f x_2_R)) -> a Critical pair: (g z_1_L) ≈ a [(= z_1_L 3)] which reaches the trivial constrained equation (≈ (g z_1_L) a) [(= z_1_L 3)] -||-> (≈ a a) [(= z_1_L 3)] Elapsed Time: 17.71 ms