YES(?,O(n^2))

Problem:
 implies(not(x),y) -> or(x,y)
 implies(not(x),or(y,z)) -> implies(y,or(x,z))
 implies(x,or(y,z)) -> or(y,implies(x,z))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                  [1 4]          [0]
   [or](x0, x1) = [0 0]x0 + x1 + [1],
   
                       [1 4]     [1 1]     [14]
   [implies](x0, x1) = [0 0]x0 + [0 1]x1 + [2 ],
   
               [1  12]     [1]
   [not](x0) = [0  1 ]x0 + [0]
  orientation:
                       [1  16]    [1 1]    [15]    [1 4]        [0]          
   implies(not(x),y) = [0  0 ]x + [0 1]y + [2 ] >= [0 0]x + y + [1] = or(x,y)
   
                             [1  16]    [1 4]    [1 1]    [16]    [1 4]    [1 4]    [1 1]    [15]                     
   implies(not(x),or(y,z)) = [0  0 ]x + [0 0]y + [0 1]z + [3 ] >= [0 0]x + [0 0]y + [0 1]z + [3 ] = implies(y,or(x,z))
   
                        [1 4]    [1 4]    [1 1]    [15]    [1 4]    [1 4]    [1 1]    [14]                     
   implies(x,or(y,z)) = [0 0]x + [0 0]y + [0 1]z + [3 ] >= [0 0]x + [0 0]y + [0 1]z + [3 ] = or(y,implies(x,z))
  problem:
   
  Qed