YES

Problem:
 g(h(x1)) -> g(f(s(x1)))
 f(s(s(s(x1)))) -> h(f(s(h(x1))))
 f(h(x1)) -> h(f(s(h(x1))))
 h(x1) -> x1
 f(f(s(s(x1)))) -> s(s(s(f(f(x1)))))
 b(a(x1)) -> a(b(x1))
 a(a(a(x1))) -> b(a(a(b(x1))))
 b(b(b(b(x1)))) -> a(x1)

Proof:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [b](x0) = 1x0,
   
   [a](x0) = 2x0,
   
   [f](x0) = x0,
   
   [s](x0) = x0,
   
   [g](x0) = x0,
   
   [h](x0) = x0
  orientation:
   g(h(x1)) = x1 >= x1 = g(f(s(x1)))
   
   f(s(s(s(x1)))) = x1 >= x1 = h(f(s(h(x1))))
   
   f(h(x1)) = x1 >= x1 = h(f(s(h(x1))))
   
   h(x1) = x1 >= x1 = x1
   
   f(f(s(s(x1)))) = x1 >= x1 = s(s(s(f(f(x1)))))
   
   b(a(x1)) = 3x1 >= 3x1 = a(b(x1))
   
   a(a(a(x1))) = 6x1 >= 6x1 = b(a(a(b(x1))))
   
   b(b(b(b(x1)))) = 4x1 >= 2x1 = a(x1)
  problem:
   g(h(x1)) -> g(f(s(x1)))
   f(s(s(s(x1)))) -> h(f(s(h(x1))))
   f(h(x1)) -> h(f(s(h(x1))))
   h(x1) -> x1
   f(f(s(s(x1)))) -> s(s(s(f(f(x1)))))
   b(a(x1)) -> a(b(x1))
   a(a(a(x1))) -> b(a(a(b(x1))))
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [b](x0) = x0,
    
    [a](x0) = 2x0,
    
    [f](x0) = x0,
    
    [s](x0) = x0,
    
    [g](x0) = 12x0,
    
    [h](x0) = x0
   orientation:
    g(h(x1)) = 12x1 >= 12x1 = g(f(s(x1)))
    
    f(s(s(s(x1)))) = x1 >= x1 = h(f(s(h(x1))))
    
    f(h(x1)) = x1 >= x1 = h(f(s(h(x1))))
    
    h(x1) = x1 >= x1 = x1
    
    f(f(s(s(x1)))) = x1 >= x1 = s(s(s(f(f(x1)))))
    
    b(a(x1)) = 2x1 >= 2x1 = a(b(x1))
    
    a(a(a(x1))) = 6x1 >= 4x1 = b(a(a(b(x1))))
   problem:
    g(h(x1)) -> g(f(s(x1)))
    f(s(s(s(x1)))) -> h(f(s(h(x1))))
    f(h(x1)) -> h(f(s(h(x1))))
    h(x1) -> x1
    f(f(s(s(x1)))) -> s(s(s(f(f(x1)))))
    b(a(x1)) -> a(b(x1))
   Bounds Processor:
    bound: 1
    enrichment: match
    automaton:
     final states: {14,9,2,5,1}
     transitions:
      g1(18) -> 19*
      f1(17) -> 18*
      f1(26) -> 27*
      s1(25) -> 26*
      s1(16) -> 17*
      h1(40) -> 41*
      h1(27) -> 28*
      h1(44) -> 45*
      h1(34) -> 35*
      h1(24) -> 25*
      f60() -> 2*
      g0(4) -> 1*
      f0(10) -> 11*
      f0(7) -> 8*
      f0(2) -> 10*
      f0(3) -> 4*
      s0(12) -> 13*
      s0(2) -> 3*
      s0(11) -> 12*
      s0(6) -> 7*
      s0(13) -> 9*
      h0(2) -> 6*
      h0(8) -> 5*
      a0(15) -> 14*
      b0(2) -> 15*
      2 -> 6*
      5 -> 10,4,8
      8 -> 24,16,5
      9 -> 10,11
      11 -> 34*
      12 -> 40*
      13 -> 44*
      14 -> 15*
      19 -> 1*
      24 -> 25*
      27 -> 28,11
      28 -> 27,11
      34 -> 35,25
      35 -> 25*
      40 -> 41,25
      41 -> 25*
      44 -> 45,25
      45 -> 25*
    problem:
     
    Qed