MAYBE
(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 ]
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 ]
New rules by rule reversing:
   [ f(f(?x,?y),?z) -> f(f(?x,?y),?z),
     f(f(?x,?z),f(?y,?z)) -> f(f(?x,?y),?z),
     @(@(@(S,?x),?y),?z) -> @(@(?x,?z),@(?y,?z)),
     @(@(K,?x),?y) -> ?x,
     @(I,?x) -> ?x,
     @(@(D,?x),?x) -> ?x ]
unknown UNC Completion (Development Closed)
problems/ex7.trs: Failure(unknown UNC)
(0 msec.)