Problem Rubio 04 bintrees

Tool CaT

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputRubio 04 bintrees

stdout:

YES(?,O(n^1))

Problem:
 concat(leaf(),Y) -> Y
 concat(cons(U,V),Y) -> cons(U,concat(V,Y))
 lessleaves(X,leaf()) -> false()
 lessleaves(leaf(),cons(W,Z)) -> true()
 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {6,5}
   transitions:
    lessleaves1(7,7) -> 6*
    lessleaves1(7,9) -> 6*
    lessleaves1(9,7) -> 6*
    lessleaves1(9,9) -> 6*
    concat1(3,1) -> 7*
    concat1(3,3) -> 7*
    concat1(3,7) -> 7*
    concat1(3,9) -> 7*
    concat1(4,2) -> 7*
    concat1(4,4) -> 9*
    concat1(1,2) -> 7*
    concat1(1,4) -> 7*
    concat1(2,1) -> 7*
    concat1(2,3) -> 7*
    concat1(2,7) -> 7*
    concat1(2,9) -> 7*
    concat1(3,2) -> 7*
    concat1(3,4) -> 7*
    concat1(4,1) -> 7*
    concat1(4,3) -> 7*
    concat1(4,7) -> 7*
    concat1(4,9) -> 7*
    concat1(1,1) -> 7*
    concat1(1,3) -> 7*
    concat1(1,7) -> 7*
    concat1(1,9) -> 7*
    concat1(2,2) -> 7*
    concat1(2,4) -> 9*
    true1() -> 6*
    false1() -> 6*
    cons1(3,7) -> 7,9,5
    cons1(3,9) -> 9,5
    cons1(2,7) -> 7,9,5
    cons1(2,9) -> 9,5
    cons1(4,7) -> 7,9,5
    cons1(4,9) -> 9,5
    cons1(1,7) -> 7,9,5
    cons1(1,9) -> 9,5
    lessleaves2(16,16) -> 6*
    lessleaves2(11,16) -> 6*
    lessleaves2(12,11) -> 6*
    lessleaves2(16,11) -> 6*
    lessleaves2(11,11) -> 6*
    concat2(3,7) -> 11*
    concat2(3,9) -> 12,11
    concat2(2,7) -> 11*
    concat2(2,9) -> 16*
    concat2(4,7) -> 11*
    concat2(4,9) -> 16*
    concat2(1,7) -> 11*
    concat2(1,9) -> 16*
    concat0(3,1) -> 5*
    concat0(3,3) -> 5*
    concat0(4,2) -> 5*
    concat0(4,4) -> 5*
    concat0(1,2) -> 5*
    concat0(1,4) -> 5*
    concat0(2,1) -> 5*
    concat0(2,3) -> 5*
    concat0(3,2) -> 5*
    concat0(3,4) -> 5*
    concat0(4,1) -> 5*
    concat0(4,3) -> 5*
    concat0(1,1) -> 5*
    concat0(1,3) -> 5*
    concat0(2,2) -> 5*
    concat0(2,4) -> 5*
    leaf0() -> 1*
    cons0(3,1) -> 2*
    cons0(3,3) -> 2*
    cons0(4,2) -> 2*
    cons0(4,4) -> 2*
    cons0(1,2) -> 2*
    cons0(1,4) -> 2*
    cons0(2,1) -> 2*
    cons0(2,3) -> 2*
    cons0(3,2) -> 2*
    cons0(3,4) -> 2*
    cons0(4,1) -> 2*
    cons0(4,3) -> 2*
    cons0(1,1) -> 2*
    cons0(1,3) -> 2*
    cons0(2,2) -> 2*
    cons0(2,4) -> 2*
    lessleaves0(3,1) -> 6*
    lessleaves0(3,3) -> 6*
    lessleaves0(4,2) -> 6*
    lessleaves0(4,4) -> 6*
    lessleaves0(1,2) -> 6*
    lessleaves0(1,4) -> 6*
    lessleaves0(2,1) -> 6*
    lessleaves0(2,3) -> 6*
    lessleaves0(3,2) -> 6*
    lessleaves0(3,4) -> 6*
    lessleaves0(4,1) -> 6*
    lessleaves0(4,3) -> 6*
    lessleaves0(1,1) -> 6*
    lessleaves0(1,3) -> 6*
    lessleaves0(2,2) -> 6*
    lessleaves0(2,4) -> 6*
    false0() -> 3*
    true0() -> 4*
    1 -> 7,5
    2 -> 7,5
    3 -> 7,5
    4 -> 7,5
    7 -> 11*
    9 -> 7,16
  problem:
   
  Qed

Tool IRC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputRubio 04 bintrees

stdout:

YES(?,O(n^1))

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputRubio 04 bintrees

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:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}

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:
         {  concat(leaf(), Y) -> Y
          , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
          , lessleaves(X, leaf()) -> false()
          , lessleaves(leaf(), cons(W, Z)) -> true()
          , lessleaves(cons(U, V), cons(W, Z)) ->
            lessleaves(concat(U, V), concat(W, Z))}
     
     Proof Output:    
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  concat_0(2, 2) -> 1
        , concat_1(2, 2) -> 3
        , concat_1(2, 2) -> 4
        , concat_1(2, 2) -> 5
        , concat_1(2, 3) -> 3
        , concat_1(2, 3) -> 4
        , concat_1(2, 3) -> 5
        , concat_2(2, 3) -> 4
        , concat_2(2, 3) -> 5
        , leaf_0() -> 1
        , leaf_0() -> 2
        , leaf_0() -> 3
        , leaf_0() -> 4
        , leaf_0() -> 5
        , cons_0(2, 2) -> 1
        , cons_0(2, 2) -> 2
        , cons_0(2, 2) -> 3
        , cons_0(2, 2) -> 4
        , cons_0(2, 2) -> 5
        , cons_1(2, 3) -> 1
        , cons_1(2, 3) -> 3
        , cons_1(2, 3) -> 4
        , cons_1(2, 3) -> 5
        , lessleaves_0(2, 2) -> 1
        , lessleaves_1(3, 3) -> 1
        , lessleaves_2(4, 5) -> 1
        , false_0() -> 1
        , false_0() -> 2
        , false_0() -> 3
        , false_0() -> 4
        , false_0() -> 5
        , false_1() -> 1
        , true_0() -> 1
        , true_0() -> 2
        , true_0() -> 3
        , true_0() -> 4
        , true_0() -> 5
        , true_1() -> 1}

Tool RC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputRubio 04 bintrees

stdout:

YES(?,O(n^1))

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputRubio 04 bintrees

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}

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:
         {  concat(leaf(), Y) -> Y
          , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
          , lessleaves(X, leaf()) -> false()
          , lessleaves(leaf(), cons(W, Z)) -> true()
          , lessleaves(cons(U, V), cons(W, Z)) ->
            lessleaves(concat(U, V), concat(W, Z))}
     
     Proof Output:    
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  concat_0(2, 2) -> 1
        , concat_1(2, 2) -> 3
        , concat_1(2, 2) -> 4
        , concat_1(2, 2) -> 5
        , concat_1(2, 3) -> 3
        , concat_1(2, 3) -> 4
        , concat_1(2, 3) -> 5
        , concat_2(2, 3) -> 4
        , concat_2(2, 3) -> 5
        , leaf_0() -> 1
        , leaf_0() -> 2
        , leaf_0() -> 3
        , leaf_0() -> 4
        , leaf_0() -> 5
        , cons_0(2, 2) -> 1
        , cons_0(2, 2) -> 2
        , cons_0(2, 2) -> 3
        , cons_0(2, 2) -> 4
        , cons_0(2, 2) -> 5
        , cons_1(2, 3) -> 1
        , cons_1(2, 3) -> 3
        , cons_1(2, 3) -> 4
        , cons_1(2, 3) -> 5
        , lessleaves_0(2, 2) -> 1
        , lessleaves_1(3, 3) -> 1
        , lessleaves_2(4, 5) -> 1
        , false_0() -> 1
        , false_0() -> 2
        , false_0() -> 3
        , false_0() -> 4
        , false_0() -> 5
        , false_1() -> 1
        , true_0() -> 1
        , true_0() -> 2
        , true_0() -> 3
        , true_0() -> 4
        , true_0() -> 5
        , true_1() -> 1}