Problem Rubio 04 gm

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Rubio 04 gm

stdout:

MAYBE

Problem:
minus(X,0()) -> X
minus(s(X),s(Y)) -> p(minus(X,Y))
p(s(X)) -> X
div(0(),s(Y)) -> 0()
div(s(X),s(Y)) -> s(div(minus(X,Y),s(Y)))

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Rubio 04 gm

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Rubio 04 gm

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:
    {  minus(X, 0()) -> X
     , minus(s(X), s(Y)) -> p(minus(X, Y))
     , p(s(X)) -> X
     , div(0(), s(Y)) -> 0()
     , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))}

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:
         {  minus(X, 0()) -> X
          , minus(s(X), s(Y)) -> p(minus(X, Y))
          , p(s(X)) -> X
          , div(0(), s(Y)) -> 0()
          , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))}

     Proof Output:
       The following argument positions are usable:
         Uargs(minus) = {}, Uargs(s) = {1}, Uargs(p) = {1}, Uargs(div) = {1}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        minus(x1, x2) = [1] x1 + [0] x2 + [1]
        0() = [4]
        s(x1) = [1] x1 + [4]
        p(x1) = [1] x1 + [0]
        div(x1, x2) = [2] x1 + [0] x2 + [0]

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Rubio 04 gm

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Rubio 04 gm

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  minus(X, 0()) -> X
     , minus(s(X), s(Y)) -> p(minus(X, Y))
     , p(s(X)) -> X
     , div(0(), s(Y)) -> 0()
     , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))}

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:
         {  minus(X, 0()) -> X
          , minus(s(X), s(Y)) -> p(minus(X, Y))
          , p(s(X)) -> X
          , div(0(), s(Y)) -> 0()
          , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))}

     Proof Output:
       The following argument positions are usable:
         Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(p) = {1},
         Uargs(div) = {1}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        minus(x1, x2) = [1] x1 + [0] x2 + [1]
        0() = [0]
        s(x1) = [1] x1 + [2]
        p(x1) = [1] x1 + [0]
        div(x1, x2) = [3] x1 + [3] x2 + [0]