Problem Strategy outermost added 08 OvConsOS nosorts-noand FR

Tool CaT

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

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(activate(X1),activate(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(activate(X1),activate(X2))
   activate(X) -> X
  weak:

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

     [nil] = 0,

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

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

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

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

     [s](x0) = x0 + 4,

     [length](x0) = x0 + 16,

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

     [activate](x0) = x0 + 1,

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

     [tt] = 25,

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

     [n__zeros] = 1,

     [0] = 2,

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

     U11(tt(),L) = L + 45 >= L + 32 = U12(tt(),activate(L))

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

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

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

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

     length(nil()) = 16 >= 2 = 0()

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

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

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

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

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

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

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

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

       [nil] = 40,

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

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

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

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

       [s](x0) = x0 + 50,

       [length](x0) = x0,

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

       [activate](x0) = x0 + 8,

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

       [tt] = 57,

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

       [n__zeros] = 16,

       [0] = 40,

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

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

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

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

       zeros() = 24 >= 16 = n__zeros()

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

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

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

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

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

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

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

       activate(n__zeros()) = 24 >= 24 = zeros()

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

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

         [nil] = 56,

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

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

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

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

         [s](x0) = x0 + 69,

         [length](x0) = x0,

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

         [activate](x0) = x0 + 20,

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

         [tt] = 35,

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

         [n__zeros] = 0,

         [0] = 56,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

         activate(X) = X + 20 >= X = X
        problem:
         strict:
          zeros() -> cons(0(),n__zeros())
          U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
          length(cons(N,L)) -> U11(tt(),activate(L))
          take(X1,X2) -> n__take(X1,X2)
         weak:
          take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
          zeros() -> 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)))
          length(nil()) -> 0()
          take(0(),IL) -> nil()
          activate(n__zeros()) -> zeros()
          activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
          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 + 9,

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

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

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

           [s](x0) = x0 + 10,

           [length](x0) = x0,

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

           [activate](x0) = x0,

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

           [tt] = 8,

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

           [n__zeros] = 8,

           [0] = 0,

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

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

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

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

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

           zeros() = 8 >= 8 = n__zeros()

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

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

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

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

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

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

           activate(n__zeros()) = 8 >= 8 = zeros()

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

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

             [nil] = 57,

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

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

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

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

             [s](x0) = x0 + 32,

             [length](x0) = x0,

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

             [activate](x0) = x0 + 2,

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

             [tt] = 34,

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

             [n__zeros] = 16,

             [0] = 0,

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

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

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

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

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

             zeros() = 18 >= 16 = n__zeros()

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

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

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

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

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

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

             activate(n__zeros()) = 18 >= 18 = zeros()

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

             activate(X) = X + 2 >= X = X
            problem:
             strict:
              length(cons(N,L)) -> U11(tt(),activate(L))
              take(X1,X2) -> n__take(X1,X2)
             weak:
              zeros() -> cons(0(),n__zeros())
              U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
              take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
              zeros() -> 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)))
              length(nil()) -> 0()
              take(0(),IL) -> nil()
              activate(n__zeros()) -> zeros()
              activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
              activate(X) -> X
            Open

Tool IRC1

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

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 OvConsOS nosorts-noand 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())
     , 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(activate(X1), activate(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 FR

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

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

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(activate(X1), activate(X2))
     , activate(X) -> X}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds