Equilateral triangles on the sides of a triangle
Let ABC be a triangle with vertex A, B and C, and let A1BC, AB1C and ABC1 be three equilateral triangles erected on the three sides of ABC. Then, check if the segments B1C1 and A1C have the same length, that is, B1C1 =A1C.
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).