Problem Strategy outermost added 08 ExIntrod GM01 FR

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 ExIntrod GM01 FR

stdout:

MAYBE

Problem:
incr(nil()) -> nil()
incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
adx(nil()) -> nil()
adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
nats() -> adx(zeros())
zeros() -> cons(0(),n__zeros())
head(cons(X,L)) -> X
tail(cons(X,L)) -> activate(L)
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
zeros() -> n__zeros()
activate(n__incr(X)) -> incr(activate(X))
activate(n__adx(X)) -> adx(activate(X))
activate(n__zeros()) -> zeros()
activate(X) -> X

Proof:
Complexity Transformation Processor:
  strict:
   incr(nil()) -> nil()
   incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
   adx(nil()) -> nil()
   adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
   nats() -> adx(zeros())
   zeros() -> cons(0(),n__zeros())
   head(cons(X,L)) -> X
   tail(cons(X,L)) -> activate(L)
   incr(X) -> n__incr(X)
   adx(X) -> n__adx(X)
   zeros() -> n__zeros()
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__adx(X)) -> adx(activate(X))
   activate(n__zeros()) -> zeros()
   activate(X) -> X
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [tail](x0) = x0 + 12,

     [head](x0) = x0 + 3,

     [n__zeros] = 5,

     [0] = 6,

     [zeros] = 5,

     [nats] = 0,

     [n__adx](x0) = x0 + 7,

     [adx](x0) = x0 + 11,

     [n__incr](x0) = x0 + 5,

     [activate](x0) = x0 + 3,

     [s](x0) = x0 + 3,

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

     [incr](x0) = x0 + 9,

     [nil] = 17
    orientation:
     incr(nil()) = 26 >= 17 = nil()

     incr(cons(X,L)) = L + X + 38 >= L + X + 40 = cons(s(X),n__incr(activate(L)))

     adx(nil()) = 28 >= 17 = nil()

     adx(cons(X,L)) = L + X + 40 >= L + X + 48 = incr(cons(X,n__adx(activate(L))))

     nats() = 0 >= 16 = adx(zeros())

     zeros() = 5 >= 40 = cons(0(),n__zeros())

     head(cons(X,L)) = L + X + 32 >= X = X

     tail(cons(X,L)) = L + X + 41 >= L + 3 = activate(L)

     incr(X) = X + 9 >= X + 5 = n__incr(X)

     adx(X) = X + 11 >= X + 7 = n__adx(X)

     zeros() = 5 >= 5 = n__zeros()

     activate(n__incr(X)) = X + 8 >= X + 12 = incr(activate(X))

     activate(n__adx(X)) = X + 10 >= X + 14 = adx(activate(X))

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

     activate(X) = X + 3 >= X = X
    problem:
     strict:
      incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
      adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
      nats() -> adx(zeros())
      zeros() -> cons(0(),n__zeros())
      zeros() -> n__zeros()
      activate(n__incr(X)) -> incr(activate(X))
      activate(n__adx(X)) -> adx(activate(X))
     weak:
      incr(nil()) -> nil()
      adx(nil()) -> nil()
      head(cons(X,L)) -> X
      tail(cons(X,L)) -> activate(L)
      incr(X) -> n__incr(X)
      adx(X) -> n__adx(X)
      activate(n__zeros()) -> zeros()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [tail](x0) = x0 + 4,

       [head](x0) = x0 + 9,

       [n__zeros] = 3,

       [0] = 1,

       [zeros] = 4,

       [nats] = 0,

       [n__adx](x0) = x0,

       [adx](x0) = x0,

       [n__incr](x0) = x0,

       [activate](x0) = x0 + 8,

       [s](x0) = x0 + 4,

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

       [incr](x0) = x0,

       [nil] = 0
      orientation:
       incr(cons(X,L)) = L + X + 8 >= L + X + 20 = cons(s(X),n__incr(activate(L)))

       adx(cons(X,L)) = L + X + 8 >= L + X + 16 = incr(cons(X,n__adx(activate(L))))

       nats() = 0 >= 4 = adx(zeros())

       zeros() = 4 >= 12 = cons(0(),n__zeros())

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

       activate(n__incr(X)) = X + 8 >= X + 8 = incr(activate(X))

       activate(n__adx(X)) = X + 8 >= X + 8 = adx(activate(X))

       incr(nil()) = 0 >= 0 = nil()

       adx(nil()) = 0 >= 0 = nil()

       head(cons(X,L)) = L + X + 17 >= X = X

       tail(cons(X,L)) = L + X + 12 >= L + 8 = activate(L)

       incr(X) = X >= X = n__incr(X)

       adx(X) = X >= X = n__adx(X)

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

       activate(X) = X + 8 >= X = X
      problem:
       strict:
        incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
        adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
        nats() -> adx(zeros())
        zeros() -> cons(0(),n__zeros())
        activate(n__incr(X)) -> incr(activate(X))
        activate(n__adx(X)) -> adx(activate(X))
       weak:
        zeros() -> n__zeros()
        incr(nil()) -> nil()
        adx(nil()) -> nil()
        head(cons(X,L)) -> X
        tail(cons(X,L)) -> activate(L)
        incr(X) -> n__incr(X)
        adx(X) -> n__adx(X)
        activate(n__zeros()) -> zeros()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [tail](x0) = x0 + 4,

         [head](x0) = x0,

         [n__zeros] = 0,

         [0] = 15,

         [zeros] = 0,

         [nats] = 9,

         [n__adx](x0) = x0 + 8,

         [adx](x0) = x0 + 8,

         [n__incr](x0) = x0,

         [activate](x0) = x0 + 1,

         [s](x0) = x0,

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

         [incr](x0) = x0,

         [nil] = 1
        orientation:
         incr(cons(X,L)) = L + X + 11 >= L + X + 12 = cons(s(X),n__incr(activate(L)))

         adx(cons(X,L)) = L + X + 19 >= L + X + 20 = incr(cons(X,n__adx(activate(L))))

         nats() = 9 >= 8 = adx(zeros())

         zeros() = 0 >= 26 = cons(0(),n__zeros())

         activate(n__incr(X)) = X + 1 >= X + 1 = incr(activate(X))

         activate(n__adx(X)) = X + 9 >= X + 9 = adx(activate(X))

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

         incr(nil()) = 1 >= 1 = nil()

         adx(nil()) = 9 >= 1 = nil()

         head(cons(X,L)) = L + X + 11 >= X = X

         tail(cons(X,L)) = L + X + 15 >= L + 1 = activate(L)

         incr(X) = X >= X = n__incr(X)

         adx(X) = X + 8 >= X + 8 = n__adx(X)

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

         activate(X) = X + 1 >= X = X
        problem:
         strict:
          incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
          adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
          zeros() -> cons(0(),n__zeros())
          activate(n__incr(X)) -> incr(activate(X))
          activate(n__adx(X)) -> adx(activate(X))
         weak:
          nats() -> adx(zeros())
          zeros() -> n__zeros()
          incr(nil()) -> nil()
          adx(nil()) -> nil()
          head(cons(X,L)) -> X
          tail(cons(X,L)) -> activate(L)
          incr(X) -> n__incr(X)
          adx(X) -> n__adx(X)
          activate(n__zeros()) -> zeros()
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [tail](x0) = x0 + 32,

           [head](x0) = x0 + 42,

           [n__zeros] = 41,

           [0] = 3,

           [zeros] = 52,

           [nats] = 52,

           [n__adx](x0) = x0,

           [adx](x0) = x0,

           [n__incr](x0) = x0,

           [activate](x0) = x0 + 32,

           [s](x0) = x0 + 39,

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

           [incr](x0) = x0,

           [nil] = 1
          orientation:
           incr(cons(X,L)) = L + X >= L + X + 71 = cons(s(X),n__incr(activate(L)))

           adx(cons(X,L)) = L + X >= L + X + 32 = incr(cons(X,n__adx(activate(L))))

           zeros() = 52 >= 44 = cons(0(),n__zeros())

           activate(n__incr(X)) = X + 32 >= X + 32 = incr(activate(X))

           activate(n__adx(X)) = X + 32 >= X + 32 = adx(activate(X))

           nats() = 52 >= 52 = adx(zeros())

           zeros() = 52 >= 41 = n__zeros()

           incr(nil()) = 1 >= 1 = nil()

           adx(nil()) = 1 >= 1 = nil()

           head(cons(X,L)) = L + X + 42 >= X = X

           tail(cons(X,L)) = L + X + 32 >= L + 32 = activate(L)

           incr(X) = X >= X = n__incr(X)

           adx(X) = X >= X = n__adx(X)

           activate(n__zeros()) = 73 >= 52 = zeros()

           activate(X) = X + 32 >= X = X
          problem:
           strict:
            incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
            adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
            activate(n__incr(X)) -> incr(activate(X))
            activate(n__adx(X)) -> adx(activate(X))
           weak:
            zeros() -> cons(0(),n__zeros())
            nats() -> adx(zeros())
            zeros() -> n__zeros()
            incr(nil()) -> nil()
            adx(nil()) -> nil()
            head(cons(X,L)) -> X
            tail(cons(X,L)) -> activate(L)
            incr(X) -> n__incr(X)
            adx(X) -> n__adx(X)
            activate(n__zeros()) -> zeros()
            activate(X) -> X
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [tail](x0) = x0 + 20,

             [head](x0) = x0 + 21,

             [n__zeros] = 0,

             [0] = 0,

             [zeros] = 0,

             [nats] = 0,

             [n__adx](x0) = x0,

             [adx](x0) = x0,

             [n__incr](x0) = x0 + 32,

             [activate](x0) = x0 + 1,

             [s](x0) = x0,

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

             [incr](x0) = x0 + 49,

             [nil] = 20
            orientation:
             incr(cons(X,L)) = L + X + 49 >= L + X + 33 = cons(s(X),n__incr(activate(L)))

             adx(cons(X,L)) = L + X >= L + X + 50 = incr(cons(X,n__adx(activate(L))))

             activate(n__incr(X)) = X + 33 >= X + 50 = incr(activate(X))

             activate(n__adx(X)) = X + 1 >= X + 1 = adx(activate(X))

             zeros() = 0 >= 0 = cons(0(),n__zeros())

             nats() = 0 >= 0 = adx(zeros())

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

             incr(nil()) = 69 >= 20 = nil()

             adx(nil()) = 20 >= 20 = nil()

             head(cons(X,L)) = L + X + 21 >= X = X

             tail(cons(X,L)) = L + X + 20 >= L + 1 = activate(L)

             incr(X) = X + 49 >= X + 32 = n__incr(X)

             adx(X) = X >= X = n__adx(X)

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

             activate(X) = X + 1 >= X = X
            problem:
             strict:
              adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
              activate(n__incr(X)) -> incr(activate(X))
              activate(n__adx(X)) -> adx(activate(X))
             weak:
              incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
              zeros() -> cons(0(),n__zeros())
              nats() -> adx(zeros())
              zeros() -> n__zeros()
              incr(nil()) -> nil()
              adx(nil()) -> nil()
              head(cons(X,L)) -> X
              tail(cons(X,L)) -> activate(L)
              incr(X) -> n__incr(X)
              adx(X) -> n__adx(X)
              activate(n__zeros()) -> zeros()
              activate(X) -> X
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [tail](x0) = x0,

               [head](x0) = x0 + 20,

               [n__zeros] = 12,

               [0] = 0,

               [zeros] = 12,

               [nats] = 32,

               [n__adx](x0) = x0,

               [adx](x0) = x0 + 1,

               [n__incr](x0) = x0,

               [activate](x0) = x0,

               [s](x0) = x0,

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

               [incr](x0) = x0,

               [nil] = 27
              orientation:
               adx(cons(X,L)) = L + X + 1 >= L + X = incr(cons(X,n__adx(activate(L))))

               activate(n__incr(X)) = X >= X = incr(activate(X))

               activate(n__adx(X)) = X >= X + 1 = adx(activate(X))

               incr(cons(X,L)) = L + X >= L + X = cons(s(X),n__incr(activate(L)))

               zeros() = 12 >= 12 = cons(0(),n__zeros())

               nats() = 32 >= 13 = adx(zeros())

               zeros() = 12 >= 12 = n__zeros()

               incr(nil()) = 27 >= 27 = nil()

               adx(nil()) = 28 >= 27 = nil()

               head(cons(X,L)) = L + X + 20 >= X = X

               tail(cons(X,L)) = L + X >= L = activate(L)

               incr(X) = X >= X = n__incr(X)

               adx(X) = X + 1 >= X = n__adx(X)

               activate(n__zeros()) = 12 >= 12 = zeros()

               activate(X) = X >= X = X
              problem:
               strict:
                activate(n__incr(X)) -> incr(activate(X))
                activate(n__adx(X)) -> adx(activate(X))
               weak:
                adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
                incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
                zeros() -> cons(0(),n__zeros())
                nats() -> adx(zeros())
                zeros() -> n__zeros()
                incr(nil()) -> nil()
                adx(nil()) -> nil()
                head(cons(X,L)) -> X
                tail(cons(X,L)) -> activate(L)
                incr(X) -> n__incr(X)
                adx(X) -> n__adx(X)
                activate(n__zeros()) -> zeros()
                activate(X) -> X
              Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 ExIntrod GM01 FR

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 ExIntrod GM01 FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  incr(nil()) -> nil()
     , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L)))
     , adx(nil()) -> nil()
     , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L))))
     , nats() -> adx(zeros())
     , zeros() -> cons(0(), n__zeros())
     , head(cons(X, L)) -> X
     , tail(cons(X, L)) -> activate(L)
     , incr(X) -> n__incr(X)
     , adx(X) -> n__adx(X)
     , zeros() -> n__zeros()
     , activate(n__incr(X)) -> incr(activate(X))
     , activate(n__adx(X)) -> adx(activate(X))
     , 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 ExIntrod GM01 FR

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 ExIntrod GM01 FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  incr(nil()) -> nil()
     , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L)))
     , adx(nil()) -> nil()
     , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L))))
     , nats() -> adx(zeros())
     , zeros() -> cons(0(), n__zeros())
     , head(cons(X, L)) -> X
     , tail(cons(X, L)) -> activate(L)
     , incr(X) -> n__incr(X)
     , adx(X) -> n__adx(X)
     , zeros() -> n__zeros()
     , activate(n__incr(X)) -> incr(activate(X))
     , activate(n__adx(X)) -> adx(activate(X))
     , activate(n__zeros()) -> zeros()
     , activate(X) -> X}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds