Problem Strategy outermost added 08 LengthOfFiniteLists nosorts-noand FR

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 LengthOfFiniteLists 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)))
length(nil()) -> 0()
length(cons(N,L)) -> U11(tt(),activate(L))
zeros() -> n__zeros()
activate(n__zeros()) -> zeros()
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)))
   length(nil()) -> 0()
   length(cons(N,L)) -> U11(tt(),activate(L))
   zeros() -> n__zeros()
   activate(n__zeros()) -> zeros()
   activate(X) -> X
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [nil] = 0,

     [s](x0) = x0,

     [length](x0) = x0 + 1,

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

     [activate](x0) = x0 + 15,

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

     [tt] = 18,

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

     [n__zeros] = 24,

     [0] = 2,

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

     U11(tt(),L) = L + 18 >= L + 35 = U12(tt(),activate(L))

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

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

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

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

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

     activate(X) = X + 15 >= X = X
    problem:
     strict:
      zeros() -> cons(0(),n__zeros())
      U11(tt(),L) -> U12(tt(),activate(L))
      length(nil()) -> 0()
      length(cons(N,L)) -> U11(tt(),activate(L))
      zeros() -> n__zeros()
     weak:
      U12(tt(),L) -> s(length(activate(L)))
      activate(n__zeros()) -> zeros()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [nil] = 1,

       [s](x0) = x0 + 33,

       [length](x0) = x0 + 63,

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

       [activate](x0) = x0,

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

       [tt] = 96,

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

       [n__zeros] = 2,

       [0] = 98,

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

       U11(tt(),L) = L + 160 >= L + 96 = U12(tt(),activate(L))

       length(nil()) = 64 >= 98 = 0()

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

       zeros() = 2 >= 2 = n__zeros()

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

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

       activate(X) = X >= X = X
      problem:
       strict:
        zeros() -> cons(0(),n__zeros())
        length(nil()) -> 0()
        length(cons(N,L)) -> U11(tt(),activate(L))
        zeros() -> n__zeros()
       weak:
        U11(tt(),L) -> U12(tt(),activate(L))
        U12(tt(),L) -> s(length(activate(L)))
        activate(n__zeros()) -> zeros()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [nil] = 123,

         [s](x0) = x0 + 123,

         [length](x0) = x0 + 5,

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

         [activate](x0) = x0,

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

         [tt] = 128,

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

         [n__zeros] = 1,

         [0] = 16,

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

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

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

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

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

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

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

         activate(X) = X >= X = X
        problem:
         strict:
          zeros() -> cons(0(),n__zeros())
          length(cons(N,L)) -> U11(tt(),activate(L))
          zeros() -> n__zeros()
         weak:
          length(nil()) -> 0()
          U11(tt(),L) -> U12(tt(),activate(L))
          U12(tt(),L) -> s(length(activate(L)))
          activate(n__zeros()) -> zeros()
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [nil] = 20,

           [s](x0) = x0 + 48,

           [length](x0) = x0 + 42,

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

           [activate](x0) = x0,

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

           [tt] = 48,

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

           [n__zeros] = 0,

           [0] = 62,

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

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

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

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

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

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

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

           activate(X) = X >= X = X
          problem:
           strict:
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
           weak:
            length(cons(N,L)) -> U11(tt(),activate(L))
            length(nil()) -> 0()
            U11(tt(),L) -> U12(tt(),activate(L))
            U12(tt(),L) -> s(length(activate(L)))
            activate(n__zeros()) -> zeros()
            activate(X) -> X
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [nil] = 140,

             [s](x0) = x0 + 10,

             [length](x0) = x0 + 98,

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

             [activate](x0) = x0 + 2,

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

             [tt] = 98,

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

             [n__zeros] = 3,

             [0] = 76,

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

             zeros() = 4 >= 3 = n__zeros()

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

             length(nil()) = 238 >= 76 = 0()

             U11(tt(),L) = L + 122 >= L + 112 = U12(tt(),activate(L))

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

             activate(n__zeros()) = 5 >= 4 = zeros()

             activate(X) = X + 2 >= X = X
            problem:
             strict:
              zeros() -> cons(0(),n__zeros())
             weak:
              zeros() -> n__zeros()
              length(cons(N,L)) -> U11(tt(),activate(L))
              length(nil()) -> 0()
              U11(tt(),L) -> U12(tt(),activate(L))
              U12(tt(),L) -> s(length(activate(L)))
              activate(n__zeros()) -> zeros()
              activate(X) -> X
            Open

Tool IRC1

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

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 LengthOfFiniteLists 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)))
     , length(nil()) -> 0()
     , length(cons(N, L)) -> U11(tt(), activate(L))
     , zeros() -> n__zeros()
     , activate(n__zeros()) -> zeros()
     , 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 LengthOfFiniteLists nosorts-noand FR

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 LengthOfFiniteLists 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)))
     , length(nil()) -> 0()
     , length(cons(N, L)) -> U11(tt(), activate(L))
     , zeros() -> n__zeros()
     , activate(n__zeros()) -> zeros()
     , activate(X) -> X}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds