We consider the following Problem:

  Strict Trs:
    {  xor(x, F()) -> x
     , xor(x, neg(x)) -> F()
     , and(x, T()) -> x
     , and(x, F()) -> F()
     , and(x, x) -> x
     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
     , xor(x, x) -> F()
     , impl(x, y) -> xor(and(x, y), xor(x, T()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , equiv(x, y) -> xor(x, xor(y, T()))
     , neg(x) -> xor(x, T())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  Arguments of following rules are not normal-forms:
  {xor(x, neg(x)) -> F()}
  
  All above mentioned rules can be savely removed.
  
  We consider the following Problem:
  
    Strict Trs:
      {  xor(x, F()) -> x
       , and(x, T()) -> x
       , and(x, F()) -> F()
       , and(x, x) -> x
       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
       , xor(x, x) -> F()
       , impl(x, y) -> xor(and(x, y), xor(x, T()))
       , or(x, y) -> xor(and(x, y), xor(x, y))
       , equiv(x, y) -> xor(x, xor(y, T()))
       , neg(x) -> xor(x, T())}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^1))
  
  Proof:
    We consider the following Problem:
    
      Strict Trs:
        {  xor(x, F()) -> x
         , and(x, T()) -> x
         , and(x, F()) -> F()
         , and(x, x) -> x
         , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
         , xor(x, x) -> F()
         , impl(x, y) -> xor(and(x, y), xor(x, T()))
         , or(x, y) -> xor(and(x, y), xor(x, y))
         , equiv(x, y) -> xor(x, xor(y, T()))
         , neg(x) -> xor(x, T())}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^1))
    
    Proof:
      We have computed the following dependency pairs
      
        Strict DPs:
          {  xor^#(x, F()) -> c_1()
           , and^#(x, T()) -> c_2()
           , and^#(x, F()) -> c_3()
           , and^#(x, x) -> c_4()
           , and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
           , xor^#(x, x) -> c_6()
           , impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
           , or^#(x, y) -> xor^#(and(x, y), xor(x, y))
           , equiv^#(x, y) -> xor^#(x, xor(y, T()))
           , neg^#(x) -> xor^#(x, T())}
      
      We consider the following Problem:
      
        Strict DPs:
          {  xor^#(x, F()) -> c_1()
           , and^#(x, T()) -> c_2()
           , and^#(x, F()) -> c_3()
           , and^#(x, x) -> c_4()
           , and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
           , xor^#(x, x) -> c_6()
           , impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
           , or^#(x, y) -> xor^#(and(x, y), xor(x, y))
           , equiv^#(x, y) -> xor^#(x, xor(y, T()))
           , neg^#(x) -> xor^#(x, T())}
        Strict Trs:
          {  xor(x, F()) -> x
           , and(x, T()) -> x
           , and(x, F()) -> F()
           , and(x, x) -> x
           , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
           , xor(x, x) -> F()
           , impl(x, y) -> xor(and(x, y), xor(x, T()))
           , or(x, y) -> xor(and(x, y), xor(x, y))
           , equiv(x, y) -> xor(x, xor(y, T()))
           , neg(x) -> xor(x, T())}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^1))
      
      Proof:
        We replace strict/weak-rules by the corresponding usable rules:
        
          Strict Usable Rules:
            {  xor(x, F()) -> x
             , and(x, T()) -> x
             , and(x, F()) -> F()
             , and(x, x) -> x
             , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
             , xor(x, x) -> F()}
        
        We consider the following Problem:
        
          Strict DPs:
            {  xor^#(x, F()) -> c_1()
             , and^#(x, T()) -> c_2()
             , and^#(x, F()) -> c_3()
             , and^#(x, x) -> c_4()
             , and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
             , xor^#(x, x) -> c_6()
             , impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
             , or^#(x, y) -> xor^#(and(x, y), xor(x, y))
             , equiv^#(x, y) -> xor^#(x, xor(y, T()))
             , neg^#(x) -> xor^#(x, T())}
          Strict Trs:
            {  xor(x, F()) -> x
             , and(x, T()) -> x
             , and(x, F()) -> F()
             , and(x, x) -> x
             , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
             , xor(x, x) -> F()}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^1))
        
        Proof:
          The weightgap principle applies, where following rules are oriented strictly:
          
          Dependency Pairs:
            {and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
          TRS Component:
            {  xor(x, F()) -> x
             , and(x, T()) -> x
             , and(x, F()) -> F()
             , and(x, x) -> x
             , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
             , xor(x, x) -> F()}
          
          Interpretation of constant growth:
          ----------------------------------
            The following argument positions are usable:
              Uargs(xor) = {1, 2}, Uargs(neg) = {}, Uargs(and) = {},
              Uargs(impl) = {}, Uargs(or) = {}, Uargs(equiv) = {},
              Uargs(xor^#) = {1, 2}, Uargs(and^#) = {}, Uargs(impl^#) = {},
              Uargs(or^#) = {}, Uargs(equiv^#) = {}, Uargs(neg^#) = {}
            We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             xor(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                           [0 1]      [0 2]      [3]
             F() = [0]
                   [0]
             neg(x1) = [0 0] x1 + [0]
                       [0 0]      [0]
             and(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                           [0 2]      [0 0]      [0]
             T() = [0]
                   [0]
             impl(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
             or(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                          [0 0]      [0 0]      [0]
             equiv(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
             xor^#(x1, x2) = [2 0] x1 + [1 0] x2 + [0]
                             [0 0]      [0 0]      [0]
             c_1() = [0]
                     [0]
             and^#(x1, x2) = [2 2] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
             c_2() = [0]
                     [0]
             c_3() = [0]
                     [0]
             c_4() = [0]
                     [0]
             c_6() = [0]
                     [0]
             impl^#(x1, x2) = [3 2] x1 + [0 0] x2 + [0]
                              [0 0]      [0 0]      [0]
             or^#(x1, x2) = [3 2] x1 + [2 0] x2 + [0]
                            [0 0]      [0 0]      [0]
             equiv^#(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
                               [0 0]      [0 0]      [0]
             neg^#(x1) = [2 0] x1 + [0]
                         [0 0]      [0]
          
          The strictly oriented rules are moved into the weak component.
          
          We consider the following Problem:
          
            Strict DPs:
              {  xor^#(x, F()) -> c_1()
               , and^#(x, T()) -> c_2()
               , and^#(x, F()) -> c_3()
               , and^#(x, x) -> c_4()
               , xor^#(x, x) -> c_6()
               , impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
               , or^#(x, y) -> xor^#(and(x, y), xor(x, y))
               , equiv^#(x, y) -> xor^#(x, xor(y, T()))
               , neg^#(x) -> xor^#(x, T())}
            Weak DPs: {and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
            Weak Trs:
              {  xor(x, F()) -> x
               , and(x, T()) -> x
               , and(x, F()) -> F()
               , and(x, x) -> x
               , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
               , xor(x, x) -> F()}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(?,O(n^1))
          
          Proof:
            We use following congruence DG for path analysis
            
            ->9:{2}                                                     [   YES(O(1),O(1))   ]
            
            ->8:{3}                                                     [   YES(O(1),O(1))   ]
            
            ->7:{4}                                                     [   YES(O(1),O(1))   ]
            
            ->5:{6}                                                     [   YES(O(1),O(1))   ]
               |
               |->10:{1}                                                [   YES(O(1),O(1))   ]
               |
               `->6:{5}                                                 [   YES(O(1),O(1))   ]
            
            ->4:{7}                                                     [   YES(O(1),O(1))   ]
               |
               |->10:{1}                                                [   YES(O(1),O(1))   ]
               |
               `->6:{5}                                                 [   YES(O(1),O(1))   ]
            
            ->3:{8}                                                     [   YES(O(1),O(1))   ]
               |
               |->10:{1}                                                [   YES(O(1),O(1))   ]
               |
               `->6:{5}                                                 [   YES(O(1),O(1))   ]
            
            ->2:{9}                                                     [   YES(O(1),O(1))   ]
               |
               `->6:{5}                                                 [   YES(O(1),O(1))   ]
            
            ->1:{10}                                                    [      subsumed      ]
               |
               |->10:{1}                                                [   YES(O(1),O(1))   ]
               |
               `->6:{5}                                                 [   YES(O(1),O(1))   ]
            
            
            Here dependency-pairs are as follows:
            
            Strict DPs:
              {  1: xor^#(x, F()) -> c_1()
               , 2: and^#(x, T()) -> c_2()
               , 3: and^#(x, F()) -> c_3()
               , 4: and^#(x, x) -> c_4()
               , 5: xor^#(x, x) -> c_6()
               , 6: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
               , 7: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
               , 8: equiv^#(x, y) -> xor^#(x, xor(y, T()))
               , 9: neg^#(x) -> xor^#(x, T())}
            WeakDPs DPs:
              {10: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
            
            * Path 9:{2}: YES(O(1),O(1))
              --------------------------
              
              We consider the following Problem:
              
                Strict DPs: {and^#(x, T()) -> c_2()}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: and^#(x, T()) -> c_2()
                  
                
                together with the congruence-graph
                
                  ->1:{1}                                                     Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: and^#(x, T()) -> c_2()}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {1: and^#(x, T()) -> c_2()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 8:{3}: YES(O(1),O(1))
              --------------------------
              
              We consider the following Problem:
              
                Strict DPs: {and^#(x, F()) -> c_3()}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: and^#(x, F()) -> c_3()
                  
                
                together with the congruence-graph
                
                  ->1:{1}                                                     Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: and^#(x, F()) -> c_3()}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {1: and^#(x, F()) -> c_3()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 7:{4}: YES(O(1),O(1))
              --------------------------
              
              We consider the following Problem:
              
                Strict DPs: {and^#(x, x) -> c_4()}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: and^#(x, x) -> c_4()
                  
                
                together with the congruence-graph
                
                  ->1:{1}                                                     Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: and^#(x, x) -> c_4()}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {1: and^#(x, x) -> c_4()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 5:{6}: YES(O(1),O(1))
              --------------------------
              
              We consider the following Problem:
              
                Strict DPs: {impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
                  
                
                together with the congruence-graph
                
                  ->1:{1}                                                     Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {1: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 5:{6}->10:{1}: YES(O(1),O(1))
              ----------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, F()) -> c_1()}
                Weak DPs: {impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, F()) -> c_1()
                  
                  2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
                     -->_1 xor^#(x, F()) -> c_1() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, F()) -> c_1()}
                  WeakDPs DPs:
                    {2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
                   , 1: xor^#(x, F()) -> c_1()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 5:{6}->6:{5}: YES(O(1),O(1))
              ---------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, x) -> c_6()}
                Weak DPs: {impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, x) -> c_6()
                  
                  2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
                     -->_1 xor^#(x, x) -> c_6() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, x) -> c_6()}
                  WeakDPs DPs:
                    {2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
                   , 1: xor^#(x, x) -> c_6()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 4:{7}: YES(O(1),O(1))
              --------------------------
              
              We consider the following Problem:
              
                Strict DPs: {or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
                  
                
                together with the congruence-graph
                
                  ->1:{1}                                                     Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {1: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 4:{7}->10:{1}: YES(O(1),O(1))
              ----------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, F()) -> c_1()}
                Weak DPs: {or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, F()) -> c_1()
                  
                  2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
                     -->_1 xor^#(x, F()) -> c_1() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, F()) -> c_1()}
                  WeakDPs DPs:
                    {2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
                   , 1: xor^#(x, F()) -> c_1()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 4:{7}->6:{5}: YES(O(1),O(1))
              ---------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, x) -> c_6()}
                Weak DPs: {or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, x) -> c_6()
                  
                  2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
                     -->_1 xor^#(x, x) -> c_6() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, x) -> c_6()}
                  WeakDPs DPs:
                    {2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
                   , 1: xor^#(x, x) -> c_6()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 3:{8}: YES(O(1),O(1))
              --------------------------
              
              We consider the following Problem:
              
                Strict DPs: {equiv^#(x, y) -> xor^#(x, xor(y, T()))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: equiv^#(x, y) -> xor^#(x, xor(y, T()))
                  
                
                together with the congruence-graph
                
                  ->1:{1}                                                     Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {1: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 3:{8}->10:{1}: YES(O(1),O(1))
              ----------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, F()) -> c_1()}
                Weak DPs: {equiv^#(x, y) -> xor^#(x, xor(y, T()))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, F()) -> c_1()
                  
                  2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
                     -->_1 xor^#(x, F()) -> c_1() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, F()) -> c_1()}
                  WeakDPs DPs:
                    {2: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
                   , 1: xor^#(x, F()) -> c_1()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 3:{8}->6:{5}: YES(O(1),O(1))
              ---------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, x) -> c_6()}
                Weak DPs: {equiv^#(x, y) -> xor^#(x, xor(y, T()))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, x) -> c_6()
                  
                  2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
                     -->_1 xor^#(x, x) -> c_6() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, x) -> c_6()}
                  WeakDPs DPs:
                    {2: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
                   , 1: xor^#(x, x) -> c_6()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 2:{9}: YES(O(1),O(1))
              --------------------------
              
              We consider the following Problem:
              
                Strict DPs: {neg^#(x) -> xor^#(x, T())}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: neg^#(x) -> xor^#(x, T())
                  
                
                together with the congruence-graph
                
                  ->1:{1}                                                     Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: neg^#(x) -> xor^#(x, T())}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {1: neg^#(x) -> xor^#(x, T())}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 2:{9}->6:{5}: YES(O(1),O(1))
              ---------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, x) -> c_6()}
                Weak DPs: {neg^#(x) -> xor^#(x, T())}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, x) -> c_6()
                  
                  2: neg^#(x) -> xor^#(x, T()) -->_1 xor^#(x, x) -> c_6() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, x) -> c_6()}
                  WeakDPs DPs:
                    {2: neg^#(x) -> xor^#(x, T())}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: neg^#(x) -> xor^#(x, T())
                   , 1: xor^#(x, x) -> c_6()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 1:{10}: subsumed
              ---------------------
              
              This path is subsumed by the proof of paths 1:{10}->10:{1},
                                                          1:{10}->6:{5}.
            
            * Path 1:{10}->10:{1}: YES(O(1),O(1))
              -----------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, F()) -> c_1()}
                Weak DPs: {and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, F()) -> c_1()
                  
                  2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
                     -->_1 xor^#(x, F()) -> c_1() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, F()) -> c_1()}
                  WeakDPs DPs:
                    {2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
                   , 1: xor^#(x, F()) -> c_1()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded
            
            * Path 1:{10}->6:{5}: YES(O(1),O(1))
              ----------------------------------
              
              We consider the following Problem:
              
                Strict DPs: {xor^#(x, x) -> c_6()}
                Weak DPs: {and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
                Weak Trs:
                  {  xor(x, F()) -> x
                   , and(x, T()) -> x
                   , and(x, F()) -> F()
                   , and(x, x) -> x
                   , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                   , xor(x, x) -> F()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                We consider the the dependency-graph
                
                  1: xor^#(x, x) -> c_6()
                  
                  2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
                     -->_1 xor^#(x, x) -> c_6() :1
                  
                
                together with the congruence-graph
                
                  ->1:{2}                                                     Weak SCC
                     |
                     `->2:{1}                                                 Noncyclic, trivial, SCC
                  
                  
                  Here dependency-pairs are as follows:
                  
                  Strict DPs:
                    {1: xor^#(x, x) -> c_6()}
                  WeakDPs DPs:
                    {2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
                
                The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                
                  {  2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
                   , 1: xor^#(x, x) -> c_6()}
                
                We consider the following Problem:
                
                  Weak Trs:
                    {  xor(x, F()) -> x
                     , and(x, T()) -> x
                     , and(x, F()) -> F()
                     , and(x, x) -> x
                     , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                     , xor(x, x) -> F()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(O(1),O(1))
                
                Proof:
                  We consider the following Problem:
                  
                    Weak Trs:
                      {  xor(x, F()) -> x
                       , and(x, T()) -> x
                       , and(x, F()) -> F()
                       , and(x, x) -> x
                       , and(xor(x, y), z) -> xor(and(x, z), and(y, z))
                       , xor(x, x) -> F()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(O(1),O(1))
                  
                  Proof:
                    No rule is usable.
                    
                    We consider the following Problem:
                    
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(O(1),O(1))
                    
                    Proof:
                      Empty rules are trivially bounded

Hurray, we answered YES(?,O(n^1))