Problem Strategy outermost added 08 Ex1 Luc04b Z

Tool CaT

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

stdout:

MAYBE

Problem:
nats() -> cons(0(),n__incr(nats()))
pairs() -> cons(0(),n__incr(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)
activate(n__incr(X)) -> incr(X)
activate(X) -> X

Proof:
Complexity Transformation Processor:
  strict:
   nats() -> cons(0(),n__incr(nats()))
   pairs() -> cons(0(),n__incr(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)
   activate(n__incr(X)) -> incr(X)
   activate(X) -> X
  weak:

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

     [head](x0) = x0 + 6,

     [activate](x0) = x0 + 33,

     [s](x0) = x0 + 22,

     [incr](x0) = x0 + 15,

     [odds] = 19,

     [pairs] = 33,

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

     [n__incr](x0) = x0 + 7,

     [0] = 2,

     [nats] = 122
    orientation:
     nats() = 122 >= 245 = cons(0(),n__incr(nats()))

     pairs() = 33 >= 142 = cons(0(),n__incr(odds()))

     odds() = 19 >= 48 = incr(pairs())

     incr(cons(X,XS)) = X + XS + 129 >= X + XS + 176 = cons(s(X),n__incr(activate(XS)))

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

     tail(cons(X,XS)) = X + XS + 128 >= XS + 33 = activate(XS)

     incr(X) = X + 15 >= X + 7 = n__incr(X)

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

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

       [head](x0) = x0,

       [activate](x0) = x0 + 1,

       [s](x0) = x0,

       [incr](x0) = x0 + 6,

       [odds] = 20,

       [pairs] = 12,

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

       [n__incr](x0) = x0 + 5,

       [0] = 21,

       [nats] = 6
      orientation:
       nats() = 6 >= 32 = cons(0(),n__incr(nats()))

       pairs() = 12 >= 46 = cons(0(),n__incr(odds()))

       odds() = 20 >= 18 = incr(pairs())

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

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

       tail(cons(X,XS)) = X + XS + 4 >= XS + 1 = activate(XS)

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

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

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

Tool IRC1

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

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

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

stdout:

TIMEOUT

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

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

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

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  nats() -> cons(0(), n__incr(nats()))
     , pairs() -> cons(0(), n__incr(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)
     , activate(n__incr(X)) -> incr(X)
     , activate(X) -> X}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds