NO

Problem:
 c() -> a()
 b() -> f(h(a(),a()))
 f(a()) -> b()
 h(a(),b()) -> a()

Proof:
 sorted: (order-sorted)
 0:c() -> a()
 1:b() -> f(h(a(),a()))
   f(a()) -> b()
   h(a(),b()) -> a()
 -----
 sorts
   [0>3, 1>2, 2>3]
 sort attachment (non-strict)
   c : 0
   a : 3
   b : 1
   f : 1 -> 1
   h : 2 x 1 -> 1
 -----
 0:c() -> a()
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed
 
 
 1:b() -> f(h(a(),a()))
   f(a()) -> b()
   h(a(),b()) -> a()
   Nonconfluence Processor:
    terms: h(a(),f(h(a(),a()))) *<- h(a(),b()) ->* a()
    Qed
    
    first automaton:
     final states: {1}
     transitions:
      h(3,2) -> 4*
      h(6,5) -> 1*
      a() -> 6,3,2
      f(4) -> 5*
    
    second automaton:
     final states: {7}
     transitions:
      a() -> 7*