MAYBE

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)))
  CDG 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)))
    Open
    
    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)))
    Open