YES
Input TRS:
    1: f(x,x) -> unit() | x --> a()
    2: f(x,unit()) -> x
    3: f(f(x,y),z) -> f(x,f(y,z))
Infeasibility test:
    a() --> f(a(),a())
Symbol transition graph:
    f	-->  # a f unit
  Collapsable symbols: { f }