MAYBE

Problem:
 intlist(nil()) -> nil()
 intlist(cons(x,y)) -> cons(s(x),intlist(y))
 int(0(),0()) -> cons(0(),nil())
 int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
 int(s(x),0()) -> nil()
 int(s(x),s(y)) -> intlist(int(x,y))

Proof:
 DP Processor:
  DPs:
   intlist#(cons(x,y)) -> intlist#(y)
   int#(0(),s(y)) -> int#(s(0()),s(y))
   int#(s(x),s(y)) -> int#(x,y)
   int#(s(x),s(y)) -> intlist#(int(x,y))
  TRS:
   intlist(nil()) -> nil()
   intlist(cons(x,y)) -> cons(s(x),intlist(y))
   int(0(),0()) -> cons(0(),nil())
   int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
   int(s(x),0()) -> nil()
   int(s(x),s(y)) -> intlist(int(x,y))
  TDG Processor:
   DPs:
    intlist#(cons(x,y)) -> intlist#(y)
    int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(s(x),s(y)) -> int#(x,y)
    int#(s(x),s(y)) -> intlist#(int(x,y))
   TRS:
    intlist(nil()) -> nil()
    intlist(cons(x,y)) -> cons(s(x),intlist(y))
    int(0(),0()) -> cons(0(),nil())
    int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
    int(s(x),0()) -> nil()
    int(s(x),s(y)) -> intlist(int(x,y))
   graph:
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(s(x),s(y)) -> intlist#(int(x,y))
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(s(x),s(y)) -> int#(x,y)
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(s(x),s(y)) -> int#(x,y) ->
    int#(s(x),s(y)) -> intlist#(int(x,y))
    int#(s(x),s(y)) -> int#(x,y) -> int#(s(x),s(y)) -> int#(x,y)
    int#(s(x),s(y)) -> int#(x,y) ->
    int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(s(x),s(y)) -> intlist#(int(x,y)) ->
    intlist#(cons(x,y)) -> intlist#(y)
    intlist#(cons(x,y)) -> intlist#(y) -> intlist#(cons(x,y)) -> intlist#(y)
   EDG Processor:
    DPs:
     intlist#(cons(x,y)) -> intlist#(y)
     int#(0(),s(y)) -> int#(s(0()),s(y))
     int#(s(x),s(y)) -> int#(x,y)
     int#(s(x),s(y)) -> intlist#(int(x,y))
    TRS:
     intlist(nil()) -> nil()
     intlist(cons(x,y)) -> cons(s(x),intlist(y))
     int(0(),0()) -> cons(0(),nil())
     int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
     int(s(x),0()) -> nil()
     int(s(x),s(y)) -> intlist(int(x,y))
    graph:
     int#(0(),s(y)) -> int#(s(0()),s(y)) ->
     int#(s(x),s(y)) -> int#(x,y)
     int#(0(),s(y)) -> int#(s(0()),s(y)) ->
     int#(s(x),s(y)) -> intlist#(int(x,y))
     int#(s(x),s(y)) -> int#(x,y) ->
     int#(0(),s(y)) -> int#(s(0()),s(y))
     int#(s(x),s(y)) -> int#(x,y) -> int#(s(x),s(y)) -> int#(x,y)
     int#(s(x),s(y)) -> int#(x,y) ->
     int#(s(x),s(y)) -> intlist#(int(x,y))
     int#(s(x),s(y)) -> intlist#(int(x,y)) ->
     intlist#(cons(x,y)) -> intlist#(y)
     intlist#(cons(x,y)) -> intlist#(y) -> intlist#(cons(x,y)) -> intlist#(y)
    Restore Modifier:
     DPs:
      intlist#(cons(x,y)) -> intlist#(y)
      int#(0(),s(y)) -> int#(s(0()),s(y))
      int#(s(x),s(y)) -> int#(x,y)
      int#(s(x),s(y)) -> intlist#(int(x,y))
     TRS:
      intlist(nil()) -> nil()
      intlist(cons(x,y)) -> cons(s(x),intlist(y))
      int(0(),0()) -> cons(0(),nil())
      int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
      int(s(x),0()) -> nil()
      int(s(x),s(y)) -> intlist(int(x,y))
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 7/16
      DPs:
       int#(0(),s(y)) -> int#(s(0()),s(y))
       int#(s(x),s(y)) -> int#(x,y)
      TRS:
       intlist(nil()) -> nil()
       intlist(cons(x,y)) -> cons(s(x),intlist(y))
       int(0(),0()) -> cons(0(),nil())
       int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
       int(s(x),0()) -> nil()
       int(s(x),s(y)) -> intlist(int(x,y))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [int#](x0, x1) = x1 + 1,
        
        [int](x0, x1) = 0,
        
        [0] = 1,
        
        [s](x0) = x0 + 1,
        
        [cons](x0, x1) = 0,
        
        [intlist](x0) = 0,
        
        [nil] = 0
       orientation:
        int#(0(),s(y)) = y + 2 >= y + 2 = int#(s(0()),s(y))
        
        int#(s(x),s(y)) = y + 2 >= y + 1 = int#(x,y)
        
        intlist(nil()) = 0 >= 0 = nil()
        
        intlist(cons(x,y)) = 0 >= 0 = cons(s(x),intlist(y))
        
        int(0(),0()) = 0 >= 0 = cons(0(),nil())
        
        int(0(),s(y)) = 0 >= 0 = cons(0(),int(s(0()),s(y)))
        
        int(s(x),0()) = 0 >= 0 = nil()
        
        int(s(x),s(y)) = 0 >= 0 = intlist(int(x,y))
       problem:
        DPs:
         int#(0(),s(y)) -> int#(s(0()),s(y))
        TRS:
         intlist(nil()) -> nil()
         intlist(cons(x,y)) -> cons(s(x),intlist(y))
         int(0(),0()) -> cons(0(),nil())
         int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
         int(s(x),0()) -> nil()
         int(s(x),s(y)) -> intlist(int(x,y))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [int#](x0, x1) = x0,
         
         [int](x0, x1) = x0 + 1,
         
         [0] = 1,
         
         [s](x0) = 0,
         
         [cons](x0, x1) = x0 + 1,
         
         [intlist](x0) = 1,
         
         [nil] = 1
        orientation:
         int#(0(),s(y)) = 1 >= 0 = int#(s(0()),s(y))
         
         intlist(nil()) = 1 >= 1 = nil()
         
         intlist(cons(x,y)) = 1 >= 1 = cons(s(x),intlist(y))
         
         int(0(),0()) = 2 >= 2 = cons(0(),nil())
         
         int(0(),s(y)) = 2 >= 2 = cons(0(),int(s(0()),s(y)))
         
         int(s(x),0()) = 1 >= 1 = nil()
         
         int(s(x),s(y)) = 1 >= 1 = intlist(int(x,y))
        problem:
         DPs:
          
         TRS:
          intlist(nil()) -> nil()
          intlist(cons(x,y)) -> cons(s(x),intlist(y))
          int(0(),0()) -> cons(0(),nil())
          int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
          int(s(x),0()) -> nil()
          int(s(x),s(y)) -> intlist(int(x,y))
        Qed
      
      DPs:
       intlist#(cons(x,y)) -> intlist#(y)
      TRS:
       intlist(nil()) -> nil()
       intlist(cons(x,y)) -> cons(s(x),intlist(y))
       int(0(),0()) -> cons(0(),nil())
       int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
       int(s(x),0()) -> nil()
       int(s(x),s(y)) -> intlist(int(x,y))
      Open