YES

Problem:
 f(0()) -> true()
 f(1()) -> false()
 f(s(x)) -> f(x)
 if(true(),s(x),s(y)) -> s(x)
 if(false(),s(x),s(y)) -> s(y)
 g(x,c(y)) -> c(g(x,y))
 g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))

Proof:
 DP Processor:
  DPs:
   f#(s(x)) -> f#(x)
   g#(x,c(y)) -> g#(x,y)
   g#(x,c(y)) -> g#(s(x),y)
   g#(x,c(y)) -> f#(x)
   g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
   g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
  TRS:
   f(0()) -> true()
   f(1()) -> false()
   f(s(x)) -> f(x)
   if(true(),s(x),s(y)) -> s(x)
   if(false(),s(x),s(y)) -> s(y)
   g(x,c(y)) -> c(g(x,y))
   g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
  TDG Processor:
   DPs:
    f#(s(x)) -> f#(x)
    g#(x,c(y)) -> g#(x,y)
    g#(x,c(y)) -> g#(s(x),y)
    g#(x,c(y)) -> f#(x)
    g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
   TRS:
    f(0()) -> true()
    f(1()) -> false()
    f(s(x)) -> f(x)
    if(true(),s(x),s(y)) -> s(x)
    if(false(),s(x),s(y)) -> s(y)
    g(x,c(y)) -> c(g(x,y))
    g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
   graph:
    g#(x,c(y)) -> g#(s(x),y) ->
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
    g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
    g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> f#(x)
    g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> g#(s(x),y)
    g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> g#(x,y)
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y))) ->
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y))) ->
    g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y))) ->
    g#(x,c(y)) -> f#(x)
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y))) ->
    g#(x,c(y)) -> g#(s(x),y)
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y))) -> g#(x,c(y)) -> g#(x,y)
    g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
    g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
    g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> f#(x)
    g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> g#(s(x),y)
    g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> g#(x,y)
    g#(x,c(y)) -> f#(x) -> f#(s(x)) -> f#(x)
    f#(s(x)) -> f#(x) -> f#(s(x)) -> f#(x)
   EDG Processor:
    DPs:
     f#(s(x)) -> f#(x)
     g#(x,c(y)) -> g#(x,y)
     g#(x,c(y)) -> g#(s(x),y)
     g#(x,c(y)) -> f#(x)
     g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
     g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
    TRS:
     f(0()) -> true()
     f(1()) -> false()
     f(s(x)) -> f(x)
     if(true(),s(x),s(y)) -> s(x)
     if(false(),s(x),s(y)) -> s(y)
     g(x,c(y)) -> c(g(x,y))
     g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
    graph:
     g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> g#(x,y)
     g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> g#(s(x),y)
     g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> f#(x)
     g#(x,c(y)) -> g#(s(x),y) -> g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
     g#(x,c(y)) -> g#(s(x),y) ->
     g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
     g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> g#(x,y)
     g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> g#(s(x),y)
     g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> f#(x)
     g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
     g#(x,c(y)) -> g#(x,y) -> g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
     g#(x,c(y)) -> f#(x) -> f#(s(x)) -> f#(x)
     f#(s(x)) -> f#(x) -> f#(s(x)) -> f#(x)
    SCC Processor:
     #sccs: 2
     #rules: 3
     #arcs: 12/36
     DPs:
      g#(x,c(y)) -> g#(s(x),y)
      g#(x,c(y)) -> g#(x,y)
     TRS:
      f(0()) -> true()
      f(1()) -> false()
      f(s(x)) -> f(x)
      if(true(),s(x),s(y)) -> s(x)
      if(false(),s(x),s(y)) -> s(y)
      g(x,c(y)) -> c(g(x,y))
      g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(f) = []
       pi(true) = []
       pi(1) = []
       pi(false) = []
       pi(s) = []
       pi(if) = 1
       pi(c) = [0]
       pi(g) = 1
       pi(g#) = 1
      weight function:
       w0 = 1
       w(g#) = w(g) = w(c) = w(if) = w(s) = w(false) = w(1) = w(true) = w(f) = w(0) = 1
      precedence:
       g# ~ c ~ s ~ 1 ~ f > g ~ if ~ false ~ true ~ 0
      problem:
       DPs:
        
       TRS:
        f(0()) -> true()
        f(1()) -> false()
        f(s(x)) -> f(x)
        if(true(),s(x),s(y)) -> s(x)
        if(false(),s(x),s(y)) -> s(y)
        g(x,c(y)) -> c(g(x,y))
        g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
      Qed
     
     DPs:
      f#(s(x)) -> f#(x)
     TRS:
      f(0()) -> true()
      f(1()) -> false()
      f(s(x)) -> f(x)
      if(true(),s(x),s(y)) -> s(x)
      if(false(),s(x),s(y)) -> s(y)
      g(x,c(y)) -> c(g(x,y))
      g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(f) = [0]
       pi(true) = []
       pi(1) = []
       pi(false) = []
       pi(s) = [0]
       pi(if) = [0,1,2]
       pi(c) = []
       pi(g) = [0]
       pi(f#) = 0
      weight function:
       w0 = 1
       w(f#) = w(g) = w(c) = w(s) = w(false) = w(1) = w(true) = w(f) = w(0) = 1
       w(if) = 0
      precedence:
       f# ~ g ~ c ~ if ~ s ~ false ~ 1 ~ true ~ f ~ 0
      problem:
       DPs:
        
       TRS:
        f(0()) -> true()
        f(1()) -> false()
        f(s(x)) -> f(x)
        if(true(),s(x),s(y)) -> s(x)
        if(false(),s(x),s(y)) -> s(y)
        g(x,c(y)) -> c(g(x,y))
        g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
      Qed