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

Proof:
 sorted: (order-sorted)
 0:a() -> c()
   f(a()) -> b()
 1:a() -> c()
   h(h(b(),b()),a()) -> a()
 -----
 sorts
   [0>3, 0>4, 1>2, 2>3, 2>5, 4>5, 5>6]
 sort attachment (non-strict)
   a : 5
   c : 6
   h : 1 x 2 -> 1
   b : 3
   f : 4 -> 0
 -----
 0:a() -> c()
   f(a()) -> b()
   Nonconfluence Processor:
    terms: f(c()) *<- f(a()) ->* b()
    Qed
 
 
 1:a() -> c()
   h(h(b(),b()),a()) -> a()
   Open