Problem Strategy outermost added 08 Ex1 GL02a L

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 Ex1 GL02a L

stdout:

MAYBE

Problem:
eq() -> true()
eq() -> eq()
eq() -> false()
inf(X) -> cons()
take(0(),X) -> nil()
take(s(),cons()) -> cons()
length(nil()) -> 0()
length(cons()) -> s()

Proof:
Complexity Transformation Processor:
  strict:
   eq() -> true()
   eq() -> eq()
   eq() -> false()
   inf(X) -> cons()
   take(0(),X) -> nil()
   take(s(),cons()) -> cons()
   length(nil()) -> 0()
   length(cons()) -> s()
  weak:

  Bounds Processor:
   bound: 1
   enrichment: match
   automaton:
    final states: {10,9,8,7}
    transitions:
     true1() -> 11*
     eq0() -> 7*
     true0() -> 1*
     false0() -> 7,2
     inf0(5) -> 8*
     inf0(2) -> 8*
     inf0(4) -> 8*
     inf0(6) -> 8*
     inf0(1) -> 8*
     inf0(3) -> 8*
     cons0() -> 9,8,3
     take0(3,1) -> 9*
     take0(3,3) -> 9*
     take0(3,5) -> 9*
     take0(4,2) -> 9*
     take0(4,4) -> 9*
     take0(4,6) -> 9*
     take0(5,1) -> 9*
     take0(5,3) -> 9*
     take0(5,5) -> 9*
     take0(6,2) -> 9*
     take0(1,2) -> 9*
     take0(6,4) -> 9*
     take0(1,4) -> 9*
     take0(6,6) -> 9*
     take0(1,6) -> 9*
     take0(2,1) -> 9*
     take0(2,3) -> 9*
     take0(2,5) -> 9*
     take0(3,2) -> 9*
     take0(3,4) -> 9*
     take0(3,6) -> 9*
     take0(4,1) -> 9*
     take0(4,3) -> 9*
     take0(4,5) -> 9*
     take0(5,2) -> 9*
     take0(5,4) -> 9*
     take0(5,6) -> 9*
     take0(6,1) -> 9*
     take0(1,1) -> 9*
     take0(6,3) -> 9*
     take0(1,3) -> 9*
     take0(6,5) -> 9*
     take0(1,5) -> 9*
     take0(2,2) -> 9*
     take0(2,4) -> 9*
     take0(2,6) -> 9*
     00() -> 10,4
     nil0() -> 9,5
     s0() -> 10,6
     length0(5) -> 10*
     length0(2) -> 10*
     length0(4) -> 10*
     length0(6) -> 10*
     length0(1) -> 10*
     length0(3) -> 10*
     11 -> 7*
   problem:
    strict:
     eq() -> eq()
     eq() -> false()
     inf(X) -> cons()
     take(0(),X) -> nil()
     take(s(),cons()) -> cons()
     length(nil()) -> 0()
     length(cons()) -> s()
    weak:
     eq() -> true()
   Bounds Processor:
    bound: 1
    enrichment: match
    automaton:
     final states: {10,9,8,7}
     transitions:
      false1() -> 12*
      eq0() -> 7*
      true0() -> 7,6
      false0() -> 1*
      inf0(5) -> 8*
      inf0(2) -> 8*
      inf0(4) -> 8*
      inf0(6) -> 8*
      inf0(1) -> 8*
      inf0(3) -> 8*
      cons0() -> 9,8,2
      take0(3,1) -> 9*
      take0(3,3) -> 9*
      take0(3,5) -> 9*
      take0(4,2) -> 9*
      take0(4,4) -> 9*
      take0(4,6) -> 9*
      take0(5,1) -> 9*
      take0(5,3) -> 9*
      take0(5,5) -> 9*
      take0(6,2) -> 9*
      take0(1,2) -> 9*
      take0(6,4) -> 9*
      take0(1,4) -> 9*
      take0(6,6) -> 9*
      take0(1,6) -> 9*
      take0(2,1) -> 9*
      take0(2,3) -> 9*
      take0(2,5) -> 9*
      take0(3,2) -> 9*
      take0(3,4) -> 9*
      take0(3,6) -> 9*
      take0(4,1) -> 9*
      take0(4,3) -> 9*
      take0(4,5) -> 9*
      take0(5,2) -> 9*
      take0(5,4) -> 9*
      take0(5,6) -> 9*
      take0(6,1) -> 9*
      take0(1,1) -> 9*
      take0(6,3) -> 9*
      take0(1,3) -> 9*
      take0(6,5) -> 9*
      take0(1,5) -> 9*
      take0(2,2) -> 9*
      take0(2,4) -> 9*
      take0(2,6) -> 9*
      00() -> 10,3
      nil0() -> 9,4
      s0() -> 10,5
      length0(5) -> 10*
      length0(2) -> 10*
      length0(4) -> 10*
      length0(6) -> 10*
      length0(1) -> 10*
      length0(3) -> 10*
      12 -> 7*
    problem:
     strict:
      eq() -> eq()
      inf(X) -> cons()
      take(0(),X) -> nil()
      take(s(),cons()) -> cons()
      length(nil()) -> 0()
      length(cons()) -> s()
     weak:
      eq() -> false()
      eq() -> true()
    Bounds Processor:
     bound: 1
     enrichment: match
     automaton:
      final states: {10,9,8,7}
      transitions:
       cons1() -> 12*
       eq0() -> 7*
       true0() -> 7,6
       false0() -> 7,5
       inf0(5) -> 8*
       inf0(2) -> 8*
       inf0(4) -> 8*
       inf0(6) -> 8*
       inf0(1) -> 8*
       inf0(3) -> 8*
       cons0() -> 9,1
       take0(3,1) -> 9*
       take0(3,3) -> 9*
       take0(3,5) -> 9*
       take0(4,2) -> 9*
       take0(4,4) -> 9*
       take0(4,6) -> 9*
       take0(5,1) -> 9*
       take0(5,3) -> 9*
       take0(5,5) -> 9*
       take0(6,2) -> 9*
       take0(1,2) -> 9*
       take0(6,4) -> 9*
       take0(1,4) -> 9*
       take0(6,6) -> 9*
       take0(1,6) -> 9*
       take0(2,1) -> 9*
       take0(2,3) -> 9*
       take0(2,5) -> 9*
       take0(3,2) -> 9*
       take0(3,4) -> 9*
       take0(3,6) -> 9*
       take0(4,1) -> 9*
       take0(4,3) -> 9*
       take0(4,5) -> 9*
       take0(5,2) -> 9*
       take0(5,4) -> 9*
       take0(5,6) -> 9*
       take0(6,1) -> 9*
       take0(1,1) -> 9*
       take0(6,3) -> 9*
       take0(1,3) -> 9*
       take0(6,5) -> 9*
       take0(1,5) -> 9*
       take0(2,2) -> 9*
       take0(2,4) -> 9*
       take0(2,6) -> 9*
       00() -> 10,2
       nil0() -> 9,3
       s0() -> 10,4
       length0(5) -> 10*
       length0(2) -> 10*
       length0(4) -> 10*
       length0(6) -> 10*
       length0(1) -> 10*
       length0(3) -> 10*
       12 -> 8*
     problem:
      strict:
       eq() -> eq()
       take(0(),X) -> nil()
       take(s(),cons()) -> cons()
       length(nil()) -> 0()
       length(cons()) -> s()
      weak:
       inf(X) -> cons()
       eq() -> false()
       eq() -> true()
     Bounds Processor:
      bound: 1
      enrichment: match
      automaton:
       final states: {10,9,8,7}
       transitions:
        nil1() -> 8*
        eq0() -> 7*
        true0() -> 7,6
        false0() -> 7,5
        inf0(5) -> 10*
        inf0(2) -> 10*
        inf0(4) -> 10*
        inf0(6) -> 10*
        inf0(1) -> 10*
        inf0(3) -> 10*
        cons0() -> 10,8,4
        take0(3,1) -> 8*
        take0(3,3) -> 8*
        take0(3,5) -> 8*
        take0(4,2) -> 8*
        take0(4,4) -> 8*
        take0(4,6) -> 8*
        take0(5,1) -> 8*
        take0(5,3) -> 8*
        take0(5,5) -> 8*
        take0(6,2) -> 8*
        take0(1,2) -> 8*
        take0(6,4) -> 8*
        take0(1,4) -> 8*
        take0(6,6) -> 8*
        take0(1,6) -> 8*
        take0(2,1) -> 8*
        take0(2,3) -> 8*
        take0(2,5) -> 8*
        take0(3,2) -> 8*
        take0(3,4) -> 8*
        take0(3,6) -> 8*
        take0(4,1) -> 8*
        take0(4,3) -> 8*
        take0(4,5) -> 8*
        take0(5,2) -> 8*
        take0(5,4) -> 8*
        take0(5,6) -> 8*
        take0(6,1) -> 8*
        take0(1,1) -> 8*
        take0(6,3) -> 8*
        take0(1,3) -> 8*
        take0(6,5) -> 8*
        take0(1,5) -> 8*
        take0(2,2) -> 8*
        take0(2,4) -> 8*
        take0(2,6) -> 8*
        00() -> 9,1
        nil0() -> 2*
        s0() -> 9,3
        length0(5) -> 9*
        length0(2) -> 9*
        length0(4) -> 9*
        length0(6) -> 9*
        length0(1) -> 9*
        length0(3) -> 9*
      problem:
       strict:
        eq() -> eq()
        take(s(),cons()) -> cons()
        length(nil()) -> 0()
        length(cons()) -> s()
       weak:
        take(0(),X) -> nil()
        inf(X) -> cons()
        eq() -> false()
        eq() -> true()
      Bounds Processor:
       bound: 1
       enrichment: match
       automaton:
        final states: {10,9,8,7}
        transitions:
         cons1() -> 8*
         eq0() -> 7*
         true0() -> 7,6
         false0() -> 7,5
         inf0(5) -> 10*
         inf0(2) -> 10*
         inf0(4) -> 10*
         inf0(6) -> 10*
         inf0(1) -> 10*
         inf0(3) -> 10*
         cons0() -> 10,2
         take0(3,1) -> 8*
         take0(3,3) -> 8*
         take0(3,5) -> 8*
         take0(4,2) -> 8*
         take0(4,4) -> 8*
         take0(4,6) -> 8*
         take0(5,1) -> 8*
         take0(5,3) -> 8*
         take0(5,5) -> 8*
         take0(6,2) -> 8*
         take0(1,2) -> 8*
         take0(6,4) -> 8*
         take0(1,4) -> 8*
         take0(6,6) -> 8*
         take0(1,6) -> 8*
         take0(2,1) -> 8*
         take0(2,3) -> 8*
         take0(2,5) -> 8*
         take0(3,2) -> 8*
         take0(3,4) -> 8*
         take0(3,6) -> 8*
         take0(4,1) -> 8*
         take0(4,3) -> 8*
         take0(4,5) -> 8*
         take0(5,2) -> 8*
         take0(5,4) -> 8*
         take0(5,6) -> 8*
         take0(6,1) -> 8*
         take0(1,1) -> 8*
         take0(6,3) -> 8*
         take0(1,3) -> 8*
         take0(6,5) -> 8*
         take0(1,5) -> 8*
         take0(2,2) -> 8*
         take0(2,4) -> 8*
         take0(2,6) -> 8*
         00() -> 9,4
         nil0() -> 8,3
         s0() -> 9,1
         length0(5) -> 9*
         length0(2) -> 9*
         length0(4) -> 9*
         length0(6) -> 9*
         length0(1) -> 9*
         length0(3) -> 9*
       problem:
        strict:
         eq() -> eq()
         length(nil()) -> 0()
         length(cons()) -> s()
        weak:
         take(s(),cons()) -> cons()
         take(0(),X) -> nil()
         inf(X) -> cons()
         eq() -> false()
         eq() -> true()
       Bounds Processor:
        bound: 1
        enrichment: match
        automaton:
         final states: {10,9,8,7}
         transitions:
          01() -> 12*
          eq0() -> 7*
          true0() -> 7,6
          false0() -> 7,5
          inf0(5) -> 10*
          inf0(2) -> 10*
          inf0(4) -> 10*
          inf0(6) -> 10*
          inf0(1) -> 10*
          inf0(3) -> 10*
          cons0() -> 10,9,3
          take0(3,1) -> 9*
          take0(3,3) -> 9*
          take0(3,5) -> 9*
          take0(4,2) -> 9*
          take0(4,4) -> 9*
          take0(4,6) -> 9*
          take0(5,1) -> 9*
          take0(5,3) -> 9*
          take0(5,5) -> 9*
          take0(6,2) -> 9*
          take0(1,2) -> 9*
          take0(6,4) -> 9*
          take0(1,4) -> 9*
          take0(6,6) -> 9*
          take0(1,6) -> 9*
          take0(2,1) -> 9*
          take0(2,3) -> 9*
          take0(2,5) -> 9*
          take0(3,2) -> 9*
          take0(3,4) -> 9*
          take0(3,6) -> 9*
          take0(4,1) -> 9*
          take0(4,3) -> 9*
          take0(4,5) -> 9*
          take0(5,2) -> 9*
          take0(5,4) -> 9*
          take0(5,6) -> 9*
          take0(6,1) -> 9*
          take0(1,1) -> 9*
          take0(6,3) -> 9*
          take0(1,3) -> 9*
          take0(6,5) -> 9*
          take0(1,5) -> 9*
          take0(2,2) -> 9*
          take0(2,4) -> 9*
          take0(2,6) -> 9*
          00() -> 2*
          nil0() -> 9,1
          s0() -> 8,4
          length0(5) -> 8*
          length0(2) -> 8*
          length0(4) -> 8*
          length0(6) -> 8*
          length0(1) -> 8*
          length0(3) -> 8*
          12 -> 8*
        problem:
         strict:
          eq() -> eq()
          length(cons()) -> s()
         weak:
          length(nil()) -> 0()
          take(s(),cons()) -> cons()
          take(0(),X) -> nil()
          inf(X) -> cons()
          eq() -> false()
          eq() -> true()
        Bounds Processor:
         bound: 1
         enrichment: match
         automaton:
          final states: {10,9,8,7}
          transitions:
           s1() -> 12*
           eq0() -> 7*
           true0() -> 7,6
           false0() -> 7,5
           inf0(5) -> 10*
           inf0(2) -> 10*
           inf0(4) -> 10*
           inf0(6) -> 10*
           inf0(1) -> 10*
           inf0(3) -> 10*
           cons0() -> 10,9,1
           take0(3,1) -> 9*
           take0(3,3) -> 9*
           take0(3,5) -> 9*
           take0(4,2) -> 9*
           take0(4,4) -> 9*
           take0(4,6) -> 9*
           take0(5,1) -> 9*
           take0(5,3) -> 9*
           take0(5,5) -> 9*
           take0(6,2) -> 9*
           take0(1,2) -> 9*
           take0(6,4) -> 9*
           take0(1,4) -> 9*
           take0(6,6) -> 9*
           take0(1,6) -> 9*
           take0(2,1) -> 9*
           take0(2,3) -> 9*
           take0(2,5) -> 9*
           take0(3,2) -> 9*
           take0(3,4) -> 9*
           take0(3,6) -> 9*
           take0(4,1) -> 9*
           take0(4,3) -> 9*
           take0(4,5) -> 9*
           take0(5,2) -> 9*
           take0(5,4) -> 9*
           take0(5,6) -> 9*
           take0(6,1) -> 9*
           take0(1,1) -> 9*
           take0(6,3) -> 9*
           take0(1,3) -> 9*
           take0(6,5) -> 9*
           take0(1,5) -> 9*
           take0(2,2) -> 9*
           take0(2,4) -> 9*
           take0(2,6) -> 9*
           00() -> 8,4
           nil0() -> 9,3
           s0() -> 2*
           length0(5) -> 8*
           length0(2) -> 8*
           length0(4) -> 8*
           length0(6) -> 8*
           length0(1) -> 8*
           length0(3) -> 8*
           12 -> 8*
         problem:
          strict:
           eq() -> eq()
          weak:
           length(cons()) -> s()
           length(nil()) -> 0()
           take(s(),cons()) -> cons()
           take(0(),X) -> nil()
           inf(X) -> cons()
           eq() -> false()
           eq() -> true()
         Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 Ex1 GL02a L

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 Ex1 GL02a L

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  eq() -> true()
     , eq() -> eq()
     , eq() -> false()
     , inf(X) -> cons()
     , take(0(), X) -> nil()
     , take(s(), cons()) -> cons()
     , length(nil()) -> 0()
     , length(cons()) -> s()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 Ex1 GL02a L

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 Ex1 GL02a L

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  eq() -> true()
     , eq() -> eq()
     , eq() -> false()
     , inf(X) -> cons()
     , take(0(), X) -> nil()
     , take(s(), cons()) -> cons()
     , length(nil()) -> 0()
     , length(cons()) -> s()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds