YES input TRS: [ a -> a, f(f(?x,b),?y) -> f(?y,b), f(b,?y) -> f(?y,b), f(?x,a) -> b ] Try persistent and layer-preserving decomposition... Sort Assignment: a : =>10 b : =>10 f : 10*10=>10 maximal types: {10} ...decomposition failed. TRS: [ a -> a, f(f(?x,b),?y) -> f(?y,b), f(b,?y) -> f(?y,b), f(?x,a) -> b ] unknown Non-Omega-Overlapping unknown Right-Reducible Check distinct normal forms in critical pair closure...failed Obtained TRSs: [ a -> a, f(f(?x,b),?y) -> f(?y,b), f(b,?y) -> f(?y,b), f(?x,a) -> b, f(a,b) -> b ] ...linear strongly closed TRS UNC Completion (General) problems/ex6.trs: Success(UNC) (0 msec.)