YES (format LCTRS :logic QF_LIA) (fun f2 1 :sort (Int Int)) (fun u_10 1 :sort (Int Int)) (fun u_15 1 :sort (Int Int)) (rule (u_15 x_0) x_0 :guard (>= x_0 0) :vars ((x_0 Int))) (rule (u_15 x_1) 0 :guard (< x_1 0) :vars ((x_1 Int))) (rule (f2 x_2) (u_15 x_2) :guard (<= x_2 1) :vars ((x_2 Int))) (rule (u_10 w_2_3) (u_15 (+ w_2_3 2)) :vars ((w_2_3 Int))) (rule (f2 x_4) (u_10 (f2 (- x_4 2))) :guard (> x_4 1) :vars ((x_4 Int))) Confluent by Weak Orthogonality with proof: no critical pairs Elapsed Time: 30.31 ms