YES
* Step 1: UnsatPaths YES
    + Considered Problem:
        Rules:
          0.  eval1(A,B,C,D) -> eval2(-1 + A,B,C,D)      [A >= 2]                                                     (1,1)
          1.  eval1(A,B,C,D) -> eval2(A,-1 + B,C,D)      [1 >= A]                                                     (1,1)
          2.  eval2(A,B,C,D) -> eval3(A,B,A,2*A)         [B >= 2]                                                     (?,1)
          3.  eval3(A,B,C,D) -> eval4(A,B,C,D)           [-2 + B >= 0 && B >= D && B >= 1 + D]                        (?,1)
          4.  eval3(A,B,C,D) -> eval4(A,B,C,1 + D)       [-2 + B >= 0 && B >= D && B >= 1 + D]                        (?,1)
          5.  eval3(A,B,C,D) -> eval3(A,B,D,2*D)         [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]              (?,1)
          6.  eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]              (?,1)
          7.  eval3(A,B,C,D) -> eval4(A,B,C,D)           [-2 + B >= 0 && B = D]                                       (?,1)
          8.  eval3(A,B,C,D) -> eval3(A,B,D,2*D)         [-2 + B >= 0 && D >= 1 && B = D]                             (?,1)
          9.  eval4(A,B,C,D) -> eval2(-1 + A,B,C,D)      [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] (?,1)
          10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D)      [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1]            (?,1)
        Signature:
          {(eval1,4);(eval2,4);(eval3,4);(eval4,4)}
        Flow Graph:
          [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{3,4,5
          ,6,7,8},9->{2},10->{2}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(8,3),(8,4),(8,5),(8,6),(8,7),(8,8)]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0.  eval1(A,B,C,D) -> eval2(-1 + A,B,C,D)      [A >= 2]                                                     (1,1)
          1.  eval1(A,B,C,D) -> eval2(A,-1 + B,C,D)      [1 >= A]                                                     (1,1)
          2.  eval2(A,B,C,D) -> eval3(A,B,A,2*A)         [B >= 2]                                                     (?,1)
          3.  eval3(A,B,C,D) -> eval4(A,B,C,D)           [-2 + B >= 0 && B >= D && B >= 1 + D]                        (?,1)
          4.  eval3(A,B,C,D) -> eval4(A,B,C,1 + D)       [-2 + B >= 0 && B >= D && B >= 1 + D]                        (?,1)
          5.  eval3(A,B,C,D) -> eval3(A,B,D,2*D)         [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]              (?,1)
          6.  eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]              (?,1)
          7.  eval3(A,B,C,D) -> eval4(A,B,C,D)           [-2 + B >= 0 && B = D]                                       (?,1)
          8.  eval3(A,B,C,D) -> eval3(A,B,D,2*D)         [-2 + B >= 0 && D >= 1 && B = D]                             (?,1)
          9.  eval4(A,B,C,D) -> eval2(-1 + A,B,C,D)      [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] (?,1)
          10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D)      [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1]            (?,1)
        Signature:
          {(eval1,4);(eval2,4);(eval3,4);(eval4,4)}
        Flow Graph:
          [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{}
          ,9->{2},10->{2}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          eval1(A,B,C,D) -> eval2(-1 + A,B,C,D)       [A >= 2]
          eval1(A,B,C,D) -> eval2(A,-1 + B,C,D)       [1 >= A]
          eval2(A,B,C,D) -> eval3(A,B,A,2*A)          [B >= 2]
          eval3(A,B,C,D) -> eval4(A,B,C,D)            [-2 + B >= 0 && B >= D && B >= 1 + D]
          eval3(A,B,C,D) -> eval4(A,B,C,1 + D)        [-2 + B >= 0 && B >= D && B >= 1 + D]
          eval3(A,B,C,D) -> eval3(A,B,D,2*D)          [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]
          eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D)  [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]
          eval3(A,B,C,D) -> eval4(A,B,C,D)            [-2 + B >= 0 && B = D]
          eval3(A,B,C,D) -> eval3(A,B,D,2*D)          [-2 + B >= 0 && D >= 1 && B = D]
          eval4(A,B,C,D) -> eval2(-1 + A,B,C,D)       [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2]
          eval4(A,B,C,D) -> eval2(A,-1 + B,C,D)       [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1]
        Signature:
          {(eval1,4);(eval2,4);(eval3,4);(eval4,4)}
        Rule Graph:
          [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{}
          ,9->{2},10->{2}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10]
          |
          `- p:[2,9,3,5,6,4,7,10] c: [10]
             |
             `- p:[2,9,3,5,6,4,7] c: [2,3,4,7,9]
                |
                `- p:[5,6] c: [6]
                   |
                   `- p:[5] c: [5]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          eval1(A,B,C,D) -> eval2(-1 + A,B,C,D)       [A >= 2]
          eval1(A,B,C,D) -> eval2(A,-1 + B,C,D)       [1 >= A]
          eval2(A,B,C,D) -> eval3(A,B,A,2*A)          [B >= 2]
          eval3(A,B,C,D) -> eval4(A,B,C,D)            [-2 + B >= 0 && B >= D && B >= 1 + D]
          eval3(A,B,C,D) -> eval4(A,B,C,1 + D)        [-2 + B >= 0 && B >= D && B >= 1 + D]
          eval3(A,B,C,D) -> eval3(A,B,D,2*D)          [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]
          eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D)  [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1]
          eval3(A,B,C,D) -> eval4(A,B,C,D)            [-2 + B >= 0 && B = D]
          eval3(A,B,C,D) -> eval3(A,B,D,2*D)          [-2 + B >= 0 && D >= 1 && B = D]
          eval4(A,B,C,D) -> eval2(-1 + A,B,C,D)       [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2]
          eval4(A,B,C,D) -> eval2(A,-1 + B,C,D)       [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1]
        Signature:
          {(eval1,4);(eval2,4);(eval3,4);(eval4,4)}
        Rule Graph:
          [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{}
          ,9->{2},10->{2}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10]
          |
          `- p:[2,9,3,5,6,4,7,10] c: [10]
             |
             `- p:[2,9,3,5,6,4,7] c: [2,3,4,7,9]
                |
                `- p:[5,6] c: [6]
                   |
                   `- p:[5] c: [5])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES