MAYBE Trs: { D(t()) -> 1(), D(constant()) -> 0(), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(+(x, y)) -> +(D(x), D(y)), D(-(x, y)) -> -(D(x), D(y))} Comment: We consider a duplicating trs. FAIL: Open