Problem SK90 4.61

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.61

stdout:

MAYBE

Problem:
 bsort(nil()) -> nil()
 bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
 bubble(nil()) -> nil()
 bubble(.(x,nil())) -> .(x,nil())
 bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
 last(nil()) -> 0()
 last(.(x,nil())) -> x
 last(.(x,.(y,z))) -> last(.(y,z))
 butlast(nil()) -> nil()
 butlast(.(x,nil())) -> nil()
 butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.61

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.61

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  bsort(nil()) -> nil()
     , bsort(.(x, y)) ->
       last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
     , bubble(nil()) -> nil()
     , bubble(.(x, nil())) -> .(x, nil())
     , bubble(.(x, .(y, z))) ->
       if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
     , last(nil()) -> 0()
     , last(.(x, nil())) -> x
     , last(.(x, .(y, z))) -> last(.(y, z))
     , butlast(nil()) -> nil()
     , butlast(.(x, nil())) -> nil()
     , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))}

Proof Output:    
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: bsort^#(nil()) -> c_0()
              , 2: bsort^#(.(x, y)) ->
                   c_1(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))))
              , 3: bubble^#(nil()) -> c_2()
              , 4: bubble^#(.(x, nil())) -> c_3()
              , 5: bubble^#(.(x, .(y, z))) ->
                   c_4(bubble^#(.(x, z)), bubble^#(.(y, z)))
              , 6: last^#(nil()) -> c_5()
              , 7: last^#(.(x, nil())) -> c_6()
              , 8: last^#(.(x, .(y, z))) -> c_7(last^#(.(y, z)))
              , 9: butlast^#(nil()) -> c_8()
              , 10: butlast^#(.(x, nil())) -> c_9()
              , 11: butlast^#(.(x, .(y, z))) -> c_10(butlast^#(.(y, z)))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{11}                                                      [   YES(?,O(n^1))    ]
                |
                `->{10}                                                  [   YES(?,O(n^1))    ]
             
             ->{9}                                                       [    YES(?,O(1))     ]
             
             ->{6}                                                       [    YES(?,O(1))     ]
             
             ->{5}                                                       [       MAYBE        ]
                |
                `->{4}                                                   [         NA         ]
             
             ->{3}                                                       [    YES(?,O(1))     ]
             
             ->{2}                                                       [     inherited      ]
                |
                |->{7}                                                   [         NA         ]
                |
                `->{8}                                                   [     inherited      ]
                    |
                    `->{7}                                               [         NA         ]
             
             ->{1}                                                       [    YES(?,O(1))     ]
             
           
         
         Sub-problems:
         -------------
           * Path {1}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {bsort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(bsort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                bsort^#(x1) = [1] x1 + [7]
                c_0() = [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{8}->{7}.
           
           * Path {2}->{7}: NA
             -----------------
             
             The usable rules for this path are:
             
               {  bsort(nil()) -> nil()
                , bsort(.(x, y)) ->
                  last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
                , bubble(nil()) -> nil()
                , bubble(.(x, nil())) -> .(x, nil())
                , bubble(.(x, .(y, z))) ->
                  if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
                , butlast(nil()) -> nil()
                , butlast(.(x, nil())) -> nil()
                , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))
                , last(nil()) -> 0()
                , last(.(x, nil())) -> x
                , last(.(x, .(y, z))) -> last(.(y, z))}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {2}->{8}: inherited
             ------------------------
             
             This path is subsumed by the proof of path {2}->{8}->{7}.
           
           * Path {2}->{8}->{7}: NA
             ----------------------
             
             The usable rules for this path are:
             
               {  bsort(nil()) -> nil()
                , bsort(.(x, y)) ->
                  last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
                , bubble(nil()) -> nil()
                , bubble(.(x, nil())) -> .(x, nil())
                , bubble(.(x, .(y, z))) ->
                  if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
                , butlast(nil()) -> nil()
                , butlast(.(x, nil())) -> nil()
                , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))
                , last(nil()) -> 0()
                , last(.(x, nil())) -> x
                , last(.(x, .(y, z))) -> last(.(y, z))}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {3}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {bubble^#(nil()) -> c_2()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(bubble^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                bubble^#(x1) = [1] x1 + [7]
                c_2() = [1]
           
           * Path {5}: MAYBE
             ---------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {1, 2},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [3] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [1] x1 + [1] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules:
                 {bubble^#(.(x, .(y, z))) ->
                  c_4(bubble^#(.(x, z)), bubble^#(.(y, z)))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {5}->{4}: NA
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {1, 2},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [1] x1 + [1] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [0] x1 + [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {6}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {last^#(nil()) -> c_5()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(last^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                last^#(x1) = [1] x1 + [7]
                c_5() = [1]
           
           * Path {9}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {butlast^#(nil()) -> c_8()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(butlast^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                butlast^#(x1) = [1] x1 + [7]
                c_8() = [1]
           
           * Path {11}: YES(?,O(n^1))
             ------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [1] x1 + [1] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [3] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [1] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules:
                 {butlast^#(.(x, .(y, z))) -> c_10(butlast^#(.(y, z)))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(.) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                .(x1, x2) = [1] x1 + [1] x2 + [2]
                butlast^#(x1) = [2] x1 + [0]
                c_10(x1) = [1] x1 + [3]
           
           * Path {11}->{10}: YES(?,O(n^1))
             ------------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_4) = {},
                 Uargs(c_7) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3() = [0]
                c_4(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5() = [0]
                c_6() = [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1) = [1] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {butlast^#(.(x, nil())) -> c_9()}
               Weak Rules: {butlast^#(.(x, .(y, z))) -> c_10(butlast^#(.(y, z)))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(.) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [0]
                .(x1, x2) = [1] x1 + [0] x2 + [0]
                butlast^#(x1) = [0] x1 + [1]
                c_9() = [0]
                c_10(x1) = [1] x1 + [0]
    
    2) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    4) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.61

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.61

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  bsort(nil()) -> nil()
     , bsort(.(x, y)) ->
       last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
     , bubble(nil()) -> nil()
     , bubble(.(x, nil())) -> .(x, nil())
     , bubble(.(x, .(y, z))) ->
       if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
     , last(nil()) -> 0()
     , last(.(x, nil())) -> x
     , last(.(x, .(y, z))) -> last(.(y, z))
     , butlast(nil()) -> nil()
     , butlast(.(x, nil())) -> nil()
     , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))}

Proof Output:    
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: bsort^#(nil()) -> c_0()
              , 2: bsort^#(.(x, y)) ->
                   c_1(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))))
              , 3: bubble^#(nil()) -> c_2()
              , 4: bubble^#(.(x, nil())) -> c_3(x)
              , 5: bubble^#(.(x, .(y, z))) ->
                   c_4(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z)))
              , 6: last^#(nil()) -> c_5()
              , 7: last^#(.(x, nil())) -> c_6(x)
              , 8: last^#(.(x, .(y, z))) -> c_7(last^#(.(y, z)))
              , 9: butlast^#(nil()) -> c_8()
              , 10: butlast^#(.(x, nil())) -> c_9()
              , 11: butlast^#(.(x, .(y, z))) -> c_10(x, butlast^#(.(y, z)))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{11}                                                      [   YES(?,O(n^1))    ]
                |
                `->{10}                                                  [   YES(?,O(n^1))    ]
             
             ->{9}                                                       [    YES(?,O(1))     ]
             
             ->{6}                                                       [    YES(?,O(1))     ]
             
             ->{5}                                                       [       MAYBE        ]
                |
                `->{4}                                                   [         NA         ]
             
             ->{3}                                                       [    YES(?,O(1))     ]
             
             ->{2}                                                       [     inherited      ]
                |
                |->{7}                                                   [         NA         ]
                |
                `->{8}                                                   [     inherited      ]
                    |
                    `->{7}                                               [         NA         ]
             
             ->{1}                                                       [    YES(?,O(1))     ]
             
           
         
         Sub-problems:
         -------------
           * Path {1}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0] x5 + [0] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [0] x1 + [0] x2 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {bsort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(bsort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                bsort^#(x1) = [1] x1 + [7]
                c_0() = [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{8}->{7}.
           
           * Path {2}->{7}: NA
             -----------------
             
             The usable rules for this path are:
             
               {  bsort(nil()) -> nil()
                , bsort(.(x, y)) ->
                  last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
                , bubble(nil()) -> nil()
                , bubble(.(x, nil())) -> .(x, nil())
                , bubble(.(x, .(y, z))) ->
                  if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
                , butlast(nil()) -> nil()
                , butlast(.(x, nil())) -> nil()
                , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))
                , last(nil()) -> 0()
                , last(.(x, nil())) -> x
                , last(.(x, .(y, z))) -> last(.(y, z))}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {2}->{8}: inherited
             ------------------------
             
             This path is subsumed by the proof of path {2}->{8}->{7}.
           
           * Path {2}->{8}->{7}: NA
             ----------------------
             
             The usable rules for this path are:
             
               {  bsort(nil()) -> nil()
                , bsort(.(x, y)) ->
                  last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
                , bubble(nil()) -> nil()
                , bubble(.(x, nil())) -> .(x, nil())
                , bubble(.(x, .(y, z))) ->
                  if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
                , butlast(nil()) -> nil()
                , butlast(.(x, nil())) -> nil()
                , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))
                , last(nil()) -> 0()
                , last(.(x, nil())) -> x
                , last(.(x, .(y, z))) -> last(.(y, z))}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {3}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0] x5 + [0] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [0] x1 + [0] x2 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {bubble^#(nil()) -> c_2()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(bubble^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                bubble^#(x1) = [1] x1 + [7]
                c_2() = [1]
           
           * Path {5}: MAYBE
             ---------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {4, 6}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [3] x1 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [1] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [0] x1 + [0] x2 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules:
                 {bubble^#(.(x, .(y, z))) ->
                  c_4(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z)))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {5}->{4}: NA
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {4, 6}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [1] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [3] x1 + [0]
                c_2() = [0]
                c_3(x1) = [1] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [1] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [0] x1 + [0] x2 + [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {6}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0] x5 + [0] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [0] x1 + [0] x2 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {last^#(nil()) -> c_5()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(last^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                last^#(x1) = [1] x1 + [7]
                c_5() = [1]
           
           * Path {9}: YES(?,O(1))
             ---------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0] x5 + [0] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [0] x1 + [0] x2 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {butlast^#(nil()) -> c_8()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(butlast^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                butlast^#(x1) = [1] x1 + [7]
                c_8() = [1]
           
           * Path {11}: YES(?,O(n^1))
             ------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [1] x1 + [1] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0] x5 + [0] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [3] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [1] x1 + [1] x2 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules:
                 {butlast^#(.(x, .(y, z))) -> c_10(x, butlast^#(.(y, z)))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(.) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                .(x1, x2) = [1] x1 + [1] x2 + [1]
                butlast^#(x1) = [1] x1 + [0]
                c_10(x1, x2) = [1] x1 + [1] x2 + [0]
           
           * Path {11}->{10}: YES(?,O(n^1))
             ------------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(bsort) = {}, Uargs(.) = {}, Uargs(last) = {},
                 Uargs(bubble) = {}, Uargs(butlast) = {}, Uargs(if) = {},
                 Uargs(&lt;=) = {}, Uargs(bsort^#) = {}, Uargs(c_1) = {},
                 Uargs(last^#) = {}, Uargs(bubble^#) = {}, Uargs(c_3) = {},
                 Uargs(c_4) = {}, Uargs(c_6) = {}, Uargs(c_7) = {},
                 Uargs(butlast^#) = {}, Uargs(c_10) = {2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                bsort(x1) = [0] x1 + [0]
                nil() = [0]
                .(x1, x2) = [0] x1 + [0] x2 + [0]
                last(x1) = [0] x1 + [0]
                bubble(x1) = [0] x1 + [0]
                butlast(x1) = [0] x1 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                &lt;=(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                bsort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                last^#(x1) = [0] x1 + [0]
                bubble^#(x1) = [0] x1 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                c_4(x1, x2, x3, x4, x5, x6) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0] x5 + [0] x6 + [0]
                c_5() = [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                butlast^#(x1) = [0] x1 + [0]
                c_8() = [0]
                c_9() = [0]
                c_10(x1, x2) = [0] x1 + [1] x2 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {butlast^#(.(x, nil())) -> c_9()}
               Weak Rules:
                 {butlast^#(.(x, .(y, z))) -> c_10(x, butlast^#(.(y, z)))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(.) = {}, Uargs(butlast^#) = {}, Uargs(c_10) = {2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [0]
                .(x1, x2) = [1] x1 + [1] x2 + [2]
                butlast^#(x1) = [2] x1 + [0]
                c_9() = [1]
                c_10(x1, x2) = [0] x1 + [1] x2 + [2]
    
    2) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    4) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    

Tool pair1rc

Execution TimeUnknown
Answer
TIMEOUT
InputSK90 4.61

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  bsort(nil()) -> nil()
     , bsort(.(x, y)) ->
       last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
     , bubble(nil()) -> nil()
     , bubble(.(x, nil())) -> .(x, nil())
     , bubble(.(x, .(y, z))) ->
       if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
     , last(nil()) -> 0()
     , last(.(x, nil())) -> x
     , last(.(x, .(y, z))) -> last(.(y, z))
     , butlast(nil()) -> nil()
     , butlast(.(x, nil())) -> nil()
     , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair2rc

Execution TimeUnknown
Answer
TIMEOUT
InputSK90 4.61

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  bsort(nil()) -> nil()
     , bsort(.(x, y)) ->
       last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
     , bubble(nil()) -> nil()
     , bubble(.(x, nil())) -> .(x, nil())
     , bubble(.(x, .(y, z))) ->
       if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
     , last(nil()) -> 0()
     , last(.(x, nil())) -> x
     , last(.(x, .(y, z))) -> last(.(y, z))
     , butlast(nil()) -> nil()
     , butlast(.(x, nil())) -> nil()
     , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3irc

Execution TimeUnknown
Answer
TIMEOUT
InputSK90 4.61

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  bsort(nil()) -> nil()
     , bsort(.(x, y)) ->
       last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
     , bubble(nil()) -> nil()
     , bubble(.(x, nil())) -> .(x, nil())
     , bubble(.(x, .(y, z))) ->
       if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
     , last(nil()) -> 0()
     , last(.(x, nil())) -> x
     , last(.(x, .(y, z))) -> last(.(y, z))
     , butlast(nil()) -> nil()
     , butlast(.(x, nil())) -> nil()
     , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3rc

Execution TimeUnknown
Answer
TIMEOUT
InputSK90 4.61

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  bsort(nil()) -> nil()
     , bsort(.(x, y)) ->
       last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
     , bubble(nil()) -> nil()
     , bubble(.(x, nil())) -> .(x, nil())
     , bubble(.(x, .(y, z))) ->
       if(&lt;=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
     , last(nil()) -> 0()
     , last(.(x, nil())) -> x
     , last(.(x, .(y, z))) -> last(.(y, z))
     , butlast(nil()) -> nil()
     , butlast(.(x, nil())) -> nil()
     , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..