YES
TRS:
 {           f(0()) -> true(),
             f(1()) -> false(),
            f(s(x)) -> f(x),
   if(true(), x, y) -> x,
  if(false(), x, y) -> y,
         g(x, c(y)) -> g(x, g(s(c(y)), y)),
      g(s(x), s(y)) -> if(f(x), s(x), s(y))}
 DP:
  Strict:
   {      f#(s(x)) -> f#(x),
       g#(x, c(y)) -> g#(x, g(s(c(y)), y)),
       g#(x, c(y)) -> g#(s(c(y)), y),
    g#(s(x), s(y)) -> f#(x),
    g#(s(x), s(y)) -> if#(f(x), s(x), s(y))}
  Weak:
  {           f(0()) -> true(),
              f(1()) -> false(),
             f(s(x)) -> f(x),
    if(true(), x, y) -> x,
   if(false(), x, y) -> y,
          g(x, c(y)) -> g(x, g(s(c(y)), y)),
       g(s(x), s(y)) -> if(f(x), s(x), s(y))}
  EDG:
   {(g#(s(x), s(y)) -> f#(x), f#(s(x)) -> f#(x))
    (g#(x, c(y)) -> g#(s(c(y)), y), g#(x, c(y)) -> g#(x, g(s(c(y)), y)))
    (g#(x, c(y)) -> g#(s(c(y)), y), g#(x, c(y)) -> g#(s(c(y)), y))
    (g#(x, c(y)) -> g#(s(c(y)), y), g#(s(x), s(y)) -> f#(x))
    (g#(x, c(y)) -> g#(s(c(y)), y), g#(s(x), s(y)) -> if#(f(x), s(x), s(y)))
    (g#(x, c(y)) -> g#(x, g(s(c(y)), y)), g#(x, c(y)) -> g#(x, g(s(c(y)), y)))
    (g#(x, c(y)) -> g#(x, g(s(c(y)), y)), g#(x, c(y)) -> g#(s(c(y)), y))
    (g#(x, c(y)) -> g#(x, g(s(c(y)), y)), g#(s(x), s(y)) -> f#(x))
    (g#(x, c(y)) -> g#(x, g(s(c(y)), y)), g#(s(x), s(y)) -> if#(f(x), s(x), s(y)))
    (f#(s(x)) -> f#(x), f#(s(x)) -> f#(x))}
   SCCS:
    Scc:
     {g#(x, c(y)) -> g#(x, g(s(c(y)), y)),
      g#(x, c(y)) -> g#(s(c(y)), y)}
    Scc:
     {f#(s(x)) -> f#(x)}
    SCC:
     Strict:
      {g#(x, c(y)) -> g#(x, g(s(c(y)), y)),
       g#(x, c(y)) -> g#(s(c(y)), y)}
     Weak:
     {           f(0()) -> true(),
                 f(1()) -> false(),
                f(s(x)) -> f(x),
       if(true(), x, y) -> x,
      if(false(), x, y) -> y,
             g(x, c(y)) -> g(x, g(s(c(y)), y)),
          g(s(x), s(y)) -> if(f(x), s(x), s(y))}
     POLY:
      Argument Filtering:
       pi(c) = [0], pi(g#) = [1], pi(g) = 1, pi(if) = [1,2], pi(s) = [], pi(1) = [], pi(false) = [], pi(0) = [], pi(f) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [g#](x0) = x0 + 1,
       [c](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {           f(0()) -> true(),
                   f(1()) -> false(),
                  f(s(x)) -> f(x),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
               g(x, c(y)) -> g(x, g(s(c(y)), y)),
            g(s(x), s(y)) -> if(f(x), s(x), s(y))}
      Qed
    SCC:
     Strict:
      {f#(s(x)) -> f#(x)}
     Weak:
     {           f(0()) -> true(),
                 f(1()) -> false(),
                f(s(x)) -> f(x),
       if(true(), x, y) -> x,
      if(false(), x, y) -> y,
             g(x, c(y)) -> g(x, g(s(c(y)), y)),
          g(s(x), s(y)) -> if(f(x), s(x), s(y))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {}
      Qed