Problem Mixed innermost wiehe14

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputMixed innermost wiehe14

stdout:

MAYBE

Problem:
 even(0()) -> true()
 even(s(0())) -> false()
 even(s(s(x))) -> even(x)
 half(0()) -> 0()
 half(s(s(x))) -> s(half(x))
 plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
 plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
 plus(zero(),y) -> y
 plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
 id(x) -> x
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 not(x) -> if(x,false(),true())
 gt(s(x),zero()) -> true()
 gt(zero(),y) -> false()
 gt(s(x),s(y)) -> gt(x,y)
 times(0(),y) -> 0()
 times(s(x),y) -> if_times(even(s(x)),s(x),y)
 if_times(true(),s(x),y) -> plus(times(half(s(x)),y),times(half(s(x)),y))
 if_times(false(),s(x),y) -> plus(y,times(x,y))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputMixed innermost wiehe14

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
MAYBE
InputMixed innermost wiehe14

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  even(0()) -> true()
     , even(s(0())) -> false()
     , even(s(s(x))) -> even(x)
     , half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(s(x), s(y)) ->
       s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
     , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
     , plus(zero(), y) -> y
     , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
     , id(x) -> x
     , if(true(), x, y) -> x
     , if(false(), x, y) -> y
     , not(x) -> if(x, false(), true())
     , gt(s(x), zero()) -> true()
     , gt(zero(), y) -> false()
     , gt(s(x), s(y)) -> gt(x, y)
     , times(0(), y) -> 0()
     , times(s(x), y) -> if_times(even(s(x)), s(x), y)
     , if_times(true(), s(x), y) ->
       plus(times(half(s(x)), y), times(half(s(x)), y))
     , if_times(false(), s(x), y) -> plus(y, times(x, y))}

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: even^#(0()) -> c_0()
              , 2: even^#(s(0())) -> c_1()
              , 3: even^#(s(s(x))) -> c_2(even^#(x))
              , 4: half^#(0()) -> c_3()
              , 5: half^#(s(s(x))) -> c_4(half^#(x))
              , 6: plus^#(s(x), s(y)) ->
                   c_5(plus^#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
              , 7: plus^#(s(x), x) ->
                   c_6(plus^#(if(gt(x, x), id(x), id(x)), s(x)))
              , 8: plus^#(zero(), y) -> c_7()
              , 9: plus^#(id(x), s(y)) ->
                   c_8(plus^#(x, if(gt(s(y), y), y, s(y))))
              , 10: id^#(x) -> c_9()
              , 11: if^#(true(), x, y) -> c_10()
              , 12: if^#(false(), x, y) -> c_11()
              , 13: not^#(x) -> c_12(if^#(x, false(), true()))
              , 14: gt^#(s(x), zero()) -> c_13()
              , 15: gt^#(zero(), y) -> c_14()
              , 16: gt^#(s(x), s(y)) -> c_15(gt^#(x, y))
              , 17: times^#(0(), y) -> c_16()
              , 18: times^#(s(x), y) -> c_17(if_times^#(even(s(x)), s(x), y))
              , 19: if_times^#(true(), s(x), y) ->
                    c_18(plus^#(times(half(s(x)), y), times(half(s(x)), y)))
              , 20: if_times^#(false(), s(x), y) -> c_19(plus^#(y, times(x, y)))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{18}                                                      [     inherited      ]
                |
                |->{19}                                                  [     inherited      ]
                |   |
                |   |->{6,9,7}                                           [     inherited      ]
                |   |   |
                |   |   `->{8}                                           [         NA         ]
                |   |
                |   `->{8}                                               [         NA         ]
                |
                `->{20}                                                  [     inherited      ]
                    |
                    |->{6,9,7}                                           [     inherited      ]
                    |   |
                    |   `->{8}                                           [         NA         ]
                    |
                    `->{8}                                               [       MAYBE        ]
             
             ->{17}                                                      [    YES(?,O(1))     ]
             
             ->{16}                                                      [   YES(?,O(n^1))    ]
                |
                |->{14}                                                  [   YES(?,O(n^1))    ]
                |
                `->{15}                                                  [   YES(?,O(n^1))    ]
             
             ->{13}                                                      [    YES(?,O(1))     ]
                |
                |->{11}                                                  [    YES(?,O(1))     ]
                |
                `->{12}                                                  [    YES(?,O(1))     ]
             
             ->{10}                                                      [    YES(?,O(1))     ]
             
             ->{5}                                                       [   YES(?,O(n^1))    ]
                |
                `->{4}                                                   [   YES(?,O(n^1))    ]
             
             ->{3}                                                       [   YES(?,O(n^1))    ]
                |
                |->{1}                                                   [   YES(?,O(n^1))    ]
                |
                `->{2}                                                   [    YES(?,O(1))     ]
             
           
         
         Sub-problems:
         -------------
           * Path {3}: YES(?,O(n^1))
             -----------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {1}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [1] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [3] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {even^#(s(s(x))) -> c_2(even^#(x))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(even^#) = {}, Uargs(c_2) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                even^#(x1) = [2] x1 + [0]
                c_2(x1) = [1] x1 + [7]
           
           * Path {3}->{1}: YES(?,O(n^1))
             ----------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {1}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {even^#(0()) -> c_0()}
               Weak Rules: {even^#(s(s(x))) -> c_2(even^#(x))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(even^#) = {}, Uargs(c_2) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [2]
                s(x1) = [1] x1 + [0]
                even^#(x1) = [2] x1 + [4]
                c_0() = [1]
                c_2(x1) = [1] x1 + [0]
           
           * Path {3}->{2}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {1}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {even^#(s(0())) -> c_1()}
               Weak Rules: {even^#(s(s(x))) -> c_2(even^#(x))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(even^#) = {}, Uargs(c_2) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [0]
                s(x1) = [0] x1 + [0]
                even^#(x1) = [0] x1 + [1]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
           
           * Path {5}: YES(?,O(n^1))
             -----------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {1}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [1] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [3] x1 + [0]
                c_3() = [0]
                c_4(x1) = [1] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_4) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                half^#(x1) = [2] x1 + [0]
                c_4(x1) = [1] x1 + [7]
           
           * Path {5}->{4}: YES(?,O(n^1))
             ----------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {1}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [1] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {half^#(0()) -> c_3()}
               Weak Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_4) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [2]
                s(x1) = [1] x1 + [0]
                half^#(x1) = [2] x1 + [4]
                c_3() = [1]
                c_4(x1) = [1] x1 + [0]
           
           * Path {10}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {id^#(x) -> c_9()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(id^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                id^#(x1) = [0] x1 + [7]
                c_9() = [0]
           
           * Path {13}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [1] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [3] x1 + [0]
                c_12(x1) = [3] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {not^#(x) -> c_12(if^#(x, false(), true()))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                true() = [0]
                false() = [0]
                if^#(x1, x2, x3) = [7] x1 + [0] x2 + [0] x3 + [4]
                not^#(x1) = [7] x1 + [7]
                c_12(x1) = [0] x1 + [3]
           
           * Path {13}->{11}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {1},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [1] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {if^#(true(), x, y) -> c_10()}
               Weak Rules: {not^#(x) -> c_12(if^#(x, false(), true()))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                true() = [2]
                false() = [0]
                if^#(x1, x2, x3) = [2] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [1]
                not^#(x1) = [7] x1 + [7]
                c_12(x1) = [2] x1 + [7]
           
           * Path {13}->{12}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {1},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [1] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {if^#(false(), x, y) -> c_11()}
               Weak Rules: {not^#(x) -> c_12(if^#(x, false(), true()))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                true() = [0]
                false() = [2]
                if^#(x1, x2, x3) = [2] x1 + [0] x2 + [0] x3 + [4]
                c_11() = [1]
                not^#(x1) = [7] x1 + [7]
                c_12(x1) = [1] x1 + [3]
           
           * Path {16}: YES(?,O(n^1))
             ------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {1}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [1] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [3] x1 + [3] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [1] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {gt^#(s(x), s(y)) -> c_15(gt^#(x, y))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                gt^#(x1, x2) = [2] x1 + [2] x2 + [0]
                c_15(x1) = [1] x1 + [7]
           
           * Path {16}->{14}: YES(?,O(n^1))
             ------------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {1}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [1] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {gt^#(s(x), zero()) -> c_13()}
               Weak Rules: {gt^#(s(x), s(y)) -> c_15(gt^#(x, y))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                zero() = [2]
                gt^#(x1, x2) = [2] x1 + [2] x2 + [0]
                c_13() = [1]
                c_15(x1) = [1] x1 + [7]
           
           * Path {16}->{15}: YES(?,O(n^1))
             ------------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {1}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [1] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {gt^#(zero(), y) -> c_14()}
               Weak Rules: {gt^#(s(x), s(y)) -> c_15(gt^#(x, y))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                zero() = [2]
                gt^#(x1, x2) = [2] x1 + [0] x2 + [4]
                c_14() = [1]
                c_15(x1) = [1] x1 + [2]
           
           * Path {17}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_8) = {}, Uargs(id^#) = {},
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {},
                 Uargs(gt^#) = {}, Uargs(c_15) = {}, Uargs(times^#) = {},
                 Uargs(c_17) = {}, Uargs(if_times^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7() = [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9() = [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10() = [0]
                c_11() = [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {times^#(0(), y) -> c_16()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(times^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [7]
                times^#(x1, x2) = [1] x1 + [0] x2 + [7]
                c_16() = [1]
           
           * Path {18}: inherited
             --------------------
             
             This path is subsumed by the proof of path {18}->{20}->{6,9,7}->{8}.
           
           * Path {18}->{19}: inherited
             --------------------------
             
             This path is subsumed by the proof of path {18}->{19}->{6,9,7}->{8}.
           
           * Path {18}->{19}->{6,9,7}: inherited
             -----------------------------------
             
             This path is subsumed by the proof of path {18}->{19}->{6,9,7}->{8}.
           
           * Path {18}->{19}->{6,9,7}->{8}: NA
             ---------------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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 {18}->{19}->{8}: NA
             ------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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 {18}->{20}: inherited
             --------------------------
             
             This path is subsumed by the proof of path {18}->{20}->{6,9,7}->{8}.
           
           * Path {18}->{20}->{6,9,7}: inherited
             -----------------------------------
             
             This path is subsumed by the proof of path {18}->{20}->{6,9,7}->{8}.
           
           * Path {18}->{20}->{6,9,7}->{8}: NA
             ---------------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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 {18}->{20}->{8}: MAYBE
             ---------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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:
                 {  if_times^#(false(), s(x), y) -> c_19(plus^#(y, times(x, y)))
                  , times^#(s(x), y) -> c_17(if_times^#(even(s(x)), s(x), y))
                  , plus^#(zero(), y) -> c_7()
                  , even(0()) -> true()
                  , even(s(0())) -> false()
                  , even(s(s(x))) -> even(x)
                  , times(0(), y) -> 0()
                  , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                  , if_times(true(), s(x), y) ->
                    plus(times(half(s(x)), y), times(half(s(x)), y))
                  , if_times(false(), s(x), y) -> plus(y, times(x, y))
                  , half(0()) -> 0()
                  , half(s(s(x))) -> s(half(x))
                  , plus(s(x), s(y)) ->
                    s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                  , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                  , plus(zero(), y) -> y
                  , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                  , id(x) -> x
                  , if(true(), x, y) -> x
                  , if(false(), x, y) -> y
                  , not(x) -> if(x, false(), true())
                  , gt(s(x), zero()) -> true()
                  , gt(zero(), y) -> false()
                  , gt(s(x), s(y)) -> gt(x, y)}
             
             Proof Output:    
               The input cannot be shown compatible
    
    2) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    4) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputMixed innermost wiehe14

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
MAYBE
InputMixed innermost wiehe14

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  even(0()) -> true()
     , even(s(0())) -> false()
     , even(s(s(x))) -> even(x)
     , half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(s(x), s(y)) ->
       s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
     , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
     , plus(zero(), y) -> y
     , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
     , id(x) -> x
     , if(true(), x, y) -> x
     , if(false(), x, y) -> y
     , not(x) -> if(x, false(), true())
     , gt(s(x), zero()) -> true()
     , gt(zero(), y) -> false()
     , gt(s(x), s(y)) -> gt(x, y)
     , times(0(), y) -> 0()
     , times(s(x), y) -> if_times(even(s(x)), s(x), y)
     , if_times(true(), s(x), y) ->
       plus(times(half(s(x)), y), times(half(s(x)), y))
     , if_times(false(), s(x), y) -> plus(y, times(x, y))}

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: even^#(0()) -> c_0()
              , 2: even^#(s(0())) -> c_1()
              , 3: even^#(s(s(x))) -> c_2(even^#(x))
              , 4: half^#(0()) -> c_3()
              , 5: half^#(s(s(x))) -> c_4(half^#(x))
              , 6: plus^#(s(x), s(y)) ->
                   c_5(plus^#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
              , 7: plus^#(s(x), x) ->
                   c_6(plus^#(if(gt(x, x), id(x), id(x)), s(x)))
              , 8: plus^#(zero(), y) -> c_7(y)
              , 9: plus^#(id(x), s(y)) ->
                   c_8(plus^#(x, if(gt(s(y), y), y, s(y))))
              , 10: id^#(x) -> c_9(x)
              , 11: if^#(true(), x, y) -> c_10(x)
              , 12: if^#(false(), x, y) -> c_11(y)
              , 13: not^#(x) -> c_12(if^#(x, false(), true()))
              , 14: gt^#(s(x), zero()) -> c_13()
              , 15: gt^#(zero(), y) -> c_14()
              , 16: gt^#(s(x), s(y)) -> c_15(gt^#(x, y))
              , 17: times^#(0(), y) -> c_16()
              , 18: times^#(s(x), y) -> c_17(if_times^#(even(s(x)), s(x), y))
              , 19: if_times^#(true(), s(x), y) ->
                    c_18(plus^#(times(half(s(x)), y), times(half(s(x)), y)))
              , 20: if_times^#(false(), s(x), y) -> c_19(plus^#(y, times(x, y)))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{18}                                                      [     inherited      ]
                |
                |->{19}                                                  [     inherited      ]
                |   |
                |   |->{6,9,7}                                           [     inherited      ]
                |   |   |
                |   |   `->{8}                                           [         NA         ]
                |   |
                |   `->{8}                                               [         NA         ]
                |
                `->{20}                                                  [     inherited      ]
                    |
                    |->{6,9,7}                                           [     inherited      ]
                    |   |
                    |   `->{8}                                           [         NA         ]
                    |
                    `->{8}                                               [       MAYBE        ]
             
             ->{17}                                                      [    YES(?,O(1))     ]
             
             ->{16}                                                      [   YES(?,O(n^1))    ]
                |
                |->{14}                                                  [   YES(?,O(n^1))    ]
                |
                `->{15}                                                  [   YES(?,O(n^1))    ]
             
             ->{13}                                                      [    YES(?,O(1))     ]
                |
                |->{11}                                                  [    YES(?,O(1))     ]
                |
                `->{12}                                                  [    YES(?,O(1))     ]
             
             ->{10}                                                      [    YES(?,O(1))     ]
             
             ->{5}                                                       [   YES(?,O(n^1))    ]
                |
                `->{4}                                                   [   YES(?,O(n^1))    ]
             
             ->{3}                                                       [   YES(?,O(n^1))    ]
                |
                |->{1}                                                   [   YES(?,O(n^1))    ]
                |
                `->{2}                                                   [    YES(?,O(1))     ]
             
           
         
         Sub-problems:
         -------------
           * Path {3}: YES(?,O(n^1))
             -----------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {1}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [1] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [3] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {even^#(s(s(x))) -> c_2(even^#(x))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(even^#) = {}, Uargs(c_2) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                even^#(x1) = [2] x1 + [0]
                c_2(x1) = [1] x1 + [7]
           
           * Path {3}->{1}: YES(?,O(n^1))
             ----------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {1}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {even^#(0()) -> c_0()}
               Weak Rules: {even^#(s(s(x))) -> c_2(even^#(x))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(even^#) = {}, Uargs(c_2) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [2]
                s(x1) = [1] x1 + [0]
                even^#(x1) = [2] x1 + [4]
                c_0() = [1]
                c_2(x1) = [1] x1 + [0]
           
           * Path {3}->{2}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {1}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {even^#(s(0())) -> c_1()}
               Weak Rules: {even^#(s(s(x))) -> c_2(even^#(x))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(even^#) = {}, Uargs(c_2) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [0]
                s(x1) = [0] x1 + [0]
                even^#(x1) = [0] x1 + [1]
                c_1() = [0]
                c_2(x1) = [1] x1 + [0]
           
           * Path {5}: YES(?,O(n^1))
             -----------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {1}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [1] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [3] x1 + [0]
                c_3() = [0]
                c_4(x1) = [1] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_4) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                half^#(x1) = [2] x1 + [0]
                c_4(x1) = [1] x1 + [7]
           
           * Path {5}->{4}: YES(?,O(n^1))
             ----------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {1}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [1] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {half^#(0()) -> c_3()}
               Weak Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_4) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [2]
                s(x1) = [1] x1 + [0]
                half^#(x1) = [2] x1 + [4]
                c_3() = [1]
                c_4(x1) = [1] x1 + [0]
           
           * Path {10}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [3] x1 + [0]
                c_9(x1) = [1] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {id^#(x) -> c_9(x)}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(id^#) = {}, Uargs(c_9) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                id^#(x1) = [7] x1 + [7]
                c_9(x1) = [1] x1 + [0]
           
           * Path {13}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [1] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [3] x1 + [0]
                c_12(x1) = [3] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {not^#(x) -> c_12(if^#(x, false(), true()))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(if^#) = {}, Uargs(not^#) = {}, Uargs(c_12) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                true() = [0]
                false() = [0]
                if^#(x1, x2, x3) = [7] x1 + [0] x2 + [0] x3 + [4]
                not^#(x1) = [7] x1 + [7]
                c_12(x1) = [0] x1 + [3]
           
           * Path {13}->{11}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {1}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [3] x2 + [0] x3 + [0]
                c_10(x1) = [1] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [1] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {if^#(true(), x, y) -> c_10(x)}
               Weak Rules: {not^#(x) -> c_12(if^#(x, false(), true()))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(if^#) = {}, Uargs(c_10) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                true() = [2]
                false() = [0]
                if^#(x1, x2, x3) = [2] x1 + [2] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [1]
                not^#(x1) = [7] x1 + [7]
                c_12(x1) = [2] x1 + [7]
           
           * Path {13}->{12}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {1}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [3] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [1] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [1] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {if^#(false(), x, y) -> c_11(y)}
               Weak Rules: {not^#(x) -> c_12(if^#(x, false(), true()))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(if^#) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                true() = [0]
                false() = [2]
                if^#(x1, x2, x3) = [2] x1 + [0] x2 + [0] x3 + [4]
                c_11(x1) = [0] x1 + [1]
                not^#(x1) = [7] x1 + [7]
                c_12(x1) = [1] x1 + [3]
           
           * Path {16}: YES(?,O(n^1))
             ------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [1] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [3] x1 + [3] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [1] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {gt^#(s(x), s(y)) -> c_15(gt^#(x, y))}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                gt^#(x1, x2) = [2] x1 + [2] x2 + [0]
                c_15(x1) = [1] x1 + [7]
           
           * Path {16}->{14}: YES(?,O(n^1))
             ------------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [1] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {gt^#(s(x), zero()) -> c_13()}
               Weak Rules: {gt^#(s(x), s(y)) -> c_15(gt^#(x, y))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                zero() = [2]
                gt^#(x1, x2) = [2] x1 + [2] x2 + [0]
                c_13() = [1]
                c_15(x1) = [1] x1 + [7]
           
           * Path {16}->{15}: YES(?,O(n^1))
             ------------------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [1] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(n^1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {gt^#(zero(), y) -> c_14()}
               Weak Rules: {gt^#(s(x), s(y)) -> c_15(gt^#(x, y))}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(s) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {1}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                s(x1) = [1] x1 + [2]
                zero() = [2]
                gt^#(x1, x2) = [2] x1 + [0] x2 + [4]
                c_14() = [1]
                c_15(x1) = [1] x1 + [2]
           
           * Path {17}: 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(even) = {}, Uargs(s) = {}, Uargs(half) = {},
                 Uargs(plus) = {}, Uargs(if) = {}, Uargs(gt) = {}, Uargs(not) = {},
                 Uargs(id) = {}, Uargs(times) = {}, Uargs(if_times) = {},
                 Uargs(even^#) = {}, Uargs(c_2) = {}, Uargs(half^#) = {},
                 Uargs(c_4) = {}, Uargs(plus^#) = {}, Uargs(c_5) = {},
                 Uargs(c_6) = {}, Uargs(c_7) = {}, Uargs(c_8) = {},
                 Uargs(id^#) = {}, Uargs(c_9) = {}, Uargs(if^#) = {},
                 Uargs(c_10) = {}, Uargs(c_11) = {}, Uargs(not^#) = {},
                 Uargs(c_12) = {}, Uargs(gt^#) = {}, Uargs(c_15) = {},
                 Uargs(times^#) = {}, Uargs(c_17) = {}, Uargs(if_times^#) = {},
                 Uargs(c_18) = {}, Uargs(c_19) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                even(x1) = [0] x1 + [0]
                0() = [0]
                true() = [0]
                s(x1) = [0] x1 + [0]
                false() = [0]
                half(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                gt(x1, x2) = [0] x1 + [0] x2 + [0]
                not(x1) = [0] x1 + [0]
                id(x1) = [0] x1 + [0]
                zero() = [0]
                times(x1, x2) = [0] x1 + [0] x2 + [0]
                if_times(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                even^#(x1) = [0] x1 + [0]
                c_0() = [0]
                c_1() = [0]
                c_2(x1) = [0] x1 + [0]
                half^#(x1) = [0] x1 + [0]
                c_3() = [0]
                c_4(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                c_6(x1) = [0] x1 + [0]
                c_7(x1) = [0] x1 + [0]
                c_8(x1) = [0] x1 + [0]
                id^#(x1) = [0] x1 + [0]
                c_9(x1) = [0] x1 + [0]
                if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                c_11(x1) = [0] x1 + [0]
                not^#(x1) = [0] x1 + [0]
                c_12(x1) = [0] x1 + [0]
                gt^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13() = [0]
                c_14() = [0]
                c_15(x1) = [0] x1 + [0]
                times^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_16() = [0]
                c_17(x1) = [0] x1 + [0]
                if_times^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19(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: {times^#(0(), y) -> c_16()}
               Weak Rules: {}
             
             Proof Output:    
               The following argument positions are usable:
                 Uargs(times^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                0() = [7]
                times^#(x1, x2) = [1] x1 + [0] x2 + [7]
                c_16() = [1]
           
           * Path {18}: inherited
             --------------------
             
             This path is subsumed by the proof of path {18}->{20}->{6,9,7}->{8}.
           
           * Path {18}->{19}: inherited
             --------------------------
             
             This path is subsumed by the proof of path {18}->{19}->{6,9,7}->{8}.
           
           * Path {18}->{19}->{6,9,7}: inherited
             -----------------------------------
             
             This path is subsumed by the proof of path {18}->{19}->{6,9,7}->{8}.
           
           * Path {18}->{19}->{6,9,7}->{8}: NA
             ---------------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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 {18}->{19}->{8}: NA
             ------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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 {18}->{20}: inherited
             --------------------------
             
             This path is subsumed by the proof of path {18}->{20}->{6,9,7}->{8}.
           
           * Path {18}->{20}->{6,9,7}: inherited
             -----------------------------------
             
             This path is subsumed by the proof of path {18}->{20}->{6,9,7}->{8}.
           
           * Path {18}->{20}->{6,9,7}->{8}: NA
             ---------------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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 {18}->{20}->{8}: MAYBE
             ---------------------------
             
             The usable rules for this path are:
             
               {  even(0()) -> true()
                , even(s(0())) -> false()
                , even(s(s(x))) -> even(x)
                , times(0(), y) -> 0()
                , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                , if_times(true(), s(x), y) ->
                  plus(times(half(s(x)), y), times(half(s(x)), y))
                , if_times(false(), s(x), y) -> plus(y, times(x, y))
                , half(0()) -> 0()
                , half(s(s(x))) -> s(half(x))
                , plus(s(x), s(y)) ->
                  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                , plus(zero(), y) -> y
                , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                , id(x) -> x
                , if(true(), x, y) -> x
                , if(false(), x, y) -> y
                , not(x) -> if(x, false(), true())
                , gt(s(x), zero()) -> true()
                , gt(zero(), y) -> false()
                , gt(s(x), s(y)) -> gt(x, y)}
             
             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:
                 {  if_times^#(false(), s(x), y) -> c_19(plus^#(y, times(x, y)))
                  , times^#(s(x), y) -> c_17(if_times^#(even(s(x)), s(x), y))
                  , plus^#(zero(), y) -> c_7(y)
                  , even(0()) -> true()
                  , even(s(0())) -> false()
                  , even(s(s(x))) -> even(x)
                  , times(0(), y) -> 0()
                  , times(s(x), y) -> if_times(even(s(x)), s(x), y)
                  , if_times(true(), s(x), y) ->
                    plus(times(half(s(x)), y), times(half(s(x)), y))
                  , if_times(false(), s(x), y) -> plus(y, times(x, y))
                  , half(0()) -> 0()
                  , half(s(s(x))) -> s(half(x))
                  , plus(s(x), s(y)) ->
                    s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
                  , plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
                  , plus(zero(), y) -> y
                  , plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
                  , id(x) -> x
                  , if(true(), x, y) -> x
                  , if(false(), x, y) -> y
                  , not(x) -> if(x, false(), true())
                  , gt(s(x), zero()) -> true()
                  , gt(zero(), y) -> false()
                  , gt(s(x), s(y)) -> gt(x, y)}
             
             Proof Output:    
               The input cannot be shown compatible
    
    2) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    4) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.