A computer-aided proof of a conjecture in Euclidean geometry

We prove a conjecture of Daia [L. Daia, On a conjecture, Gaz. Math. 89 (1984) 276–279 (in Romanian)] asserting that if a point PP in the interior of the square ABCDABCD has the property that the quadrilateral with vertices in the incenters of triangles ABPABP, BCPBCP, CDPCDP, DAPDAP is cyclic, then PP is on a diagonal. Co-operation man-machine is needed for the proof.