YES (format LCTRS) (fun * 2 :sort (Unit Unit Unit)) (fun + 2 :sort (Unit Unit Unit)) (rule (+ x_0 y_1) (+ y_1 x_0) :vars ((x_0 Unit) (y_1 Unit))) (rule (* (+ x_2 y_3) z_4) (+ (* x_2 z_4) (* y_3 z_4)) :vars ((x_2 Unit) (y_3 Unit) (z_4 Unit))) (rule (* (+ y_5 x_6) z_7) (+ (* x_6 z_7) (* y_5 z_7)) :vars ((y_5 Unit) (x_6 Unit) (z_7 Unit))) Confluent by Almost Parallel Closedness with proof: * CriticalPair Left rule: (+ x_0_L y_1_L) -> (+ y_1_L x_0_L) Right rule: (* (+ x_2_R y_3_R) z_4_R) -> (+ (* x_2_R z_4_R) (* y_3_R z_4_R)) Critical pair: (* (+ y_3_R x_2_R) z_4_R) ≈ (+ (* x_2_R z_4_R) (* y_3_R z_4_R)) which reaches the trivial constrained equation (≈ (* (+ y_3_R x_2_R) z_4_R) (+ (* x_2_R z_4_R) (* y_3_R z_4_R))) [] -||-> (≈ (+ (* x_2_R z_4_R) (* y_3_R z_4_R)) (+ (* x_2_R z_4_R) (* y_3_R z_4_R))) [] * CriticalPair Left rule: (* (+ y_5_L x_6_L) z_7_L) -> (+ (* x_6_L z_7_L) (* y_5_L z_7_L)) Right rule: (* (+ x_2_R y_3_R) z_4_R) -> (+ (* x_2_R z_4_R) (* y_3_R z_4_R)) Critical pair: (+ (* y_3_R z_4_R) (* x_2_R z_4_R)) ≈ (+ (* x_2_R z_4_R) (* y_3_R z_4_R)) which reaches the trivial constrained equation (≈ (+ (* y_3_R z_4_R) (* x_2_R z_4_R)) (+ (* x_2_R z_4_R) (* y_3_R z_4_R))) [] -||-> (≈ (+ (* y_3_R z_4_R) (* x_2_R z_4_R)) (+ (* y_3_R z_4_R) (* x_2_R z_4_R))) [] * CriticalPair Left rule: (+ x_0_L y_1_L) -> (+ y_1_L x_0_L) Right rule: (* (+ y_5_R x_6_R) z_7_R) -> (+ (* x_6_R z_7_R) (* y_5_R z_7_R)) Critical pair: (* (+ x_6_R y_5_R) z_7_R) ≈ (+ (* x_6_R z_7_R) (* y_5_R z_7_R)) which reaches the trivial constrained equation (≈ (* (+ x_6_R y_5_R) z_7_R) (+ (* x_6_R z_7_R) (* y_5_R z_7_R))) [] -||-> (≈ (+ (* x_6_R z_7_R) (* y_5_R z_7_R)) (+ (* x_6_R z_7_R) (* y_5_R z_7_R))) [] * CriticalPair Left rule: (* (+ x_2_L y_3_L) z_4_L) -> (+ (* x_2_L z_4_L) (* y_3_L z_4_L)) Right rule: (* (+ y_5_R x_6_R) z_7_R) -> (+ (* x_6_R z_7_R) (* y_5_R z_7_R)) Critical pair: (+ (* y_5_R z_7_R) (* x_6_R z_7_R)) ≈ (+ (* x_6_R z_7_R) (* y_5_R z_7_R)) which reaches the trivial constrained equation (≈ (+ (* y_5_R z_7_R) (* x_6_R z_7_R)) (+ (* x_6_R z_7_R) (* y_5_R z_7_R))) [] -||-> (≈ (+ (* y_5_R z_7_R) (* x_6_R z_7_R)) (+ (* y_5_R z_7_R) (* x_6_R z_7_R))) [] Elapsed Time: 68.96 ms