Basic predicates technique developed by Helen Mironchick for problem #18 of DEL(X) type

Denote by DEL (n, m) the statement "a natural number n is divided without a remainder by a positive integer m". For what is the smallest natural number A, the formula
    (D(34)⊕D(51) => ¬D(A)^D(425)) v ¬D(125) ≡ 1  
is identically true (that is, it takes the value 1 for any natural value of the variable x)?

Convert original equation from implication to disjunction

(D(34)≡D(51)) v ¬D(A)^D(425)) v ¬D(125) ≡ 1
D(34)^D(51) v ¬D(34)^¬D(51) v ¬D(A)^D(425)) v ¬D(125) ≡ 1

Supress D(17) in first and fourth terms via ¬D(17),
then supress D(5^2) via ¬D(5^3) in fourth term

D(34) = D(2)^D(17)
D(51) = D(3)^D(17)
D(31)*D(51) = D(2)^D(3)^D(17)

¬D(34) = (¬D(2) v ¬D(17))
¬D(51) = (¬D(3) v ¬D(17))

¬D(34)*¬D(34) = ¬D(2)*¬D(3) v ¬D(17)

D(2)^D(3)^D(17) v ¬D(2)^¬D(3) v ¬D(17) v 
  v  ¬D(A)^D(17)^D(5^2) v ¬D(5^3) ≡ 1

D(6) v ¬D(2)^¬D(3) v ¬D(17) v ¬D(A) v ¬D(5^3) ≡ 1

Thus A(min) = 6