YES(?,O(n^1))

Problem:
 f(f(x)) -> f(c(f(x)))
 f(f(x)) -> f(d(f(x)))
 g(c(x)) -> x
 g(d(x)) -> x
 g(c(h(0()))) -> g(d(1()))
 g(c(1())) -> g(d(h(0())))
 g(h(x)) -> g(x)

Proof:
 RT Transformation Processor:
  strict:
   f(f(x)) -> f(c(f(x)))
   f(f(x)) -> f(d(f(x)))
   g(c(x)) -> x
   g(d(x)) -> x
   g(c(h(0()))) -> g(d(1()))
   g(c(1())) -> g(d(h(0())))
   g(h(x)) -> g(x)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [1] = 15,
    
    [h](x0) = x0 + 20,
    
    [0] = 4,
    
    [g](x0) = x0 + 20,
    
    [d](x0) = x0 + 1,
    
    [c](x0) = x0 + 18,
    
    [f](x0) = x0 + 19
   orientation:
    f(f(x)) = x + 38 >= x + 56 = f(c(f(x)))
    
    f(f(x)) = x + 38 >= x + 39 = f(d(f(x)))
    
    g(c(x)) = x + 38 >= x = x
    
    g(d(x)) = x + 21 >= x = x
    
    g(c(h(0()))) = 62 >= 36 = g(d(1()))
    
    g(c(1())) = 53 >= 45 = g(d(h(0())))
    
    g(h(x)) = x + 40 >= x + 20 = g(x)
   problem:
    strict:
     f(f(x)) -> f(c(f(x)))
     f(f(x)) -> f(d(f(x)))
    weak:
     g(c(x)) -> x
     g(d(x)) -> x
     g(c(h(0()))) -> g(d(1()))
     g(c(1())) -> g(d(h(0())))
     g(h(x)) -> g(x)
   Bounds Processor:
    bound: 2
    enrichment: match-rt
    automaton:
     final states: {8}
     transitions:
      f1(21) -> 22*
      f1(23) -> 24*
      c1(55) -> 56*
      c1(57) -> 58*
      d1(25) -> 26*
      d1(22) -> 23*
      d1(74) -> 75*
      f2(41) -> 42*
      f2(43) -> 44*
      d2(42) -> 43*
      c2(71) -> 72*
      g1(75) -> 76*
      g1(101) -> 102*
      h1(73) -> 74*
      f0(8) -> 8*
      01() -> 73*
      c0(8) -> 8*
      11() -> 89*
      d0(8) -> 8*
      g0(8) -> 8*
      h0(8) -> 8*
      00() -> 8*
      10() -> 8*
      8 -> 21*
      22 -> 57*
      23 -> 41*
      24 -> 55,22,25,8
      26 -> 23*
      42 -> 71*
      44 -> 22*
      56 -> 23*
      58 -> 23*
      72 -> 43*
      73 -> 101*
      74 -> 76,8
      76 -> 8,21
      89 -> 74*
      102 -> 8,21
    problem:
     strict:
      f(f(x)) -> f(c(f(x)))
     weak:
      f(f(x)) -> f(d(f(x)))
      g(c(x)) -> x
      g(d(x)) -> x
      g(c(h(0()))) -> g(d(1()))
      g(c(1())) -> g(d(h(0())))
      g(h(x)) -> g(x)
    Bounds Processor:
     bound: 2
     enrichment: match-rt
     automaton:
      final states: {8}
      transitions:
       f1(15) -> 16*
       f1(13) -> 14*
       c1(17) -> 18*
       c1(14) -> 15*
       d1(42) -> 43*
       d1(31) -> 32*
       d1(33) -> 34*
       f2(25) -> 26*
       f2(23) -> 24*
       d2(39) -> 40*
       c2(24) -> 25*
       g1(54) -> 55*
       g1(43) -> 44*
       h1(41) -> 42*
       f0(8) -> 8*
       01() -> 41*
       c0(8) -> 8*
       11() -> 49*
       d0(8) -> 8*
       g0(8) -> 8*
       h0(8) -> 8*
       00() -> 8*
       10() -> 8*
       8 -> 13*
       14 -> 33*
       15 -> 23*
       16 -> 31,14,17,8
       18 -> 15*
       24 -> 39*
       26 -> 14*
       32 -> 15*
       34 -> 15*
       40 -> 25*
       41 -> 54*
       42 -> 44,8
       44 -> 8,13
       49 -> 42*
       55 -> 8,13
     problem:
      strict:
       
      weak:
       f(f(x)) -> f(c(f(x)))
       f(f(x)) -> f(d(f(x)))
       g(c(x)) -> x
       g(d(x)) -> x
       g(c(h(0()))) -> g(d(1()))
       g(c(1())) -> g(d(h(0())))
       g(h(x)) -> g(x)
     Qed