MAYBE

Problem:
 empty(nil()) -> true()
 empty(cons(x,l)) -> false()
 head(cons(x,l)) -> x
 tail(nil()) -> nil()
 tail(cons(x,l)) -> l
 rev(nil()) -> nil()
 rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
 last(x,l) -> if(empty(l),x,l)
 if(true(),x,l) -> x
 if(false(),x,l) -> last(head(l),tail(l))
 rev2(x,nil()) -> nil()
 rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

Proof:
 DP Processor:
  DPs:
   rev#(cons(x,l)) -> rev2#(x,l)
   last#(x,l) -> empty#(l)
   last#(x,l) -> if#(empty(l),x,l)
   if#(false(),x,l) -> tail#(l)
   if#(false(),x,l) -> head#(l)
   if#(false(),x,l) -> last#(head(l),tail(l))
   rev2#(x,cons(y,l)) -> rev2#(y,l)
   rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
  TRS:
   empty(nil()) -> true()
   empty(cons(x,l)) -> false()
   head(cons(x,l)) -> x
   tail(nil()) -> nil()
   tail(cons(x,l)) -> l
   rev(nil()) -> nil()
   rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
   last(x,l) -> if(empty(l),x,l)
   if(true(),x,l) -> x
   if(false(),x,l) -> last(head(l),tail(l))
   rev2(x,nil()) -> nil()
   rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
  TDG Processor:
   DPs:
    rev#(cons(x,l)) -> rev2#(x,l)
    last#(x,l) -> empty#(l)
    last#(x,l) -> if#(empty(l),x,l)
    if#(false(),x,l) -> tail#(l)
    if#(false(),x,l) -> head#(l)
    if#(false(),x,l) -> last#(head(l),tail(l))
    rev2#(x,cons(y,l)) -> rev2#(y,l)
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
   TRS:
    empty(nil()) -> true()
    empty(cons(x,l)) -> false()
    head(cons(x,l)) -> x
    tail(nil()) -> nil()
    tail(cons(x,l)) -> l
    rev(nil()) -> nil()
    rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
    last(x,l) -> if(empty(l),x,l)
    if(true(),x,l) -> x
    if(false(),x,l) -> last(head(l),tail(l))
    rev2(x,nil()) -> nil()
    rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
   graph:
    if#(false(),x,l) -> last#(head(l),tail(l)) ->
    last#(x,l) -> if#(empty(l),x,l)
    if#(false(),x,l) -> last#(head(l),tail(l)) ->
    last#(x,l) -> empty#(l)
    last#(x,l) -> if#(empty(l),x,l) ->
    if#(false(),x,l) -> last#(head(l),tail(l))
    last#(x,l) -> if#(empty(l),x,l) -> if#(false(),x,l) -> head#(l)
    last#(x,l) -> if#(empty(l),x,l) -> if#(false(),x,l) -> tail#(l)
    rev2#(x,cons(y,l)) -> rev2#(y,l) ->
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
    rev2#(x,cons(y,l)) -> rev2#(y,l) ->
    rev2#(x,cons(y,l)) -> rev2#(y,l)
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l))) ->
    rev#(cons(x,l)) -> rev2#(x,l)
    rev#(cons(x,l)) -> rev2#(x,l) ->
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
    rev#(cons(x,l)) -> rev2#(x,l) -> rev2#(x,cons(y,l)) -> rev2#(y,l)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 10/64
    DPs:
     rev2#(x,cons(y,l)) -> rev2#(y,l)
     rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
     rev#(cons(x,l)) -> rev2#(x,l)
    TRS:
     empty(nil()) -> true()
     empty(cons(x,l)) -> false()
     head(cons(x,l)) -> x
     tail(nil()) -> nil()
     tail(cons(x,l)) -> l
     rev(nil()) -> nil()
     rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
     last(x,l) -> if(empty(l),x,l)
     if(true(),x,l) -> x
     if(false(),x,l) -> last(head(l),tail(l))
     rev2(x,nil()) -> nil()
     rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
      [rev2#](x0, x1) = [0 0]x0 + [0 1]x1 + [0],
      
      [rev#](x0) = [0 0]x0 + [0],
      
                         [-& -&]          [3 2]     [3]
      [if](x0, x1, x2) = [0  0 ]x0 + x1 + [3 0]x2 + [0],
      
                       [0 0]     [3 2]     [3]
      [last](x0, x1) = [0 0]x0 + [3 0]x1 + [0],
      
                       [0 0]  
      [rev2](x0, x1) = [0 0]x1,
      
                       [0 0]     [2 ]
      [rev1](x0, x1) = [0 0]x1 + [-&],
      
                  [0  -&]     [1]
      [rev](x0) = [0  -&]x0 + [2],
      
                        [-&]
      [tail](x0) = x0 + [0 ],
      
                   [0 0]     [3]
      [head](x0) = [2 0]x0 + [1],
      
                [0]
      [false] = [3],
      
                       [-& -&]     [2 2]     [0]
      [cons](x0, x1) = [0  0 ]x0 + [2 0]x1 + [2],
      
               [0 ]
      [true] = [-&],
      
                    [0 0]     [0 ]
      [empty](x0) = [3 0]x0 + [-&],
      
              [0]
      [nil] = [0]
     orientation:
      rev2#(x,cons(y,l)) = [3 2]l + [0 0]x + [1 1]y + [3] >= [0 1]l + [0 0]y + [0] = rev2#(y,l)
      
      rev2#(x,cons(y,l)) = [3 2]l + [0 0]x + [1 1]y + [3] >= [2 2]l + [0 0]x + [2] = rev#(cons(x,rev2(y,l)))
      
      rev#(cons(x,l)) = [2 2]l + [0 0]x + [2] >= [0 1]l + [0 0]x + [0] = rev2#(x,l)
      
                     [0]    [0 ]         
      empty(nil()) = [3] >= [-&] = true()
      
                         [2 2]    [0 0]    [2]    [0]          
      empty(cons(x,l)) = [5 5]l + [0 0]x + [3] >= [3] = false()
      
                        [2 2]    [0 0]    [3]         
      head(cons(x,l)) = [4 4]l + [0 0]x + [2] >= x = x
      
                    [0]    [0]        
      tail(nil()) = [0] >= [0] = nil()
      
                        [2 2]    [-& -&]    [0]         
      tail(cons(x,l)) = [2 0]l + [0  0 ]x + [2] >= l = l
      
                   [1]    [0]        
      rev(nil()) = [2] >= [0] = nil()
      
                       [2 2]    [1]    [2 2]    [0]                            
      rev(cons(x,l)) = [2 2]l + [2] >= [2 2]l + [2] = cons(rev1(x,l),rev2(x,l))
      
                  [3 2]    [0 0]    [3]    [3 2]        [3]                   
      last(x,l) = [3 0]l + [0 0]x + [0] >= [3 0]l + x + [0] = if(empty(l),x,l)
      
                       [3 2]        [3]         
      if(true(),x,l) = [3 0]l + x + [0] >= x = x
      
                        [3 2]        [3]    [3 2]    [3]                        
      if(false(),x,l) = [3 0]l + x + [3] >= [3 0]l + [3] = last(head(l),tail(l))
      
                      [0]    [0]        
      rev2(x,nil()) = [0] >= [0] = nil()
      
                          [2 2]    [0 0]    [2]    [2 2]    [1]                         
      rev2(x,cons(y,l)) = [2 2]l + [0 0]y + [2] >= [2 2]l + [2] = rev(cons(x,rev2(y,l)))
     problem:
      DPs:
       rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
       rev#(cons(x,l)) -> rev2#(x,l)
      TRS:
       empty(nil()) -> true()
       empty(cons(x,l)) -> false()
       head(cons(x,l)) -> x
       tail(nil()) -> nil()
       tail(cons(x,l)) -> l
       rev(nil()) -> nil()
       rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
       last(x,l) -> if(empty(l),x,l)
       if(true(),x,l) -> x
       if(false(),x,l) -> last(head(l),tail(l))
       rev2(x,nil()) -> nil()
       rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
     Arctic Interpretation Processor:
      dimension: 2
      interpretation:
       [rev2#](x0, x1) = [0 1]x1,
       
       [rev#](x0) = [-& 0 ]x0 + [0],
       
                          [-& 0 ]          [2 2]     [0]
       [if](x0, x1, x2) = [0  0 ]x0 + x1 + [0 2]x2 + [0],
       
                        [0  2 ]     [2 2]     [1]
       [last](x0, x1) = [-& 0 ]x0 + [1 2]x1 + [3],
       
                        [0  0 ]     [1 ]
       [rev2](x0, x1) = [-& 0 ]x1 + [-&],
       
                        [-& -&]     [0]
       [rev1](x0, x1) = [0  -&]x1 + [0],
       
                   [-& 0 ]     [0]
       [rev](x0) = [-& 0 ]x0 + [0],
       
                    [-& 0 ]     [0]
       [tail](x0) = [-& 0 ]x0 + [1],
       
                    [0  -&]     [0 ]
       [head](x0) = [0  -&]x0 + [-&],
       
                 [1]
       [false] = [3],
       
                        [0  0 ]     [0 0]     [-&]
       [cons](x0, x1) = [-& -&]x0 + [0 1]x1 + [1 ],
       
                [1]
       [true] = [0],
       
                     [0 1]     [2]
       [empty](x0) = [1 2]x0 + [0],
       
               [0]
       [nil] = [1]
      orientation:
       rev2#(x,cons(y,l)) = [1 2]l + [0 0]y + [2] >= [0 1]l + [1] = rev#(cons(x,rev2(y,l)))
       
       rev#(cons(x,l)) = [0 1]l + [1] >= [0 1]l = rev2#(x,l)
       
                      [2]    [1]         
       empty(nil()) = [3] >= [0] = true()
       
                          [1 2]    [0 0]    [2]    [1]          
       empty(cons(x,l)) = [2 3]l + [1 1]x + [3] >= [3] = false()
       
                         [0 0]    [0 0]    [0 ]         
       head(cons(x,l)) = [0 0]l + [0 0]x + [-&] >= x = x
       
                     [1]    [0]        
       tail(nil()) = [1] >= [1] = nil()
       
                         [0 1]    [1]         
       tail(cons(x,l)) = [0 1]l + [1] >= l = l
       
                    [1]    [0]        
       rev(nil()) = [1] >= [1] = nil()
       
                        [0 1]    [1]    [0 0]    [1]                            
       rev(cons(x,l)) = [0 1]l + [1] >= [0 1]l + [1] = cons(rev1(x,l),rev2(x,l))
       
                   [2 2]    [0  2 ]    [1]    [2 2]        [0]                   
       last(x,l) = [1 2]l + [-& 0 ]x + [3] >= [1 2]l + x + [2] = if(empty(l),x,l)
       
                        [2 2]        [0]         
       if(true(),x,l) = [0 2]l + x + [1] >= x = x
       
                         [2 2]        [3]    [2 2]    [3]                        
       if(false(),x,l) = [0 2]l + x + [3] >= [0 2]l + [3] = last(head(l),tail(l))
       
                       [1]    [0]        
       rev2(x,nil()) = [1] >= [1] = nil()
       
                           [0 1]    [0  0 ]    [1]    [0 1]    [1]                         
       rev2(x,cons(y,l)) = [0 1]l + [-& -&]y + [1] >= [0 1]l + [1] = rev(cons(x,rev2(y,l)))
      problem:
       DPs:
        rev#(cons(x,l)) -> rev2#(x,l)
       TRS:
        empty(nil()) -> true()
        empty(cons(x,l)) -> false()
        head(cons(x,l)) -> x
        tail(nil()) -> nil()
        tail(cons(x,l)) -> l
        rev(nil()) -> nil()
        rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
        last(x,l) -> if(empty(l),x,l)
        if(true(),x,l) -> x
        if(false(),x,l) -> last(head(l),tail(l))
        rev2(x,nil()) -> nil()
        rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 5/1
       
    
    DPs:
     if#(false(),x,l) -> last#(head(l),tail(l))
     last#(x,l) -> if#(empty(l),x,l)
    TRS:
     empty(nil()) -> true()
     empty(cons(x,l)) -> false()
     head(cons(x,l)) -> x
     tail(nil()) -> nil()
     tail(cons(x,l)) -> l
     rev(nil()) -> nil()
     rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
     last(x,l) -> if(empty(l),x,l)
     if(true(),x,l) -> x
     if(false(),x,l) -> last(head(l),tail(l))
     rev2(x,nil()) -> nil()
     rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
    Open