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

Proof:
 Nonconfluence Processor:
  terms: h(f(c())) *<- a() ->* f(c())
  Qed
  
  first automaton:
   final states: {7}
   transitions:
    h(9) -> 7*
    h(53) -> 9*
    c() -> 8*
    f(8) -> 9*
    g(9) -> 9*
    g(53) -> 53*
    g(8) -> 53*
  
  second automaton:
   final states: {15}
   transitions:
    h(54) -> 15*
    c() -> 16*
    f(16) -> 15*
    g(54) -> 54*
    g(16) -> 54*