Problem Mixed TRS perfect

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputMixed TRS perfect

stdout:

MAYBE

Problem:
 perfectp(0()) -> false()
 perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
 f(0(),y,0(),u) -> true()
 f(0(),y,s(z),u) -> false()
 f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
 f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputMixed TRS perfect

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputMixed TRS perfect

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:
    {  perfectp(0()) -> false()
     , perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
     , f(0(), y, 0(), u) -> true()
     , f(0(), y, s(z), u) -> false()
     , f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
     , f(s(x), s(y), z, u) ->
       if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}

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:
         {  perfectp(0()) -> false()
          , perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
          , f(0(), y, 0(), u) -> true()
          , f(0(), y, s(z), u) -> false()
          , f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
          , f(s(x), s(y), z, u) ->
            if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}
     
     Proof Output:    
       The following argument positions are usable:
         Uargs(perfectp) = {}, Uargs(s) = {}, Uargs(f) = {},
         Uargs(minus) = {}, Uargs(if) = {3}, Uargs(le) = {}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        perfectp(x1) = [7] x1 + [1]
        0() = [2]
        false() = [0]
        s(x1) = [1] x1 + [2]
        f(x1, x2, x3, x4) = [2] x1 + [0] x2 + [1] x3 + [3] x4 + [5]
        true() = [0]
        minus(x1, x2) = [1] x1 + [0] x2 + [3]
        if(x1, x2, x3) = [1] x1 + [0] x2 + [1] x3 + [0]
        le(x1, x2) = [0] x1 + [0] x2 + [3]

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputMixed TRS perfect

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputMixed TRS perfect

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  perfectp(0()) -> false()
     , perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
     , f(0(), y, 0(), u) -> true()
     , f(0(), y, s(z), u) -> false()
     , f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
     , f(s(x), s(y), z, u) ->
       if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}

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:
         {  perfectp(0()) -> false()
          , perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
          , f(0(), y, 0(), u) -> true()
          , f(0(), y, s(z), u) -> false()
          , f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
          , f(s(x), s(y), z, u) ->
            if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}
     
     Proof Output:    
       The following argument positions are usable:
         Uargs(perfectp) = {}, Uargs(s) = {}, Uargs(f) = {},
         Uargs(minus) = {}, Uargs(if) = {3}, Uargs(le) = {}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        perfectp(x1) = [7] x1 + [1]
        0() = [2]
        false() = [0]
        s(x1) = [1] x1 + [2]
        f(x1, x2, x3, x4) = [2] x1 + [0] x2 + [1] x3 + [3] x4 + [5]
        true() = [0]
        minus(x1, x2) = [1] x1 + [0] x2 + [3]
        if(x1, x2, x3) = [1] x1 + [0] x2 + [1] x3 + [0]
        le(x1, x2) = [0] x1 + [0] x2 + [3]