Problem:
 a() -> f(a())
 a() -> g(h(a()))
 f(x) -> h(g(x))
 h(x) -> f(g(x))

Proof:
 Nonconfluence Processor:
  terms: g(h(a())) *<- a() ->* f(a())
  Qed
  
  first automaton:
   final states: {1}
   transitions:
    a() -> 2*
    f(2) -> 2*
    f(28) -> 3*
    h(2) -> 3*
    h(28) -> 2*
    g(2) -> 28*
    g(28) -> 2*
    g(3) -> 2,1
  
  second automaton:
   final states: {4}
   transitions:
    a() -> 5*
    f(5) -> 5,4
    f(27) -> 16*
    h(5) -> 16*
    h(27) -> 5,4
    g(5) -> 27*
    g(27) -> 5*
    g(16) -> 5*