YES

(format LCTRS :logic QF_LIA)
(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) (+ (f z_2 y_1) 1) :guard (and (>= x_0 1) (= z_2 (- x_0 1))) :vars ((x_0 Int) (y_1 Int) (z_2 Int)))
(rule (g 0 y_3) y_3 :guard (<= x_4 0) :vars ((y_3 Int) (x_4 Int)))
(rule (f x_5 0) (g 1 x_5) :guard (<= x_5 1) :vars ((x_5 Int)))
(rule (g 1 1) (+ (g 1 0) 1))
(rule (h x_6) (+ (g 1 x_6) 1) :guard (<= x_6 1) :vars ((x_6 Int)))
(rule (h x_7) (+ (+ (f z_8 0) 1) 1) :guard (and (> x_7 1) (= z_8 (- x_7 1))) :vars ((x_7 Int) (z_8 Int)))

Confluent by Almost Parallel Closedness with proof:
* CriticalPair
  Left rule: (f x_0_L y_1_L) -> (+ (f z_2_L y_1_L) 1) [(and (>= x_0_L 1) (= z_2_L (- x_0_L 1)))]
  Right rule: (f x_0_R y_1_R) -> (+ (f z_2_R y_1_R) 1) [(and (>= x_0_R 1) (= z_2_R (- x_0_R 1)))]
  Critical pair: (+ (f z_2_L y_1_R) 1) ≈ (+ (f z_2_R y_1_R) 1) [(and (and (>= x_0_R 1) (= z_2_L (- x_0_R 1))) (and (>= x_0_R 1) (= z_2_R (- x_0_R 1))))]
 which reaches the trivial constrained equation
  (≈ (+ (f z_2_L y_1_R) 1) (+ (f z_2_R y_1_R) 1)) [(and (and (>= x_0_R 1) (= z_2_L (- x_0_R 1))) (and (>= x_0_R 1) (= z_2_R (- x_0_R 1))))]
* CriticalPair
  Left rule: (f x_5_L ?fresh_10_L) -> (g 1 x_5_L) [(and (<= x_5_L 1) (= ?fresh_10_L 0))]
  Right rule: (f x_0_R y_1_R) -> (+ (f z_2_R y_1_R) 1) [(and (>= x_0_R 1) (= z_2_R (- x_0_R 1)))]
  Critical pair: (g 1 x_0_R) ≈ (+ (f z_2_R y_1_R) 1) [(and (<= x_0_R 1) (= y_1_R 0) (and (>= x_0_R 1) (= z_2_R (- x_0_R 1))))]
 which reaches the trivial constrained equation
  (≈ (g 1 x_0_R) (+ (f z_2_R y_1_R) 1)) [(and (<= x_0_R 1) (= y_1_R 0) (and (>= x_0_R 1) (= z_2_R (- x_0_R 1))))]
	-||-> (≈ (+ (g 1 0) 1) (+ (f z_2_R y_1_R) 1)) [(and (<= x_0_R 1) (= y_1_R 0) (and (>= x_0_R 1) (= z_2_R (- x_0_R 1))))]
	-||-> (≈ (+ (g 1 0) 1) (+ (g 1 z_2_R) 1)) [(and (<= x_0_R 1) (= y_1_R 0) (and (>= x_0_R 1) (= z_2_R (- x_0_R 1))) (<= x_0_R 1) (= y_1_R 0) (and (>= x_0_R 1) (= z_2_R (- x_0_R 1))))]
* CriticalPair
  Left rule: (f x_0_L y_1_L) -> (+ (f z_2_L y_1_L) 1) [(and (>= x_0_L 1) (= z_2_L (- x_0_L 1)))]
  Right rule: (f x_5_R ?fresh_10_R) -> (g 1 x_5_R) [(and (<= x_5_R 1) (= ?fresh_10_R 0))]
  Critical pair: (+ (f z_2_L ?fresh_10_R) 1) ≈ (g 1 x_5_R) [(and (and (>= x_5_R 1) (= z_2_L (- x_5_R 1))) (<= x_5_R 1) (= ?fresh_10_R 0))]
 which reaches the trivial constrained equation
  (≈ (+ (f z_2_L ?fresh_10) 1) (g 1 x_5_R)) [(and (and (>= x_5_R 1) (= z_2_L (- x_5_R 1))) (<= x_5_R 1) (= ?fresh_10 0))]
	-||-> (≈ (+ (g 1 z_2_L) 1) (g 1 x_5_R)) [(and (and (>= x_5_R 1) (= z_2_L (- x_5_R 1))) (<= x_5_R 1) (= ?fresh_10 0) (and (>= x_5_R 1) (= z_2_L (- x_5_R 1))) (<= x_5_R 1) (= ?fresh_10 0))]
	-||-> (≈ (+ (g 1 z_2_L) 1) (+ (g 1 0) 1)) [(and (and (>= x_5_R 1) (= z_2_L (- x_5_R 1))) (<= x_5_R 1) (= ?fresh_10 0) (and (>= x_5_R 1) (= z_2_L (- x_5_R 1))) (<= x_5_R 1) (= ?fresh_10 0))]
* CriticalPair
  Left rule: (h x_7_L) -> (+ (+ (f z_8_L 0) 1) 1) [(and (> x_7_L 1) (= z_8_L (- x_7_L 1)))]
  Right rule: (h x_7_R) -> (+ (+ (f z_8_R 0) 1) 1) [(and (> x_7_R 1) (= z_8_R (- x_7_R 1)))]
  Critical pair: (+ (+ (f z_8_L 0) 1) 1) ≈ (+ (+ (f z_8_R 0) 1) 1) [(and (and (> x_7_R 1) (= z_8_L (- x_7_R 1))) (and (> x_7_R 1) (= z_8_R (- x_7_R 1))))]
 which reaches the trivial constrained equation
  (≈ (+ (+ (f z_8_L 0) 1) 1) (+ (+ (f z_8_R 0) 1) 1)) [(and (and (> x_7_R 1) (= z_8_L (- x_7_R 1))) (and (> x_7_R 1) (= z_8_R (- x_7_R 1))))]


Elapsed Time: 635.86 ms