YES

(format LCTRS :logic QF_LIA)
(fun f 2 :sort (Int Int Int))

(rule (f x_0 y_1) 0 :guard (or (or (>= (- x_0 1) y_1) (< (- x_0 1) 0)) (< y_1 0)) :vars ((x_0 Int) (y_1 Int)))
(rule (f x_2 y_3) 0 :guard (or (< x_2 0) (<= y_3 0)) :vars ((x_2 Int) (y_3 Int)))
(rule (f 0 y_4) 0 :guard (>= y_4 0) :vars ((y_4 Int)))
(rule (f x_5 y_6) (f (- x_5 1) y_6) :guard (and (and (< (- x_5 1) y_6) (>= (- x_5 1) 0)) (>= y_6 0)) :vars ((x_5 Int) (y_6 Int)))

Confluent by Parallel Closedness with proof:
* CriticalPair
  Left rule: (f x_2_L y_3_L) -> 0 [(or (< x_2_L 0) (<= y_3_L 0))]
  Right rule: (f x_0_R y_1_R) -> 0 [(or (or (>= (- x_0_R 1) y_1_R) (< (- x_0_R 1) 0)) (< y_1_R 0))]
  Critical pair: 0 ≈ 0 [(and (or (< x_0_R 0) (<= y_1_R 0)) (or (or (>= (- x_0_R 1) y_1_R) (< (- x_0_R 1) 0)) (< y_1_R 0)))]
 which reaches the trivial constrained equation
  (≈ 0 0) [(and (or (< x_0_R 0) (<= y_1_R 0)) (or (or (>= (- x_0_R 1) y_1_R) (< (- x_0_R 1) 0)) (< y_1_R 0)))]
* CriticalPair
  Left rule: (f ?fresh_7_L y_4_L) -> 0 [(and (>= y_4_L 0) (= ?fresh_7_L 0))]
  Right rule: (f x_0_R y_1_R) -> 0 [(or (or (>= (- x_0_R 1) y_1_R) (< (- x_0_R 1) 0)) (< y_1_R 0))]
  Critical pair: 0 ≈ 0 [(and (>= y_1_R 0) (= x_0_R 0) (or (or (>= (- x_0_R 1) y_1_R) (< (- x_0_R 1) 0)) (< y_1_R 0)))]
 which reaches the trivial constrained equation
  (≈ 0 0) [(and (>= y_1_R 0) (= x_0_R 0) (or (or (>= (- x_0_R 1) y_1_R) (< (- x_0_R 1) 0)) (< y_1_R 0)))]
* CriticalPair
  Left rule: (f x_0_L y_1_L) -> 0 [(or (or (>= (- x_0_L 1) y_1_L) (< (- x_0_L 1) 0)) (< y_1_L 0))]
  Right rule: (f x_2_R y_3_R) -> 0 [(or (< x_2_R 0) (<= y_3_R 0))]
  Critical pair: 0 ≈ 0 [(and (or (or (>= (- x_2_R 1) y_3_R) (< (- x_2_R 1) 0)) (< y_3_R 0)) (or (< x_2_R 0) (<= y_3_R 0)))]
 which reaches the trivial constrained equation
  (≈ 0 0) [(and (or (or (>= (- x_2_R 1) y_3_R) (< (- x_2_R 1) 0)) (< y_3_R 0)) (or (< x_2_R 0) (<= y_3_R 0)))]
* CriticalPair
  Left rule: (f ?fresh_7_L y_4_L) -> 0 [(and (>= y_4_L 0) (= ?fresh_7_L 0))]
  Right rule: (f x_2_R y_3_R) -> 0 [(or (< x_2_R 0) (<= y_3_R 0))]
  Critical pair: 0 ≈ 0 [(and (>= y_3_R 0) (= x_2_R 0) (or (< x_2_R 0) (<= y_3_R 0)))]
 which reaches the trivial constrained equation
  (≈ 0 0) [(and (>= y_3_R 0) (= x_2_R 0) (or (< x_2_R 0) (<= y_3_R 0)))]
* CriticalPair
  Left rule: (f x_0_L y_1_L) -> 0 [(or (or (>= (- x_0_L 1) y_1_L) (< (- x_0_L 1) 0)) (< y_1_L 0))]
  Right rule: (f ?fresh_7_R y_4_R) -> 0 [(and (>= y_4_R 0) (= ?fresh_7_R 0))]
  Critical pair: 0 ≈ 0 [(and (or (or (>= (- ?fresh_7_R 1) y_4_R) (< (- ?fresh_7_R 1) 0)) (< y_4_R 0)) (>= y_4_R 0) (= ?fresh_7_R 0))]
 which reaches the trivial constrained equation
  (≈ 0 0) [(and (or (or (>= (- ?fresh_7 1) y_4_R) (< (- ?fresh_7 1) 0)) (< y_4_R 0)) (>= y_4_R 0) (= ?fresh_7 0))]
* CriticalPair
  Left rule: (f x_2_L y_3_L) -> 0 [(or (< x_2_L 0) (<= y_3_L 0))]
  Right rule: (f ?fresh_7_R y_4_R) -> 0 [(and (>= y_4_R 0) (= ?fresh_7_R 0))]
  Critical pair: 0 ≈ 0 [(and (or (< ?fresh_7_R 0) (<= y_4_R 0)) (>= y_4_R 0) (= ?fresh_7_R 0))]
 which reaches the trivial constrained equation
  (≈ 0 0) [(and (or (< ?fresh_7 0) (<= y_4_R 0)) (>= y_4_R 0) (= ?fresh_7 0))]


Elapsed Time:  19.58 ms