YES
(ignored inputs)COMMENT Example 6
input TRS:
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)),
     @(@(@(S,?x),?y),?z) -> @(@(?x,?z),@(?y,?z)),
     @(@(K,?x),?y) -> ?x,
     @(I,?x) -> ?x,
     @(@(D,?x),?x) -> ?x ]
Try persistent and layer-preserving decomposition...
Sort Assignment:
 @ : 21*21=>21
 D : =>21
 I : =>21
 K : =>21
 S : =>21
 f : 19*19=>19
maximal types: {19}{21}
Sort Assignment:
 @ : 15*15=>15
 D : =>15
 I : =>15
 K : =>15
 S : =>15
maximal types: {15}
Sort Assignment:
 f : 5*5=>5
maximal types: {5}
...result of decompositions:
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)) ]
   [ @(@(@(S,?x),?y),?z) -> @(@(?x,?z),@(?y,?z)),
     @(@(K,?x),?y) -> ?x,
     @(I,?x) -> ?x,
     @(@(D,?x),?x) -> ?x ]
TRS:
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)) ]
unknown Non-Omega-Overlapping
Right-Reducible
TRS:
   [ @(@(@(S,?x),?y),?z) -> @(@(?x,?z),@(?y,?z)),
     @(@(K,?x),?y) -> ?x,
     @(I,?x) -> ?x,
     @(@(D,?x),?x) -> ?x ]
Non-Omega-Overlapping
problems/ex7.trs: Success(UNC)
(4 msec.)