YES

# orthogonality

Consider the left-linear TRS R:

  a() -> a()
  b() -> h(f(f(f(b()))),h(b(),f(a())))

The left-linear and non-overlapping TRS is confluent