Problem SK90 2.30

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputSK90 2.30

stdout:

MAYBE

Problem:
 not(x) -> xor(x,true())
 implies(x,y) -> xor(and(x,y),xor(x,true()))
 or(x,y) -> xor(and(x,y),xor(x,y))
 =(x,y) -> xor(x,xor(y,true()))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
YES(?,O(1))
InputSK90 2.30

stdout:

YES(?,O(1))

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(1))
InputSK90 2.30

stdout:

YES(?,O(1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}

Proof Output:    
  'wdg' proved the best result:
  
  Details:
  --------
    'wdg' succeeded with the following output:
     'wdg'
     -----
     Answer:           YES(?,O(1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  not(x) -> xor(x, true())
          , implies(x, y) -> xor(and(x, y), xor(x, true()))
          , or(x, y) -> xor(and(x, y), xor(x, y))
          , =(x, y) -> xor(x, xor(y, true()))}
     
     Proof Output:    
       Transformation Details:
       -----------------------
         We have computed the following set of weak (innermost) dependency pairs:
         
           {  1: not^#(x) -> c_0()
            , 2: implies^#(x, y) -> c_1()
            , 3: or^#(x, y) -> c_2()
            , 4: =^#(x, y) -> c_3()}
         
         The dependency graph contains no edges and the usable rules are empty.
       

Tool RC1

Execution TimeUnknown
Answer
YES(?,O(1))
InputSK90 2.30

stdout:

YES(?,O(1))

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(1))
InputSK90 2.30

stdout:

YES(?,O(1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}

Proof Output:    
  'wdg' proved the best result:
  
  Details:
  --------
    'wdg' succeeded with the following output:
     'wdg'
     -----
     Answer:           YES(?,O(1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  not(x) -> xor(x, true())
          , implies(x, y) -> xor(and(x, y), xor(x, true()))
          , or(x, y) -> xor(and(x, y), xor(x, y))
          , =(x, y) -> xor(x, xor(y, true()))}
     
     Proof Output:    
       Transformation Details:
       -----------------------
         We have computed the following set of weak (innermost) dependency pairs:
         
           {  1: not^#(x) -> c_0(x)
            , 2: implies^#(x, y) -> c_1(x, y, x)
            , 3: or^#(x, y) -> c_2(x, y, x, y)
            , 4: =^#(x, y) -> c_3(x, y)}
         
         The dependency graph contains no edges and the usable rules are empty.
       

Tool pair1rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.30

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: none

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

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(not) = {}, Uargs(xor) = {}, Uargs(implies) = {},
       Uargs(and) = {}, Uargs(or) = {}, Uargs(=) = {}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      not(x1) = [2 2] x1 + [2]
                [2 1]      [2]
      xor(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                    [0 0]      [0 0]      [1]
      true() = [1]
               [1]
      implies(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                        [1 2]      [1 2]      [2]
      and(x1, x2) = [1 2] x1 + [1 1] x2 + [1]
                    [0 0]      [0 0]      [1]
      or(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                   [1 2]      [1 2]      [2]
      =(x1, x2) = [2 2] x1 + [1 2] x2 + [2]
                  [1 2]      [1 1]      [1]
  

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

Tool pair2rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.30

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: none

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

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(not) = {}, Uargs(xor) = {}, Uargs(implies) = {},
       Uargs(and) = {}, Uargs(or) = {}, Uargs(=) = {}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      not(x1) = [2 2] x1 + [2]
                [2 1]      [2]
      xor(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                    [0 0]      [0 0]      [1]
      true() = [1]
               [1]
      implies(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                        [1 2]      [1 2]      [2]
      and(x1, x2) = [1 2] x1 + [1 1] x2 + [1]
                    [0 0]      [0 0]      [1]
      or(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                   [1 2]      [1 2]      [2]
      =(x1, x2) = [2 2] x1 + [1 2] x2 + [2]
                  [1 2]      [1 1]      [1]
  

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

Tool pair3irc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.30

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: innermost

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

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(not) = {}, Uargs(xor) = {}, Uargs(implies) = {},
       Uargs(and) = {}, Uargs(or) = {}, Uargs(=) = {}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      not(x1) = [2 2] x1 + [2]
                [2 1]      [2]
      xor(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                    [0 0]      [0 0]      [1]
      true() = [1]
               [1]
      implies(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                        [1 2]      [1 2]      [2]
      and(x1, x2) = [1 2] x1 + [1 1] x2 + [1]
                    [0 0]      [0 0]      [1]
      or(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                   [1 2]      [1 2]      [2]
      =(x1, x2) = [2 2] x1 + [1 2] x2 + [2]
                  [1 2]      [1 1]      [1]
  

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

Tool pair3rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.30

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: none

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

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(not) = {}, Uargs(xor) = {}, Uargs(implies) = {},
       Uargs(and) = {}, Uargs(or) = {}, Uargs(=) = {}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      not(x1) = [2 2] x1 + [2]
                [2 1]      [2]
      xor(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                    [0 0]      [0 0]      [1]
      true() = [1]
               [1]
      implies(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                        [1 2]      [1 2]      [2]
      and(x1, x2) = [1 2] x1 + [1 1] x2 + [1]
                    [0 0]      [0 0]      [1]
      or(x1, x2) = [2 2] x1 + [2 2] x2 + [2]
                   [1 2]      [1 2]      [2]
      =(x1, x2) = [2 2] x1 + [1 2] x2 + [2]
                  [1 2]      [1 1]      [1]
  

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

Tool rc

Execution TimeUnknown
Answer
YES(O(1),O(1))
InputSK90 2.30

stdout:

YES(O(1),O(1))

We consider the following Problem:

  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(O(1),O(1))

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  'dp' proved the goal fastest:
  
  We have computed the following dependency pairs
  
  Strict Dependency Pairs:
    {  not^#(x) -> c_1(x)
     , implies^#(x, y) -> c_2(x, y, x)
     , or^#(x, y) -> c_3(x, y, x, y)
     , =^#(x, y) -> c_4(x, y)}
  
  We consider the following Problem:
  
    Strict DPs:
      {  not^#(x) -> c_1(x)
       , implies^#(x, y) -> c_2(x, y, x)
       , or^#(x, y) -> c_3(x, y, x, y)
       , =^#(x, y) -> c_4(x, y)}
    Strict Trs:
      {  not(x) -> xor(x, true())
       , implies(x, y) -> xor(and(x, y), xor(x, true()))
       , or(x, y) -> xor(and(x, y), xor(x, y))
       , =(x, y) -> xor(x, xor(y, true()))}
    StartTerms: basic terms
    Strategy: none
  
  Certificate: YES(O(1),O(1))
  
  Application of 'usablerules':
  -----------------------------
    No rule is usable.
    
    We consider the following Problem:
    
      Strict DPs:
        {  not^#(x) -> c_1(x)
         , implies^#(x, y) -> c_2(x, y, x)
         , or^#(x, y) -> c_3(x, y, x, y)
         , =^#(x, y) -> c_4(x, y)}
      StartTerms: basic terms
      Strategy: none
    
    Certificate: YES(O(1),O(1))
    
    Application of 'Fastest':
    -------------------------
      'removetails >>> ... >>> ... >>> ...' proved the goal fastest:
      
      We consider the the dependency-graph
      
        1: not^#(x) -> c_1(x)
        
        2: implies^#(x, y) -> c_2(x, y, x)
        
        3: or^#(x, y) -> c_3(x, y, x, y)
        
        4: =^#(x, y) -> c_4(x, y)
        
      
      together with the congruence-graph
      
        ->{1}                                                       Noncyclic, trivial, SCC
        
        ->{2}                                                       Noncyclic, trivial, SCC
        
        ->{3}                                                       Noncyclic, trivial, SCC
        
        ->{4}                                                       Noncyclic, trivial, SCC
        
        
        Here rules are as follows:
        
          {  1: not^#(x) -> c_1(x)
           , 2: implies^#(x, y) -> c_2(x, y, x)
           , 3: or^#(x, y) -> c_3(x, y, x, y)
           , 4: =^#(x, y) -> c_4(x, y)}
      
      The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
      
        {  4: =^#(x, y) -> c_4(x, y)
         , 3: or^#(x, y) -> c_3(x, y, x, y)
         , 2: implies^#(x, y) -> c_2(x, y, x)
         , 1: not^#(x) -> c_1(x)}
      
      We consider the following Problem:
      
        StartTerms: basic terms
        Strategy: none
      
      Certificate: YES(O(1),O(1))
      
      Application of 'simpDPRHS >>> ...':
      -----------------------------------
        No rule was simplified
        
        We apply the transformation 'usablerules' on the resulting sub-problems:
        Sub-problem 1:
        --------------
          We consider the problem
          
          StartTerms: basic terms
          Strategy: none
          
          The input problem is not a DP-problem.
        
        We abort the transformation and continue with the subprocessor on the problem
        
        StartTerms: basic terms
        Strategy: none
        
        1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
           
             All strict components are empty, nothing to further orient
           
           We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
           
           StartTerms: basic terms
           Strategy: none
           
             We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
             
               All strict components are empty, nothing to further orient
             
             We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
             
             StartTerms: basic terms
             Strategy: none
             
               All strict components are empty, nothing to further orient
           
           We abort the transformation and continue with the subprocessor on the problem
           
           StartTerms: basic terms
           Strategy: none
           
           1) No dependency-pair could be removed
              
              We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
              Sub-problem 1:
              --------------
                We consider the problem
                
                StartTerms: basic terms
                Strategy: none
                
                We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                
                  All strict components are empty, nothing to further orient
                
                We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                
                StartTerms: basic terms
                Strategy: none
                
                  We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                  
                    All strict components are empty, nothing to further orient
                  
                  We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                  
                  StartTerms: basic terms
                  Strategy: none
                  
                    All strict components are empty, nothing to further orient
              
              We abort the transformation and continue with the subprocessor on the problem
              
              StartTerms: basic terms
              Strategy: none
              
              1) 'Sequentially' proved the goal fastest:
                 
                 'empty' succeeded:
                 
                 Empty rules are trivially bounded
              
           
        

Hurray, we answered YES(O(1),O(1))

Tool tup3irc

Execution Time6.1435938e-2ms
Answer
YES(O(1),O(1))
InputSK90 2.30

stdout:

YES(O(1),O(1))

We consider the following Problem:

  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(O(1),O(1))

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  not(x) -> xor(x, true())
     , implies(x, y) -> xor(and(x, y), xor(x, true()))
     , or(x, y) -> xor(and(x, y), xor(x, y))
     , =(x, y) -> xor(x, xor(y, true()))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'dp' proved the goal fastest:
     
     We have computed the following dependency pairs
     
     Strict Dependency Pairs:
       {  not^#(x) -> c_1()
        , implies^#(x, y) -> c_2()
        , or^#(x, y) -> c_3()
        , =^#(x, y) -> c_4()}
     
     We consider the following Problem:
     
       Strict DPs:
         {  not^#(x) -> c_1()
          , implies^#(x, y) -> c_2()
          , or^#(x, y) -> c_3()
          , =^#(x, y) -> c_4()}
       Weak Trs:
         {  not(x) -> xor(x, true())
          , implies(x, y) -> xor(and(x, y), xor(x, true()))
          , or(x, y) -> xor(and(x, y), xor(x, y))
          , =(x, y) -> xor(x, xor(y, true()))}
       StartTerms: basic terms
       Strategy: innermost
     
     Certificate: YES(O(1),O(1))
     
     Application of 'Fastest':
     -------------------------
       'compose (statically using 'split all congruence from CWD except leafs', multiplication)' proved the goal fastest:
       
       Compose is inapplicable since some weak rule is size increasing
       
       We abort the transformation and continue with the subprocessor on the problem
       
       Strict DPs:
         {  not^#(x) -> c_1()
          , implies^#(x, y) -> c_2()
          , or^#(x, y) -> c_3()
          , =^#(x, y) -> c_4()}
       Weak Trs:
         {  not(x) -> xor(x, true())
          , implies(x, y) -> xor(and(x, y), xor(x, true()))
          , or(x, y) -> xor(and(x, y), xor(x, y))
          , =(x, y) -> xor(x, xor(y, true()))}
       StartTerms: basic terms
       Strategy: innermost
       
       1) We consider the the dependency-graph
          
            1: not^#(x) -> c_1()
            
            2: implies^#(x, y) -> c_2()
            
            3: or^#(x, y) -> c_3()
            
            4: =^#(x, y) -> c_4()
            
          
          together with the congruence-graph
          
            ->{1}                                                       Noncyclic, trivial, SCC
            
            ->{2}                                                       Noncyclic, trivial, SCC
            
            ->{3}                                                       Noncyclic, trivial, SCC
            
            ->{4}                                                       Noncyclic, trivial, SCC
            
            
            Here rules are as follows:
            
              {  1: not^#(x) -> c_1()
               , 2: implies^#(x, y) -> c_2()
               , 3: or^#(x, y) -> c_3()
               , 4: =^#(x, y) -> c_4()}
          
          The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
          
            {  4: =^#(x, y) -> c_4()
             , 3: or^#(x, y) -> c_3()
             , 2: implies^#(x, y) -> c_2()
             , 1: not^#(x) -> c_1()}
          
          We consider the following Problem:
          
            Weak Trs:
              {  not(x) -> xor(x, true())
               , implies(x, y) -> xor(and(x, y), xor(x, true()))
               , or(x, y) -> xor(and(x, y), xor(x, y))
               , =(x, y) -> xor(x, xor(y, true()))}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(O(1),O(1))
          
          Application of 'simpDPRHS >>> ...':
          -----------------------------------
            No rule was simplified
            
            We apply the transformation 'usablerules' on the resulting sub-problems:
            Sub-problem 1:
            --------------
              We consider the problem
              
              Weak Trs:
                {  not(x) -> xor(x, true())
                 , implies(x, y) -> xor(and(x, y), xor(x, true()))
                 , or(x, y) -> xor(and(x, y), xor(x, y))
                 , =(x, y) -> xor(x, xor(y, true()))}
              StartTerms: basic terms
              Strategy: innermost
              
              The input problem is not a DP-problem.
            
            We abort the transformation and continue with the subprocessor on the problem
            
            Weak Trs:
              {  not(x) -> xor(x, true())
               , implies(x, y) -> xor(and(x, y), xor(x, true()))
               , or(x, y) -> xor(and(x, y), xor(x, y))
               , =(x, y) -> xor(x, xor(y, true()))}
            StartTerms: basic terms
            Strategy: innermost
            
            1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
               
                 All strict components are empty, nothing to further orient
               
               We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
               
               Weak Trs:
                 {  not(x) -> xor(x, true())
                  , implies(x, y) -> xor(and(x, y), xor(x, true()))
                  , or(x, y) -> xor(and(x, y), xor(x, y))
                  , =(x, y) -> xor(x, xor(y, true()))}
               StartTerms: basic terms
               Strategy: innermost
               
                 We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                 
                   All strict components are empty, nothing to further orient
                 
                 We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                 
                 Weak Trs:
                   {  not(x) -> xor(x, true())
                    , implies(x, y) -> xor(and(x, y), xor(x, true()))
                    , or(x, y) -> xor(and(x, y), xor(x, y))
                    , =(x, y) -> xor(x, xor(y, true()))}
                 StartTerms: basic terms
                 Strategy: innermost
                 
                   All strict components are empty, nothing to further orient
               
               We abort the transformation and continue with the subprocessor on the problem
               
               Weak Trs:
                 {  not(x) -> xor(x, true())
                  , implies(x, y) -> xor(and(x, y), xor(x, true()))
                  , or(x, y) -> xor(and(x, y), xor(x, y))
                  , =(x, y) -> xor(x, xor(y, true()))}
               StartTerms: basic terms
               Strategy: innermost
               
               1) No dependency-pair could be removed
                  
                  We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                  Sub-problem 1:
                  --------------
                    We consider the problem
                    
                    Weak Trs:
                      {  not(x) -> xor(x, true())
                       , implies(x, y) -> xor(and(x, y), xor(x, true()))
                       , or(x, y) -> xor(and(x, y), xor(x, y))
                       , =(x, y) -> xor(x, xor(y, true()))}
                    StartTerms: basic terms
                    Strategy: innermost
                    
                    We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                    
                      All strict components are empty, nothing to further orient
                    
                    We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                    
                    Weak Trs:
                      {  not(x) -> xor(x, true())
                       , implies(x, y) -> xor(and(x, y), xor(x, true()))
                       , or(x, y) -> xor(and(x, y), xor(x, y))
                       , =(x, y) -> xor(x, xor(y, true()))}
                    StartTerms: basic terms
                    Strategy: innermost
                    
                      We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                      
                        All strict components are empty, nothing to further orient
                      
                      We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                      
                      Weak Trs:
                        {  not(x) -> xor(x, true())
                         , implies(x, y) -> xor(and(x, y), xor(x, true()))
                         , or(x, y) -> xor(and(x, y), xor(x, y))
                         , =(x, y) -> xor(x, xor(y, true()))}
                      StartTerms: basic terms
                      Strategy: innermost
                      
                        All strict components are empty, nothing to further orient
                  
                  We abort the transformation and continue with the subprocessor on the problem
                  
                  Weak Trs:
                    {  not(x) -> xor(x, true())
                     , implies(x, y) -> xor(and(x, y), xor(x, true()))
                     , or(x, y) -> xor(and(x, y), xor(x, y))
                     , =(x, y) -> xor(x, xor(y, true()))}
                  StartTerms: basic terms
                  Strategy: innermost
                  
                  1) 'empty' succeeded:
                     
                     Empty rules are trivially bounded
                  
               
            
       
  

Hurray, we answered YES(O(1),O(1))