Problem Strategy outermost added 08 OvConsOS nosorts FR

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 OvConsOS nosorts FR

stdout:

MAYBE

Problem:
 zeros() -> cons(0(),n__zeros())
 and(tt(),X) -> activate(X)
 length(nil()) -> 0()
 length(cons(N,L)) -> s(length(activate(L)))
 take(0(),IL) -> nil()
 take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
 zeros() -> n__zeros()
 take(X1,X2) -> n__take(X1,X2)
 activate(n__zeros()) -> zeros()
 activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
 activate(X) -> X

Proof:
 Complexity Transformation Processor:
  strict:
   zeros() -> cons(0(),n__zeros())
   and(tt(),X) -> activate(X)
   length(nil()) -> 0()
   length(cons(N,L)) -> s(length(activate(L)))
   take(0(),IL) -> nil()
   take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
   zeros() -> n__zeros()
   take(X1,X2) -> n__take(X1,X2)
   activate(n__zeros()) -> zeros()
   activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
   activate(X) -> X
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [n__take](x0, x1) = x0 + x1 + 1,
     
     [take](x0, x1) = x0 + x1 + 3,
     
     [s](x0) = x0 + 6,
     
     [length](x0) = x0 + 12,
     
     [nil] = 0,
     
     [activate](x0) = x0 + 1,
     
     [and](x0, x1) = x0 + x1,
     
     [tt] = 0,
     
     [cons](x0, x1) = x0 + x1 + 4,
     
     [n__zeros] = 9,
     
     [0] = 3,
     
     [zeros] = 0
    orientation:
     zeros() = 0 >= 16 = cons(0(),n__zeros())
     
     and(tt(),X) = X >= X + 1 = activate(X)
     
     length(nil()) = 12 >= 3 = 0()
     
     length(cons(N,L)) = L + N + 16 >= L + 19 = s(length(activate(L)))
     
     take(0(),IL) = IL + 6 >= 0 = nil()
     
     take(s(M),cons(N,IL)) = IL + M + N + 13 >= IL + M + N + 6 = cons(N,n__take(M,activate(IL)))
     
     zeros() = 0 >= 9 = n__zeros()
     
     take(X1,X2) = X1 + X2 + 3 >= X1 + X2 + 1 = n__take(X1,X2)
     
     activate(n__zeros()) = 10 >= 0 = zeros()
     
     activate(n__take(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 5 = take(activate(X1),activate(X2))
     
     activate(X) = X + 1 >= X = X
    problem:
     strict:
      zeros() -> cons(0(),n__zeros())
      and(tt(),X) -> activate(X)
      length(cons(N,L)) -> s(length(activate(L)))
      zeros() -> n__zeros()
      activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
     weak:
      length(nil()) -> 0()
      take(0(),IL) -> nil()
      take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
      take(X1,X2) -> n__take(X1,X2)
      activate(n__zeros()) -> zeros()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [n__take](x0, x1) = x0 + x1,
       
       [take](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 31,
       
       [length](x0) = x0,
       
       [nil] = 0,
       
       [activate](x0) = x0 + 1,
       
       [and](x0, x1) = x0 + x1,
       
       [tt] = 4,
       
       [cons](x0, x1) = x0 + x1 + 26,
       
       [n__zeros] = 6,
       
       [0] = 0,
       
       [zeros] = 7
      orientation:
       zeros() = 7 >= 32 = cons(0(),n__zeros())
       
       and(tt(),X) = X + 4 >= X + 1 = activate(X)
       
       length(cons(N,L)) = L + N + 26 >= L + 32 = s(length(activate(L)))
       
       zeros() = 7 >= 6 = n__zeros()
       
       activate(n__take(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 2 = take(activate(X1),activate(X2))
       
       length(nil()) = 0 >= 0 = 0()
       
       take(0(),IL) = IL >= 0 = nil()
       
       take(s(M),cons(N,IL)) = IL + M + N + 57 >= IL + M + N + 27 = cons(N,n__take(M,activate(IL)))
       
       take(X1,X2) = X1 + X2 >= X1 + X2 = n__take(X1,X2)
       
       activate(n__zeros()) = 7 >= 7 = zeros()
       
       activate(X) = X + 1 >= X = X
      problem:
       strict:
        zeros() -> cons(0(),n__zeros())
        length(cons(N,L)) -> s(length(activate(L)))
        activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
       weak:
        and(tt(),X) -> activate(X)
        zeros() -> n__zeros()
        length(nil()) -> 0()
        take(0(),IL) -> nil()
        take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
        take(X1,X2) -> n__take(X1,X2)
        activate(n__zeros()) -> zeros()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [n__take](x0, x1) = x0 + x1,
         
         [take](x0, x1) = x0 + x1,
         
         [s](x0) = x0 + 4,
         
         [length](x0) = x0,
         
         [nil] = 0,
         
         [activate](x0) = x0 + 1,
         
         [and](x0, x1) = x0 + x1 + 1,
         
         [tt] = 0,
         
         [cons](x0, x1) = x0 + x1 + 6,
         
         [n__zeros] = 2,
         
         [0] = 0,
         
         [zeros] = 2
        orientation:
         zeros() = 2 >= 8 = cons(0(),n__zeros())
         
         length(cons(N,L)) = L + N + 6 >= L + 5 = s(length(activate(L)))
         
         activate(n__take(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 2 = take(activate(X1),activate(X2))
         
         and(tt(),X) = X + 1 >= X + 1 = activate(X)
         
         zeros() = 2 >= 2 = n__zeros()
         
         length(nil()) = 0 >= 0 = 0()
         
         take(0(),IL) = IL >= 0 = nil()
         
         take(s(M),cons(N,IL)) = IL + M + N + 10 >= IL + M + N + 7 = cons(N,n__take(M,activate(IL)))
         
         take(X1,X2) = X1 + X2 >= X1 + X2 = n__take(X1,X2)
         
         activate(n__zeros()) = 3 >= 2 = zeros()
         
         activate(X) = X + 1 >= X = X
        problem:
         strict:
          zeros() -> cons(0(),n__zeros())
          activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
         weak:
          length(cons(N,L)) -> s(length(activate(L)))
          and(tt(),X) -> activate(X)
          zeros() -> n__zeros()
          length(nil()) -> 0()
          take(0(),IL) -> nil()
          take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
          take(X1,X2) -> n__take(X1,X2)
          activate(n__zeros()) -> zeros()
          activate(X) -> X
        Open
  

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 OvConsOS nosorts FR

stdout:

MAYBE
 Warning when parsing problem:
                             
                               Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputStrategy outermost added 08 OvConsOS nosorts FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  zeros() -> cons(0(), n__zeros())
     , and(tt(), X) -> activate(X)
     , length(nil()) -> 0()
     , length(cons(N, L)) -> s(length(activate(L)))
     , take(0(), IL) -> nil()
     , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL)))
     , zeros() -> n__zeros()
     , take(X1, X2) -> n__take(X1, X2)
     , activate(n__zeros()) -> zeros()
     , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
     , activate(X) -> X}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 OvConsOS nosorts FR

stdout:

MAYBE
 Warning when parsing problem:
                             
                               Unsupported strategy 'OUTERMOST'

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputStrategy outermost added 08 OvConsOS nosorts FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  zeros() -> cons(0(), n__zeros())
     , and(tt(), X) -> activate(X)
     , length(nil()) -> 0()
     , length(cons(N, L)) -> s(length(activate(L)))
     , take(0(), IL) -> nil()
     , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL)))
     , zeros() -> n__zeros()
     , take(X1, X2) -> n__take(X1, X2)
     , activate(n__zeros()) -> zeros()
     , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
     , activate(X) -> X}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds