Problem Waldmann 06 SRS e

Tool Bounds

Execution Time60.065628ms
Answer
TIMEOUT
InputWaldmann 06 SRS e

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  0(3(x1)) -> 5(3(x1))
     , 6(6(x1)) -> 3(x1)
     , 2(4(x1)) -> 0(7(x1))
     , 6(2(x1)) -> 7(7(x1))
     , 9(x1) -> 6(7(x1))
     , 4(x1) -> 9(6(6(x1)))
     , 9(5(9(x1))) -> 5(7(x1))
     , 6(9(x1)) -> 9(x1)
     , 7(0(x1)) -> 9(3(x1))
     , 7(2(x1)) -> 4(x1)
     , 9(7(x1)) -> 7(5(x1))
     , 5(2(6(x1))) -> 6(2(4(x1)))
     , 4(7(x1)) -> 1(3(x1))
     , 2(8(x1)) -> 7(x1)
     , 5(3(x1)) -> 6(0(x1))
     , 4(x1) -> 5(2(3(x1)))
     , 5(9(x1)) -> 0(x1)
     , 2(8(x1)) -> 4(x1)
     , 2(8(1(x1))) -> 8(x1)
     , 2(7(x1)) -> 1(8(x1))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time7.633134ms
Answer
MAYBE
InputWaldmann 06 SRS e

stdout:

MAYBE

Statistics:
Number of monomials: 1513
Last formula building started for bound 3
Last SAT solving started for bound 3

Tool EDA

Execution Time60.0574ms
Answer
TIMEOUT
InputWaldmann 06 SRS e

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  0(3(x1)) -> 5(3(x1))
     , 6(6(x1)) -> 3(x1)
     , 2(4(x1)) -> 0(7(x1))
     , 6(2(x1)) -> 7(7(x1))
     , 9(x1) -> 6(7(x1))
     , 4(x1) -> 9(6(6(x1)))
     , 9(5(9(x1))) -> 5(7(x1))
     , 6(9(x1)) -> 9(x1)
     , 7(0(x1)) -> 9(3(x1))
     , 7(2(x1)) -> 4(x1)
     , 9(7(x1)) -> 7(5(x1))
     , 5(2(6(x1))) -> 6(2(4(x1)))
     , 4(7(x1)) -> 1(3(x1))
     , 2(8(x1)) -> 7(x1)
     , 5(3(x1)) -> 6(0(x1))
     , 4(x1) -> 5(2(3(x1)))
     , 5(9(x1)) -> 0(x1)
     , 2(8(x1)) -> 4(x1)
     , 2(8(1(x1))) -> 8(x1)
     , 2(7(x1)) -> 1(8(x1))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool IDA

Execution Time39.92965ms
Answer
MAYBE
InputWaldmann 06 SRS e

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(3(x1)) -> 5(3(x1))
     , 6(6(x1)) -> 3(x1)
     , 2(4(x1)) -> 0(7(x1))
     , 6(2(x1)) -> 7(7(x1))
     , 9(x1) -> 6(7(x1))
     , 4(x1) -> 9(6(6(x1)))
     , 9(5(9(x1))) -> 5(7(x1))
     , 6(9(x1)) -> 9(x1)
     , 7(0(x1)) -> 9(3(x1))
     , 7(2(x1)) -> 4(x1)
     , 9(7(x1)) -> 7(5(x1))
     , 5(2(6(x1))) -> 6(2(4(x1)))
     , 4(7(x1)) -> 1(3(x1))
     , 2(8(x1)) -> 7(x1)
     , 5(3(x1)) -> 6(0(x1))
     , 4(x1) -> 5(2(3(x1)))
     , 5(9(x1)) -> 0(x1)
     , 2(8(x1)) -> 4(x1)
     , 2(8(1(x1))) -> 8(x1)
     , 2(7(x1)) -> 1(8(x1))}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    2) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    4) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible
    
    6) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    

Arrrr..

Tool TRI

Execution Time52.92706ms
Answer
MAYBE
InputWaldmann 06 SRS e

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(3(x1)) -> 5(3(x1))
     , 6(6(x1)) -> 3(x1)
     , 2(4(x1)) -> 0(7(x1))
     , 6(2(x1)) -> 7(7(x1))
     , 9(x1) -> 6(7(x1))
     , 4(x1) -> 9(6(6(x1)))
     , 9(5(9(x1))) -> 5(7(x1))
     , 6(9(x1)) -> 9(x1)
     , 7(0(x1)) -> 9(3(x1))
     , 7(2(x1)) -> 4(x1)
     , 9(7(x1)) -> 7(5(x1))
     , 5(2(6(x1))) -> 6(2(4(x1)))
     , 4(7(x1)) -> 1(3(x1))
     , 2(8(x1)) -> 7(x1)
     , 5(3(x1)) -> 6(0(x1))
     , 4(x1) -> 5(2(3(x1)))
     , 5(9(x1)) -> 0(x1)
     , 2(8(x1)) -> 4(x1)
     , 2(8(1(x1))) -> 8(x1)
     , 2(7(x1)) -> 1(8(x1))}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'matrix-interpretation of dimension 6' failed due to the following reason:
         The input cannot be shown compatible
    
    2) 'matrix-interpretation of dimension 5' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'matrix-interpretation of dimension 4' failed due to the following reason:
         The input cannot be shown compatible
    
    4) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible
    
    6) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    

Arrrr..

Tool TRI2

Execution Time0.503078ms
Answer
MAYBE
InputWaldmann 06 SRS e

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(3(x1)) -> 5(3(x1))
     , 6(6(x1)) -> 3(x1)
     , 2(4(x1)) -> 0(7(x1))
     , 6(2(x1)) -> 7(7(x1))
     , 9(x1) -> 6(7(x1))
     , 4(x1) -> 9(6(6(x1)))
     , 9(5(9(x1))) -> 5(7(x1))
     , 6(9(x1)) -> 9(x1)
     , 7(0(x1)) -> 9(3(x1))
     , 7(2(x1)) -> 4(x1)
     , 9(7(x1)) -> 7(5(x1))
     , 5(2(6(x1))) -> 6(2(4(x1)))
     , 4(7(x1)) -> 1(3(x1))
     , 2(8(x1)) -> 7(x1)
     , 5(3(x1)) -> 6(0(x1))
     , 4(x1) -> 5(2(3(x1)))
     , 5(9(x1)) -> 0(x1)
     , 2(8(x1)) -> 4(x1)
     , 2(8(1(x1))) -> 8(x1)
     , 2(7(x1)) -> 1(8(x1))}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..