YES (format LCTRS :logic QF_LIA) (fun max 2 :sort (Int Int Int)) (rule (max x_0 y_1) x_0 :guard (>= x_0 y_1) :vars ((x_0 Int) (y_1 Int))) (rule (max x_2 y_3) y_3 :guard (>= y_3 x_2) :vars ((x_2 Int) (y_3 Int))) (rule (max x_4 y_5) (max y_5 x_4) :vars ((x_4 Int) (y_5 Int))) Confluent by Almost Parallel Closedness with proof: * CriticalPair Left rule: (max x_2_L y_3_L) -> y_3_L [(>= y_3_L x_2_L)] Right rule: (max x_0_R y_1_R) -> x_0_R [(>= x_0_R y_1_R)] Critical pair: y_1_R ≈ x_0_R [(and (>= y_1_R x_0_R) (>= x_0_R y_1_R))] which reaches the trivial constrained equation (≈ y_1_R x_0_R) [(and (>= y_1_R x_0_R) (>= x_0_R y_1_R))] * CriticalPair Left rule: (max x_4_L y_5_L) -> (max y_5_L x_4_L) Right rule: (max x_0_R y_1_R) -> x_0_R [(>= x_0_R y_1_R)] Critical pair: (max y_1_R x_0_R) ≈ x_0_R [(>= x_0_R y_1_R)] which reaches the trivial constrained equation (≈ (max y_1_R x_0_R) x_0_R) [(>= x_0_R y_1_R)] -||-> (≈ x_0_R x_0_R) [(>= x_0_R y_1_R)] * CriticalPair Left rule: (max x_0_L y_1_L) -> x_0_L [(>= x_0_L y_1_L)] Right rule: (max x_2_R y_3_R) -> y_3_R [(>= y_3_R x_2_R)] Critical pair: x_2_R ≈ y_3_R [(and (>= x_2_R y_3_R) (>= y_3_R x_2_R))] which reaches the trivial constrained equation (≈ x_2_R y_3_R) [(and (>= x_2_R y_3_R) (>= y_3_R x_2_R))] * CriticalPair Left rule: (max x_4_L y_5_L) -> (max y_5_L x_4_L) Right rule: (max x_2_R y_3_R) -> y_3_R [(>= y_3_R x_2_R)] Critical pair: (max y_3_R x_2_R) ≈ y_3_R [(>= y_3_R x_2_R)] which reaches the trivial constrained equation (≈ (max y_3_R x_2_R) y_3_R) [(>= y_3_R x_2_R)] -||-> (≈ y_3_R y_3_R) [(>= y_3_R x_2_R)] * CriticalPair Left rule: (max x_0_L y_1_L) -> x_0_L [(>= x_0_L y_1_L)] Right rule: (max x_4_R y_5_R) -> (max y_5_R x_4_R) Critical pair: x_4_R ≈ (max y_5_R x_4_R) [(>= x_4_R y_5_R)] which reaches the trivial constrained equation (≈ x_4_R (max y_5_R x_4_R)) [(>= x_4_R y_5_R)] -||-> (≈ x_4_R x_4_R) [(>= x_4_R y_5_R)] * CriticalPair Left rule: (max x_2_L y_3_L) -> y_3_L [(>= y_3_L x_2_L)] Right rule: (max x_4_R y_5_R) -> (max y_5_R x_4_R) Critical pair: y_5_R ≈ (max y_5_R x_4_R) [(>= y_5_R x_4_R)] which reaches the trivial constrained equation (≈ y_5_R (max y_5_R x_4_R)) [(>= y_5_R x_4_R)] -||-> (≈ y_5_R y_5_R) [(>= y_5_R x_4_R)] Elapsed Time: 74.33 ms