YES

Problem:
 0(#()) -> #()
 +(#(),x) -> x
 +(x,#()) -> x
 +(0(x),0(y)) -> 0(+(x,y))
 +(0(x),1(y)) -> 1(+(x,y))
 +(1(x),0(y)) -> 1(+(x,y))
 +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
 +(+(x,y),z) -> +(x,+(y,z))
 -(#(),x) -> #()
 -(x,#()) -> x
 -(0(x),0(y)) -> 0(-(x,y))
 -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
 -(1(x),0(y)) -> 1(-(x,y))
 -(1(x),1(y)) -> 0(-(x,y))
 not(true()) -> false()
 not(false()) -> true()
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 ge(0(x),0(y)) -> ge(x,y)
 ge(0(x),1(y)) -> not(ge(y,x))
 ge(1(x),0(y)) -> ge(x,y)
 ge(1(x),1(y)) -> ge(x,y)
 ge(x,#()) -> true()
 ge(#(),0(x)) -> ge(#(),x)
 ge(#(),1(x)) -> false()
 log(x) -> -(log'(x),1(#()))
 log'(#()) -> #()
 log'(1(x)) -> +(log'(x),1(#()))
 log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [log'](x0) = x0 + 7,
   
   [log](x0) = x0 + 7,
   
   [ge](x0, x1) = x0 + x1,
   
   [if](x0, x1, x2) = 3x0 + x1 + x2,
   
   [false] = 0,
   
   [not](x0) = 4x0,
   
   [true] = 0,
   
   [-](x0, x1) = x0 + 2x1,
   
   [1](x0) = 4x0,
   
   [+](x0, x1) = x0 + x1,
   
   [0](x0) = 4x0,
   
   [#] = 0
  orientation:
   0(#()) = 0 >= 0 = #()
   
   +(#(),x) = x >= x = x
   
   +(x,#()) = x >= x = x
   
   +(0(x),0(y)) = 4x + 4y >= 4x + 4y = 0(+(x,y))
   
   +(0(x),1(y)) = 4x + 4y >= 4x + 4y = 1(+(x,y))
   
   +(1(x),0(y)) = 4x + 4y >= 4x + 4y = 1(+(x,y))
   
   +(1(x),1(y)) = 4x + 4y >= 4x + 4y = 0(+(+(x,y),1(#())))
   
   +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
   
   -(#(),x) = 2x >= 0 = #()
   
   -(x,#()) = x >= x = x
   
   -(0(x),0(y)) = 4x + 8y >= 4x + 8y = 0(-(x,y))
   
   -(0(x),1(y)) = 4x + 8y >= 4x + 8y = 1(-(-(x,y),1(#())))
   
   -(1(x),0(y)) = 4x + 8y >= 4x + 8y = 1(-(x,y))
   
   -(1(x),1(y)) = 4x + 8y >= 4x + 8y = 0(-(x,y))
   
   not(true()) = 0 >= 0 = false()
   
   not(false()) = 0 >= 0 = true()
   
   if(true(),x,y) = x + y >= x = x
   
   if(false(),x,y) = x + y >= y = y
   
   ge(0(x),0(y)) = 4x + 4y >= x + y = ge(x,y)
   
   ge(0(x),1(y)) = 4x + 4y >= 4x + 4y = not(ge(y,x))
   
   ge(1(x),0(y)) = 4x + 4y >= x + y = ge(x,y)
   
   ge(1(x),1(y)) = 4x + 4y >= x + y = ge(x,y)
   
   ge(x,#()) = x >= 0 = true()
   
   ge(#(),0(x)) = 4x >= x = ge(#(),x)
   
   ge(#(),1(x)) = 4x >= 0 = false()
   
   log(x) = x + 7 >= x + 7 = -(log'(x),1(#()))
   
   log'(#()) = 7 >= 0 = #()
   
   log'(1(x)) = 4x + 7 >= x + 7 = +(log'(x),1(#()))
   
   log'(0(x)) = 4x + 7 >= 4x + 7 = if(ge(x,1(#())),+(log'(x),1(#())),#())
  problem:
   0(#()) -> #()
   +(#(),x) -> x
   +(x,#()) -> x
   +(0(x),0(y)) -> 0(+(x,y))
   +(0(x),1(y)) -> 1(+(x,y))
   +(1(x),0(y)) -> 1(+(x,y))
   +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
   +(+(x,y),z) -> +(x,+(y,z))
   -(#(),x) -> #()
   -(x,#()) -> x
   -(0(x),0(y)) -> 0(-(x,y))
   -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
   -(1(x),0(y)) -> 1(-(x,y))
   -(1(x),1(y)) -> 0(-(x,y))
   not(true()) -> false()
   not(false()) -> true()
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   ge(0(x),0(y)) -> ge(x,y)
   ge(0(x),1(y)) -> not(ge(y,x))
   ge(1(x),0(y)) -> ge(x,y)
   ge(1(x),1(y)) -> ge(x,y)
   ge(x,#()) -> true()
   ge(#(),0(x)) -> ge(#(),x)
   ge(#(),1(x)) -> false()
   log(x) -> -(log'(x),1(#()))
   log'(1(x)) -> +(log'(x),1(#()))
   log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [log'](x0) = x0,
    
    [log](x0) = 4x0 + 4,
    
    [ge](x0, x1) = x0 + 2x1,
    
    [if](x0, x1, x2) = 2x0 + x1 + 4x2,
    
    [false] = 0,
    
    [not](x0) = x0,
    
    [true] = 0,
    
    [-](x0, x1) = x0 + 4x1,
    
    [1](x0) = 3x0,
    
    [+](x0, x1) = x0 + x1,
    
    [0](x0) = 3x0,
    
    [#] = 0
   orientation:
    0(#()) = 0 >= 0 = #()
    
    +(#(),x) = x >= x = x
    
    +(x,#()) = x >= x = x
    
    +(0(x),0(y)) = 3x + 3y >= 3x + 3y = 0(+(x,y))
    
    +(0(x),1(y)) = 3x + 3y >= 3x + 3y = 1(+(x,y))
    
    +(1(x),0(y)) = 3x + 3y >= 3x + 3y = 1(+(x,y))
    
    +(1(x),1(y)) = 3x + 3y >= 3x + 3y = 0(+(+(x,y),1(#())))
    
    +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
    
    -(#(),x) = 4x >= 0 = #()
    
    -(x,#()) = x >= x = x
    
    -(0(x),0(y)) = 3x + 12y >= 3x + 12y = 0(-(x,y))
    
    -(0(x),1(y)) = 3x + 12y >= 3x + 12y = 1(-(-(x,y),1(#())))
    
    -(1(x),0(y)) = 3x + 12y >= 3x + 12y = 1(-(x,y))
    
    -(1(x),1(y)) = 3x + 12y >= 3x + 12y = 0(-(x,y))
    
    not(true()) = 0 >= 0 = false()
    
    not(false()) = 0 >= 0 = true()
    
    if(true(),x,y) = x + 4y >= x = x
    
    if(false(),x,y) = x + 4y >= y = y
    
    ge(0(x),0(y)) = 3x + 6y >= x + 2y = ge(x,y)
    
    ge(0(x),1(y)) = 3x + 6y >= 2x + y = not(ge(y,x))
    
    ge(1(x),0(y)) = 3x + 6y >= x + 2y = ge(x,y)
    
    ge(1(x),1(y)) = 3x + 6y >= x + 2y = ge(x,y)
    
    ge(x,#()) = x >= 0 = true()
    
    ge(#(),0(x)) = 6x >= 2x = ge(#(),x)
    
    ge(#(),1(x)) = 6x >= 0 = false()
    
    log(x) = 4x + 4 >= x = -(log'(x),1(#()))
    
    log'(1(x)) = 3x >= x = +(log'(x),1(#()))
    
    log'(0(x)) = 3x >= 3x = if(ge(x,1(#())),+(log'(x),1(#())),#())
   problem:
    0(#()) -> #()
    +(#(),x) -> x
    +(x,#()) -> x
    +(0(x),0(y)) -> 0(+(x,y))
    +(0(x),1(y)) -> 1(+(x,y))
    +(1(x),0(y)) -> 1(+(x,y))
    +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
    +(+(x,y),z) -> +(x,+(y,z))
    -(#(),x) -> #()
    -(x,#()) -> x
    -(0(x),0(y)) -> 0(-(x,y))
    -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
    -(1(x),0(y)) -> 1(-(x,y))
    -(1(x),1(y)) -> 0(-(x,y))
    not(true()) -> false()
    not(false()) -> true()
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    ge(0(x),0(y)) -> ge(x,y)
    ge(0(x),1(y)) -> not(ge(y,x))
    ge(1(x),0(y)) -> ge(x,y)
    ge(1(x),1(y)) -> ge(x,y)
    ge(x,#()) -> true()
    ge(#(),0(x)) -> ge(#(),x)
    ge(#(),1(x)) -> false()
    log'(1(x)) -> +(log'(x),1(#()))
    log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
   Matrix Interpretation Processor: dim=3
    
    interpretation:
                  [1 1 0]     [0]
     [log'](x0) = [1 1 0]x0 + [0]
                  [0 1 0]     [1],
     
                    [1 0 0]     [1 0 0]  
     [ge](x0, x1) = [1 0 0]x0 + [0 0 0]x1
                    [0 0 0]     [1 0 0]  ,
     
                        [1 0 0]            
     [if](x0, x1, x2) = [0 0 0]x0 + x1 + x2
                        [0 0 0]            ,
     
               [0]
     [false] = [0]
               [0],
     
                 [1 0 0]  
     [not](x0) = [0 0 0]x0
                 [0 0 0]  ,
     
              [0]
     [true] = [0]
              [0],
     
                        [1 0 0]  
     [-](x0, x1) = x0 + [0 1 0]x1
                        [1 0 0]  ,
     
               [1 0 0]     [0]
     [1](x0) = [1 1 0]x0 + [1]
               [0 0 0]     [0],
     
                          
     [+](x0, x1) = x0 + x1
                          ,
     
               [1 0 0]     [0]
     [0](x0) = [1 1 0]x0 + [1]
               [0 0 0]     [0],
     
           [0]
     [#] = [0]
           [0]
    orientation:
              [0]    [0]      
     0(#()) = [1] >= [0] = #()
              [0]    [0]      
     
                          
     +(#(),x) = x >= x = x
                          
     
                          
     +(x,#()) = x >= x = x
                          
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]            
     +(0(x),0(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [1] = 0(+(x,y))
                    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]            
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]            
     +(0(x),1(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [1] = 1(+(x,y))
                    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]            
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]            
     +(1(x),0(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [1] = 1(+(x,y))
                    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]            
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]                      
     +(1(x),1(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [2] = 0(+(+(x,y),1(#())))
                    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                      
     
                                                       
     +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
                                                       
     
                [1 0 0]     [0]      
     -(#(),x) = [0 1 0]x >= [0] = #()
                [1 0 0]     [0]      
     
                          
     -(x,#()) = x >= x = x
                          
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]            
     -(0(x),0(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [1] = 0(-(x,y))
                    [0 0 0]    [1 0 0]    [0]    [0 0 0]    [0 0 0]    [0]            
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]                      
     -(0(x),1(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [2] = 1(-(-(x,y),1(#())))
                    [0 0 0]    [1 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                      
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]            
     -(1(x),0(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [1] = 1(-(x,y))
                    [0 0 0]    [1 0 0]    [0]    [0 0 0]    [0 0 0]    [0]            
     
                    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [0]            
     -(1(x),1(y)) = [1 1 0]x + [1 1 0]y + [2] >= [1 1 0]x + [1 1 0]y + [1] = 0(-(x,y))
                    [0 0 0]    [1 0 0]    [0]    [0 0 0]    [0 0 0]    [0]            
     
                   [0]    [0]          
     not(true()) = [0] >= [0] = false()
                   [0]    [0]          
     
                    [0]    [0]         
     not(false()) = [0] >= [0] = true()
                    [0]    [0]         
     
                                    
     if(true(),x,y) = x + y >= x = x
                                    
     
                                     
     if(false(),x,y) = x + y >= y = y
                                     
     
                     [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]           
     ge(0(x),0(y)) = [1 0 0]x + [0 0 0]y >= [1 0 0]x + [0 0 0]y = ge(x,y)
                     [0 0 0]    [1 0 0]     [0 0 0]    [1 0 0]           
     
                     [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]                
     ge(0(x),1(y)) = [1 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = not(ge(y,x))
                     [0 0 0]    [1 0 0]     [0 0 0]    [0 0 0]                
     
                     [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]           
     ge(1(x),0(y)) = [1 0 0]x + [0 0 0]y >= [1 0 0]x + [0 0 0]y = ge(x,y)
                     [0 0 0]    [1 0 0]     [0 0 0]    [1 0 0]           
     
                     [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]           
     ge(1(x),1(y)) = [1 0 0]x + [0 0 0]y >= [1 0 0]x + [0 0 0]y = ge(x,y)
                     [0 0 0]    [1 0 0]     [0 0 0]    [1 0 0]           
     
                 [1 0 0]     [0]         
     ge(x,#()) = [1 0 0]x >= [0] = true()
                 [0 0 0]     [0]         
     
                    [1 0 0]     [1 0 0]             
     ge(#(),0(x)) = [0 0 0]x >= [0 0 0]x = ge(#(),x)
                    [1 0 0]     [1 0 0]             
     
                    [1 0 0]     [0]          
     ge(#(),1(x)) = [0 0 0]x >= [0] = false()
                    [1 0 0]     [0]          
     
                  [2 1 0]    [1]    [1 1 0]    [0]                    
     log'(1(x)) = [2 1 0]x + [1] >= [1 1 0]x + [1] = +(log'(x),1(#()))
                  [1 1 0]    [2]    [0 1 0]    [1]                    
     
                  [2 1 0]    [1]    [2 1 0]    [0]                                         
     log'(0(x)) = [2 1 0]x + [1] >= [1 1 0]x + [1] = if(ge(x,1(#())),+(log'(x),1(#())),#())
                  [1 1 0]    [2]    [0 1 0]    [1]                                         
    problem:
     0(#()) -> #()
     +(#(),x) -> x
     +(x,#()) -> x
     +(0(x),0(y)) -> 0(+(x,y))
     +(0(x),1(y)) -> 1(+(x,y))
     +(1(x),0(y)) -> 1(+(x,y))
     +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
     +(+(x,y),z) -> +(x,+(y,z))
     -(#(),x) -> #()
     -(x,#()) -> x
     -(0(x),0(y)) -> 0(-(x,y))
     -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
     -(1(x),0(y)) -> 1(-(x,y))
     -(1(x),1(y)) -> 0(-(x,y))
     not(true()) -> false()
     not(false()) -> true()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     ge(0(x),0(y)) -> ge(x,y)
     ge(0(x),1(y)) -> not(ge(y,x))
     ge(1(x),0(y)) -> ge(x,y)
     ge(1(x),1(y)) -> ge(x,y)
     ge(x,#()) -> true()
     ge(#(),0(x)) -> ge(#(),x)
     ge(#(),1(x)) -> false()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [ge](x0, x1) = x0 + x1,
      
      [if](x0, x1, x2) = x0 + x1 + x2,
      
      [false] = 0,
      
      [not](x0) = x0 + 2,
      
      [true] = 0,
      
      [-](x0, x1) = x0 + x1,
      
      [1](x0) = x0 + 1,
      
      [+](x0, x1) = x0 + x1,
      
      [0](x0) = x0 + 1,
      
      [#] = 0
     orientation:
      0(#()) = 1 >= 0 = #()
      
      +(#(),x) = x >= x = x
      
      +(x,#()) = x >= x = x
      
      +(0(x),0(y)) = x + y + 2 >= x + y + 1 = 0(+(x,y))
      
      +(0(x),1(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),0(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),1(y)) = x + y + 2 >= x + y + 2 = 0(+(+(x,y),1(#())))
      
      +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
      
      -(#(),x) = x >= 0 = #()
      
      -(x,#()) = x >= x = x
      
      -(0(x),0(y)) = x + y + 2 >= x + y + 1 = 0(-(x,y))
      
      -(0(x),1(y)) = x + y + 2 >= x + y + 2 = 1(-(-(x,y),1(#())))
      
      -(1(x),0(y)) = x + y + 2 >= x + y + 1 = 1(-(x,y))
      
      -(1(x),1(y)) = x + y + 2 >= x + y + 1 = 0(-(x,y))
      
      not(true()) = 2 >= 0 = false()
      
      not(false()) = 2 >= 0 = true()
      
      if(true(),x,y) = x + y >= x = x
      
      if(false(),x,y) = x + y >= y = y
      
      ge(0(x),0(y)) = x + y + 2 >= x + y = ge(x,y)
      
      ge(0(x),1(y)) = x + y + 2 >= x + y + 2 = not(ge(y,x))
      
      ge(1(x),0(y)) = x + y + 2 >= x + y = ge(x,y)
      
      ge(1(x),1(y)) = x + y + 2 >= x + y = ge(x,y)
      
      ge(x,#()) = x >= 0 = true()
      
      ge(#(),0(x)) = x + 1 >= x = ge(#(),x)
      
      ge(#(),1(x)) = x + 1 >= 0 = false()
     problem:
      +(#(),x) -> x
      +(x,#()) -> x
      +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
      +(+(x,y),z) -> +(x,+(y,z))
      -(#(),x) -> #()
      -(x,#()) -> x
      -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      ge(0(x),1(y)) -> not(ge(y,x))
      ge(x,#()) -> true()
     Matrix Interpretation Processor: dim=3
      
      interpretation:
                      [1 0 0]     [1 0 0]  
       [ge](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                      [0 0 0]     [0 0 0]  ,
       
                          [1 0 0]               [1]
       [if](x0, x1, x2) = [0 0 0]x0 + x1 + x2 + [0]
                          [0 0 0]               [0],
       
                 [0]
       [false] = [0]
                 [0],
       
                   [1 0 0]  
       [not](x0) = [0 0 0]x0
                   [0 0 0]  ,
       
                [0]
       [true] = [0]
                [0],
       
                          [1 0 0]  
       [-](x0, x1) = x0 + [0 0 0]x1
                          [0 0 0]  ,
       
                 [1 0 1]  
       [1](x0) = [0 0 0]x0
                 [0 0 0]  ,
       
                            
       [+](x0, x1) = x0 + x1
                            ,
       
                 [1 0 1]  
       [0](x0) = [0 0 0]x0
                 [0 0 0]  ,
       
             [0]
       [#] = [0]
             [0]
      orientation:
                            
       +(#(),x) = x >= x = x
                            
       
                            
       +(x,#()) = x >= x = x
                            
       
                      [1 0 1]    [1 0 1]     [1 0 1]    [1 0 1]                       
       +(1(x),1(y)) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = 0(+(+(x,y),1(#())))
                      [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]                       
       
                                                         
       +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
                                                         
       
                  [1 0 0]     [0]      
       -(#(),x) = [0 0 0]x >= [0] = #()
                  [0 0 0]     [0]      
       
                            
       -(x,#()) = x >= x = x
                            
       
                      [1 0 1]    [1 0 1]     [1 0 1]    [1 0 0]                       
       -(0(x),1(y)) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = 1(-(-(x,y),1(#())))
                      [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]                       
       
                                [1]         
       if(true(),x,y) = x + y + [0] >= x = x
                                [0]         
       
                                 [1]         
       if(false(),x,y) = x + y + [0] >= y = y
                                 [0]         
       
                       [1 0 1]    [1 0 1]     [1 0 0]    [1 0 0]                
       ge(0(x),1(y)) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = not(ge(y,x))
                       [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]                
       
                   [1 0 0]     [0]         
       ge(x,#()) = [0 0 0]x >= [0] = true()
                   [0 0 0]     [0]         
      problem:
       +(#(),x) -> x
       +(x,#()) -> x
       +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
       +(+(x,y),z) -> +(x,+(y,z))
       -(#(),x) -> #()
       -(x,#()) -> x
       -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
       ge(0(x),1(y)) -> not(ge(y,x))
       ge(x,#()) -> true()
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                       [1 0 0]     [1 0 0]     [1]
        [ge](x0, x1) = [0 0 0]x0 + [1 0 0]x1 + [0]
                       [0 0 0]     [0 0 0]     [0],
        
                    [1 0 0]  
        [not](x0) = [0 0 0]x0
                    [0 0 0]  ,
        
                 [0]
        [true] = [0]
                 [0],
        
                           [1 0 0]  
        [-](x0, x1) = x0 + [1 0 0]x1
                           [1 0 0]  ,
        
                  [1 0 0]  
        [1](x0) = [0 0 1]x0
                  [0 0 0]  ,
        
                             
        [+](x0, x1) = x0 + x1
                             ,
        
                  [1 0 0]  
        [0](x0) = [0 0 1]x0
                  [0 0 0]  ,
        
              [0]
        [#] = [0]
              [1]
       orientation:
                       [0]         
        +(#(),x) = x + [0] >= x = x
                       [1]         
        
                       [0]         
        +(x,#()) = x + [0] >= x = x
                       [1]         
        
                       [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]                       
        +(1(x),1(y)) = [0 0 1]x + [0 0 1]y >= [0 0 1]x + [0 0 1]y = 0(+(+(x,y),1(#())))
                       [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]                       
        
                                                          
        +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
                                                          
        
                   [1 0 0]    [0]    [0]      
        -(#(),x) = [1 0 0]x + [0] >= [0] = #()
                   [1 0 0]    [1]    [1]      
        
                             
        -(x,#()) = x >= x = x
                             
        
                       [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]                       
        -(0(x),1(y)) = [0 0 1]x + [1 0 0]y >= [0 0 1]x + [1 0 0]y = 1(-(-(x,y),1(#())))
                       [0 0 0]    [1 0 0]     [0 0 0]    [0 0 0]                       
        
                        [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1]               
        ge(0(x),1(y)) = [0 0 0]x + [1 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = not(ge(y,x))
                        [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]               
        
                    [1 0 0]    [1]    [0]         
        ge(x,#()) = [0 0 0]x + [0] >= [0] = true()
                    [0 0 0]    [0]    [0]         
       problem:
        +(#(),x) -> x
        +(x,#()) -> x
        +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
        +(+(x,y),z) -> +(x,+(y,z))
        -(#(),x) -> #()
        -(x,#()) -> x
        -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
        ge(0(x),1(y)) -> not(ge(y,x))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [ge](x0, x1) = 2x0 + 2x1 + 1,
         
         [not](x0) = x0 + 7,
         
         [-](x0, x1) = x0 + 4x1,
         
         [1](x0) = x0 + 4,
         
         [+](x0, x1) = x0 + x1,
         
         [0](x0) = x0 + 4,
         
         [#] = 0
        orientation:
         +(#(),x) = x >= x = x
         
         +(x,#()) = x >= x = x
         
         +(1(x),1(y)) = x + y + 8 >= x + y + 8 = 0(+(+(x,y),1(#())))
         
         +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
         
         -(#(),x) = 4x >= 0 = #()
         
         -(x,#()) = x >= x = x
         
         -(0(x),1(y)) = x + 4y + 20 >= x + 4y + 20 = 1(-(-(x,y),1(#())))
         
         ge(0(x),1(y)) = 2x + 2y + 17 >= 2x + 2y + 8 = not(ge(y,x))
        problem:
         +(#(),x) -> x
         +(x,#()) -> x
         +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
         +(+(x,y),z) -> +(x,+(y,z))
         -(#(),x) -> #()
         -(x,#()) -> x
         -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
        WPO Processor:
         algebra: Sum
         weight function:
          w0 = 0
          w(1) = w(0) = 2
          w(-) = w(+) = w(#) = 0
         status function:
          st(-) = [0, 1]
          st(1) = [0]
          st(+) = [0, 1]
          st(0) = [0]
          st(#) = []
         precedence:
          + > - > 1 ~ 0 ~ #
         problem:
          
         Qed