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

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