geometry - 平方交差をサポートする幾何学定理証明器

Question

「7 つの互いに素な正方形の 3 つのコレクションごとに、各コレクションから 1 つの正方形を選択して、3 つの代表が内部的に互いに素になるようにすることは可能ですか?」など、正方形に関連する幾何学のいくつかの定理を自動的に証明/反証しようとしています。

私はOpenGeoProverを使用しようとしましたが、正方形の次の説明を思いつきました:

    <!-- define a 'free' point - the south-western corner of the square: -->
    <pfree       label="square1southwest"/>

    <!-- define a line that is parallel to the x axis and goes throught that point - the southern boundary: -->
    <lparallel   label="square1south" point="square1southwest" baseline="xaxis" />

    <!-- define a random point on the southern line, which will be the south-eastern corner: -->
    <prandline   label="square1southeast" line="square1south" />

    <!-- rotate the south-eastern corner 90 degrees around the south-western corner, to create the north-western corner: -->
    <protated    label="square1northwest" origpt="square1southeast" center="square1southwest" angmeasure="-90"/>

    <!-- translate the north-western corner by the vector between the two southern corners, to create the north-eastern corner of the square: -->
    <ptranslated label="square1northeast" origpt="square1northwest" point1="square1southwest" point2="square1southeast"/>

これが私が立ち往生している場所です:「正方形Aと正方形Bが交差する」という単純なステートメントをどのように定義するのですか?

Z3 では、この問題にどのようにアプローチできますか?