Problem TCT 09 ma8

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	TCT 09 ma8

stdout:

MAYBE

Problem:
f(0(),n) -> g(0(),n)
f(m,0()) -> g(m,0())
f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
g(n,m) -> bot()
p(m,n) -> bot()
h(k,l,m,n) -> bot()

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	TCT 09 ma8

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	TCT 09 ma8

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:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}

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:
         {  f(0(), n) -> g(0(), n)
          , f(m, 0()) -> g(m, 0())
          , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
          , g(n, m) -> bot()
          , p(m, n) -> bot()
          , h(k, l, m, n) -> bot()}

     Proof Output:
       The following argument positions are usable:
         Uargs(f) = {2}, Uargs(g) = {}, Uargs(s) = {}, Uargs(h) = {3, 4},
         Uargs(p) = {}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        f(x1, x2) = [0] x1 + [1] x2 + [2]
        0() = [0]
        g(x1, x2) = [0] x1 + [0] x2 + [1]
        s(x1) = [1] x1 + [6]
        h(x1, x2, x3, x4) = [0] x1 + [0] x2 + [1] x3 + [1] x4 + [1]
        p(x1, x2) = [0] x1 + [0] x2 + [1]
        bot() = [0]

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	TCT 09 ma8

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	TCT 09 ma8

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}

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:
         {  f(0(), n) -> g(0(), n)
          , f(m, 0()) -> g(m, 0())
          , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
          , g(n, m) -> bot()
          , p(m, n) -> bot()
          , h(k, l, m, n) -> bot()}

     Proof Output:
       The following argument positions are usable:
         Uargs(f) = {2}, Uargs(g) = {2}, Uargs(s) = {}, Uargs(h) = {3, 4},
         Uargs(p) = {}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        f(x1, x2) = [0] x1 + [1] x2 + [3]
        0() = [1]
        g(x1, x2) = [0] x1 + [1] x2 + [1]
        s(x1) = [1] x1 + [7]
        h(x1, x2, x3, x4) = [0] x1 + [0] x2 + [1] x3 + [1] x4 + [1]
        p(x1, x2) = [0] x1 + [0] x2 + [2]
        bot() = [0]

Tool pair1rc

Execution Time	Unknown
Answer	TIMEOUT
Input	TCT 09 ma8

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}
  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 pair3irc

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	TCT 09 ma8

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}
  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:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}
  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(f) = {2}, Uargs(g) = {}, Uargs(s) = {}, Uargs(h) = {3, 4},
       Uargs(p) = {}
     We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      f(x1, x2) = [0 0] x1 + [1 2] x2 + [2]
                  [0 0]      [0 0]      [0]
      0() = [0]
            [0]
      g(x1, x2) = [0 0] x1 + [1 1] x2 + [1]
                  [0 0]      [0 0]      [0]
      s(x1) = [1 2] x1 + [1]
              [0 0]      [2]
      h(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1 0] x4 + [1]
                          [0 0]      [0 0]      [0 0]      [0 0]      [0]
      p(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                  [0 0]      [0 0]      [0]
      bot() = [0]
              [0]


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

Tool pair3rc

Execution Time	Unknown
Answer	TIMEOUT
Input	TCT 09 ma8

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}
  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	TCT 09 ma8

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}
  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	75.714935ms
Answer	TIMEOUT
Input	TCT 09 ma8

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(0(), n) -> g(0(), n)
     , f(m, 0()) -> g(m, 0())
     , f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
     , g(n, m) -> bot()
     , p(m, n) -> bot()
     , h(k, l, m, n) -> bot()}
  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..