YES (format LCTRS :logic QF_LIA) (fun a 0 :sort (Int)) (fun b 0 :sort (Int)) (fun f 2 :sort (Int Int Int)) (fun g 2 :sort (Int Int Int)) (fun h 1 :sort (Int Int)) (rule (f x_0 y_1) (g a (+ y_1 y_1)) :guard (and (>= y_1 x_0) (= y_1 1)) :vars ((x_0 Int) (y_1 Int))) (rule (h (f x_2 y_3)) (h (g b 2)) :guard (>= x_2 y_3) :vars ((x_2 Int) (y_3 Int))) (rule a b) (rule (g x_4 y_5) (g y_5 x_4) :vars ((x_4 Int) (y_5 Int))) Confluent by Parallel Closedness with proof: * CriticalPair Left rule: (f x_0_L y_1_L) -> (g a (+ y_1_L y_1_L)) [(and (>= y_1_L x_0_L) (= y_1_L 1))] Right rule: (h (f x_2_R y_3_R)) -> (h (g b 2)) [(and (>= x_2_R y_3_R) (>= x_2_R y_3_R))] Critical pair: (h (g a (+ y_3_R y_3_R))) ≈ (h (g b 2)) [(and (and (>= y_3_R x_2_R) (= y_3_R 1)) (>= x_2_R y_3_R) (>= x_2_R y_3_R))] which reaches the trivial constrained equation (≈ (h (g a (+ y_3_R y_3_R))) (h (g b 2))) [(and (and (>= y_3_R x_2_R) (= y_3_R 1)) (>= x_2_R y_3_R) (>= x_2_R y_3_R))] -||-> (≈ (h (g b ?fresh_396)) (h (g b 2))) [(and (and (>= y_3_R x_2_R) (= y_3_R 1)) (>= x_2_R y_3_R) (>= x_2_R y_3_R) (and (>= y_3_R x_2_R) (= y_3_R 1)) (>= x_2_R y_3_R) (>= x_2_R y_3_R) (= ?fresh_396 (+ y_3_R y_3_R)))] Elapsed Time: 15.70 ms