YES (format LCTRS :logic QF_LIA) (fun a 0 :sort (Unit)) (fun b 0 :sort (Unit)) (fun c 0 :sort (Unit)) (fun d 0 :sort (Unit)) (fun f 2 :sort (Int Unit Unit)) (rule d d) (rule (f x_0 b) c :guard (<= x_0 10) :vars ((x_0 Int))) (rule a b) (rule (f x_1 a) c :guard (<= x_1 3) :vars ((x_1 Int))) Confluent by Almost Parallel Closedness with proof: * CriticalPair Left rule: a -> b Right rule: (f x_1_R a) -> c [(and (<= x_1_R 3) (<= x_1_R 3))] Critical pair: (f x_1_R b) ≈ c [(and (<= x_1_R 3) (<= x_1_R 3))] which reaches the trivial constrained equation (≈ (f x_1_R b) c) [(and (<= x_1_R 3) (<= x_1_R 3))] -||-> (≈ c c) [(and (<= x_1_R 3) (<= x_1_R 3))] Elapsed Time: 17.72 ms