Let ABC be a triangle with vertex A, B and C, and let A[sub]1[/sub]BC, AB[sub]1[/sub]C and ABC[sub]1[/sub] be three equilateral triangles erected on the three sides of ABC. Then, check if the segments B[sub]1[/sub]C[sub]1[/sub] and A[sub]1[/sub]C have the same length, that is, B[sub]1[/sub]C[sub]1[/sub] =A[sub]1[/sub]C.[br][br]This example appears as example 3.8 in: Zhou, J., Wang, D., Sun, Y.: Automated reducible geometric theorem proving and discovery by Gröbner basis method, Journal of Automated Reasoning, 59(3), 331-344 (2017).