MAYBE
Time: 0.340453
TRS:
 {f(x, c x, c y) -> f(y, y, f(y, x, y)),
    f(c x, x, y) -> c y,
    f(s x, y, z) -> f(x, s c y, c z),
         g(x, y) -> y,
         g(x, y) -> x}
 DP:
  DP:
   {f#(x, c x, c y) -> f#(y, y, f(y, x, y)),
    f#(x, c x, c y) -> f#(y, x, y),
      f#(s x, y, z) -> f#(x, s c y, c z)}
  TRS:
  {f(x, c x, c y) -> f(y, y, f(y, x, y)),
     f(c x, x, y) -> c y,
     f(s x, y, z) -> f(x, s c y, c z),
          g(x, y) -> y,
          g(x, y) -> x}
  EDG:
   {(f#(x, c x, c y) -> f#(y, x, y), f#(s x, y, z) -> f#(x, s c y, c z))
    (f#(x, c x, c y) -> f#(y, x, y), f#(x, c x, c y) -> f#(y, x, y))
    (f#(x, c x, c y) -> f#(y, x, y), f#(x, c x, c y) -> f#(y, y, f(y, x, y)))
    (f#(s x, y, z) -> f#(x, s c y, c z), f#(s x, y, z) -> f#(x, s c y, c z))
    (f#(x, c x, c y) -> f#(y, y, f(y, x, y)), f#(x, c x, c y) -> f#(y, y, f(y, x, y)))
    (f#(x, c x, c y) -> f#(y, y, f(y, x, y)), f#(x, c x, c y) -> f#(y, x, y))
    (f#(x, c x, c y) -> f#(y, y, f(y, x, y)), f#(s x, y, z) -> f#(x, s c y, c z))}
   STATUS:
    arrows: 0.222222
    SCCS (2):
     Scc:
      {f#(x, c x, c y) -> f#(y, y, f(y, x, y)),
       f#(x, c x, c y) -> f#(y, x, y)}
     Scc:
      {f#(s x, y, z) -> f#(x, s c y, c z)}
     
     SCC (2):
      Strict:
       {f#(x, c x, c y) -> f#(y, y, f(y, x, y)),
        f#(x, c x, c y) -> f#(y, x, y)}
      Weak:
      {f(x, c x, c y) -> f(y, y, f(y, x, y)),
         f(c x, x, y) -> c y,
         f(s x, y, z) -> f(x, s c y, c z),
              g(x, y) -> y,
              g(x, y) -> x}
      Fail
     SCC (1):
      Strict:
       {f#(s x, y, z) -> f#(x, s c y, c z)}
      Weak:
      {f(x, c x, c y) -> f(y, y, f(y, x, y)),
         f(c x, x, y) -> c y,
         f(s x, y, z) -> f(x, s c y, c z),
              g(x, y) -> y,
              g(x, y) -> x}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1, x2) = x0 + x1 + x2,
        
        [g](x0, x1) = 0,
        
        [c](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [f#](x0, x1, x2) = x0
       Strict:
        f#(s x, y, z) -> f#(x, s c y, c z)
        1 + 0y + 1x + 0z >= 0 + 0y + 1x + 0z
       Weak:
        g(x, y) -> x
        0 + 0y + 0x >= 1x
        g(x, y) -> y
        0 + 0y + 0x >= 1y
        f(s x, y, z) -> f(x, s c y, c z)
        1 + 1y + 1x + 1z >= 1 + 1y + 1x + 1z
        f(c x, x, y) -> c y
        0 + 1y + 2x >= 0 + 1y
        f(x, c x, c y) -> f(y, y, f(y, x, y))
        0 + 1y + 2x >= 0 + 4y + 1x
      Qed