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 P in the interior of the square ABCD has the property that the quadrilateral with vertices in the incenters of triangles ABP, BCP, CDP, DAP is cyclic, then P is on a diagonal. Co-operation man-machine is needed for the proof.