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

Proof:
 Nonconfluence Processor:
  terms: h(g(c())) *<- a() ->* h(f(c()))
  Qed
  
  first automaton:
   final states: {1}
   transitions:
    h(3) -> 1*
    c() -> 2*
    f(56) -> 1*
    g(2) -> 3*
    g(56) -> 3*
    g(3) -> 56*
  
  second automaton:
   final states: {7}
   transitions:
    h(55) -> 9*
    h(9) -> 7*
    c() -> 8*
    f(142) -> 7*
    f(8) -> 9*
    g(55) -> 8*
    g(142) -> 9*
    g(9) -> 142*
    g(8) -> 55*