MAYBE

Problem:
 f(s(x)) -> f(id_inc(c(x,x)))
 f(c(s(x),y)) -> g(c(x,y))
 g(c(s(x),y)) -> g(c(y,x))
 g(c(x,s(y))) -> g(c(y,x))
 g(c(x,x)) -> f(x)
 id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
 id_inc(s(x)) -> s(id_inc(x))
 id_inc(0()) -> 0()
 id_inc(0()) -> s(0())

Proof:
 DP Processor:
  DPs:
   f#(s(x)) -> id_inc#(c(x,x))
   f#(s(x)) -> f#(id_inc(c(x,x)))
   f#(c(s(x),y)) -> g#(c(x,y))
   g#(c(s(x),y)) -> g#(c(y,x))
   g#(c(x,s(y))) -> g#(c(y,x))
   g#(c(x,x)) -> f#(x)
   id_inc#(c(x,y)) -> id_inc#(y)
   id_inc#(c(x,y)) -> id_inc#(x)
   id_inc#(s(x)) -> id_inc#(x)
  TRS:
   f(s(x)) -> f(id_inc(c(x,x)))
   f(c(s(x),y)) -> g(c(x,y))
   g(c(s(x),y)) -> g(c(y,x))
   g(c(x,s(y))) -> g(c(y,x))
   g(c(x,x)) -> f(x)
   id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
   id_inc(s(x)) -> s(id_inc(x))
   id_inc(0()) -> 0()
   id_inc(0()) -> s(0())
  Usable Rule Processor:
   DPs:
    f#(s(x)) -> id_inc#(c(x,x))
    f#(s(x)) -> f#(id_inc(c(x,x)))
    f#(c(s(x),y)) -> g#(c(x,y))
    g#(c(s(x),y)) -> g#(c(y,x))
    g#(c(x,s(y))) -> g#(c(y,x))
    g#(c(x,x)) -> f#(x)
    id_inc#(c(x,y)) -> id_inc#(y)
    id_inc#(c(x,y)) -> id_inc#(x)
    id_inc#(s(x)) -> id_inc#(x)
   TRS:
    f9(x,y) -> x
    f9(x,y) -> y
    id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
    id_inc(s(x)) -> s(id_inc(x))
    id_inc(0()) -> 0()
    id_inc(0()) -> s(0())
   EDG Processor:
    DPs:
     f#(s(x)) -> id_inc#(c(x,x))
     f#(s(x)) -> f#(id_inc(c(x,x)))
     f#(c(s(x),y)) -> g#(c(x,y))
     g#(c(s(x),y)) -> g#(c(y,x))
     g#(c(x,s(y))) -> g#(c(y,x))
     g#(c(x,x)) -> f#(x)
     id_inc#(c(x,y)) -> id_inc#(y)
     id_inc#(c(x,y)) -> id_inc#(x)
     id_inc#(s(x)) -> id_inc#(x)
    TRS:
     f9(x,y) -> x
     f9(x,y) -> y
     id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
     id_inc(s(x)) -> s(id_inc(x))
     id_inc(0()) -> 0()
     id_inc(0()) -> s(0())
    graph:
     g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(s(x),y)) -> g#(c(y,x))
     g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(x,s(y))) -> g#(c(y,x))
     g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(x,x)) -> f#(x)
     g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(s(x),y)) -> g#(c(y,x))
     g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(x,s(y))) -> g#(c(y,x))
     g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(x,x)) -> f#(x)
     g#(c(x,x)) -> f#(x) -> f#(s(x)) -> id_inc#(c(x,x))
     g#(c(x,x)) -> f#(x) -> f#(s(x)) -> f#(id_inc(c(x,x)))
     g#(c(x,x)) -> f#(x) -> f#(c(s(x),y)) -> g#(c(x,y))
     id_inc#(c(x,y)) -> id_inc#(y) -> id_inc#(c(x,y)) -> id_inc#(y)
     id_inc#(c(x,y)) -> id_inc#(y) -> id_inc#(c(x,y)) -> id_inc#(x)
     id_inc#(c(x,y)) -> id_inc#(y) -> id_inc#(s(x)) -> id_inc#(x)
     id_inc#(c(x,y)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(y)
     id_inc#(c(x,y)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(x)
     id_inc#(c(x,y)) -> id_inc#(x) -> id_inc#(s(x)) -> id_inc#(x)
     id_inc#(s(x)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(y)
     id_inc#(s(x)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(x)
     id_inc#(s(x)) -> id_inc#(x) -> id_inc#(s(x)) -> id_inc#(x)
     f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(s(x),y)) -> g#(c(y,x))
     f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(x,s(y))) -> g#(c(y,x))
     f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(x,x)) -> f#(x)
     f#(s(x)) -> id_inc#(c(x,x)) -> id_inc#(c(x,y)) -> id_inc#(y)
     f#(s(x)) -> id_inc#(c(x,x)) -> id_inc#(c(x,y)) -> id_inc#(x)
     f#(s(x)) -> f#(id_inc(c(x,x))) -> f#(s(x)) -> id_inc#(c(x,x))
     f#(s(x)) -> f#(id_inc(c(x,x))) -> f#(s(x)) -> f#(id_inc(c(x,x)))
     f#(s(x)) -> f#(id_inc(c(x,x))) -> f#(c(s(x),y)) -> g#(c(x,y))
    Restore Modifier:
     DPs:
      f#(s(x)) -> id_inc#(c(x,x))
      f#(s(x)) -> f#(id_inc(c(x,x)))
      f#(c(s(x),y)) -> g#(c(x,y))
      g#(c(s(x),y)) -> g#(c(y,x))
      g#(c(x,s(y))) -> g#(c(y,x))
      g#(c(x,x)) -> f#(x)
      id_inc#(c(x,y)) -> id_inc#(y)
      id_inc#(c(x,y)) -> id_inc#(x)
      id_inc#(s(x)) -> id_inc#(x)
     TRS:
      f(s(x)) -> f(id_inc(c(x,x)))
      f(c(s(x),y)) -> g(c(x,y))
      g(c(s(x),y)) -> g(c(y,x))
      g(c(x,s(y))) -> g(c(y,x))
      g(c(x,x)) -> f(x)
      id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
      id_inc(s(x)) -> s(id_inc(x))
      id_inc(0()) -> 0()
      id_inc(0()) -> s(0())
     SCC Processor:
      #sccs: 2
      #rules: 8
      #arcs: 26/81
      DPs:
       g#(c(s(x),y)) -> g#(c(y,x))
       g#(c(x,x)) -> f#(x)
       f#(c(s(x),y)) -> g#(c(x,y))
       g#(c(x,s(y))) -> g#(c(y,x))
       f#(s(x)) -> f#(id_inc(c(x,x)))
      TRS:
       f(s(x)) -> f(id_inc(c(x,x)))
       f(c(s(x),y)) -> g(c(x,y))
       g(c(s(x),y)) -> g(c(y,x))
       g(c(x,s(y))) -> g(c(y,x))
       g(c(x,x)) -> f(x)
       id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
       id_inc(s(x)) -> s(id_inc(x))
       id_inc(0()) -> 0()
       id_inc(0()) -> s(0())
      Open
      
      DPs:
       id_inc#(c(x,y)) -> id_inc#(x)
       id_inc#(s(x)) -> id_inc#(x)
       id_inc#(c(x,y)) -> id_inc#(y)
      TRS:
       f(s(x)) -> f(id_inc(c(x,x)))
       f(c(s(x),y)) -> g(c(x,y))
       g(c(s(x),y)) -> g(c(y,x))
       g(c(x,s(y))) -> g(c(y,x))
       g(c(x,x)) -> f(x)
       id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
       id_inc(s(x)) -> s(id_inc(x))
       id_inc(0()) -> 0()
       id_inc(0()) -> s(0())
      Open