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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 1
   g(b()) <-2|0[]- g(a()) -0|[]-> f(g(a()))
  Redundant Rules Transformation:
   g(b()) -> c(a())
   a() -> b()
   f(x) -> h(x)
   h(x) -> c(b())
   Church Rosser Transformation Processor (ac):
    g(b()) -> c(a())
    a() -> b()
    f(x) -> h(x)
    h(x) -> c(b())
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      f > h > a > b > g > c
      weight function:
       w0 = 1
       w(h) = w(f) = 5
       w(c) = w(g) = 4
       w(b) = w(a) = 2
      problem:
       
      Qed