YES (format LCTRS :logic QF_LIA) (fun quad 1 :sort (Int Int)) (fun twice 1 :sort (Int Int)) (fun u 3 :sort (Int Int Int Int)) (rule (quad x_0) (+ (twice x_0) (twice x_0)) :vars ((x_0 Int))) (rule (u x_1 i_2 z_3) z_3 :guard (not (< i_2 x_1)) :vars ((x_1 Int) (i_2 Int) (z_3 Int))) (rule (u x_4 i_5 z_6) (u x_4 (+ i_5 1) (+ z_6 2)) :guard (< i_5 x_4) :vars ((x_4 Int) (i_5 Int) (z_6 Int))) (rule (twice x_7) (u x_7 0 0) :vars ((x_7 Int))) Confluent by Almost Parallel Closedness with proof: no critical pairs Elapsed Time: 15.42 ms