Let ABC be a triangle, ACDE and BCFG be two squares drawn on the two sides AC and BC respectively, and M be the midpoint of the line segment AB. Checking whether the conclusion |DF| = 2|CM| is true or not.[br][br]This example appears as Example 3.7 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).