Theorem([arbitrary(E,F,A,C), equiangle(A,C,F,F,C,E), equidistance(E,C,F,D), equidistance(F,D,C,D), equidistance(E,C,C,D), equidistance(A,B,F,D), equidistance(D,B,E,A), intersection(F,B,C,D,H), equidistance(E,B,F,B), equidistance(F,C,A,B), equidistance(A,B,C,D), equidistance(D,B,C,A), equidistance(C,A,F,D), equidistance(E,A,C,D), equidistance(C,A,C,D), equidistance(A,B,E,C), equidistance(C,A,A,B), equidistance(E,A,F,C), equidistance(C,A,F,C), equidistance(E,A,E,C), equidistance(E,A,F,D), equidistance(G,A,H,D), equidistance(E,A,A,B), equidistance(D,B,C,D), equidistance(E,G,F,H), equidistance(F,C,E,C), intersection(E,B,A,C,G), equidistance(C,A,E,C), equidistance(C,A,E,A), equidistance(D,B,F,C), equidistance(D,B,E,C), equidistance(D,B,F,D), parallel(A,B,C,D), parallel(B,D,A,C), perpendicular(A,C,C,D), perpendicular(A,C,A,B), perpendicular(B,D,C,D), perpendicular(B,D,A,B), equidistance(G,B,H,B), equidistance(C,G,C,H), equidistance(E,F,E,B), equidistance(E,F,F,B), equidistance(F,C,F,D), equidistance(F,C,C,D)],[equidistance(D,B,A,B)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G, H} are reassigned Theorem: If the points E, F, A, and C are arbitrary, the angle ACF is equal to the angle FCE, the distance between E and C is equal to the distance between F and D, the distance between F and D is equal to the distance between C and D, the distance between E and C is equal to the distance between C and D, the distance between A and B is equal to the distance between F and D, the distance between D and B is equal to the distance between E and A, the two lines FB and CD intersect at H, the distance between E and B is equal to the distance between F and B, the distance between F and C is equal to the distance between A and B, the distance between A and B is equal to the distance between C and D, the distance between D and B is equal to the distance between C and A, the distance between C and A is equal to the distance between F and D, the distance between E and A is equal to the distance between C and D, the distance between C and A is equal to the distance between C and D, the distance between A and B is equal to the distance between E and C, the distance between C and A is equal to the distance between A and B, the distance between E and A is equal to the distance between F and C, the distance between C and A is equal to the distance between F and C, the distance between E and A is equal to the distance between E and C, the distance between E and A is equal to the distance between F and D, the distance between G and A is equal to the distance between H and D, the distance between E and A is equal to the distance between A and B, the distance between D and B is equal to the distance between C and D, the distance between E and G is equal to the distance between F and H, the distance between F and C is equal to the distance between E and C, the two lines EB and AC intersect at G, the distance between C and A is equal to the distance between E and C, the distance between C and A is equal to the distance between E and A, the distance between D and B is equal to the distance between F and C, the distance between D and B is equal to the distance between E and C, the distance between D and B is equal to the distance between F and D, the line AB is parallel to the line CD, the line BD is parallel to the line AC, the line AC is perpendicular to the line CD, the line AC is perpendicular to the line AB, the line BD is perpendicular to the line CD, the line BD is perpendicular to the line AB, the distance between G and B is equal to the distance between H and B, the distance between C and G is equal to the distance between C and H, the distance between E and F is equal to the distance between E and B, the distance between E and F is equal to the distance between F and B, the distance between F and C is equal to the distance between F and D, and the distance between F and C is equal to the distance between C and D, then the distance between D and B is equal to the distance between A and B. Proof: Status: used = 2426341, alloced = 91920, time = 255.01399999999998 Status: used = 2489576, alloced = 91920, time = 261.005 Status: used = 2514537, alloced = 91920, time = 263.501 Status: used = 2516580, alloced = 91920, time = 263.797 Status: used = 2582463, alloced = 91920, time = 269.101 Status: used = 2584061, alloced = 91920, time = 270.131 Status: used = 2585436, alloced = 91920, time = 270.396 Status: used = 2653635, alloced = 91920, time = 274.904 char set produced: [3 u3 1] [1 v1 2] [4 v2 1] [9 x1 1] [6 y1 1] [3 x2 1] [6 y2 1] [12 x3 1] [6 y3 1] [8 x4 1] [4 y4 1] char set recomputed: [6 u2 6] [3 u3 1] [5 v1 2] [4 v2 1] [6 x1 1] [9 y1 1] [3 x2 1] [3 y2 1] [4 x3 1] [4 y3 1] [3 x4 1] [4 y4 1] pseudo-remainder: [6 y2 1] = 2*v1*y2 + ... (5 terms) pseudo-remainder: [8 x2 1] = -2*v1*x2*x1 + ... (7 terms) pseudo-remainder: [9 y1 2] = -v1*y1^2 + ... (8 terms) pseudo-remainder: [31 x1 2] = -9*u1^4*u2^2*x1^2*v1 + ... (30 terms) pseudo-remainder: [21 v1 2] = -6561*u1^10*v1^2 + ... (20 terms) pseudo-remainder: [10 u2 11] = 512*u1*u2^11 + ... (9 terms) the thoerem is possibly false: further decomposition in progress char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [3 u2 2] [4 u3 1] [3 v1 2] [3 v2 1] [3 x1 1] [2 y1 1] [4 x2 1] [3 y2 1] [3 x3 1] [3 y3 1] [3 x4 1] [3 y4 1] pseudo-remainder: [6 y2 1] = 2*v1*y2 + ... (5 terms) pseudo-remainder: [8 x2 1] = 2*v1*x2*x1 + ... (7 terms) pseudo-remainder: [14 y1 2] = -u1*v1*y1^2 + ... (13 terms) pseudo-remainder: [4 x1 2] = -u1*x1^2*v1 + ... (3 terms) pseudo-remainder: [4 u2 3] = u2^3 + ... (3 terms) char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] `The theorem is true under the following subsidiary conditions:` . the three points A, E and F are not collinear . the line EF is non-isotropic . the line AF is not perpendicular to the line EF QED.
