forall V1 Z (V1 = Z and (exists Z1 Z2 (Z1 = Z and exists I$i J$i K$i (I$i = 1 and J$i = b and Z2 = K$i and I$i <= K$i <= J$i) and Z1 = Z2) and exists Z1 Z2 (exists I$i J$i (Z1 = I$i * J$i and I$i = Z and J$i = Z) and Z2 = b and Z1 <= Z2) and exists Z1 Z2 (exists I$i J$i (Z1 = I$i * J$i and exists I1$i J$i (I$i = I1$i + J$i and I1$i = Z and J$i = 1) and exists I$i J1$i (J$i = I$i + J1$i and I$i = Z and J1$i = 1)) and Z2 = b and Z1 > Z2)) -> sqrt_b(V1)).
forall V1 X Y Z (exists I$i J$i (V1 = I$i * J$i and I$i = X and J$i = Y) and (exists Z1 (Z1 = Z and sqrt_b(Z1)) and exists Z1 Z2 (Z1 = X and exists I$i J$i K$i (I$i = 2 and J$i = Z and Z2 = K$i and I$i <= K$i <= J$i) and Z1 = Z2) and exists Z Z1 (Z = Y and exists I$i J$i K$i (I$i = 2 and J$i = b and Z1 = K$i and I$i <= K$i <= J$i) and Z = Z1)) -> composite(V1)).
forall V1 X (V1 = X and (exists Z Z1 (Z = X and exists I$i J$i K$i (I$i = a and J$i = b and Z1 = K$i and I$i <= K$i <= J$i) and Z = Z1) and exists Z (Z = X and not composite(Z))) -> prime(V1)).
