Problem Strategy outermost added 08 Ex1 Luc04b FR

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 Ex1 Luc04b FR

stdout:

MAYBE

Problem:
nats() -> cons(0(),n__incr(n__nats()))
pairs() -> cons(0(),n__incr(n__odds()))
odds() -> incr(pairs())
incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
head(cons(X,XS)) -> X
tail(cons(X,XS)) -> activate(XS)
incr(X) -> n__incr(X)
nats() -> n__nats()
odds() -> n__odds()
activate(n__incr(X)) -> incr(activate(X))
activate(n__nats()) -> nats()
activate(n__odds()) -> odds()
activate(X) -> X

Proof:
Complexity Transformation Processor:
  strict:
   nats() -> cons(0(),n__incr(n__nats()))
   pairs() -> cons(0(),n__incr(n__odds()))
   odds() -> incr(pairs())
   incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
   head(cons(X,XS)) -> X
   tail(cons(X,XS)) -> activate(XS)
   incr(X) -> n__incr(X)
   nats() -> n__nats()
   odds() -> n__odds()
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__nats()) -> nats()
   activate(n__odds()) -> odds()
   activate(X) -> X
  weak:

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

     [head](x0) = x0 + 144,

     [activate](x0) = x0 + 153,

     [s](x0) = x0 + 84,

     [incr](x0) = x0 + 140,

     [odds] = 0,

     [n__odds] = 12,

     [pairs] = 8,

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

     [n__incr](x0) = x0 + 52,

     [n__nats] = 96,

     [0] = 40,

     [nats] = 0
    orientation:
     nats() = 0 >= 256 = cons(0(),n__incr(n__nats()))

     pairs() = 8 >= 172 = cons(0(),n__incr(n__odds()))

     odds() = 0 >= 148 = incr(pairs())

     incr(cons(X,XS)) = X + XS + 208 >= X + XS + 357 = cons(s(X),n__incr(activate(XS)))

     head(cons(X,XS)) = X + XS + 212 >= X = X

     tail(cons(X,XS)) = X + XS + 76 >= XS + 153 = activate(XS)

     incr(X) = X + 140 >= X + 52 = n__incr(X)

     nats() = 0 >= 96 = n__nats()

     odds() = 0 >= 12 = n__odds()

     activate(n__incr(X)) = X + 205 >= X + 293 = incr(activate(X))

     activate(n__nats()) = 249 >= 0 = nats()

     activate(n__odds()) = 165 >= 0 = odds()

     activate(X) = X + 153 >= X = X
    problem:
     strict:
      nats() -> cons(0(),n__incr(n__nats()))
      pairs() -> cons(0(),n__incr(n__odds()))
      odds() -> incr(pairs())
      incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
      tail(cons(X,XS)) -> activate(XS)
      nats() -> n__nats()
      odds() -> n__odds()
      activate(n__incr(X)) -> incr(activate(X))
     weak:
      head(cons(X,XS)) -> X
      incr(X) -> n__incr(X)
      activate(n__nats()) -> nats()
      activate(n__odds()) -> odds()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [tail](x0) = x0 + 72,

       [head](x0) = x0,

       [activate](x0) = x0 + 179,

       [s](x0) = x0,

       [incr](x0) = x0 + 137,

       [odds] = 0,

       [n__odds] = 81,

       [pairs] = 224,

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

       [n__incr](x0) = x0 + 40,

       [n__nats] = 59,

       [0] = 128,

       [nats] = 238
      orientation:
       nats() = 238 >= 227 = cons(0(),n__incr(n__nats()))

       pairs() = 224 >= 249 = cons(0(),n__incr(n__odds()))

       odds() = 0 >= 361 = incr(pairs())

       incr(cons(X,XS)) = X + XS + 137 >= X + XS + 219 = cons(s(X),n__incr(activate(XS)))

       tail(cons(X,XS)) = X + XS + 72 >= XS + 179 = activate(XS)

       nats() = 238 >= 59 = n__nats()

       odds() = 0 >= 81 = n__odds()

       activate(n__incr(X)) = X + 219 >= X + 316 = incr(activate(X))

       head(cons(X,XS)) = X + XS >= X = X

       incr(X) = X + 137 >= X + 40 = n__incr(X)

       activate(n__nats()) = 238 >= 238 = nats()

       activate(n__odds()) = 260 >= 0 = odds()

       activate(X) = X + 179 >= X = X
      problem:
       strict:
        pairs() -> cons(0(),n__incr(n__odds()))
        odds() -> incr(pairs())
        incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
        tail(cons(X,XS)) -> activate(XS)
        odds() -> n__odds()
        activate(n__incr(X)) -> incr(activate(X))
       weak:
        nats() -> cons(0(),n__incr(n__nats()))
        nats() -> n__nats()
        head(cons(X,XS)) -> X
        incr(X) -> n__incr(X)
        activate(n__nats()) -> nats()
        activate(n__odds()) -> odds()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [tail](x0) = x0,

         [head](x0) = x0 + 8,

         [activate](x0) = x0 + 13,

         [s](x0) = x0 + 6,

         [incr](x0) = x0 + 5,

         [odds] = 0,

         [n__odds] = 2,

         [pairs] = 11,

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

         [n__incr](x0) = x0 + 2,

         [n__nats] = 1,

         [0] = 3,

         [nats] = 13
        orientation:
         pairs() = 11 >= 9 = cons(0(),n__incr(n__odds()))

         odds() = 0 >= 16 = incr(pairs())

         incr(cons(X,XS)) = X + XS + 7 >= X + XS + 23 = cons(s(X),n__incr(activate(XS)))

         tail(cons(X,XS)) = X + XS + 2 >= XS + 13 = activate(XS)

         odds() = 0 >= 2 = n__odds()

         activate(n__incr(X)) = X + 15 >= X + 18 = incr(activate(X))

         nats() = 13 >= 8 = cons(0(),n__incr(n__nats()))

         nats() = 13 >= 1 = n__nats()

         head(cons(X,XS)) = X + XS + 10 >= X = X

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

         activate(n__nats()) = 14 >= 13 = nats()

         activate(n__odds()) = 15 >= 0 = odds()

         activate(X) = X + 13 >= X = X
        problem:
         strict:
          odds() -> incr(pairs())
          incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
          tail(cons(X,XS)) -> activate(XS)
          odds() -> n__odds()
          activate(n__incr(X)) -> incr(activate(X))
         weak:
          pairs() -> cons(0(),n__incr(n__odds()))
          nats() -> cons(0(),n__incr(n__nats()))
          nats() -> n__nats()
          head(cons(X,XS)) -> X
          incr(X) -> n__incr(X)
          activate(n__nats()) -> nats()
          activate(n__odds()) -> odds()
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [tail](x0) = x0 + 64,

           [head](x0) = x0 + 128,

           [activate](x0) = x0 + 68,

           [s](x0) = x0 + 65,

           [incr](x0) = x0 + 4,

           [odds] = 84,

           [n__odds] = 16,

           [pairs] = 44,

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

           [n__incr](x0) = x0 + 1,

           [n__nats] = 139,

           [0] = 12,

           [nats] = 167
          orientation:
           odds() = 84 >= 48 = incr(pairs())

           incr(cons(X,XS)) = X + XS + 19 >= X + XS + 149 = cons(s(X),n__incr(activate(XS)))

           tail(cons(X,XS)) = X + XS + 79 >= XS + 68 = activate(XS)

           odds() = 84 >= 16 = n__odds()

           activate(n__incr(X)) = X + 69 >= X + 72 = incr(activate(X))

           pairs() = 44 >= 44 = cons(0(),n__incr(n__odds()))

           nats() = 167 >= 167 = cons(0(),n__incr(n__nats()))

           nats() = 167 >= 139 = n__nats()

           head(cons(X,XS)) = X + XS + 143 >= X = X

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

           activate(n__nats()) = 207 >= 167 = nats()

           activate(n__odds()) = 84 >= 84 = odds()

           activate(X) = X + 68 >= X = X
          problem:
           strict:
            incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
            activate(n__incr(X)) -> incr(activate(X))
           weak:
            odds() -> incr(pairs())
            tail(cons(X,XS)) -> activate(XS)
            odds() -> n__odds()
            pairs() -> cons(0(),n__incr(n__odds()))
            nats() -> cons(0(),n__incr(n__nats()))
            nats() -> n__nats()
            head(cons(X,XS)) -> X
            incr(X) -> n__incr(X)
            activate(n__nats()) -> nats()
            activate(n__odds()) -> odds()
            activate(X) -> X
          Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 Ex1 Luc04b FR

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 Ex1 Luc04b FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  nats() -> cons(0(), n__incr(n__nats()))
     , pairs() -> cons(0(), n__incr(n__odds()))
     , odds() -> incr(pairs())
     , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS)))
     , head(cons(X, XS)) -> X
     , tail(cons(X, XS)) -> activate(XS)
     , incr(X) -> n__incr(X)
     , nats() -> n__nats()
     , odds() -> n__odds()
     , activate(n__incr(X)) -> incr(activate(X))
     , activate(n__nats()) -> nats()
     , activate(n__odds()) -> odds()
     , 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 Ex1 Luc04b FR

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 Ex1 Luc04b FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  nats() -> cons(0(), n__incr(n__nats()))
     , pairs() -> cons(0(), n__incr(n__odds()))
     , odds() -> incr(pairs())
     , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS)))
     , head(cons(X, XS)) -> X
     , tail(cons(X, XS)) -> activate(XS)
     , incr(X) -> n__incr(X)
     , nats() -> n__nats()
     , odds() -> n__odds()
     , activate(n__incr(X)) -> incr(activate(X))
     , activate(n__nats()) -> nats()
     , activate(n__odds()) -> odds()
     , activate(X) -> X}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds