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

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