Problem Strategy outermost added 08 OvConsOS nosorts-noand Z

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 OvConsOS nosorts-noand Z

stdout:

MAYBE

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

Proof:
Complexity Transformation Processor:
  strict:
   zeros() -> cons(0(),n__zeros())
   U11(tt(),L) -> U12(tt(),activate(L))
   U12(tt(),L) -> s(length(activate(L)))
   U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
   U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
   U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
   length(nil()) -> 0()
   length(cons(N,L)) -> U11(tt(),activate(L))
   take(0(),IL) -> nil()
   take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
   zeros() -> n__zeros()
   take(X1,X2) -> n__take(X1,X2)
   activate(n__zeros()) -> zeros()
   activate(n__take(X1,X2)) -> take(X1,X2)
   activate(X) -> X
  weak:

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

     [nil] = 0,

     [n__take](x0, x1) = x0 + x1 + 32,

     [U23](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 32,

     [U22](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 3,

     [U21](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 32,

     [s](x0) = x0,

     [length](x0) = x0 + 52,

     [U12](x0, x1) = x0 + x1 + 39,

     [activate](x0) = x0 + 6,

     [U11](x0, x1) = x0 + x1 + 6,

     [tt] = 2,

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

     [n__zeros] = 0,

     [0] = 41,

     [zeros] = 0
    orientation:
     zeros() = 0 >= 44 = cons(0(),n__zeros())

     U11(tt(),L) = L + 8 >= L + 47 = U12(tt(),activate(L))

     U12(tt(),L) = L + 41 >= L + 58 = s(length(activate(L)))

     U21(tt(),IL,M,N) = IL + M + N + 34 >= IL + M + N + 23 = U22(tt(),activate(IL),activate(M),activate(N))

     U22(tt(),IL,M,N) = IL + M + N + 5 >= IL + M + N + 52 = U23(tt(),activate(IL),activate(M),activate(N))

     U23(tt(),IL,M,N) = IL + M + N + 34 >= IL + M + N + 53 = cons(activate(N),n__take(activate(M),activate(IL)))

     length(nil()) = 52 >= 41 = 0()

     length(cons(N,L)) = L + N + 55 >= L + 14 = U11(tt(),activate(L))

     take(0(),IL) = IL + 102 >= 0 = nil()

     take(s(M),cons(N,IL)) = IL + M + N + 64 >= IL + M + N + 40 = U21(tt(),activate(IL),M,N)

     zeros() = 0 >= 0 = n__zeros()

     take(X1,X2) = X1 + X2 + 61 >= X1 + X2 + 32 = n__take(X1,X2)

     activate(n__zeros()) = 6 >= 0 = zeros()

     activate(n__take(X1,X2)) = X1 + X2 + 38 >= X1 + X2 + 61 = take(X1,X2)

     activate(X) = X + 6 >= X = X
    problem:
     strict:
      zeros() -> cons(0(),n__zeros())
      U11(tt(),L) -> U12(tt(),activate(L))
      U12(tt(),L) -> s(length(activate(L)))
      U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
      U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
      zeros() -> n__zeros()
      activate(n__take(X1,X2)) -> take(X1,X2)
     weak:
      U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
      length(nil()) -> 0()
      length(cons(N,L)) -> U11(tt(),activate(L))
      take(0(),IL) -> nil()
      take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
      take(X1,X2) -> n__take(X1,X2)
      activate(n__zeros()) -> zeros()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [take](x0, x1) = x0 + x1,

       [nil] = 0,

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

       [U23](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 7,

       [U22](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 11,

       [U21](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 14,

       [s](x0) = x0 + 20,

       [length](x0) = x0,

       [U12](x0, x1) = x0 + x1 + 11,

       [activate](x0) = x0 + 1,

       [U11](x0, x1) = x0 + x1 + 29,

       [tt] = 1,

       [cons](x0, x1) = x0 + x1 + 31,

       [n__zeros] = 0,

       [0] = 0,

       [zeros] = 0
      orientation:
       zeros() = 0 >= 31 = cons(0(),n__zeros())

       U11(tt(),L) = L + 30 >= L + 13 = U12(tt(),activate(L))

       U12(tt(),L) = L + 12 >= L + 21 = s(length(activate(L)))

       U22(tt(),IL,M,N) = IL + M + N + 12 >= IL + M + N + 11 = U23(tt(),activate(IL),activate(M),activate(N))

       U23(tt(),IL,M,N) = IL + M + N + 8 >= IL + M + N + 34 = cons(activate(N),n__take(activate(M),activate(IL)))

       zeros() = 0 >= 0 = n__zeros()

       activate(n__take(X1,X2)) = X1 + X2 + 1 >= X1 + X2 = take(X1,X2)

       U21(tt(),IL,M,N) = IL + M + N + 15 >= IL + M + N + 15 = U22(tt(),activate(IL),activate(M),activate(N))

       length(nil()) = 0 >= 0 = 0()

       length(cons(N,L)) = L + N + 31 >= L + 31 = U11(tt(),activate(L))

       take(0(),IL) = IL >= 0 = nil()

       take(s(M),cons(N,IL)) = IL + M + N + 51 >= IL + M + N + 16 = U21(tt(),activate(IL),M,N)

       take(X1,X2) = X1 + X2 >= X1 + X2 = n__take(X1,X2)

       activate(n__zeros()) = 1 >= 0 = zeros()

       activate(X) = X + 1 >= X = X
      problem:
       strict:
        zeros() -> cons(0(),n__zeros())
        U12(tt(),L) -> s(length(activate(L)))
        U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
        zeros() -> n__zeros()
       weak:
        U11(tt(),L) -> U12(tt(),activate(L))
        U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
        activate(n__take(X1,X2)) -> take(X1,X2)
        U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
        length(nil()) -> 0()
        length(cons(N,L)) -> U11(tt(),activate(L))
        take(0(),IL) -> nil()
        take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
        take(X1,X2) -> n__take(X1,X2)
        activate(n__zeros()) -> zeros()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [take](x0, x1) = x0 + x1,

         [nil] = 20,

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

         [U23](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 16,

         [U22](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 16,

         [U21](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 16,

         [s](x0) = x0,

         [length](x0) = x0,

         [U12](x0, x1) = x0 + x1 + 29,

         [activate](x0) = x0,

         [U11](x0, x1) = x0 + x1 + 29,

         [tt] = 0,

         [cons](x0, x1) = x0 + x1 + 29,

         [n__zeros] = 1,

         [0] = 20,

         [zeros] = 0
        orientation:
         zeros() = 0 >= 50 = cons(0(),n__zeros())

         U12(tt(),L) = L + 29 >= L = s(length(activate(L)))

         U23(tt(),IL,M,N) = IL + M + N + 16 >= IL + M + N + 29 = cons(activate(N),n__take(activate(M),activate(IL)))

         zeros() = 0 >= 1 = n__zeros()

         U11(tt(),L) = L + 29 >= L + 29 = U12(tt(),activate(L))

         U22(tt(),IL,M,N) = IL + M + N + 16 >= IL + M + N + 16 = U23(tt(),activate(IL),activate(M),activate(N))

         activate(n__take(X1,X2)) = X1 + X2 >= X1 + X2 = take(X1,X2)

         U21(tt(),IL,M,N) = IL + M + N + 16 >= IL + M + N + 16 = U22(tt(),activate(IL),activate(M),activate(N))

         length(nil()) = 20 >= 20 = 0()

         length(cons(N,L)) = L + N + 29 >= L + 29 = U11(tt(),activate(L))

         take(0(),IL) = IL + 20 >= 20 = nil()

         take(s(M),cons(N,IL)) = IL + M + N + 29 >= IL + M + N + 16 = U21(tt(),activate(IL),M,N)

         take(X1,X2) = X1 + X2 >= X1 + X2 = n__take(X1,X2)

         activate(n__zeros()) = 1 >= 0 = zeros()

         activate(X) = X >= X = X
        problem:
         strict:
          zeros() -> cons(0(),n__zeros())
          U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
          zeros() -> n__zeros()
         weak:
          U12(tt(),L) -> s(length(activate(L)))
          U11(tt(),L) -> U12(tt(),activate(L))
          U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
          activate(n__take(X1,X2)) -> take(X1,X2)
          U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
          length(nil()) -> 0()
          length(cons(N,L)) -> U11(tt(),activate(L))
          take(0(),IL) -> nil()
          take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
          take(X1,X2) -> n__take(X1,X2)
          activate(n__zeros()) -> zeros()
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [take](x0, x1) = x0 + x1,

           [nil] = 3,

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

           [U23](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 32,

           [U22](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 32,

           [U21](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 32,

           [s](x0) = x0 + 21,

           [length](x0) = x0,

           [U12](x0, x1) = x0 + x1 + 11,

           [activate](x0) = x0,

           [U11](x0, x1) = x0 + x1 + 11,

           [tt] = 10,

           [cons](x0, x1) = x0 + x1 + 21,

           [n__zeros] = 0,

           [0] = 3,

           [zeros] = 0
          orientation:
           zeros() = 0 >= 24 = cons(0(),n__zeros())

           U23(tt(),IL,M,N) = IL + M + N + 42 >= IL + M + N + 21 = cons(activate(N),n__take(activate(M),activate(IL)))

           zeros() = 0 >= 0 = n__zeros()

           U12(tt(),L) = L + 21 >= L + 21 = s(length(activate(L)))

           U11(tt(),L) = L + 21 >= L + 21 = U12(tt(),activate(L))

           U22(tt(),IL,M,N) = IL + M + N + 42 >= IL + M + N + 42 = U23(tt(),activate(IL),activate(M),activate(N))

           activate(n__take(X1,X2)) = X1 + X2 >= X1 + X2 = take(X1,X2)

           U21(tt(),IL,M,N) = IL + M + N + 42 >= IL + M + N + 42 = U22(tt(),activate(IL),activate(M),activate(N))

           length(nil()) = 3 >= 3 = 0()

           length(cons(N,L)) = L + N + 21 >= L + 21 = U11(tt(),activate(L))

           take(0(),IL) = IL + 3 >= 3 = nil()

           take(s(M),cons(N,IL)) = IL + M + N + 42 >= IL + M + N + 42 = U21(tt(),activate(IL),M,N)

           take(X1,X2) = X1 + X2 >= X1 + X2 = n__take(X1,X2)

           activate(n__zeros()) = 0 >= 0 = zeros()

           activate(X) = X >= X = X
          problem:
           strict:
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
           weak:
            U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
            U12(tt(),L) -> s(length(activate(L)))
            U11(tt(),L) -> U12(tt(),activate(L))
            U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
            activate(n__take(X1,X2)) -> take(X1,X2)
            U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
            length(nil()) -> 0()
            length(cons(N,L)) -> U11(tt(),activate(L))
            take(0(),IL) -> nil()
            take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
            take(X1,X2) -> n__take(X1,X2)
            activate(n__zeros()) -> zeros()
            activate(X) -> X
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [take](x0, x1) = x0 + x1 + 18,

             [nil] = 58,

             [n__take](x0, x1) = x0 + x1 + 16,

             [U23](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 36,

             [U22](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 48,

             [U21](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 60,

             [s](x0) = x0 + 40,

             [length](x0) = x0 + 7,

             [U12](x0, x1) = x0 + x1 + 7,

             [activate](x0) = x0 + 4,

             [U11](x0, x1) = x0 + x1 + 11,

             [tt] = 53,

             [cons](x0, x1) = x0 + x1 + 61,

             [n__zeros] = 17,

             [0] = 40,

             [zeros] = 21
            orientation:
             zeros() = 21 >= 118 = cons(0(),n__zeros())

             zeros() = 21 >= 17 = n__zeros()

             U23(tt(),IL,M,N) = IL + M + N + 89 >= IL + M + N + 89 = cons(activate(N),n__take(activate(M),activate(IL)))

             U12(tt(),L) = L + 60 >= L + 51 = s(length(activate(L)))

             U11(tt(),L) = L + 64 >= L + 64 = U12(tt(),activate(L))

             U22(tt(),IL,M,N) = IL + M + N + 101 >= IL + M + N + 101 = U23(tt(),activate(IL),activate(M),activate(N))

             activate(n__take(X1,X2)) = X1 + X2 + 20 >= X1 + X2 + 18 = take(X1,X2)

             U21(tt(),IL,M,N) = IL + M + N + 113 >= IL + M + N + 113 = U22(tt(),activate(IL),activate(M),activate(N))

             length(nil()) = 65 >= 40 = 0()

             length(cons(N,L)) = L + N + 68 >= L + 68 = U11(tt(),activate(L))

             take(0(),IL) = IL + 58 >= 58 = nil()

             take(s(M),cons(N,IL)) = IL + M + N + 119 >= IL + M + N + 117 = U21(tt(),activate(IL),M,N)

             take(X1,X2) = X1 + X2 + 18 >= X1 + X2 + 16 = n__take(X1,X2)

             activate(n__zeros()) = 21 >= 21 = zeros()

             activate(X) = X + 4 >= X = X
            problem:
             strict:
              zeros() -> cons(0(),n__zeros())
             weak:
              zeros() -> n__zeros()
              U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
              U12(tt(),L) -> s(length(activate(L)))
              U11(tt(),L) -> U12(tt(),activate(L))
              U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
              activate(n__take(X1,X2)) -> take(X1,X2)
              U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
              length(nil()) -> 0()
              length(cons(N,L)) -> U11(tt(),activate(L))
              take(0(),IL) -> nil()
              take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
              take(X1,X2) -> n__take(X1,X2)
              activate(n__zeros()) -> zeros()
              activate(X) -> X
            Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 OvConsOS nosorts-noand Z

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 OvConsOS nosorts-noand Z

stdout:

TIMEOUT

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

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 OvConsOS nosorts-noand Z

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 OvConsOS nosorts-noand Z

stdout:

TIMEOUT

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

Proof Output:
  Computation stopped due to timeout after 60.0 seconds