MAYBE
Trs:
 {dfib(s(s(x)), y) -> dfib(s(x), dfib(x, y))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open