Problem Strategy outermost added 08 ExIntrod GM04 FR

Tool CaT

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

stdout:

MAYBE

Problem:
nats() -> adx(zeros())
zeros() -> cons(n__0(),n__zeros())
incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
hd(cons(X,Y)) -> activate(X)
tl(cons(X,Y)) -> activate(Y)
0() -> n__0()
zeros() -> n__zeros()
s(X) -> n__s(X)
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
activate(n__0()) -> 0()
activate(n__zeros()) -> zeros()
activate(n__s(X)) -> s(X)
activate(n__incr(X)) -> incr(activate(X))
activate(n__adx(X)) -> adx(activate(X))
activate(X) -> X

Proof:
Complexity Transformation Processor:
  strict:
   nats() -> adx(zeros())
   zeros() -> cons(n__0(),n__zeros())
   incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
   adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
   hd(cons(X,Y)) -> activate(X)
   tl(cons(X,Y)) -> activate(Y)
   0() -> n__0()
   zeros() -> n__zeros()
   s(X) -> n__s(X)
   incr(X) -> n__incr(X)
   adx(X) -> n__adx(X)
   activate(n__0()) -> 0()
   activate(n__zeros()) -> zeros()
   activate(n__s(X)) -> s(X)
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__adx(X)) -> adx(activate(X))
   activate(X) -> X
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [s](x0) = x0,

     [0] = 0,

     [tl](x0) = x0 + 1,

     [hd](x0) = x0 + 1,

     [n__adx](x0) = x0 + 1,

     [n__incr](x0) = x0,

     [n__s](x0) = x0 + 10,

     [activate](x0) = x0 + 2,

     [incr](x0) = x0 + 4,

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

     [n__zeros] = 6,

     [n__0] = 12,

     [adx](x0) = x0,

     [zeros] = 8,

     [nats] = 0
    orientation:
     nats() = 0 >= 8 = adx(zeros())

     zeros() = 8 >= 29 = cons(n__0(),n__zeros())

     incr(cons(X,Y)) = X + Y + 15 >= X + Y + 25 = cons(n__s(activate(X)),n__incr(activate(Y)))

     adx(cons(X,Y)) = X + Y + 11 >= X + Y + 20 = incr(cons(activate(X),n__adx(activate(Y))))

     hd(cons(X,Y)) = X + Y + 12 >= X + 2 = activate(X)

     tl(cons(X,Y)) = X + Y + 12 >= Y + 2 = activate(Y)

     0() = 0 >= 12 = n__0()

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

     s(X) = X >= X + 10 = n__s(X)

     incr(X) = X + 4 >= X = n__incr(X)

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

     activate(n__0()) = 14 >= 0 = 0()

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

     activate(n__s(X)) = X + 12 >= X = s(X)

     activate(n__incr(X)) = X + 2 >= X + 6 = incr(activate(X))

     activate(n__adx(X)) = X + 3 >= X + 2 = adx(activate(X))

     activate(X) = X + 2 >= X = X
    problem:
     strict:
      nats() -> adx(zeros())
      zeros() -> cons(n__0(),n__zeros())
      incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
      adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
      0() -> n__0()
      s(X) -> n__s(X)
      adx(X) -> n__adx(X)
      activate(n__zeros()) -> zeros()
      activate(n__incr(X)) -> incr(activate(X))
     weak:
      hd(cons(X,Y)) -> activate(X)
      tl(cons(X,Y)) -> activate(Y)
      zeros() -> n__zeros()
      incr(X) -> n__incr(X)
      activate(n__0()) -> 0()
      activate(n__s(X)) -> s(X)
      activate(n__adx(X)) -> adx(activate(X))
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [s](x0) = x0,

       [0] = 0,

       [tl](x0) = x0,

       [hd](x0) = x0,

       [n__adx](x0) = x0,

       [n__incr](x0) = x0 + 25,

       [n__s](x0) = x0,

       [activate](x0) = x0,

       [incr](x0) = x0 + 25,

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

       [n__zeros] = 26,

       [n__0] = 0,

       [adx](x0) = x0,

       [zeros] = 26,

       [nats] = 27
      orientation:
       nats() = 27 >= 26 = adx(zeros())

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

       incr(cons(X,Y)) = X + Y + 25 >= X + Y + 25 = cons(n__s(activate(X)),n__incr(activate(Y)))

       adx(cons(X,Y)) = X + Y >= X + Y + 25 = incr(cons(activate(X),n__adx(activate(Y))))

       0() = 0 >= 0 = n__0()

       s(X) = X >= X = n__s(X)

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

       activate(n__zeros()) = 26 >= 26 = zeros()

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

       hd(cons(X,Y)) = X + Y >= X = activate(X)

       tl(cons(X,Y)) = X + Y >= Y = activate(Y)

       zeros() = 26 >= 26 = n__zeros()

       incr(X) = X + 25 >= X + 25 = n__incr(X)

       activate(n__0()) = 0 >= 0 = 0()

       activate(n__s(X)) = X >= X = s(X)

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

       activate(X) = X >= X = X
      problem:
       strict:
        zeros() -> cons(n__0(),n__zeros())
        incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
        adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
        0() -> n__0()
        s(X) -> n__s(X)
        adx(X) -> n__adx(X)
        activate(n__zeros()) -> zeros()
        activate(n__incr(X)) -> incr(activate(X))
       weak:
        nats() -> adx(zeros())
        hd(cons(X,Y)) -> activate(X)
        tl(cons(X,Y)) -> activate(Y)
        zeros() -> n__zeros()
        incr(X) -> n__incr(X)
        activate(n__0()) -> 0()
        activate(n__s(X)) -> s(X)
        activate(n__adx(X)) -> adx(activate(X))
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [s](x0) = x0,

         [0] = 0,

         [tl](x0) = x0 + 3,

         [hd](x0) = x0 + 4,

         [n__adx](x0) = x0 + 2,

         [n__incr](x0) = x0,

         [n__s](x0) = x0,

         [activate](x0) = x0 + 2,

         [incr](x0) = x0,

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

         [n__zeros] = 0,

         [n__0] = 6,

         [adx](x0) = x0,

         [zeros] = 0,

         [nats] = 0
        orientation:
         zeros() = 0 >= 11 = cons(n__0(),n__zeros())

         incr(cons(X,Y)) = X + Y + 5 >= X + Y + 9 = cons(n__s(activate(X)),n__incr(activate(Y)))

         adx(cons(X,Y)) = X + Y + 5 >= X + Y + 11 = incr(cons(activate(X),n__adx(activate(Y))))

         0() = 0 >= 6 = n__0()

         s(X) = X >= X = n__s(X)

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

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

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

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

         hd(cons(X,Y)) = X + Y + 9 >= X + 2 = activate(X)

         tl(cons(X,Y)) = X + Y + 8 >= Y + 2 = activate(Y)

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

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

         activate(n__0()) = 8 >= 0 = 0()

         activate(n__s(X)) = X + 2 >= X = s(X)

         activate(n__adx(X)) = X + 4 >= X + 2 = adx(activate(X))

         activate(X) = X + 2 >= X = X
        problem:
         strict:
          zeros() -> cons(n__0(),n__zeros())
          incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
          adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
          0() -> n__0()
          s(X) -> n__s(X)
          adx(X) -> n__adx(X)
          activate(n__incr(X)) -> incr(activate(X))
         weak:
          activate(n__zeros()) -> zeros()
          nats() -> adx(zeros())
          hd(cons(X,Y)) -> activate(X)
          tl(cons(X,Y)) -> activate(Y)
          zeros() -> n__zeros()
          incr(X) -> n__incr(X)
          activate(n__0()) -> 0()
          activate(n__s(X)) -> s(X)
          activate(n__adx(X)) -> adx(activate(X))
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [s](x0) = x0,

           [0] = 1,

           [tl](x0) = x0 + 1,

           [hd](x0) = x0 + 16,

           [n__adx](x0) = x0 + 8,

           [n__incr](x0) = x0,

           [n__s](x0) = x0 + 31,

           [activate](x0) = x0 + 1,

           [incr](x0) = x0 + 16,

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

           [n__zeros] = 1,

           [n__0] = 0,

           [adx](x0) = x0,

           [zeros] = 2,

           [nats] = 3
          orientation:
           zeros() = 2 >= 1 = cons(n__0(),n__zeros())

           incr(cons(X,Y)) = X + Y + 16 >= X + Y + 33 = cons(n__s(activate(X)),n__incr(activate(Y)))

           adx(cons(X,Y)) = X + Y >= X + Y + 26 = incr(cons(activate(X),n__adx(activate(Y))))

           0() = 1 >= 0 = n__0()

           s(X) = X >= X + 31 = n__s(X)

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

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

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

           nats() = 3 >= 2 = adx(zeros())

           hd(cons(X,Y)) = X + Y + 16 >= X + 1 = activate(X)

           tl(cons(X,Y)) = X + Y + 1 >= Y + 1 = activate(Y)

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

           incr(X) = X + 16 >= X = n__incr(X)

           activate(n__0()) = 1 >= 1 = 0()

           activate(n__s(X)) = X + 32 >= X = s(X)

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

           activate(X) = X + 1 >= X = X
          problem:
           strict:
            incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
            adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
            s(X) -> n__s(X)
            adx(X) -> n__adx(X)
            activate(n__incr(X)) -> incr(activate(X))
           weak:
            zeros() -> cons(n__0(),n__zeros())
            0() -> n__0()
            activate(n__zeros()) -> zeros()
            nats() -> adx(zeros())
            hd(cons(X,Y)) -> activate(X)
            tl(cons(X,Y)) -> activate(Y)
            zeros() -> n__zeros()
            incr(X) -> n__incr(X)
            activate(n__0()) -> 0()
            activate(n__s(X)) -> s(X)
            activate(n__adx(X)) -> adx(activate(X))
            activate(X) -> X
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [s](x0) = x0,

             [0] = 0,

             [tl](x0) = x0 + 4,

             [hd](x0) = x0 + 2,

             [n__adx](x0) = x0 + 13,

             [n__incr](x0) = x0 + 1,

             [n__s](x0) = x0,

             [activate](x0) = x0,

             [incr](x0) = x0 + 2,

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

             [n__zeros] = 0,

             [n__0] = 0,

             [adx](x0) = x0 + 2,

             [zeros] = 0,

             [nats] = 8
            orientation:
             incr(cons(X,Y)) = X + Y + 2 >= X + Y + 1 = cons(n__s(activate(X)),n__incr(activate(Y)))

             adx(cons(X,Y)) = X + Y + 2 >= X + Y + 15 = incr(cons(activate(X),n__adx(activate(Y))))

             s(X) = X >= X = n__s(X)

             adx(X) = X + 2 >= X + 13 = n__adx(X)

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

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

             0() = 0 >= 0 = n__0()

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

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

             hd(cons(X,Y)) = X + Y + 2 >= X = activate(X)

             tl(cons(X,Y)) = X + Y + 4 >= Y = activate(Y)

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

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

             activate(n__0()) = 0 >= 0 = 0()

             activate(n__s(X)) = X >= X = s(X)

             activate(n__adx(X)) = X + 13 >= X + 2 = adx(activate(X))

             activate(X) = X >= X = X
            problem:
             strict:
              adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
              s(X) -> n__s(X)
              adx(X) -> n__adx(X)
              activate(n__incr(X)) -> incr(activate(X))
             weak:
              incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
              zeros() -> cons(n__0(),n__zeros())
              0() -> n__0()
              activate(n__zeros()) -> zeros()
              nats() -> adx(zeros())
              hd(cons(X,Y)) -> activate(X)
              tl(cons(X,Y)) -> activate(Y)
              zeros() -> n__zeros()
              incr(X) -> n__incr(X)
              activate(n__0()) -> 0()
              activate(n__s(X)) -> s(X)
              activate(n__adx(X)) -> adx(activate(X))
              activate(X) -> X
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [s](x0) = x0 + 8,

               [0] = 1,

               [tl](x0) = x0 + 12,

               [hd](x0) = x0 + 34,

               [n__adx](x0) = x0 + 9,

               [n__incr](x0) = x0,

               [n__s](x0) = x0 + 7,

               [activate](x0) = x0 + 1,

               [incr](x0) = x0 + 9,

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

               [n__zeros] = 0,

               [n__0] = 0,

               [adx](x0) = x0,

               [zeros] = 0,

               [nats] = 32
              orientation:
               adx(cons(X,Y)) = X + Y >= X + Y + 20 = incr(cons(activate(X),n__adx(activate(Y))))

               s(X) = X + 8 >= X + 7 = n__s(X)

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

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

               incr(cons(X,Y)) = X + Y + 9 >= X + Y + 9 = cons(n__s(activate(X)),n__incr(activate(Y)))

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

               0() = 1 >= 0 = n__0()

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

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

               hd(cons(X,Y)) = X + Y + 34 >= X + 1 = activate(X)

               tl(cons(X,Y)) = X + Y + 12 >= Y + 1 = activate(Y)

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

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

               activate(n__0()) = 1 >= 1 = 0()

               activate(n__s(X)) = X + 8 >= X + 8 = s(X)

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

               activate(X) = X + 1 >= X = X
              problem:
               strict:
                adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
                adx(X) -> n__adx(X)
                activate(n__incr(X)) -> incr(activate(X))
               weak:
                s(X) -> n__s(X)
                incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
                zeros() -> cons(n__0(),n__zeros())
                0() -> n__0()
                activate(n__zeros()) -> zeros()
                nats() -> adx(zeros())
                hd(cons(X,Y)) -> activate(X)
                tl(cons(X,Y)) -> activate(Y)
                zeros() -> n__zeros()
                incr(X) -> n__incr(X)
                activate(n__0()) -> 0()
                activate(n__s(X)) -> s(X)
                activate(n__adx(X)) -> adx(activate(X))
                activate(X) -> X
              Open

Tool IRC1

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

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

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

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  nats() -> adx(zeros())
     , zeros() -> cons(n__0(), n__zeros())
     , incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y)))
     , adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y))))
     , hd(cons(X, Y)) -> activate(X)
     , tl(cons(X, Y)) -> activate(Y)
     , 0() -> n__0()
     , zeros() -> n__zeros()
     , s(X) -> n__s(X)
     , incr(X) -> n__incr(X)
     , adx(X) -> n__adx(X)
     , activate(n__0()) -> 0()
     , activate(n__zeros()) -> zeros()
     , activate(n__s(X)) -> s(X)
     , activate(n__incr(X)) -> incr(activate(X))
     , activate(n__adx(X)) -> adx(activate(X))
     , 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 GM04 FR

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

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

stdout:

TIMEOUT

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

Proof Output:
  Computation stopped due to timeout after 60.0 seconds