Problem:
 f(g(x,a(),b())) -> x
 p(a()) -> c()
 g(f(h(c(),d())),x,y) -> h(p(x),q(x))
 q(b()) -> d()

Proof:
 Nonconfluence Processor:
  terms: f(h(p(a()),q(a()))) *<- f(g(f(h(c(),d())),a(),b())) ->* f(h(c(),d()))
  Qed
  
  first automaton:
   final states: {1}
   transitions:
    f(6) -> 1*
    a() -> 4,2
    p(4) -> 5*
    q(2) -> 3*
    c() -> 5*
    h(5,3) -> 6*
  
  second automaton:
   final states: {7}
   transitions:
    d() -> 8*
    f(10) -> 7*
    c() -> 9*
    h(9,8) -> 10*