Problem SK90 4.43

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	SK90 4.43

stdout:

MAYBE

Problem:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))

Proof:
Complexity Transformation Processor:
  strict:
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   +(x,+(y,z)) -> +(+(x,y),z)
   f(g(f(x))) -> f(h(s(0()),x))
   f(g(h(x,y))) -> f(h(s(x),y))
   f(h(x,h(y,z))) -> f(h(+(x,y),z))
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [h](x0, x1) = x0 + x1 + 12,

     [g](x0) = x0 + 3,

     [f](x0) = x0 + 7,

     [s](x0) = x0,

     [+](x0, x1) = x0 + x1 + 1,

     [0] = 1
    orientation:
     +(x,0()) = x + 2 >= x = x

     +(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y))

     +(0(),y) = y + 2 >= y = y

     +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y))

     +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z)

     f(g(f(x))) = x + 17 >= x + 20 = f(h(s(0()),x))

     f(g(h(x,y))) = x + y + 22 >= x + y + 19 = f(h(s(x),y))

     f(h(x,h(y,z))) = x + y + z + 31 >= x + y + z + 20 = f(h(+(x,y),z))
    problem:
     strict:
      +(x,s(y)) -> s(+(x,y))
      +(s(x),y) -> s(+(x,y))
      +(x,+(y,z)) -> +(+(x,y),z)
      f(g(f(x))) -> f(h(s(0()),x))
     weak:
      +(x,0()) -> x
      +(0(),y) -> y
      f(g(h(x,y))) -> f(h(s(x),y))
      f(h(x,h(y,z))) -> f(h(+(x,y),z))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [h](x0, x1) = x0 + x1 + 73,

       [g](x0) = x0 + 72,

       [f](x0) = x0 + 72,

       [s](x0) = x0 + 39,

       [+](x0, x1) = x0 + x1 + 3,

       [0] = 10
      orientation:
       +(x,s(y)) = x + y + 42 >= x + y + 42 = s(+(x,y))

       +(s(x),y) = x + y + 42 >= x + y + 42 = s(+(x,y))

       +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z)

       f(g(f(x))) = x + 216 >= x + 194 = f(h(s(0()),x))

       +(x,0()) = x + 13 >= x = x

       +(0(),y) = y + 13 >= y = y

       f(g(h(x,y))) = x + y + 217 >= x + y + 184 = f(h(s(x),y))

       f(h(x,h(y,z))) = x + y + z + 218 >= x + y + z + 148 = f(h(+(x,y),z))
      problem:
       strict:
        +(x,s(y)) -> s(+(x,y))
        +(s(x),y) -> s(+(x,y))
        +(x,+(y,z)) -> +(+(x,y),z)
       weak:
        f(g(f(x))) -> f(h(s(0()),x))
        +(x,0()) -> x
        +(0(),y) -> y
        f(g(h(x,y))) -> f(h(s(x),y))
        f(h(x,h(y,z))) -> f(h(+(x,y),z))
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 2]
        [0 1]
        interpretation:
                       [1 1]     [1 1]     [0]
         [h](x0, x1) = [0 1]x0 + [0 1]x1 + [1],

                   [1 2]     [1]
         [g](x0) = [0 1]x0 + [0],

                        [0]
         [f](x0) = x0 + [1],

                        [1]
         [s](x0) = x0 + [0],

                            [1 1]     [0]
         [+](x0, x1) = x0 + [0 1]x1 + [1],

               [2]
         [0] = [0]
        orientation:
                         [1 1]    [1]        [1 1]    [1]
         +(x,s(y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))

                         [1 1]    [1]        [1 1]    [1]
         +(s(x),y) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))

                           [1 1]    [1 2]    [1]        [1 1]    [1 1]    [0]
         +(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z)

                      [1 2]    [3]    [1 1]    [3]
         f(g(f(x))) = [0 1]x + [2] >= [0 1]x + [2] = f(h(s(0()),x))

                        [2]
         +(x,0()) = x + [1] >= x = x

                    [1 1]    [2]
         +(0(),y) = [0 1]y + [1] >= y = y

                        [1 3]    [1 3]    [3]    [1 1]    [1 1]    [1]
         f(g(h(x,y))) = [0 1]x + [0 1]y + [2] >= [0 1]x + [0 1]y + [2] = f(h(s(x),y))

                          [1 1]    [1 2]    [1 2]    [1]    [1 1]    [1 2]    [1 1]    [1]
         f(h(x,h(y,z))) = [0 1]x + [0 1]y + [0 1]z + [3] >= [0 1]x + [0 1]y + [0 1]z + [3] = f(h(+(x,y),z))
        problem:
         strict:
          +(x,s(y)) -> s(+(x,y))
          +(s(x),y) -> s(+(x,y))
         weak:
          +(x,+(y,z)) -> +(+(x,y),z)
          f(g(f(x))) -> f(h(s(0()),x))
          +(x,0()) -> x
          +(0(),y) -> y
          f(g(h(x,y))) -> f(h(s(x),y))
          f(h(x,h(y,z))) -> f(h(+(x,y),z))
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 2]
          [0 1]
          interpretation:
                              [1 1]
           [h](x0, x1) = x0 + [0 1]x1,

                     [1 2]     [1]
           [g](x0) = [0 1]x0 + [2],

                          [1]
           [f](x0) = x0 + [0],

                          [0]
           [s](x0) = x0 + [2],

                              [1 1]
           [+](x0, x1) = x0 + [0 1]x1,

                 [0]
           [0] = [0]
          orientation:
                           [1 1]    [2]        [1 1]    [0]
           +(x,s(y)) = x + [0 1]y + [2] >= x + [0 1]y + [2] = s(+(x,y))

                           [1 1]    [0]        [1 1]    [0]
           +(s(x),y) = x + [0 1]y + [2] >= x + [0 1]y + [2] = s(+(x,y))

                             [1 1]    [1 2]         [1 1]    [1 1]
           +(x,+(y,z)) = x + [0 1]y + [0 1]z >= x + [0 1]y + [0 1]z = +(+(x,y),z)

                        [1 2]    [3]    [1 1]    [1]
           f(g(f(x))) = [0 1]x + [2] >= [0 1]x + [2] = f(h(s(0()),x))


           +(x,0()) = x >= x = x

                      [1 1]
           +(0(),y) = [0 1]y >= y = y

                          [1 2]    [1 3]    [2]        [1 1]    [1]
           f(g(h(x,y))) = [0 1]x + [0 1]y + [2] >= x + [0 1]y + [2] = f(h(s(x),y))

                                [1 1]    [1 2]    [1]        [1 1]    [1 1]    [1]
           f(h(x,h(y,z))) = x + [0 1]y + [0 1]z + [0] >= x + [0 1]y + [0 1]z + [0] = f(h(+(x,y),z))
          problem:
           strict:
            +(s(x),y) -> s(+(x,y))
           weak:
            +(x,s(y)) -> s(+(x,y))
            +(x,+(y,z)) -> +(+(x,y),z)
            f(g(f(x))) -> f(h(s(0()),x))
            +(x,0()) -> x
            +(0(),y) -> y
            f(g(h(x,y))) -> f(h(s(x),y))
            f(h(x,h(y,z))) -> f(h(+(x,y),z))
          Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	SK90 4.43

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	SK90 4.43

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool pair1rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair2rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3irc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool tup3irc

Execution Time	63.132195ms
Answer	TIMEOUT
Input	SK90 4.43

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , +(0(), y) -> y
     , +(s(x), y) -> s(+(x, y))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , f(g(f(x))) -> f(h(s(0()), x))
     , f(g(h(x, y))) -> f(h(s(x), y))
     , f(h(x, h(y, z))) -> f(h(+(x, y), z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..