YES(?,O(n^1))
* Step 1: TrivialSCCs WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. sqrt(A,B,C,D) -> f(0,1,1,D)                 True               (1,1)
          1. f(A,B,C,D)    -> f(1 + A,2 + B,2 + B + C,D) [D >= C && B >= 0] (?,1)
          2. f(A,B,C,D)    -> end(A,B,C,D)               [C >= 1 + D]       (?,1)
        Signature:
          {(end,4);(f,4);(sqrt,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. sqrt(A,B,C,D) -> f(0,1,1,D)                 True               (1,1)
          1. f(A,B,C,D)    -> f(1 + A,2 + B,2 + B + C,D) [D >= C && B >= 0] (?,1)
          2. f(A,B,C,D)    -> end(A,B,C,D)               [C >= 1 + D]       (1,1)
        Signature:
          {(end,4);(f,4);(sqrt,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(end) = 1 + -1*x3 + x4
             p(f) = 1 + -1*x3 + x4
          p(sqrt) = x4            
        
        Following rules are strictly oriented:
        [D >= C && B >= 0] ==>                           
                f(A,B,C,D)   = 1 + -1*C + D              
                             > -1 + -1*B + -1*C + D      
                             = f(1 + A,2 + B,2 + B + C,D)
        
        
        Following rules are weakly oriented:
                   True ==>             
          sqrt(A,B,C,D)   = D           
                         >= D           
                          = f(0,1,1,D)  
        
           [C >= 1 + D] ==>             
             f(A,B,C,D)   = 1 + -1*C + D
                         >= 1 + -1*C + D
                          = end(A,B,C,D)
        
        
* Step 3: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. sqrt(A,B,C,D) -> f(0,1,1,D)                 True               (1,1)
          1. f(A,B,C,D)    -> f(1 + A,2 + B,2 + B + C,D) [D >= C && B >= 0] (D,1)
          2. f(A,B,C,D)    -> end(A,B,C,D)               [C >= 1 + D]       (1,1)
        Signature:
          {(end,4);(f,4);(sqrt,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{}]
        
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

YES(?,O(n^1))