YES

Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
Call external tool:
ttt2 - trs 30
Input:
  ?1(pair(z1, z2), x, y, rest) -> cons(z1, cons(z2, rest))
  cons(x, cons(y, rest)) -> ?1(orient(x, y), x, y, rest)
  cons(x, cons(x, rest)) -> cons(x, rest)
  ?2(pair(z1, z2), x, y) -> pair(s(z1), s(z2))
  orient(s(x), s(y)) -> ?2(orient(x, y), x, y)
  orient(s(x), 0) -> pair(0, s(x))

 DP Processor:
  DPs:
   ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
   ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
   cons#(x,cons(y,rest)) -> orient#(x,y)
   cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
   orient#(s(x),s(y)) -> orient#(x,y)
   orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
  TRS:
   ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
   cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
   cons(x,cons(x,rest)) -> cons(x,rest)
   ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
   orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
   orient(s(x),0()) -> pair(0(),s(x))
  TDG Processor:
   DPs:
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
    cons#(x,cons(y,rest)) -> orient#(x,y)
    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
    orient#(s(x),s(y)) -> orient#(x,y)
    orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
   TRS:
    ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
    cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
    cons(x,cons(x,rest)) -> cons(x,rest)
    ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
    orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
    orient(s(x),0()) -> pair(0(),s(x))
   graph:
    orient#(s(x),s(y)) -> orient#(x,y) ->
    orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
    orient#(s(x),s(y)) -> orient#(x,y) ->
    orient#(s(x),s(y)) -> orient#(x,y)
    cons#(x,cons(y,rest)) -> orient#(x,y) ->
    orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
    cons#(x,cons(y,rest)) -> orient#(x,y) ->
    orient#(s(x),s(y)) -> orient#(x,y)
    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ->
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ->
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) ->
    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) ->
    cons#(x,cons(y,rest)) -> orient#(x,y)
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) ->
    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) -> cons#(x,cons(y,rest)) -> orient#(x,y)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 10/36
    DPs:
     cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
     ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
     ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
    TRS:
     ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
     cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
     cons(x,cons(x,rest)) -> cons(x,rest)
     ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
     orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
     orient(s(x),0()) -> pair(0(),s(x))
    Matrix Interpretation Processor: dim=2
     
     usable rules:
      ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
      cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
      cons(x,cons(x,rest)) -> cons(x,rest)
      ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
      orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
      orient(s(x),0()) -> pair(0(),s(x))
     interpretation:
                         [0]
      [?2](x0, x1, x2) = [0],
      
      [cons#](x0, x1) = [0 2]x1,
      
                             [0 0]     [0]
      [?1](x0, x1, x2, x3) = [0 1]x3 + [2],
      
                         [0 0]     [2]
      [orient](x0, x1) = [0 3]x1 + [0],
      
                [0]
      [s](x0) = [0],
      
                       [0 0]  
      [pair](x0, x1) = [1 1]x0,
      
      [?1#](x0, x1, x2, x3) = [0 2]x3 + [2],
      
            [1]
      [0] = [1],
      
                       [0 0]     [0]
      [cons](x0, x1) = [0 1]x1 + [1]
     orientation:
      cons#(x,cons(y,rest)) = [0 2]rest + [2] >= [0 2]rest + [2] = ?1#(orient(x,y),x,y,rest)
      
      ?1#(pair(z1,z2),x,y,rest) = [0 2]rest + [2] >= [0 2]rest = cons#(z2,rest)
      
      ?1#(pair(z1,z2),x,y,rest) = [0 2]rest + [2] >= [0 2]rest + [2] = cons#(z1,cons(z2,rest))
      
                                 [0 0]       [0]    [0 0]       [0]                         
      ?1(pair(z1,z2),x,y,rest) = [0 1]rest + [2] >= [0 1]rest + [2] = cons(z1,cons(z2,rest))
      
                             [0 0]       [0]    [0 0]       [0]                           
      cons(x,cons(y,rest)) = [0 1]rest + [2] >= [0 1]rest + [2] = ?1(orient(x,y),x,y,rest)
      
                             [0 0]       [0]    [0 0]       [0]               
      cons(x,cons(x,rest)) = [0 1]rest + [2] >= [0 1]rest + [1] = cons(x,rest)
      
                            [0]    [0]                    
      ?2(pair(z1,z2),x,y) = [0] >= [0] = pair(s(z1),s(z2))
      
                          [2]    [0]                      
      orient(s(x),s(y)) = [0] >= [0] = ?2(orient(x,y),x,y)
      
                         [2]    [0]                 
      orient(s(x),0()) = [3] >= [2] = pair(0(),s(x))
     problem:
      DPs:
       cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
       ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
      TRS:
       ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
       cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
       cons(x,cons(x,rest)) -> cons(x,rest)
       ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
       orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
       orient(s(x),0()) -> pair(0(),s(x))
     Restore Modifier:
      DPs:
       cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
       ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
      TRS:
       ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
       cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
       cons(x,cons(x,rest)) -> cons(x,rest)
       ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
       orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
       orient(s(x),0()) -> pair(0(),s(x))
      EDG Processor:
       DPs:
        cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
        ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
       TRS:
        ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
        cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
        cons(x,cons(x,rest)) -> cons(x,rest)
        ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
        orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
        orient(s(x),0()) -> pair(0(),s(x))
       graph:
        cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ->
        ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
        ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) ->
        cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
       Matrix Interpretation Processor: dim=2
        
        usable rules:
         ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
         orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
         orient(s(x),0()) -> pair(0(),s(x))
        interpretation:
                            [0 0]     [1 1]  
         [?2](x0, x1, x2) = [0 3]x0 + [0 0]x1,
         
         [cons#](x0, x1) = [0 2]x0,
         
                                [0 0]     [0 0]     [0]
         [?1](x0, x1, x2, x3) = [0 2]x0 + [1 0]x1 + [1],
         
                            [2 0]     [2 0]  
         [orient](x0, x1) = [0 1]x0 + [0 0]x1,
         
                   [1 1]     [0]
         [s](x0) = [0 3]x0 + [1],
         
                          [0 0]     [0]
         [pair](x0, x1) = [0 1]x0 + [1],
         
         [?1#](x0, x1, x2, x3) = [0 2]x0,
         
               [1]
         [0] = [0],
         
                          [0]
         [cons](x0, x1) = [0]
        orientation:
         cons#(x,cons(y,rest)) = [0 2]x >= [0 2]x = ?1#(orient(x,y),x,y,rest)
         
         ?1#(pair(z1,z2),x,y,rest) = [0 2]z1 + [2] >= [0 2]z1 = cons#(z1,cons(z2,rest))
         
                                    [0 0]    [0 0]     [0]    [0]                         
         ?1(pair(z1,z2),x,y,rest) = [1 0]x + [0 2]z1 + [3] >= [0] = cons(z1,cons(z2,rest))
         
                                [0]    [0 0]    [0]                           
         cons(x,cons(y,rest)) = [0] >= [1 2]x + [1] = ?1(orient(x,y),x,y,rest)
         
                                [0]    [0]               
         cons(x,cons(x,rest)) = [0] >= [0] = cons(x,rest)
         
                               [1 1]    [0 0]     [0]    [0 0]     [0]                    
         ?2(pair(z1,z2),x,y) = [0 0]x + [0 3]z1 + [3] >= [0 3]z1 + [2] = pair(s(z1),s(z2))
         
                             [2 2]    [2 2]    [0]    [1 1]                       
         orient(s(x),s(y)) = [0 3]x + [0 0]y + [1] >= [0 3]x = ?2(orient(x,y),x,y)
         
                            [2 2]    [2]    [0]                 
         orient(s(x),0()) = [0 3]x + [1] >= [1] = pair(0(),s(x))
        problem:
         DPs:
          cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
         TRS:
          ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
          cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
          cons(x,cons(x,rest)) -> cons(x,rest)
          ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
          orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
          orient(s(x),0()) -> pair(0(),s(x))
        Restore Modifier:
         DPs:
          cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
         TRS:
          ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
          cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
          cons(x,cons(x,rest)) -> cons(x,rest)
          ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
          orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
          orient(s(x),0()) -> pair(0(),s(x))
         EDG Processor:
          DPs:
           cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
          TRS:
           ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
           cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
           cons(x,cons(x,rest)) -> cons(x,rest)
           ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
           orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
           orient(s(x),0()) -> pair(0(),s(x))
          graph:
           
          Qed
    
    DPs:
     orient#(s(x),s(y)) -> orient#(x,y)
    TRS:
     ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
     cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
     cons(x,cons(x,rest)) -> cons(x,rest)
     ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
     orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
     orient(s(x),0()) -> pair(0(),s(x))
    Subterm Criterion Processor:
     simple projection:
      pi(orient#) = 0
     problem:
      DPs:
       
      TRS:
       ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
       cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
       cons(x,cons(x,rest)) -> cons(x,rest)
       ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
       orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
       orient(s(x),0()) -> pair(0(),s(x))
     Qed