MAYBE
Trs:
 {            p(s(x)) -> x,
         plus(0(), y) -> y,
        plus(s(x), y) -> s(plus(p(s(x)), y)),
        plus(s(x), y) -> s(plus(x, y)),
         plus(x, 0()) -> x,
        plus(x, s(y)) -> s(plus(x, p(s(y)))),
   quot(0(), s(y), z) -> 0(),
  quot(s(x), s(y), z) -> quot(x, y, z),
   quot(x, 0(), s(z)) -> s(div(x, s(z))),
    div(div(x, y), z) -> div(x, times(y, z)),
          div(0(), y) -> 0(),
            div(x, y) -> quot(x, y, y),
        times(0(), y) -> 0(),
     times(s(0()), y) -> y,
       times(s(x), y) -> plus(y, times(x, y)),
         eq(0(), 0()) -> true(),
        eq(0(), s(y)) -> false(),
        eq(s(x), 0()) -> false(),
       eq(s(x), s(y)) -> eq(x, y),
       prime(s(s(x))) -> pr(s(s(x)), s(x)),
        divides(y, x) -> eq(x, times(div(x, y), y)),
     if(true(), x, y) -> false(),
    if(false(), x, y) -> pr(x, y),
        pr(x, s(0())) -> true(),
       pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open