YES (format LCTRS :logic QF_LIA) (fun g 2 :sort (Int Int Int)) (rule (g x_0 y_1) 0 :guard (or (< x_0 0) (< y_1 0)) :vars ((x_0 Int) (y_1 Int))) (rule (g x_2 y_3) 0 :guard (or (or (>= (- x_2 1) (- y_3 1)) (< (- x_2 1) 0)) (< (- y_3 1) 0)) :vars ((x_2 Int) (y_3 Int))) (rule (g x_4 y_5) 0 :guard (or (< x_4 0) (< y_5 0)) :vars ((x_4 Int) (y_5 Int))) (rule (g 0 y_6) 0 :guard (>= y_6 0) :vars ((y_6 Int))) (rule (g x_7 y_8) (g (- x_7 1) (- y_8 1)) :guard (and (and (< (- x_7 1) (- y_8 1)) (>= (- x_7 1) 0)) (>= (- y_8 1) 0)) :vars ((x_7 Int) (y_8 Int))) Confluent by Parallel Closedness with proof: * CriticalPair Left rule: (g x_2_L y_3_L) -> 0 [(or (or (>= (- x_2_L 1) (- y_3_L 1)) (< (- x_2_L 1) 0)) (< (- y_3_L 1) 0))] Right rule: (g x_0_R y_1_R) -> 0 [(or (< x_0_R 0) (< y_1_R 0))] Critical pair: 0 ≈ 0 [(and (or (or (>= (- x_0_R 1) (- y_1_R 1)) (< (- x_0_R 1) 0)) (< (- y_1_R 1) 0)) (or (< x_0_R 0) (< y_1_R 0)))] which reaches the trivial constrained equation (≈ 0 0) [(and (or (or (>= (- x_0_R 1) (- y_1_R 1)) (< (- x_0_R 1) 0)) (< (- y_1_R 1) 0)) (or (< x_0_R 0) (< y_1_R 0)))] * CriticalPair Left rule: (g x_0_L y_1_L) -> 0 [(or (< x_0_L 0) (< y_1_L 0))] Right rule: (g x_2_R y_3_R) -> 0 [(or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0))] Critical pair: 0 ≈ 0 [(and (or (< x_2_R 0) (< y_3_R 0)) (or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0)))] which reaches the trivial constrained equation (≈ 0 0) [(and (or (< x_2_R 0) (< y_3_R 0)) (or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0)))] * CriticalPair Left rule: (g x_4_L y_5_L) -> 0 [(or (< x_4_L 0) (< y_5_L 0))] Right rule: (g x_2_R y_3_R) -> 0 [(or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0))] Critical pair: 0 ≈ 0 [(and (or (< x_2_R 0) (< y_3_R 0)) (or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0)))] which reaches the trivial constrained equation (≈ 0 0) [(and (or (< x_2_R 0) (< y_3_R 0)) (or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0)))] * CriticalPair Left rule: (g ?fresh_9_L y_6_L) -> 0 [(and (>= y_6_L 0) (= ?fresh_9_L 0))] Right rule: (g x_2_R y_3_R) -> 0 [(or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0))] Critical pair: 0 ≈ 0 [(and (>= y_3_R 0) (= x_2_R 0) (or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0)))] which reaches the trivial constrained equation (≈ 0 0) [(and (>= y_3_R 0) (= x_2_R 0) (or (or (>= (- x_2_R 1) (- y_3_R 1)) (< (- x_2_R 1) 0)) (< (- y_3_R 1) 0)))] * CriticalPair Left rule: (g x_2_L y_3_L) -> 0 [(or (or (>= (- x_2_L 1) (- y_3_L 1)) (< (- x_2_L 1) 0)) (< (- y_3_L 1) 0))] Right rule: (g x_4_R y_5_R) -> 0 [(or (< x_4_R 0) (< y_5_R 0))] Critical pair: 0 ≈ 0 [(and (or (or (>= (- x_4_R 1) (- y_5_R 1)) (< (- x_4_R 1) 0)) (< (- y_5_R 1) 0)) (or (< x_4_R 0) (< y_5_R 0)))] which reaches the trivial constrained equation (≈ 0 0) [(and (or (or (>= (- x_4_R 1) (- y_5_R 1)) (< (- x_4_R 1) 0)) (< (- y_5_R 1) 0)) (or (< x_4_R 0) (< y_5_R 0)))] * CriticalPair Left rule: (g x_2_L y_3_L) -> 0 [(or (or (>= (- x_2_L 1) (- y_3_L 1)) (< (- x_2_L 1) 0)) (< (- y_3_L 1) 0))] Right rule: (g ?fresh_9_R y_6_R) -> 0 [(and (>= y_6_R 0) (= ?fresh_9_R 0))] Critical pair: 0 ≈ 0 [(and (or (or (>= (- ?fresh_9_R 1) (- y_6_R 1)) (< (- ?fresh_9_R 1) 0)) (< (- y_6_R 1) 0)) (>= y_6_R 0) (= ?fresh_9_R 0))] which reaches the trivial constrained equation (≈ 0 0) [(and (or (or (>= (- ?fresh_9 1) (- y_6_R 1)) (< (- ?fresh_9 1) 0)) (< (- y_6_R 1) 0)) (>= y_6_R 0) (= ?fresh_9 0))] Elapsed Time: 30.47 ms