Problem SK90 2.36

Tool CaT

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

stdout:

YES(?,O(n^1))

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:
 Complexity Transformation Processor:
  strict:
   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))
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match
   automaton:
    final states: {3}
    transitions:
     or1(1,2) -> 3*
     or1(2,1) -> 3*
     or1(1,1) -> 3*
     or1(2,2) -> 3*
     implies0(1,2) -> 3*
     implies0(2,1) -> 3*
     implies0(1,1) -> 3*
     implies0(2,2) -> 3*
     not0(2) -> 1*
     not0(1) -> 1*
     or0(1,2) -> 2*
     or0(2,1) -> 2*
     or0(2,3) -> 3*
     or0(1,1) -> 2*
     or0(1,3) -> 3*
     or0(2,2) -> 2*
   problem:
    strict:
     implies(not(x),or(y,z)) -> implies(y,or(x,z))
     implies(x,or(y,z)) -> or(y,implies(x,z))
    weak:
     implies(not(x),y) -> or(x,y)
   Bounds Processor:
    bound: 1
    enrichment: match
    automaton:
     final states: {3}
     transitions:
      or1(1,2) -> 8,4
      or1(1,4) -> 8,3
      or1(1,8) -> 8,3
      or1(2,1) -> 8,7
      or1(2,7) -> 8,3
      or1(2,9) -> 8,3
      or1(1,1) -> 8,4
      or1(1,7) -> 8,3
      or1(1,9) -> 8,3
      or1(2,2) -> 8,4
      or1(2,4) -> 8,3
      or1(2,8) -> 8,3
      implies1(1,2) -> 8*
      implies1(1,4) -> 8,3
      implies1(2,1) -> 9*
      implies1(2,7) -> 8,3
      implies1(1,1) -> 8*
      implies1(1,7) -> 8,3
      implies1(2,2) -> 8*
      implies1(2,4) -> 8,3
      implies0(1,2) -> 3*
      implies0(2,1) -> 3*
      implies0(1,1) -> 3*
      implies0(2,2) -> 3*
      not0(2) -> 1*
      not0(1) -> 1*
      or0(1,2) -> 3,2
      or0(2,1) -> 3,2
      or0(2,3) -> 3*
      or0(1,1) -> 3,2
      or0(1,3) -> 3*
      or0(2,2) -> 3,2
    problem:
     strict:
      implies(x,or(y,z)) -> or(y,implies(x,z))
     weak:
      implies(not(x),or(y,z)) -> implies(y,or(x,z))
      implies(not(x),y) -> or(x,y)
    Bounds Processor:
     bound: 2
     enrichment: match
     automaton:
      final states: {3}
      transitions:
       or1(1,2) -> 3,9,4,1
       or1(1,4) -> 11,9,4,7,3
       or1(2,1) -> 3,9,4,1
       or1(2,7) -> 11,7,3
       or1(1,1) -> 3,9,4,1
       or1(1,7) -> 11,7,3
       or1(2,2) -> 3,9,4,2
       or1(2,4) -> 11,4,7,3
       implies1(1,2) -> 3,4
       implies1(2,1) -> 3,4
       implies1(1,1) -> 9,3,4,7
       implies1(2,2) -> 3,4
       or2(2,9) -> 3,9,4
       or2(2,11) -> 9,3,4,11,7
       or2(1,9) -> 3,11,7,4,9
       or2(1,11) -> 9,3,11,7,4
       implies2(1,2) -> 9*
       implies2(2,1) -> 9*
       implies2(1,1) -> 11*
       implies2(2,2) -> 9*
       implies0(1,2) -> 3*
       implies0(2,1) -> 3*
       implies0(1,1) -> 3*
       implies0(2,2) -> 3*
       not0(2) -> 2*
       not0(1) -> 2*
       or0(1,2) -> 3,1
       or0(2,1) -> 3,1
       or0(1,1) -> 3,1
       or0(2,2) -> 3,1
     problem:
      strict:
       
      weak:
       implies(x,or(y,z)) -> or(y,implies(x,z))
       implies(not(x),or(y,z)) -> implies(y,or(x,z))
       implies(not(x),y) -> or(x,y)
     Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

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

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  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 Output:    
  'matrix-interpretation of dimension 1' proved the best result:
  
  Details:
  --------
    'matrix-interpretation of dimension 1' succeeded with the following output:
     'matrix-interpretation of dimension 1'
     --------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  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 Output:    
       The following argument positions are usable:
         Uargs(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        implies(x1, x2) = [2] x1 + [2] x2 + [0]
        not(x1) = [1] x1 + [3]
        or(x1, x2) = [1] x1 + [1] x2 + [1]

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

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

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  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 Output:    
  'matrix-interpretation of dimension 1' proved the best result:
  
  Details:
  --------
    'matrix-interpretation of dimension 1' succeeded with the following output:
     'matrix-interpretation of dimension 1'
     --------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  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 Output:    
       The following argument positions are usable:
         Uargs(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        implies(x1, x2) = [2] x1 + [2] x2 + [0]
        not(x1) = [1] x1 + [3]
        or(x1, x2) = [1] x1 + [1] x2 + [1]

Tool pair1rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  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))}
  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:
    {  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))}
  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(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      implies(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
                        [0 0]      [0 0]      [0]
      not(x1) = [1 0] x1 + [2]
                [0 0]      [0]
      or(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                   [0 0]      [0 0]      [0]
  

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

Tool pair2rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  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))}
  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:
    {  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))}
  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(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      implies(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
                        [0 0]      [0 0]      [0]
      not(x1) = [1 0] x1 + [2]
                [0 0]      [0]
      or(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                   [0 0]      [0 0]      [0]
  

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

Tool pair3irc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  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))}
  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:
    {  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))}
  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(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      implies(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
                        [0 0]      [0 0]      [0]
      not(x1) = [1 0] x1 + [2]
                [0 0]      [0]
      or(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                   [0 0]      [0 0]      [0]
  

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

Tool pair3rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  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))}
  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:
    {  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))}
  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(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      implies(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
                        [0 0]      [0 0]      [0]
      not(x1) = [1 0] x1 + [2]
                [0 0]      [0]
      or(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                   [0 0]      [0 0]      [0]
  

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

Tool rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  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))}
  StartTerms: basic terms
  Strategy: none

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

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  '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(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
  We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
  Interpretation Functions:
   implies(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
                     [0 0]      [0 0]      [0]
   not(x1) = [1 0] x1 + [2]
             [0 0]      [0]
   or(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                [0 0]      [0 0]      [0]

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

Tool tup3irc

Execution Time0.8735912ms
Answer
YES(?,O(n^1))
InputSK90 2.36

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  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))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^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:
    {  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))}
  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(implies) = {}, Uargs(not) = {}, Uargs(or) = {2}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      implies(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
                        [0 0]      [0 0]      [0]
      not(x1) = [1 0] x1 + [2]
                [0 0]      [0]
      or(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                   [0 0]      [0 0]      [0]
  

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