Consider the logic program program below where the symbols x and 1 are constants, symbols A, DA, B, DB, C, and D are variables, diff is a categorical symbol, and sin, cos, *, +, - are function symbols. 1. diff (x, 1) 2. diff (A+B, 3. diff (A*B, 4. diff (sin (A), 5. diff (cos (A), (-sin (A) *DA)) diff (A, DA) DA+DB) diff (A, DA), diff (B, DB) A*DB+B*DA) - diff (A, DA), diff (B, DB) (cos (A) *DA)) - diff (A, DA) 1 (a) Use the SLD resolution method to arrive at a refutation of the goal below and calculate the resulting correct answer substitution. - diff (sin (x) *cos(x), C) (B) Construct the SLD tree corresponding to the following goal: - diff (D, x* (cos (x) *1)+sin (x) *1)