YES(?,POLY)
* Step 1: FromIts WORST_CASE(?,POLY)
    + Considered Problem:
        Rules:
          0. evalDis1start(A,B,C,D)    -> evalDis1entryin(A,B,C,D)   True         (1,1)
          1. evalDis1entryin(A,B,C,D)  -> evalDis1bb3in(B,A,D,C)     True         (?,1)
          2. evalDis1bb3in(A,B,C,D)    -> evalDis1bbin(A,B,C,D)      [A >= 1 + B] (?,1)
          3. evalDis1bb3in(A,B,C,D)    -> evalDis1returnin(A,B,C,D)  [B >= A]     (?,1)
          4. evalDis1bbin(A,B,C,D)     -> evalDis1bb1in(A,B,C,D)     [C >= 1 + D] (?,1)
          5. evalDis1bbin(A,B,C,D)     -> evalDis1bb2in(A,B,C,D)     [D >= C]     (?,1)
          6. evalDis1bb1in(A,B,C,D)    -> evalDis1bb3in(A,B,C,1 + D) True         (?,1)
          7. evalDis1bb2in(A,B,C,D)    -> evalDis1bb3in(A,1 + B,C,D) True         (?,1)
          8. evalDis1returnin(A,B,C,D) -> evalDis1stop(A,B,C,D)      True         (?,1)
        Signature:
          {(evalDis1bb1in,4)
          ;(evalDis1bb2in,4)
          ;(evalDis1bb3in,4)
          ;(evalDis1bbin,4)
          ;(evalDis1entryin,4)
          ;(evalDis1returnin,4)
          ;(evalDis1start,4)
          ;(evalDis1stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: AddSinks WORST_CASE(?,POLY)
    + Considered Problem:
        Rules:
          evalDis1start(A,B,C,D)    -> evalDis1entryin(A,B,C,D)    True
          evalDis1entryin(A,B,C,D)  -> evalDis1bb3in(B,A,D,C)      True
          evalDis1bb3in(A,B,C,D)    -> evalDis1bbin(A,B,C,D)       [A >= 1 + B]
          evalDis1bb3in(A,B,C,D)    -> evalDis1returnin(A,B,C,D)   [B >= A]
          evalDis1bbin(A,B,C,D)     -> evalDis1bb1in(A,B,C,D)      [C >= 1 + D]
          evalDis1bbin(A,B,C,D)     -> evalDis1bb2in(A,B,C,D)      [D >= C]
          evalDis1bb1in(A,B,C,D)    -> evalDis1bb3in(A,B,C,1 + D)  True
          evalDis1bb2in(A,B,C,D)    -> evalDis1bb3in(A,1 + B,C,D)  True
          evalDis1returnin(A,B,C,D) -> evalDis1stop(A,B,C,D)       True
        Signature:
          {(evalDis1bb1in,4)
          ;(evalDis1bb2in,4)
          ;(evalDis1bb3in,4)
          ;(evalDis1bbin,4)
          ;(evalDis1entryin,4)
          ;(evalDis1returnin,4)
          ;(evalDis1start,4)
          ;(evalDis1stop,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 3: Decompose WORST_CASE(?,POLY)
    + Considered Problem:
        Rules:
          evalDis1start(A,B,C,D)    -> evalDis1entryin(A,B,C,D)    True
          evalDis1entryin(A,B,C,D)  -> evalDis1bb3in(B,A,D,C)      True
          evalDis1bb3in(A,B,C,D)    -> evalDis1bbin(A,B,C,D)       [A >= 1 + B]
          evalDis1bb3in(A,B,C,D)    -> evalDis1returnin(A,B,C,D)   [B >= A]
          evalDis1bbin(A,B,C,D)     -> evalDis1bb1in(A,B,C,D)      [C >= 1 + D]
          evalDis1bbin(A,B,C,D)     -> evalDis1bb2in(A,B,C,D)      [D >= C]
          evalDis1bb1in(A,B,C,D)    -> evalDis1bb3in(A,B,C,1 + D)  True
          evalDis1bb2in(A,B,C,D)    -> evalDis1bb3in(A,1 + B,C,D)  True
          evalDis1returnin(A,B,C,D) -> evalDis1stop(A,B,C,D)       True
          evalDis1stop(A,B,C,D)     -> exitus616(A,B,C,D)          True
        Signature:
          {(evalDis1bb1in,4)
          ;(evalDis1bb2in,4)
          ;(evalDis1bb3in,4)
          ;(evalDis1bbin,4)
          ;(evalDis1entryin,4)
          ;(evalDis1returnin,4)
          ;(evalDis1start,4)
          ;(evalDis1stop,4)
          ;(exitus616,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{9}]
    + Applied Processor:
        Decompose Greedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9]
          |
          `- p:[2,6,4,7,5] c: [4,6]
             |
             `- p:[2,7,5] c: [2,5,7]
* Step 4: AbstractSize WORST_CASE(?,POLY)
    + Considered Problem:
        (Rules:
          evalDis1start(A,B,C,D)    -> evalDis1entryin(A,B,C,D)    True
          evalDis1entryin(A,B,C,D)  -> evalDis1bb3in(B,A,D,C)      True
          evalDis1bb3in(A,B,C,D)    -> evalDis1bbin(A,B,C,D)       [A >= 1 + B]
          evalDis1bb3in(A,B,C,D)    -> evalDis1returnin(A,B,C,D)   [B >= A]
          evalDis1bbin(A,B,C,D)     -> evalDis1bb1in(A,B,C,D)      [C >= 1 + D]
          evalDis1bbin(A,B,C,D)     -> evalDis1bb2in(A,B,C,D)      [D >= C]
          evalDis1bb1in(A,B,C,D)    -> evalDis1bb3in(A,B,C,1 + D)  True
          evalDis1bb2in(A,B,C,D)    -> evalDis1bb3in(A,1 + B,C,D)  True
          evalDis1returnin(A,B,C,D) -> evalDis1stop(A,B,C,D)       True
          evalDis1stop(A,B,C,D)     -> exitus616(A,B,C,D)          True
        Signature:
          {(evalDis1bb1in,4)
          ;(evalDis1bb2in,4)
          ;(evalDis1bb3in,4)
          ;(evalDis1bbin,4)
          ;(evalDis1entryin,4)
          ;(evalDis1returnin,4)
          ;(evalDis1start,4)
          ;(evalDis1stop,4)
          ;(exitus616,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{9}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9]
          |
          `- p:[2,6,4,7,5] c: [4,6]
             |
             `- p:[2,7,5] c: [2,5,7])
    + Applied Processor:
        AbstractSize Minimize
    + Details:
        ()
* Step 5: AbstractFlow WORST_CASE(?,POLY)
    + Considered Problem:
        Program:
          Domain: [A,B,C,D,0.0,0.0.0]
           evalDis1start     ~>  evalDis1entryin    [A <= A, B <= B, C <= C, D <= D]
           evalDis1entryin   ~>  evalDis1bb3in      [A <= B, B <= A, C <= D, D <= C]
           evalDis1bb3in     ~>  evalDis1bbin       [A <= A, B <= B, C <= C, D <= D]
           evalDis1bb3in     ~>  evalDis1returnin   [A <= A, B <= B, C <= C, D <= D]
           evalDis1bbin      ~>  evalDis1bb1in      [A <= A, B <= B, C <= C, D <= D]
           evalDis1bbin      ~>  evalDis1bb2in      [A <= A, B <= B, C <= C, D <= D]
           evalDis1bb1in     ~>  evalDis1bb3in      [A <= A, B <= B, C <= C, D <= K + D]
           evalDis1bb2in     ~>  evalDis1bb3in      [A <= A, B <= K + B, C <= C, D <= D]
           evalDis1returnin  ~>  evalDis1stop       [A <= A, B <= B, C <= C, D <= D]
           evalDis1stop      ~>  exitus616          [A <= A, B <= B, C <= C, D <= D]
          + Loop: [0.0 <= K + C + D]
               evalDis1bb3in  ~>  evalDis1bbin    [A <= A, B <= B, C <= C, D <= D]
               evalDis1bb1in  ~>  evalDis1bb3in   [A <= A, B <= B, C <= C, D <= K + D]
               evalDis1bbin   ~>  evalDis1bb1in   [A <= A, B <= B, C <= C, D <= D]
               evalDis1bb2in  ~>  evalDis1bb3in   [A <= A, B <= K + B, C <= C, D <= D]
               evalDis1bbin   ~>  evalDis1bb2in   [A <= A, B <= B, C <= C, D <= D]
            + Loop: [0.0.0 <= K + A + B]
                 evalDis1bb3in  ~>  evalDis1bbin    [A <= A, B <= B, C <= C, D <= D]
                 evalDis1bb2in  ~>  evalDis1bb3in   [A <= A, B <= K + B, C <= C, D <= D]
                 evalDis1bbin   ~>  evalDis1bb2in   [A <= A, B <= B, C <= C, D <= D]
    + Applied Processor:
        AbstractFlow
    + Details:
        ()
* Step 6: Lare WORST_CASE(?,POLY)
    + Considered Problem:
        Program:
          Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0]
           evalDis1start     ~>  evalDis1entryin    []
           evalDis1entryin   ~>  evalDis1bb3in      [A ~=> B,B ~=> A,C ~=> D,D ~=> C]
           evalDis1bb3in     ~>  evalDis1bbin       []
           evalDis1bb3in     ~>  evalDis1returnin   []
           evalDis1bbin      ~>  evalDis1bb1in      []
           evalDis1bbin      ~>  evalDis1bb2in      []
           evalDis1bb1in     ~>  evalDis1bb3in      [D ~+> D,K ~+> D]
           evalDis1bb2in     ~>  evalDis1bb3in      [B ~+> B,K ~+> B]
           evalDis1returnin  ~>  evalDis1stop       []
           evalDis1stop      ~>  exitus616          []
          + Loop: [C ~+> 0.0,D ~+> 0.0,K ~+> 0.0]
               evalDis1bb3in  ~>  evalDis1bbin    []
               evalDis1bb1in  ~>  evalDis1bb3in   [D ~+> D,K ~+> D]
               evalDis1bbin   ~>  evalDis1bb1in   []
               evalDis1bb2in  ~>  evalDis1bb3in   [B ~+> B,K ~+> B]
               evalDis1bbin   ~>  evalDis1bb2in   []
            + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,K ~+> 0.0.0]
                 evalDis1bb3in  ~>  evalDis1bbin    []
                 evalDis1bb2in  ~>  evalDis1bb3in   [B ~+> B,K ~+> B]
                 evalDis1bbin   ~>  evalDis1bb2in   []
    + Applied Processor:
        Lare
    + Details:
         evalDis1start  ~>  exitus616   [A ~=> B
                                        ,B ~=> A
                                        ,C ~=> D
                                        ,D ~=> C
                                        ,A ~+> B
                                        ,A ~+> 0.0.0
                                        ,A ~+> tick
                                        ,B ~+> 0.0.0
                                        ,B ~+> tick
                                        ,C ~+> D
                                        ,C ~+> 0.0
                                        ,C ~+> tick
                                        ,D ~+> 0.0
                                        ,D ~+> tick
                                        ,tick ~+> tick
                                        ,K ~+> B
                                        ,K ~+> D
                                        ,K ~+> 0.0
                                        ,K ~+> 0.0.0
                                        ,K ~+> tick
                                        ,A ~*> B
                                        ,A ~*> 0.0.0
                                        ,A ~*> tick
                                        ,B ~*> B
                                        ,B ~*> 0.0.0
                                        ,B ~*> tick
                                        ,C ~*> B
                                        ,C ~*> D
                                        ,C ~*> tick
                                        ,D ~*> B
                                        ,D ~*> D
                                        ,D ~*> tick
                                        ,K ~*> B
                                        ,K ~*> D
                                        ,K ~*> 0.0.0
                                        ,K ~*> tick
                                        ,C ~^> B
                                        ,D ~^> B
                                        ,K ~^> B]
        + <evalDis1bb3in  ~>  evalDis1bb3in>  [A ~+> 0.0.0
                                              ,A ~+> tick
                                              ,B ~+> B
                                              ,B ~+> 0.0.0
                                              ,B ~+> tick
                                              ,C ~+> 0.0
                                              ,C ~+> tick
                                              ,D ~+> D
                                              ,D ~+> 0.0
                                              ,D ~+> tick
                                              ,tick ~+> tick
                                              ,K ~+> B
                                              ,K ~+> D
                                              ,K ~+> 0.0
                                              ,K ~+> 0.0.0
                                              ,K ~+> tick
                                              ,A ~*> B
                                              ,A ~*> 0.0.0
                                              ,A ~*> tick
                                              ,B ~*> B
                                              ,B ~*> 0.0.0
                                              ,B ~*> tick
                                              ,C ~*> B
                                              ,C ~*> D
                                              ,C ~*> tick
                                              ,D ~*> B
                                              ,D ~*> D
                                              ,D ~*> tick
                                              ,K ~*> B
                                              ,K ~*> D
                                              ,K ~*> 0.0.0
                                              ,K ~*> tick
                                              ,C ~^> B
                                              ,D ~^> B
                                              ,K ~^> B]
          + <evalDis1bb3in  ~>  evalDis1bbin>   [A ~+> 0.0.0
                                                ,A ~+> tick
                                                ,B ~+> B
                                                ,B ~+> 0.0.0
                                                ,B ~+> tick
                                                ,tick ~+> tick
                                                ,K ~+> B
                                                ,K ~+> 0.0.0
                                                ,K ~+> tick
                                                ,A ~*> B
                                                ,B ~*> B
                                                ,K ~*> B]
            <evalDis1bb3in  ~>  evalDis1bb3in>  [A ~+> 0.0.0
                                                ,A ~+> tick
                                                ,B ~+> B
                                                ,B ~+> 0.0.0
                                                ,B ~+> tick
                                                ,tick ~+> tick
                                                ,K ~+> B
                                                ,K ~+> 0.0.0
                                                ,K ~+> tick
                                                ,A ~*> B
                                                ,B ~*> B
                                                ,K ~*> B]

YES(?,POLY)