MAYBE
(ignored inputs)COMMENT first 5 rules from Huet
input TRS:
   [ H(F(?x,?y)) -> F(H(R(?x)),?y),
     F(?x,K(?y,?z)) -> G(P(?y),Q(?z,?x)),
     H(Q(?x,?y)) -> Q(?x,H(R(?y))),
     Q(?x,H(R(?y))) -> H(Q(?x,?y)),
     H(G(?x,?y)) -> G(?x,H(?y)),
     K(?x,?x) -> R(?x),
     P(?y) -> C,
     C -> K(C,C),
     F(?x,R(?y)) -> G(C,Q(?y,?x)) ]
TRS:
   [ H(F(?x,?y)) -> F(H(R(?x)),?y),
     F(?x,K(?y,?z)) -> G(P(?y),Q(?z,?x)),
     H(Q(?x,?y)) -> Q(?x,H(R(?y))),
     Q(?x,H(R(?y))) -> H(Q(?x,?y)),
     H(G(?x,?y)) -> G(?x,H(?y)),
     K(?x,?x) -> R(?x),
     P(?y) -> C,
     C -> K(C,C),
     F(?x,R(?y)) -> G(C,Q(?y,?x)) ]
New rules by rule reversing:
   [ H(F(?x,?y)) -> F(H(R(?x)),?y),
     F(?x,K(?y,?z)) -> F(?x,K(?y,?z)),
     G(P(?y),Q(?z,?x)) -> F(?x,K(?y,?z)),
     H(Q(?x,?y)) -> H(Q(?x,?y)),
     Q(?x,H(R(?y))) -> H(Q(?x,?y)),
     Q(?x,H(R(?y))) -> H(Q(?x,?y)),
     H(G(?x,?y)) -> G(?x,H(?y)),
     K(?x,?x) -> R(?x),
     P(?y) -> C,
     C -> C,
     K(C,C) -> C,
     F(?x,R(?y)) -> F(?x,R(?y)),
     G(C,Q(?y,?x)) -> F(?x,R(?y)) ]
unknown Weight-Decreasing Joinable
problems/ex3.trs: Failure(unknown UNC)
(196 msec.)