Problem Strategy outermost added 08 LengthOfFiniteLists nosorts iGM

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Strategy outermost added 08 LengthOfFiniteLists nosorts iGM

stdout:

YES(?,O(n^1))

Problem:
active(zeros()) -> mark(cons(0(),zeros()))
active(and(tt(),X)) -> mark(X)
active(length(nil())) -> mark(0())
active(length(cons(N,L))) -> mark(s(length(L)))
mark(zeros()) -> active(zeros())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(tt()) -> active(tt())
mark(length(X)) -> active(length(mark(X)))
mark(nil()) -> active(nil())
mark(s(X)) -> active(s(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
length(mark(X)) -> length(X)
length(active(X)) -> length(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)

Proof:
Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {10,9,8,7,6,5}
   transitions:
    active1(15) -> 6*
    active1(14) -> 6*
    nil1() -> 14*
    tt1() -> 14*
    01() -> 15*
    zeros1() -> 14*
    mark1(16) -> 5*
    cons1(15,14) -> 16*
    active2(26) -> 5*
    active2(18) -> 25*
    cons2(18,17) -> 19*
    cons2(25,14) -> 26*
    mark2(15) -> 25*
    mark2(19) -> 6*
    02() -> 18*
    active0(2) -> 5*
    active0(4) -> 5*
    active0(1) -> 5*
    active0(3) -> 5*
    zeros2() -> 17*
    zeros0() -> 1*
    cons3(27,17) -> 28*
    cons3(18,14) -> 26*
    cons3(15,14) -> 26*
    mark0(2) -> 6*
    mark0(4) -> 6*
    mark0(1) -> 6*
    mark0(3) -> 6*
    active3(32) -> 27*
    active3(28) -> 6*
    cons0(3,1) -> 7*
    cons0(3,3) -> 7*
    cons0(4,2) -> 7*
    cons0(4,4) -> 7*
    cons0(1,2) -> 7*
    cons0(1,4) -> 7*
    cons0(2,1) -> 7*
    cons0(2,3) -> 7*
    cons0(3,2) -> 7*
    cons0(3,4) -> 7*
    cons0(4,1) -> 7*
    cons0(4,3) -> 7*
    cons0(1,1) -> 7*
    cons0(1,3) -> 7*
    cons0(2,2) -> 7*
    cons0(2,4) -> 7*
    mark3(18) -> 27*
    00() -> 2*
    cons4(18,17) -> 28*
    cons4(32,17) -> 28*
    and0(3,1) -> 8*
    and0(3,3) -> 8*
    and0(4,2) -> 8*
    and0(4,4) -> 8*
    and0(1,2) -> 8*
    and0(1,4) -> 8*
    and0(2,1) -> 8*
    and0(2,3) -> 8*
    and0(3,2) -> 8*
    and0(3,4) -> 8*
    and0(4,1) -> 8*
    and0(4,3) -> 8*
    and0(1,1) -> 8*
    and0(1,3) -> 8*
    and0(2,2) -> 8*
    and0(2,4) -> 8*
    03() -> 32*
    tt0() -> 3*
    length0(2) -> 9*
    length0(4) -> 9*
    length0(1) -> 9*
    length0(3) -> 9*
    nil0() -> 4*
    s0(2) -> 10*
    s0(4) -> 10*
    s0(1) -> 10*
    s0(3) -> 10*
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Strategy outermost added 08 LengthOfFiniteLists nosorts iGM

stdout:

YES(?,O(n^1))
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Strategy outermost added 08 LengthOfFiniteLists nosorts iGM

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  active(zeros()) -> mark(cons(0(), zeros()))
     , active(and(tt(), X)) -> mark(X)
     , active(length(nil())) -> mark(0())
     , active(length(cons(N, L))) -> mark(s(length(L)))
     , mark(zeros()) -> active(zeros())
     , mark(cons(X1, X2)) -> active(cons(mark(X1), X2))
     , mark(0()) -> active(0())
     , mark(and(X1, X2)) -> active(and(mark(X1), X2))
     , mark(tt()) -> active(tt())
     , mark(length(X)) -> active(length(mark(X)))
     , mark(nil()) -> active(nil())
     , mark(s(X)) -> active(s(mark(X)))
     , cons(mark(X1), X2) -> cons(X1, X2)
     , cons(X1, mark(X2)) -> cons(X1, X2)
     , cons(active(X1), X2) -> cons(X1, X2)
     , cons(X1, active(X2)) -> cons(X1, X2)
     , and(mark(X1), X2) -> and(X1, X2)
     , and(X1, mark(X2)) -> and(X1, X2)
     , and(active(X1), X2) -> and(X1, X2)
     , and(X1, active(X2)) -> and(X1, X2)
     , length(mark(X)) -> length(X)
     , length(active(X)) -> length(X)
     , s(mark(X)) -> s(X)
     , s(active(X)) -> s(X)}

Proof Output:
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:

  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  active(zeros()) -> mark(cons(0(), zeros()))
          , active(and(tt(), X)) -> mark(X)
          , active(length(nil())) -> mark(0())
          , active(length(cons(N, L))) -> mark(s(length(L)))
          , mark(zeros()) -> active(zeros())
          , mark(cons(X1, X2)) -> active(cons(mark(X1), X2))
          , mark(0()) -> active(0())
          , mark(and(X1, X2)) -> active(and(mark(X1), X2))
          , mark(tt()) -> active(tt())
          , mark(length(X)) -> active(length(mark(X)))
          , mark(nil()) -> active(nil())
          , mark(s(X)) -> active(s(mark(X)))
          , cons(mark(X1), X2) -> cons(X1, X2)
          , cons(X1, mark(X2)) -> cons(X1, X2)
          , cons(active(X1), X2) -> cons(X1, X2)
          , cons(X1, active(X2)) -> cons(X1, X2)
          , and(mark(X1), X2) -> and(X1, X2)
          , and(X1, mark(X2)) -> and(X1, X2)
          , and(active(X1), X2) -> and(X1, X2)
          , and(X1, active(X2)) -> and(X1, X2)
          , length(mark(X)) -> length(X)
          , length(active(X)) -> length(X)
          , s(mark(X)) -> s(X)
          , s(active(X)) -> s(X)}

     Proof Output:
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_1(4) -> 1
        , active_1(5) -> 1
        , active_2(6) -> 1
        , active_2(8) -> 7
        , active_3(11) -> 1
        , active_3(13) -> 12
        , zeros_0() -> 2
        , zeros_1() -> 5
        , zeros_2() -> 10
        , mark_0(2) -> 1
        , mark_1(3) -> 1
        , mark_2(4) -> 7
        , mark_2(9) -> 1
        , mark_3(8) -> 12
        , cons_0(2, 2) -> 1
        , cons_1(4, 5) -> 3
        , cons_2(7, 5) -> 6
        , cons_2(8, 10) -> 9
        , cons_3(4, 5) -> 6
        , cons_3(8, 5) -> 6
        , cons_3(12, 10) -> 11
        , cons_4(8, 10) -> 11
        , cons_4(13, 10) -> 11
        , 0_0() -> 2
        , 0_1() -> 4
        , 0_2() -> 8
        , 0_3() -> 13
        , and_0(2, 2) -> 1
        , tt_0() -> 2
        , tt_1() -> 4
        , tt_2() -> 8
        , tt_3() -> 13
        , length_0(2) -> 1
        , nil_0() -> 2
        , nil_1() -> 4
        , nil_2() -> 8
        , nil_3() -> 13
        , s_0(2) -> 1}

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Strategy outermost added 08 LengthOfFiniteLists nosorts iGM

stdout:

YES(?,O(n^1))
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Strategy outermost added 08 LengthOfFiniteLists nosorts iGM

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  active(zeros()) -> mark(cons(0(), zeros()))
     , active(and(tt(), X)) -> mark(X)
     , active(length(nil())) -> mark(0())
     , active(length(cons(N, L))) -> mark(s(length(L)))
     , mark(zeros()) -> active(zeros())
     , mark(cons(X1, X2)) -> active(cons(mark(X1), X2))
     , mark(0()) -> active(0())
     , mark(and(X1, X2)) -> active(and(mark(X1), X2))
     , mark(tt()) -> active(tt())
     , mark(length(X)) -> active(length(mark(X)))
     , mark(nil()) -> active(nil())
     , mark(s(X)) -> active(s(mark(X)))
     , cons(mark(X1), X2) -> cons(X1, X2)
     , cons(X1, mark(X2)) -> cons(X1, X2)
     , cons(active(X1), X2) -> cons(X1, X2)
     , cons(X1, active(X2)) -> cons(X1, X2)
     , and(mark(X1), X2) -> and(X1, X2)
     , and(X1, mark(X2)) -> and(X1, X2)
     , and(active(X1), X2) -> and(X1, X2)
     , and(X1, active(X2)) -> and(X1, X2)
     , length(mark(X)) -> length(X)
     , length(active(X)) -> length(X)
     , s(mark(X)) -> s(X)
     , s(active(X)) -> s(X)}

Proof Output:
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:

  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  active(zeros()) -> mark(cons(0(), zeros()))
          , active(and(tt(), X)) -> mark(X)
          , active(length(nil())) -> mark(0())
          , active(length(cons(N, L))) -> mark(s(length(L)))
          , mark(zeros()) -> active(zeros())
          , mark(cons(X1, X2)) -> active(cons(mark(X1), X2))
          , mark(0()) -> active(0())
          , mark(and(X1, X2)) -> active(and(mark(X1), X2))
          , mark(tt()) -> active(tt())
          , mark(length(X)) -> active(length(mark(X)))
          , mark(nil()) -> active(nil())
          , mark(s(X)) -> active(s(mark(X)))
          , cons(mark(X1), X2) -> cons(X1, X2)
          , cons(X1, mark(X2)) -> cons(X1, X2)
          , cons(active(X1), X2) -> cons(X1, X2)
          , cons(X1, active(X2)) -> cons(X1, X2)
          , and(mark(X1), X2) -> and(X1, X2)
          , and(X1, mark(X2)) -> and(X1, X2)
          , and(active(X1), X2) -> and(X1, X2)
          , and(X1, active(X2)) -> and(X1, X2)
          , length(mark(X)) -> length(X)
          , length(active(X)) -> length(X)
          , s(mark(X)) -> s(X)
          , s(active(X)) -> s(X)}

     Proof Output:
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_1(4) -> 1
        , active_1(5) -> 1
        , active_2(6) -> 1
        , active_2(8) -> 7
        , active_3(11) -> 1
        , active_3(13) -> 12
        , zeros_0() -> 2
        , zeros_1() -> 5
        , zeros_2() -> 10
        , mark_0(2) -> 1
        , mark_1(3) -> 1
        , mark_2(4) -> 7
        , mark_2(9) -> 1
        , mark_3(8) -> 12
        , cons_0(2, 2) -> 1
        , cons_1(4, 5) -> 3
        , cons_2(7, 5) -> 6
        , cons_2(8, 10) -> 9
        , cons_3(4, 5) -> 6
        , cons_3(8, 5) -> 6
        , cons_3(12, 10) -> 11
        , cons_4(8, 10) -> 11
        , cons_4(13, 10) -> 11
        , 0_0() -> 2
        , 0_1() -> 4
        , 0_2() -> 8
        , 0_3() -> 13
        , and_0(2, 2) -> 1
        , tt_0() -> 2
        , tt_1() -> 4
        , tt_2() -> 8
        , tt_3() -> 13
        , length_0(2) -> 1
        , nil_0() -> 2
        , nil_1() -> 4
        , nil_2() -> 8
        , nil_3() -> 13
        , s_0(2) -> 1}