Problem Der95 32

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

Problem:
 sort(nil()) -> nil()
 sort(cons(x,y)) -> insert(x,sort(y))
 insert(x,nil()) -> cons(x,nil())
 insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
 choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
 choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
 choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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: sort^#(nil()) -> c_0()
              , 2: sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
              , 3: insert^#(x, nil()) -> c_2()
              , 4: insert^#(x, cons(v, w)) -> c_3(choose^#(x, cons(v, w), x, v))
              , 5: choose^#(x, cons(v, w), y, 0()) -> c_4()
              , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_5(insert^#(x, w))
              , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_6(choose^#(x, cons(v, w), y, z))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2}                                                       [     inherited      ]
                |
                |->{3}                                                   [       MAYBE        ]
                |
                `->{4,6,7}                                               [     inherited      ]
                    |
                    |->{3}                                               [         NA         ]
                    |
                    `->{5}                                               [         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(sort) = {}, Uargs(cons) = {}, Uargs(insert) = {},
                 Uargs(choose) = {}, Uargs(s) = {}, Uargs(sort^#) = {},
                 Uargs(c_1) = {}, Uargs(insert^#) = {}, Uargs(c_3) = {},
                 Uargs(choose^#) = {}, Uargs(c_5) = {}, Uargs(c_6) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                sort(x1) = [0 0 0] x1 + [0]
                           [0 0 0]      [0]
                           [0 0 0]      [0]
                nil() = [0]
                        [0]
                        [0]
                cons(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                               [0 0 0]      [0 0 0]      [0]
                               [0 0 0]      [0 0 0]      [0]
                insert(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                                 [0 0 0]      [0 0 0]      [0]
                                 [0 0 0]      [0 0 0]      [0]
                choose(x1, x2, x3, x4) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 0] x4 + [0]
                                         [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                                         [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                0() = [0]
                      [0]
                      [0]
                s(x1) = [0 0 0] x1 + [0]
                        [0 0 0]      [0]
                        [0 0 0]      [0]
                sort^#(x1) = [0 0 0] x1 + [0]
                             [0 0 0]      [0]
                             [0 0 0]      [0]
                c_0() = [0]
                        [0]
                        [0]
                c_1(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                insert^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                                   [0 0 0]      [0 0 0]      [0]
                                   [0 0 0]      [0 0 0]      [0]
                c_2() = [0]
                        [0]
                        [0]
                c_3(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                choose^#(x1, x2, x3, x4) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 0] x4 + [0]
                                           [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                                           [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                c_4() = [0]
                        [0]
                        [0]
                c_5(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                c_6(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 3'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {sort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(sort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [2]
                        [2]
                        [2]
                sort^#(x1) = [0 2 0] x1 + [7]
                             [2 2 0]      [3]
                             [2 2 2]      [3]
                c_0() = [0]
                        [1]
                        [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{3}: MAYBE
             --------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 3'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost runtime-complexity with respect to
               Rules:
                 {  sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
                  , insert^#(x, nil()) -> c_2()
                  , sort(nil()) -> nil()
                  , sort(cons(x, y)) -> insert(x, sort(y))
                  , insert(x, nil()) -> cons(x, nil())
                  , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                  , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                  , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                  , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {2}->{4,6,7}: inherited
             ----------------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{4,6,7}->{3}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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}->{4,6,7}->{5}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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.
    
    2) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: sort^#(nil()) -> c_0()
              , 2: sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
              , 3: insert^#(x, nil()) -> c_2()
              , 4: insert^#(x, cons(v, w)) -> c_3(choose^#(x, cons(v, w), x, v))
              , 5: choose^#(x, cons(v, w), y, 0()) -> c_4()
              , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_5(insert^#(x, w))
              , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_6(choose^#(x, cons(v, w), y, z))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2}                                                       [     inherited      ]
                |
                |->{3}                                                   [       MAYBE        ]
                |
                `->{4,6,7}                                               [     inherited      ]
                    |
                    |->{3}                                               [         NA         ]
                    |
                    `->{5}                                               [         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(sort) = {}, Uargs(cons) = {}, Uargs(insert) = {},
                 Uargs(choose) = {}, Uargs(s) = {}, Uargs(sort^#) = {},
                 Uargs(c_1) = {}, Uargs(insert^#) = {}, Uargs(c_3) = {},
                 Uargs(choose^#) = {}, Uargs(c_5) = {}, Uargs(c_6) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                sort(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
                nil() = [0]
                        [0]
                cons(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                               [0 0]      [0 0]      [0]
                insert(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                 [0 0]      [0 0]      [0]
                choose(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
                                         [0 0]      [0 0]      [0 0]      [0 0]      [0]
                0() = [0]
                      [0]
                s(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
                sort^#(x1) = [0 0] x1 + [0]
                             [0 0]      [0]
                c_0() = [0]
                        [0]
                c_1(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                insert^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
                c_2() = [0]
                        [0]
                c_3(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                choose^#(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
                                           [0 0]      [0 0]      [0 0]      [0 0]      [0]
                c_4() = [0]
                        [0]
                c_5(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                c_6(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {sort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(sort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [2]
                        [2]
                sort^#(x1) = [2 0] x1 + [7]
                             [2 2]      [7]
                c_0() = [0]
                        [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{3}: MAYBE
             --------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost runtime-complexity with respect to
               Rules:
                 {  sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
                  , insert^#(x, nil()) -> c_2()
                  , sort(nil()) -> nil()
                  , sort(cons(x, y)) -> insert(x, sort(y))
                  , insert(x, nil()) -> cons(x, nil())
                  , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                  , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                  , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                  , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {2}->{4,6,7}: inherited
             ----------------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{4,6,7}->{3}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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}->{4,6,7}->{5}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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.
    
    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: sort^#(nil()) -> c_0()
              , 2: sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
              , 3: insert^#(x, nil()) -> c_2()
              , 4: insert^#(x, cons(v, w)) -> c_3(choose^#(x, cons(v, w), x, v))
              , 5: choose^#(x, cons(v, w), y, 0()) -> c_4()
              , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_5(insert^#(x, w))
              , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_6(choose^#(x, cons(v, w), y, z))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2}                                                       [     inherited      ]
                |
                |->{3}                                                   [       MAYBE        ]
                |
                `->{4,6,7}                                               [     inherited      ]
                    |
                    |->{3}                                               [         NA         ]
                    |
                    `->{5}                                               [         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(sort) = {}, Uargs(cons) = {}, Uargs(insert) = {},
                 Uargs(choose) = {}, Uargs(s) = {}, Uargs(sort^#) = {},
                 Uargs(c_1) = {}, Uargs(insert^#) = {}, Uargs(c_3) = {},
                 Uargs(choose^#) = {}, Uargs(c_5) = {}, Uargs(c_6) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                sort(x1) = [0] x1 + [0]
                nil() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                insert(x1, x2) = [0] x1 + [0] x2 + [0]
                choose(x1, x2, x3, x4) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0]
                0() = [0]
                s(x1) = [0] x1 + [0]
                sort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                insert^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_2() = [0]
                c_3(x1) = [0] x1 + [0]
                choose^#(x1, x2, x3, x4) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0]
                c_4() = [0]
                c_5(x1) = [0] x1 + [0]
                c_6(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: {sort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(sort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                sort^#(x1) = [1] x1 + [7]
                c_0() = [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{3}: MAYBE
             --------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost runtime-complexity with respect to
               Rules:
                 {  sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
                  , insert^#(x, nil()) -> c_2()
                  , sort(nil()) -> nil()
                  , sort(cons(x, y)) -> insert(x, sort(y))
                  , insert(x, nil()) -> cons(x, nil())
                  , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                  , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                  , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                  , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {2}->{4,6,7}: inherited
             ----------------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{4,6,7}->{3}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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}->{4,6,7}->{5}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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.
    
    4) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    6) '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
InputDer95 32

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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: sort^#(nil()) -> c_0()
              , 2: sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
              , 3: insert^#(x, nil()) -> c_2(x)
              , 4: insert^#(x, cons(v, w)) -> c_3(choose^#(x, cons(v, w), x, v))
              , 5: choose^#(x, cons(v, w), y, 0()) -> c_4(x, v, w)
              , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_5(v, insert^#(x, w))
              , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_6(choose^#(x, cons(v, w), y, z))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2}                                                       [     inherited      ]
                |
                |->{3}                                                   [       MAYBE        ]
                |
                `->{4,6,7}                                               [     inherited      ]
                    |
                    |->{3}                                               [         NA         ]
                    |
                    `->{5}                                               [         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(sort) = {}, Uargs(cons) = {}, Uargs(insert) = {},
                 Uargs(choose) = {}, Uargs(s) = {}, Uargs(sort^#) = {},
                 Uargs(c_1) = {}, Uargs(insert^#) = {}, Uargs(c_2) = {},
                 Uargs(c_3) = {}, Uargs(choose^#) = {}, Uargs(c_4) = {},
                 Uargs(c_5) = {}, Uargs(c_6) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                sort(x1) = [0 0 0] x1 + [0]
                           [0 0 0]      [0]
                           [0 0 0]      [0]
                nil() = [0]
                        [0]
                        [0]
                cons(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                               [0 0 0]      [0 0 0]      [0]
                               [0 0 0]      [0 0 0]      [0]
                insert(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                                 [0 0 0]      [0 0 0]      [0]
                                 [0 0 0]      [0 0 0]      [0]
                choose(x1, x2, x3, x4) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 0] x4 + [0]
                                         [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                                         [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                0() = [0]
                      [0]
                      [0]
                s(x1) = [0 0 0] x1 + [0]
                        [0 0 0]      [0]
                        [0 0 0]      [0]
                sort^#(x1) = [0 0 0] x1 + [0]
                             [0 0 0]      [0]
                             [0 0 0]      [0]
                c_0() = [0]
                        [0]
                        [0]
                c_1(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                insert^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                                   [0 0 0]      [0 0 0]      [0]
                                   [0 0 0]      [0 0 0]      [0]
                c_2(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                c_3(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                choose^#(x1, x2, x3, x4) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 0] x4 + [0]
                                           [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                                           [0 0 0]      [0 0 0]      [0 0 0]      [0 0 0]      [0]
                c_4(x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0]
                                  [0 0 0]      [0 0 0]      [0 0 0]      [0]
                                  [0 0 0]      [0 0 0]      [0 0 0]      [0]
                c_5(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                              [0 0 0]      [0 0 0]      [0]
                              [0 0 0]      [0 0 0]      [0]
                c_6(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 3'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {sort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(sort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [2]
                        [2]
                        [2]
                sort^#(x1) = [0 2 0] x1 + [7]
                             [2 2 0]      [3]
                             [2 2 2]      [3]
                c_0() = [0]
                        [1]
                        [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{3}: MAYBE
             --------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 3'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    runtime-complexity with respect to
               Rules:
                 {  sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
                  , insert^#(x, nil()) -> c_2(x)
                  , sort(nil()) -> nil()
                  , sort(cons(x, y)) -> insert(x, sort(y))
                  , insert(x, nil()) -> cons(x, nil())
                  , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                  , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                  , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                  , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {2}->{4,6,7}: inherited
             ----------------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{4,6,7}->{3}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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}->{4,6,7}->{5}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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.
    
    2) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: sort^#(nil()) -> c_0()
              , 2: sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
              , 3: insert^#(x, nil()) -> c_2(x)
              , 4: insert^#(x, cons(v, w)) -> c_3(choose^#(x, cons(v, w), x, v))
              , 5: choose^#(x, cons(v, w), y, 0()) -> c_4(x, v, w)
              , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_5(v, insert^#(x, w))
              , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_6(choose^#(x, cons(v, w), y, z))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2}                                                       [     inherited      ]
                |
                |->{3}                                                   [       MAYBE        ]
                |
                `->{4,6,7}                                               [     inherited      ]
                    |
                    |->{3}                                               [         NA         ]
                    |
                    `->{5}                                               [         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(sort) = {}, Uargs(cons) = {}, Uargs(insert) = {},
                 Uargs(choose) = {}, Uargs(s) = {}, Uargs(sort^#) = {},
                 Uargs(c_1) = {}, Uargs(insert^#) = {}, Uargs(c_2) = {},
                 Uargs(c_3) = {}, Uargs(choose^#) = {}, Uargs(c_4) = {},
                 Uargs(c_5) = {}, Uargs(c_6) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                sort(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
                nil() = [0]
                        [0]
                cons(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                               [0 0]      [0 0]      [0]
                insert(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                 [0 0]      [0 0]      [0]
                choose(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
                                         [0 0]      [0 0]      [0 0]      [0 0]      [0]
                0() = [0]
                      [0]
                s(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
                sort^#(x1) = [0 0] x1 + [0]
                             [0 0]      [0]
                c_0() = [0]
                        [0]
                c_1(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                insert^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
                c_2(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                c_3(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                choose^#(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
                                           [0 0]      [0 0]      [0 0]      [0 0]      [0]
                c_4(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
                                  [0 0]      [0 0]      [0 0]      [0]
                c_5(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [0 0]      [0 0]      [0]
                c_6(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {sort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(sort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [2]
                        [2]
                sort^#(x1) = [2 0] x1 + [7]
                             [2 2]      [7]
                c_0() = [0]
                        [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{3}: MAYBE
             --------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    runtime-complexity with respect to
               Rules:
                 {  sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
                  , insert^#(x, nil()) -> c_2(x)
                  , sort(nil()) -> nil()
                  , sort(cons(x, y)) -> insert(x, sort(y))
                  , insert(x, nil()) -> cons(x, nil())
                  , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                  , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                  , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                  , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {2}->{4,6,7}: inherited
             ----------------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{4,6,7}->{3}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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}->{4,6,7}->{5}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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.
    
    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: sort^#(nil()) -> c_0()
              , 2: sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
              , 3: insert^#(x, nil()) -> c_2(x)
              , 4: insert^#(x, cons(v, w)) -> c_3(choose^#(x, cons(v, w), x, v))
              , 5: choose^#(x, cons(v, w), y, 0()) -> c_4(x, v, w)
              , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_5(v, insert^#(x, w))
              , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_6(choose^#(x, cons(v, w), y, z))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2}                                                       [     inherited      ]
                |
                |->{3}                                                   [       MAYBE        ]
                |
                `->{4,6,7}                                               [     inherited      ]
                    |
                    |->{3}                                               [         NA         ]
                    |
                    `->{5}                                               [         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(sort) = {}, Uargs(cons) = {}, Uargs(insert) = {},
                 Uargs(choose) = {}, Uargs(s) = {}, Uargs(sort^#) = {},
                 Uargs(c_1) = {}, Uargs(insert^#) = {}, Uargs(c_2) = {},
                 Uargs(c_3) = {}, Uargs(choose^#) = {}, Uargs(c_4) = {},
                 Uargs(c_5) = {}, Uargs(c_6) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                sort(x1) = [0] x1 + [0]
                nil() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                insert(x1, x2) = [0] x1 + [0] x2 + [0]
                choose(x1, x2, x3, x4) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0]
                0() = [0]
                s(x1) = [0] x1 + [0]
                sort^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1(x1) = [0] x1 + [0]
                insert^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_2(x1) = [0] x1 + [0]
                c_3(x1) = [0] x1 + [0]
                choose^#(x1, x2, x3, x4) = [0] x1 + [0] x2 + [0] x3 + [0] x4 + [0]
                c_4(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_5(x1, x2) = [0] x1 + [0] x2 + [0]
                c_6(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:    DP runtime-complexity with respect to
               Strict Rules: {sort^#(nil()) -> c_0()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(sort^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                nil() = [7]
                sort^#(x1) = [1] x1 + [7]
                c_0() = [1]
           
           * Path {2}: inherited
             -------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{3}: MAYBE
             --------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    runtime-complexity with respect to
               Rules:
                 {  sort^#(cons(x, y)) -> c_1(insert^#(x, sort(y)))
                  , insert^#(x, nil()) -> c_2(x)
                  , sort(nil()) -> nil()
                  , sort(cons(x, y)) -> insert(x, sort(y))
                  , insert(x, nil()) -> cons(x, nil())
                  , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                  , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                  , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                  , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {2}->{4,6,7}: inherited
             ----------------------------
             
             This path is subsumed by the proof of path {2}->{4,6,7}->{3}.
           
           * Path {2}->{4,6,7}->{3}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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}->{4,6,7}->{5}: NA
             --------------------------
             
             The usable rules for this path are:
             
               {  sort(nil()) -> nil()
                , sort(cons(x, y)) -> insert(x, sort(y))
                , insert(x, nil()) -> cons(x, nil())
                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), 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.
    
    4) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    6) '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
MAYBE
InputDer95 32

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: none

Certificate: MAYBE

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: none
  
  1) None of the processors succeeded.
     
     Details of failed attempt(s):
     -----------------------------
       1) 'dp' failed due to the following reason:
            We have computed the following dependency pairs
            
            Strict Dependency Pairs:
              {  sort^#(nil()) -> c_1()
               , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
               , insert^#(x, nil()) -> c_3(x)
               , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
               , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
               , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
               , choose^#(x, cons(v, w), s(y), s(z)) ->
                 c_7(choose^#(x, cons(v, w), y, z))}
            
            We consider the following Problem:
            
              Strict DPs:
                {  sort^#(nil()) -> c_1()
                 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
                 , insert^#(x, nil()) -> c_3(x)
                 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
                 , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
                 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
                 , choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_7(choose^#(x, cons(v, w), y, z))}
              Strict Trs:
                {  sort(nil()) -> nil()
                 , sort(cons(x, y)) -> insert(x, sort(y))
                 , insert(x, nil()) -> cons(x, nil())
                 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                 , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
              StartTerms: basic terms
              Strategy: none
            
            Certificate: MAYBE
            
            Application of 'Fastest':
            -------------------------
              None of the processors succeeded.
              
              Details of failed attempt(s):
              -----------------------------
                1) 'pathanalysis' failed due to the following reason:
                     We use following congruence DG for path analysis
                     
                     ->{1}                                                       [         ?          ]
                     
                     ->{2}                                                       [       MAYBE        ]
                        |
                        |->{3}                                                   [         ?          ]
                        |
                        `->{4,6,7}                                               [         ?          ]
                            |
                            |->{3}                                               [         ?          ]
                            |
                            `->{5}                                               [         ?          ]
                     
                     
                     Here rules are as follows:
                     
                       {  1: sort^#(nil()) -> c_1()
                        , 2: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
                        , 3: insert^#(x, nil()) -> c_3(x)
                        , 4: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
                        , 5: choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
                        , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
                        , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                             c_7(choose^#(x, cons(v, w), y, z))}
                     
                     * Path {1}: ?
                       -----------
                       
                       CANNOT find proof of path {1}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}: MAYBE
                       ---------------
                       
                       We consider the following Problem:
                       
                         Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                         Strict Trs:
                           {  sort(nil()) -> nil()
                            , sort(cons(x, y)) -> insert(x, sort(y))
                            , insert(x, nil()) -> cons(x, nil())
                            , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                            , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                            , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                            , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                         StartTerms: basic terms
                         Strategy: none
                       
                       Certificate: MAYBE
                       
                       Application of 'removetails >>> ... >>> ... >>> ...':
                       -----------------------------------------------------
                         The processor is inapplicable since the strict component of the
                         input problem is not empty
                         
                         We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                         Sub-problem 1:
                         --------------
                           We consider the problem
                           
                           Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                           Strict Trs:
                             {  sort(nil()) -> nil()
                              , sort(cons(x, y)) -> insert(x, sort(y))
                              , insert(x, nil()) -> cons(x, nil())
                              , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                              , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                              , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                              , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                           StartTerms: basic terms
                           Strategy: none
                           
                           We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                           
                             The weightgap principle does not apply
                           
                           We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                           
                           Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                           Strict Trs:
                             {  sort(nil()) -> nil()
                              , sort(cons(x, y)) -> insert(x, sort(y))
                              , insert(x, nil()) -> cons(x, nil())
                              , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                              , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                              , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                              , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                           StartTerms: basic terms
                           Strategy: none
                           
                             We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                             
                               The weightgap principle does not apply
                             
                             We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                             
                             Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                             Strict Trs:
                               {  sort(nil()) -> nil()
                                , sort(cons(x, y)) -> insert(x, sort(y))
                                , insert(x, nil()) -> cons(x, nil())
                                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                             StartTerms: basic terms
                             Strategy: none
                             
                               The weightgap principle does not apply
                         
                         We abort the transformation and continue with the subprocessor on the problem
                         
                         Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                         Strict Trs:
                           {  sort(nil()) -> nil()
                            , sort(cons(x, y)) -> insert(x, sort(y))
                            , insert(x, nil()) -> cons(x, nil())
                            , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                            , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                            , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                            , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                         StartTerms: basic terms
                         Strategy: none
                         
                         1) None of the processors succeeded.
                            
                            Details of failed attempt(s):
                            -----------------------------
                              1) 'empty' failed due to the following reason:
                                   Empty strict component of the problem is NOT empty.
                              
                              2) 'Fastest' failed due to the following reason:
                                   None of the processors succeeded.
                                   
                                   Details of failed attempt(s):
                                   -----------------------------
                                     1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                          The input cannot be shown compatible
                                     
                                     2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                          The input cannot be shown compatible
                                     
                                     3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                          The input cannot be shown compatible
                                     
                              
                         
                     
                     * Path {2}->{3}: ?
                       ----------------
                       
                       CANNOT find proof of path {2}->{3}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}->{4,6,7}: ?
                       --------------------
                       
                       CANNOT find proof of path {2}->{4,6,7}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}->{4,6,7}->{3}: ?
                       -------------------------
                       
                       CANNOT find proof of path {2}->{4,6,7}->{3}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}->{4,6,7}->{5}: ?
                       -------------------------
                       
                       CANNOT find proof of path {2}->{4,6,7}->{5}. Propably computation has been aborted since some other path cannot be solved.
                
                2) 'Sequentially' failed due to the following reason:
                     None of the processors succeeded.
                     
                     Details of failed attempt(s):
                     -----------------------------
                       1) 'empty' failed due to the following reason:
                            Empty strict component of the problem is NOT empty.
                       
                       2) 'Fastest' failed due to the following reason:
                            None of the processors succeeded.
                            
                            Details of failed attempt(s):
                            -----------------------------
                              1) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                              2) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                       
                
       
       2) 'Fastest' failed due to the following reason:
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
              1) 'Sequentially' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'empty' failed due to the following reason:
                          Empty strict component of the problem is NOT empty.
                     
                     2) 'Fastest' failed due to the following reason:
                          None of the processors succeeded.
                          
                          Details of failed attempt(s):
                          -----------------------------
                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                     
              
              2) 'Fastest' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
                     2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
              
       
  

Arrrr..

Tool pair2rc

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: none

Certificate: MAYBE

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: none
  
  1) None of the processors succeeded.
     
     Details of failed attempt(s):
     -----------------------------
       1) 'dp' failed due to the following reason:
            We have computed the following dependency pairs
            
            Strict Dependency Pairs:
              {  sort^#(nil()) -> c_1()
               , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
               , insert^#(x, nil()) -> c_3(x)
               , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
               , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
               , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
               , choose^#(x, cons(v, w), s(y), s(z)) ->
                 c_7(choose^#(x, cons(v, w), y, z))}
            
            We consider the following Problem:
            
              Strict DPs:
                {  sort^#(nil()) -> c_1()
                 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
                 , insert^#(x, nil()) -> c_3(x)
                 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
                 , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
                 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
                 , choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_7(choose^#(x, cons(v, w), y, z))}
              Strict Trs:
                {  sort(nil()) -> nil()
                 , sort(cons(x, y)) -> insert(x, sort(y))
                 , insert(x, nil()) -> cons(x, nil())
                 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                 , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
              StartTerms: basic terms
              Strategy: none
            
            Certificate: MAYBE
            
            Application of 'Fastest':
            -------------------------
              None of the processors succeeded.
              
              Details of failed attempt(s):
              -----------------------------
                1) 'pathanalysis' failed due to the following reason:
                     We use following congruence DG for path analysis
                     
                     ->{1}                                                       [         ?          ]
                     
                     ->{2}                                                       [       MAYBE        ]
                        |
                        |->{3}                                                   [         ?          ]
                        |
                        `->{4,6,7}                                               [         ?          ]
                            |
                            |->{3}                                               [         ?          ]
                            |
                            `->{5}                                               [         ?          ]
                     
                     
                     Here rules are as follows:
                     
                       {  1: sort^#(nil()) -> c_1()
                        , 2: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
                        , 3: insert^#(x, nil()) -> c_3(x)
                        , 4: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
                        , 5: choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
                        , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
                        , 7: choose^#(x, cons(v, w), s(y), s(z)) ->
                             c_7(choose^#(x, cons(v, w), y, z))}
                     
                     * Path {1}: ?
                       -----------
                       
                       CANNOT find proof of path {1}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}: MAYBE
                       ---------------
                       
                       We consider the following Problem:
                       
                         Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                         Strict Trs:
                           {  sort(nil()) -> nil()
                            , sort(cons(x, y)) -> insert(x, sort(y))
                            , insert(x, nil()) -> cons(x, nil())
                            , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                            , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                            , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                            , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                         StartTerms: basic terms
                         Strategy: none
                       
                       Certificate: MAYBE
                       
                       Application of 'removetails >>> ... >>> ... >>> ...':
                       -----------------------------------------------------
                         The processor is inapplicable since the strict component of the
                         input problem is not empty
                         
                         We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                         Sub-problem 1:
                         --------------
                           We consider the problem
                           
                           Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                           Strict Trs:
                             {  sort(nil()) -> nil()
                              , sort(cons(x, y)) -> insert(x, sort(y))
                              , insert(x, nil()) -> cons(x, nil())
                              , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                              , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                              , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                              , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                           StartTerms: basic terms
                           Strategy: none
                           
                           We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                           
                             The weightgap principle does not apply
                           
                           We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                           
                           Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                           Strict Trs:
                             {  sort(nil()) -> nil()
                              , sort(cons(x, y)) -> insert(x, sort(y))
                              , insert(x, nil()) -> cons(x, nil())
                              , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                              , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                              , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                              , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                           StartTerms: basic terms
                           Strategy: none
                           
                             We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                             
                               The weightgap principle does not apply
                             
                             We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                             
                             Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                             Strict Trs:
                               {  sort(nil()) -> nil()
                                , sort(cons(x, y)) -> insert(x, sort(y))
                                , insert(x, nil()) -> cons(x, nil())
                                , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                                , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                                , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                                , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                             StartTerms: basic terms
                             Strategy: none
                             
                               The weightgap principle does not apply
                         
                         We abort the transformation and continue with the subprocessor on the problem
                         
                         Strict DPs: {sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))}
                         Strict Trs:
                           {  sort(nil()) -> nil()
                            , sort(cons(x, y)) -> insert(x, sort(y))
                            , insert(x, nil()) -> cons(x, nil())
                            , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                            , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                            , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                            , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
                         StartTerms: basic terms
                         Strategy: none
                         
                         1) None of the processors succeeded.
                            
                            Details of failed attempt(s):
                            -----------------------------
                              1) 'Sequentially' failed due to the following reason:
                                   None of the processors succeeded.
                                   
                                   Details of failed attempt(s):
                                   -----------------------------
                                     1) 'empty' failed due to the following reason:
                                          Empty strict component of the problem is NOT empty.
                                     
                                     2) 'Fastest' failed due to the following reason:
                                          None of the processors succeeded.
                                          
                                          Details of failed attempt(s):
                                          -----------------------------
                                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                                 The input cannot be shown compatible
                                            
                                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                                 The input cannot be shown compatible
                                            
                                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                                 The input cannot be shown compatible
                                            
                                     
                              
                              2) 'compose (statically using 'split first congruence from CWD', multiplication)' failed due to the following reason:
                                   Compose is inapplicable since some strict rule is size increasing
                                   
                                   No subproblems were generated.
                              
                         
                     
                     * Path {2}->{3}: ?
                       ----------------
                       
                       CANNOT find proof of path {2}->{3}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}->{4,6,7}: ?
                       --------------------
                       
                       CANNOT find proof of path {2}->{4,6,7}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}->{4,6,7}->{3}: ?
                       -------------------------
                       
                       CANNOT find proof of path {2}->{4,6,7}->{3}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {2}->{4,6,7}->{5}: ?
                       -------------------------
                       
                       CANNOT find proof of path {2}->{4,6,7}->{5}. Propably computation has been aborted since some other path cannot be solved.
                
                2) 'Sequentially' failed due to the following reason:
                     None of the processors succeeded.
                     
                     Details of failed attempt(s):
                     -----------------------------
                       1) 'empty' failed due to the following reason:
                            Empty strict component of the problem is NOT empty.
                       
                       2) 'Fastest' failed due to the following reason:
                            None of the processors succeeded.
                            
                            Details of failed attempt(s):
                            -----------------------------
                              1) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                              2) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                       
                
       
       2) 'Fastest' failed due to the following reason:
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
              1) 'Sequentially' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'empty' failed due to the following reason:
                          Empty strict component of the problem is NOT empty.
                     
                     2) 'Fastest' failed due to the following reason:
                          None of the processors succeeded.
                          
                          Details of failed attempt(s):
                          -----------------------------
                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                     
              
              2) 'Fastest' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
                     2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
              
       
  

Arrrr..

Tool pair3irc

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: innermost
  
  1) None of the processors succeeded.
     
     Details of failed attempt(s):
     -----------------------------
       1) 'dp' failed due to the following reason:
            We have computed the following dependency pairs
            
            Strict Dependency Pairs:
              {  sort^#(nil()) -> c_1()
               , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
               , insert^#(x, nil()) -> c_3()
               , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
               , choose^#(x, cons(v, w), y, 0()) -> c_5()
               , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
               , choose^#(x, cons(v, w), s(y), s(z)) ->
                 c_7(choose^#(x, cons(v, w), y, z))}
            
            We consider the following Problem:
            
              Strict DPs:
                {  sort^#(nil()) -> c_1()
                 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
                 , insert^#(x, nil()) -> c_3()
                 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
                 , choose^#(x, cons(v, w), y, 0()) -> c_5()
                 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
                 , choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_7(choose^#(x, cons(v, w), y, z))}
              Strict Trs:
                {  sort(nil()) -> nil()
                 , sort(cons(x, y)) -> insert(x, sort(y))
                 , insert(x, nil()) -> cons(x, nil())
                 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                 , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: MAYBE
            
            Application of 'Fastest':
            -------------------------
              None of the processors succeeded.
              
              Details of failed attempt(s):
              -----------------------------
                'Sequentially' failed due to the following reason:
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                    1) 'empty' failed due to the following reason:
                         Empty strict component of the problem is NOT empty.
                    
                    2) 'Fastest' failed due to the following reason:
                         None of the processors succeeded.
                         
                         Details of failed attempt(s):
                         -----------------------------
                           1) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                The input cannot be shown compatible
                           
                           2) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                The input cannot be shown compatible
                           
                    
       
       2) 'Fastest' failed due to the following reason:
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
              1) 'Sequentially' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'empty' failed due to the following reason:
                          Empty strict component of the problem is NOT empty.
                     
                     2) 'Fastest' failed due to the following reason:
                          None of the processors succeeded.
                          
                          Details of failed attempt(s):
                          -----------------------------
                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                     
              
              2) 'Fastest' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
                     2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
              
       
  

Arrrr..

Tool pair3rc

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: none

Certificate: MAYBE

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: none
  
  1) None of the processors succeeded.
     
     Details of failed attempt(s):
     -----------------------------
       1) 'dp' failed due to the following reason:
            We have computed the following dependency pairs
            
            Strict Dependency Pairs:
              {  sort^#(nil()) -> c_1()
               , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
               , insert^#(x, nil()) -> c_3(x)
               , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
               , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
               , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
               , choose^#(x, cons(v, w), s(y), s(z)) ->
                 c_7(choose^#(x, cons(v, w), y, z))}
            
            We consider the following Problem:
            
              Strict DPs:
                {  sort^#(nil()) -> c_1()
                 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
                 , insert^#(x, nil()) -> c_3(x)
                 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
                 , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
                 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
                 , choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_7(choose^#(x, cons(v, w), y, z))}
              Strict Trs:
                {  sort(nil()) -> nil()
                 , sort(cons(x, y)) -> insert(x, sort(y))
                 , insert(x, nil()) -> cons(x, nil())
                 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                 , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
              StartTerms: basic terms
              Strategy: none
            
            Certificate: MAYBE
            
            Application of 'Fastest':
            -------------------------
              None of the processors succeeded.
              
              Details of failed attempt(s):
              -----------------------------
                'Sequentially' failed due to the following reason:
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                    1) 'empty' failed due to the following reason:
                         Empty strict component of the problem is NOT empty.
                    
                    2) 'Fastest' failed due to the following reason:
                         None of the processors succeeded.
                         
                         Details of failed attempt(s):
                         -----------------------------
                           1) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                The input cannot be shown compatible
                           
                           2) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                The input cannot be shown compatible
                           
                    
       
       2) 'Fastest' failed due to the following reason:
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
              1) 'Sequentially' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'empty' failed due to the following reason:
                          Empty strict component of the problem is NOT empty.
                     
                     2) 'Fastest' failed due to the following reason:
                          None of the processors succeeded.
                          
                          Details of failed attempt(s):
                          -----------------------------
                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                     
              
              2) 'Fastest' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
                     2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
              
       
  

Arrrr..

Tool rc

Execution TimeUnknown
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: none

Certificate: MAYBE

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'Fastest' failed due to the following reason:
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
           1) 'Sequentially' failed due to the following reason:
                None of the processors succeeded.
                
                Details of failed attempt(s):
                -----------------------------
                  1) 'empty' failed due to the following reason:
                       Empty strict component of the problem is NOT empty.
                  
                  2) 'Fastest' failed due to the following reason:
                       None of the processors succeeded.
                       
                       Details of failed attempt(s):
                       -----------------------------
                         1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                              The input cannot be shown compatible
                         
                         2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                              The input cannot be shown compatible
                         
                         3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                              The input cannot be shown compatible
                         
                  
           
           2) 'Fastest' failed due to the following reason:
                None of the processors succeeded.
                
                Details of failed attempt(s):
                -----------------------------
                  1) 'Bounds with perSymbol-enrichment and initial automaton 'match' (timeout of 5.0 seconds)' failed due to the following reason:
                       match-boundness of the problem could not be verified.
                  
                  2) 'Bounds with minimal-enrichment and initial automaton 'match' (timeout of 100.0 seconds)' failed due to the following reason:
                       match-boundness of the problem could not be verified.
                  
           
    
    2) 'dp' failed due to the following reason:
         We have computed the following dependency pairs
         
         Strict Dependency Pairs:
           {  sort^#(nil()) -> c_1()
            , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
            , insert^#(x, nil()) -> c_3(x)
            , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
            , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
            , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
            , choose^#(x, cons(v, w), s(y), s(z)) ->
              c_7(choose^#(x, cons(v, w), y, z))}
         
         We consider the following Problem:
         
           Strict DPs:
             {  sort^#(nil()) -> c_1()
              , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)))
              , insert^#(x, nil()) -> c_3(x)
              , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
              , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w)
              , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w))
              , choose^#(x, cons(v, w), s(y), s(z)) ->
                c_7(choose^#(x, cons(v, w), y, z))}
           Strict Trs:
             {  sort(nil()) -> nil()
              , sort(cons(x, y)) -> insert(x, sort(y))
              , insert(x, nil()) -> cons(x, nil())
              , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
              , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
              , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
              , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
           StartTerms: basic terms
           Strategy: none
         
         Certificate: MAYBE
         
         Application of 'usablerules':
         -----------------------------
           All rules are usable.
           
           No subproblems were generated.
    

Arrrr..

Tool tup3irc

Execution Time50.11967ms
Answer
MAYBE
InputDer95 32

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  sort(nil()) -> nil()
     , sort(cons(x, y)) -> insert(x, sort(y))
     , insert(x, nil()) -> cons(x, nil())
     , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
     , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
     , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
     , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  StartTerms: basic terms
  Strategy: innermost
  
  1) None of the processors succeeded.
     
     Details of failed attempt(s):
     -----------------------------
       1) 'dp' failed due to the following reason:
            We have computed the following dependency pairs
            
            Strict Dependency Pairs:
              {  sort^#(nil()) -> c_1()
               , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y))
               , insert^#(x, nil()) -> c_3()
               , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
               , choose^#(x, cons(v, w), y, 0()) -> c_5()
               , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
               , choose^#(x, cons(v, w), s(y), s(z)) ->
                 c_7(choose^#(x, cons(v, w), y, z))}
            
            We consider the following Problem:
            
              Strict DPs:
                {  sort^#(nil()) -> c_1()
                 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y))
                 , insert^#(x, nil()) -> c_3()
                 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
                 , choose^#(x, cons(v, w), y, 0()) -> c_5()
                 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
                 , choose^#(x, cons(v, w), s(y), s(z)) ->
                   c_7(choose^#(x, cons(v, w), y, z))}
              Weak Trs:
                {  sort(nil()) -> nil()
                 , sort(cons(x, y)) -> insert(x, sort(y))
                 , insert(x, nil()) -> cons(x, nil())
                 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
                 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
                 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
                 , choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: MAYBE
            
            Application of 'Fastest':
            -------------------------
              None of the processors succeeded.
              
              Details of failed attempt(s):
              -----------------------------
                'Sequentially' failed due to the following reason:
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                    1) 'empty' failed due to the following reason:
                         Empty strict component of the problem is NOT empty.
                    
                    2) 'Fastest' failed due to the following reason:
                         None of the processors succeeded.
                         
                         Details of failed attempt(s):
                         -----------------------------
                           1) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                The input cannot be shown compatible
                           
                           2) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                The input cannot be shown compatible
                           
                    
       
       2) 'Fastest' failed due to the following reason:
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
              1) 'Sequentially' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'empty' failed due to the following reason:
                          Empty strict component of the problem is NOT empty.
                     
                     2) 'Fastest' failed due to the following reason:
                          None of the processors succeeded.
                          
                          Details of failed attempt(s):
                          -----------------------------
                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                     
              
              2) 'Fastest' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
                     2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
              
       
  

Arrrr..