Mined Theorems

Theorems

Theorem([arbitrary(C,A,G), oncircle(A,C,G,B), perpfoot(A,C,G,H,H), perpfoot(A,C,B,E,E), perpfoot(B,C,A,D,D), parallel(D,A,J,G), online(B,I,A), intersection(B,E,D,A,F), perpfoot(B,C,G,J,J), perpendicular(B,I,I,G), parallel(B,E,H,G), midpoint(F,G,M), online(I,J,H)],[online(I,J,M)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, M} are reassigned

Theorem: If the points C, A, and G are arbitrary, the point B is on the circumcircle of the triangle ACG, H is the perpendicular foot of the line AC to the line GH, E is the perpendicular foot of the line AC to the line BE, D is the perpendicular foot of the line BC to the line AD, the line DA is parallel to the line JG, `the point A is on the line B` || (I) , the two lines BE and DA intersect at F, J is the perpendicular foot of the line BC to the line GJ, `the line B` || (I) || ` is perpendicular to the line ` || (I) || G , the line BE is parallel to the line HG, M is the midpoint of F and G, and `the point H is on the line ` || (I) || J , then `the point M is on the line ` || (I) || J .

Proof:

Status: used = 770, alloced = 3072, time = 4.601999999999999
char set produced: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [8 x4 1] [4 y4 1] [7 x5 1] [4 y5 1] [12 x6 1] [4 y6 1] [12 x7 1] [6 y7 1] [2 x8 1] [3 y8 1]
char set recomputed: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [12 x4 1] [4 y4 1] [8 x5 1] [4 y5 1] [25 x6 1] [4 y6 1] [2 x7 1] [10 y7 1] [2 x8 1] [3 y8 1]
pseudo-remainder: [6 y8 1] = x5*y8 + ... (5 terms)
pseudo-remainder: [8 x8 1] = -2*y5*x8 + ... (7 terms)
pseudo-remainder: [8 y7 1] = y7*x5 + ... (7 terms)
pseudo-remainder: [40 x7 1] = u1*u2*v1*x7*y5 + ... (39 terms)
pseudo-remainder: [40 y6 1] = x1*u1*u2*v1*y6 + ... (39 terms)
pseudo-remainder: [59 x6 1] = v1^2*u2^2*u1*x6 + ... (58 terms)
pseudo-remainder: [246 y5 1] = 2*u1^4*u2^4*v1^2*y5 + ... (245 terms)
pseudo-remainder: [186 x5 1] = u1^5*u2^2*v1^3*x5 + ... (185 terms)
pseudo-remainder: [342 x4 1] = u1^6*x4*v1^4*u2^2 + ... (341 terms)
pseudo-remainder: [425 y1 5] = -2*u1^7*y1^5*u2^2*v1^2 + ... (424 terms)

`The theorem is true under the following subsidiary conditions:`
. the three points A, C and G are not collinear
. the line CG is non-isotropic
. the line AG is not perpendicular to the line AC
. v1*u1^2-u1*u2*v1-u1*v1*x1+u1*y1*u2+y1*v1^2+x1*u2*v1 <> 0
. -u1*v1*x1+u1*u2*v1-u1*y1*u2-x1*u2*v1-y1*v1^2+v1*x1^2 <> 0
. -u1^2*v1*x1*u2+u1^2*v1*u2^2-u1^2*y1*u2^2+x1^2*v1*u2*u1-u1*v1^2*x1*y1-y1*v1^2*u2*u1-u1*x1*v1^3+u1*v1^3*u2-x1*v1*u2^2*u1+x1^2*v1^3-u2*v1^2*x1*y1+y1*v1^2*x1^2-y1*v1^4-u2*x1*v1^3 <> 0
. the three points A, B and C are not collinear
. the line AC is not perpendicular to the line AB
. the line AC is not perpendicular to the line BC

QED.

Theorem([arbitrary(C,A,G), oncircle(A,C,G,B), perpfoot(A,C,G,H,H), perpfoot(A,C,B,E,E), perpfoot(B,C,A,D,D), parallel(D,A,J,G), online(B,I,A), intersection(B,E,D,A,F), perpfoot(B,C,G,J,J), perpendicular(B,I,I,G), parallel(B,E,H,G), midpoint(F,G,M), online(I,J,M)],[online(I,J,H)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, M} are reassigned

Theorem: If the points C, A, and G are arbitrary, the point B is on the circumcircle of the triangle ACG, H is the perpendicular foot of the line AC to the line GH, E is the perpendicular foot of the line AC to the line BE, D is the perpendicular foot of the line BC to the line AD, the line DA is parallel to the line JG, `the point A is on the line B` || (I) , the two lines BE and DA intersect at F, J is the perpendicular foot of the line BC to the line GJ, `the line B` || (I) || ` is perpendicular to the line ` || (I) || G , the line BE is parallel to the line HG, M is the midpoint of F and G, and `the point M is on the line ` || (I) || J , then `the point H is on the line ` || (I) || J .

Proof:

Status: used = 3232, alloced = 5506, time = 4.758000000000001
Status: used = 12372, alloced = 13080, time = 5.6000000000000005
char set produced: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [8 x4 1] [4 y4 1] [7 x5 1] [4 y5 1] [81 x6 1] [4 y6 1] [12 x7 1] [6 y7 1] [2 x8 1] [3 y8 1]
char set recomputed: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [12 x4 1] [4 y4 1] [8 x5 1] [4 y5 1] [473 x6 1] [4 y6 1] [2 x7 1] [10 y7 1] [2 x8 1] [3 y8 1]
pseudo-remainder: [6 y6 1] = y6*x2 + ... (5 terms)
pseudo-remainder: [12 x6 1] = u2*x6*y2 + ... (11 terms)
pseudo-remainder: [1784 y5 1] = 2*u1^9*u2^9*v1*y5 + ... (1783 terms)
pseudo-remainder: [1571 x5 1] = 2*u1^10*u2^7*v1*x5*y2 + ... (1570 terms)
pseudo-remainder: [3048 x4 1] = 2*u1^11*u2^7*v1^2*x4*y2 + ... (3047 terms)
pseudo-remainder: [3549 y2 1] = 2*u1^13*u2^8*v1^3*y2 + ... (3548 terms)
pseudo-remainder: [1444 x2 1] = -2*u1^11*u2^7*v1^2*x2*y1^2 + ... (1443 terms)
pseudo-remainder: [695 y1 3] = 2*y1^3*v1*u1^10*u2^7 + ... (694 terms)

`The theorem is true under the following subsidiary conditions:`
. the three points A, C and G are not collinear
. the line AG is not perpendicular to the line AC
. v1*u1^2-u1*u2*v1-u1*v1*x1+u1*y1*u2+y1*v1^2+x1*u2*v1 <> 0
. -u1*v1*x1+u1*u2*v1-u1*y1*u2-x1*u2*v1-y1*v1^2+v1*x1^2 <> 0
. -u1^2*v1*x1*u2+u1^2*v1*u2^2-u1^2*y1*u2^2+x1^2*v1*u2*u1-u1*v1^2*x1*y1-y1*v1^2*u2*u1-u1*x1*v1^3+u1*v1^3*u2-x1*v1*u2^2*u1+x1^2*v1^3-u2*v1^2*x1*y1+y1*v1^2*x1^2-y1*v1^4-u2*x1*v1^3 <> 0
. -2*u1^7*u2^5*v1^4*y1-2*u1^6*u2^6*v1^4*y1+7*u1^8*u2^5*v1^3*x1+4*u1^7*u2^6*v1^3*x1-9*u1^6*u2^6*v1^3*x1^2-10*u1^5*u2^6*v1^4*x1*y1+3*u1^5*u2^6*v1^3*x1^3+5*u1^4*u2^6*v1^4*x1^2*y1-12*u1^4*u2^4*v1^4*x1^4*y1+6*u1^4*u2^3*v1^4*x1^5*y1+u1^4*u2^5*v1^4*x1^3*y1-28*u1^5*u2^3*v1^4*x1^4*y1+8*u1^5*u2^5*v1^4*x1^2*y1-8*u1^5*u2^5*v1^3*x1^4+36*u1^5*u2^4*v1^4*x1^3*y1+4*u1^5*u2^4*v1^3*x1^5-6*u1^6*u2^4*v1^4*x1^2*y1-17*u1^6*u2^4*v1^3*x1^4+38*u1^6*u2^3*v1^4*x1^3*y1-28*u1^6*u2^5*v1^4*x1*y1+29*u1^6*u2^5*v1^3*x1^3-28*u1^7*u2^5*v1^3*x1^2-18*u1^7*u2^4*v1^4*x1*y1+22*u1^7*u2^4*v1^3*x1^3-16*u1^7*u2^3*v1^4*x1^2*y1-9*u1^8*u2^4*v1^3*x1^2-v1^16*y1+v1^15*x1^2-5*v1^13*x1^4+6*v1^11*x1^6-v1^9*x1^8+3*u1^8*u2^6*v1*x1^2+u1^7*u2^7*v1*x1^2-u1^7*u2^6*v1*x1^3-5*u2^2*v1^12*x1^2*y1+3*u2^2*v1^8*x1^6*y1-5*u2*v1^14*x1*y1+15*u2*v1^12*x1^3*y1-6*u2*v1^10*x1^5*y1-u2*v1^8*x1^7*y1+2*u2^4*v1^9*x1^4-2*u2^3*v1^11*x1^3-4*u2^2*v1^13*x1^2+10*u2^2*v1^11*x1^4+3*u2^2*v1^9*x1^6-u2*v1^15*x1+9*u2*v1^13*x1^3-14*u2*v1^11*x1^5+u2*v1^9*x1^7+6*v1^14*x1^2*y1-10*v1^12*x1^4*y1+4*v1^10*x1^6*y1-2*u1^9*u2^6*v1*x1-3*u1^8*u2^7*v1*x1+u1^8*u2^7*x1*y1-2*u1^8*u2^6*v1^2*y1-2*u1^7*u2^7*v1^2*y1+12*u1^7*u2^4*v1^5*x1-5*u1^7*u2^3*v1^5*x1^2-3*u1^6*u2^7*v1^3*x1+18*u1^6*u2^5*v1^5*x1-2*u1^6*u2^4*v1^6*y1-36*u1^6*u2^4*v1^5*x1^2+13*u1^6*u2^3*v1^7*x1-14*u1^6*u2^3*v1^5*x1^3-3*u1^6*u2^2*v1^7*x1^2+30*u1^6*u2^2*v1^5*x1^4-11*u1^6*u2*v1^7*x1^3+u1^5*u2^7*v1^3*x1^2+6*u1^5*u2^6*v1^5*x1-2*u1^5*u2^5*v1^6*y1+24*u1^5*u2^4*v1^7*x1+16*u1^5*u2^4*v1^5*x1^3-2*u1^5*u2^3*v1^8*y1-29*u1^5*u2^3*v1^7*x1^2+52*u1^5*u2^3*v1^5*x1^4+10*u1^5*u2^2*v1^9*x1-33*u1^5*u2^2*v1^7*x1^3-36*u1^5*u2^2*v1^5*x1^5+32*u1^5*u2*v1^7*x1^4-4*u1^5*v1^8*x1^3*y1-12*u1^4*u2^6*v1^5*x1^2+11*u1^4*u2^5*v1^7*x1-2*u1^4*u2^4*v1^8*y1-35*u1^4*u2^4*v1^7*x1^2+13*u1^4*u2^4*v1^5*x1^4+22*u1^4*u2^3*v1^9*x1-30*u1^4*u2^3*v1^7*x1^3-42*u1^4*u2^3*v1^5*x1^5-28*u1^4*u2^2*v1^9*x1^2+90*u1^4*u2^2*v1^7*x1^4+18*u1^4*u2^2*v1^5*x1^6-13*u1^4*u2*v1^9*x1^3-30*u1^4*u2*v1^7*x1^5-10*u1^4*v1^10*x1^2*y1+12*u1^4*v1^8*x1^4*y1+4*u1^3*u2^6*v1^5*x1^3-10*u1^3*u2^5*v1^7*x1^2-5*u1^3*u2^5*v1^5*x1^4+12*u1^3*u2^4*v1^9*x1-14*u1^3*u2^4*v1^7*x1^3-5*u1^3*u2^4*v1^5*x1^5-33*u1^3*u2^3*v1^9*x1^2+84*u1^3*u2^3*v1^7*x1^4-19*u1^3*u2^2*v1^9*x1^3-72*u1^3*u2^2*v1^7*x1^5-3*u1^3*u2^2*v1^5*x1^7+54*u1^3*u2*v1^9*x1^4+8*u1^3*u2*v1^7*x1^6+16*u1^3*v1^10*x1^3*y1-6*u1^2*u2^5*v1^7*x1^3-8*u1^2*u2^4*v1^9*x1^2+32*u1^2*u2^4*v1^7*x1^4-18*u1^2*u2^3*v1^9*x1^3-47*u1^2*u2^3*v1^7*x1^5+70*u1^2*u2^2*v1^9*x1^4+21*u1^2*u2^2*v1^7*x1^6-44*u1^2*u2*v1^9*x1^5+3*u1*u2^5*v1^7*x1^4-8*u1*u2^4*v1^9*x1^3-9*u1*u2^4*v1^7*x1^5+32*u1*u2^3*v1^9*x1^4+9*u1*u2^3*v1^7*x1^6-36*u1*u2^2*v1^9*x1^5+u2^4*v1^8*x1^4*y1+2*u2^3*v1^10*x1^3*y1-12*u1^3*v1^8*x1^5*y1+u1^2*u2*v1^7*x1^7-3*u1*u2^2*v1^7*x1^7-3*u2^3*v1^8*x1^5*y1-21*u1^6*u2^3*v1^6*x1*y1-27*u1^6*u2^2*v1^6*x1^2*y1-5*u1^6*u2*v1^6*x1^3*y1-38*u1^5*u2^4*v1^6*x1*y1-40*u1^5*u2^3*v1^6*x1^2*y1-20*u1^5*u2^2*v1^8*x1*y1+48*u1^5*u2^2*v1^6*x1^3*y1-24*u1^5*u2*v1^8*x1^2*y1+16*u1^5*u2*v1^6*x1^4*y1-17*u1^4*u2^5*v1^6*x1*y1-24*u1^4*u2^4*v1^6*x1^2*y1-40*u1^4*u2^3*v1^8*x1*y1+86*u1^4*u2^3*v1^6*x1^3*y1-47*u1^4*u2^2*v1^8*x1^2*y1-12*u1^4*u2^2*v1^6*x1^4*y1-15*u1^4*u2*v1^10*x1*y1+37*u1^4*u2*v1^8*x1^3*y1-18*u1^4*u2*v1^6*x1^5*y1-8*u1^3*u2^5*v1^6*x1^2*y1-20*u1^3*u2^4*v1^8*x1*y1+40*u1^3*u2^4*v1^6*x1^3*y1-40*u1^3*u2^3*v1^8*x1^2*y1-28*u1^3*u2^3*v1^6*x1^4*y1-34*u1^3*u2^2*v1^10*x1*y1+88*u1^3*u2^2*v1^8*x1^3*y1-12*u1^3*u2^2*v1^6*x1^5*y1-24*u1^3*u2*v1^10*x1^2*y1+4*u1^3*u2*v1^8*x1^4*y1+6*u1^2*u2^5*v1^6*x1^3*y1-18*u1^2*u2^4*v1^8*x1^2*y1-11*u1^2*u2^4*v1^6*x1^4*y1-19*u1^2*u2^3*v1^10*x1*y1+50*u1^2*u2^3*v1^8*x1^3*y1+3*u1^2*u2^3*v1^6*x1^5*y1-25*u1^2*u2^2*v1^10*x1^2*y1-12*u1^2*u2^2*v1^8*x1^4*y1+57*u1^2*u2*v1^10*x1^3*y1+4*u1*u2^4*v1^8*x1^3*y1-16*u1*u2^3*v1^10*x1^2*y1+40*u1*u2^2*v1^10*x1^3*y1+8*u1^3*u2*v1^6*x1^6*y1-24*u1^2*u2*v1^8*x1^5*y1-12*u1*u2^2*v1^8*x1^5*y1-11*u1^8*u2^5*v1^2*x1*y1-10*u1^7*u2^6*v1^2*x1*y1+16*u1^7*u2^5*v1^2*x1^2*y1+u1^6*u2^7*v1^2*x1*y1+5*u1^6*u2^6*v1^2*x1^2*y1-5*u1^6*u2^5*v1^2*x1^3*y1+2*u1^9*u2^7*v1-2*u1^9*u2^7*y1+2*u1^6*u2^4*v1^7-u1^6*v1^7*x1^4+2*u1^5*u2^5*v1^7-6*u1^5*v1^9*x1^3+4*u1^5*v1^7*x1^5+17*u1^4*v1^9*x1^4-6*u1^4*v1^7*x1^6-14*u1^3*v1^9*x1^5-5*u2^3*v1^9*x1^5+4*u1^3*v1^7*x1^7+u1^3*u2*v1^13-u1^3*v1^13*x1+4*u1^3*v1^11*x1^3+2*u1^2*u2^2*v1^13-u1^2*v1^14*y1-4*u1^2*v1^13*x1^2+13*u1^2*v1^11*x1^4-u1^2*v1^7*x1^8+u1*u2*v1^15-u1*v1^15*x1+10*u1*v1^13*x1^3-18*u1*v1^11*x1^5+4*u1*v1^9*x1^7+2*u1^8*u2^6*v1^3+2*u1^7*u2^7*v1^3+2*u1^7*u2^5*v1^5+2*u1^6*u2^6*v1^5+2*u1^5*u2^3*v1^9+2*u1^4*u2^4*v1^9+2*u1^4*u2^2*v1^11-5*u1^4*v1^11*x1^2+2*u1^3*u2^3*v1^11-6*u1^5*u2*v1^9*x1^2+23*u1^4*u2^5*v1^5*x1^3-2*u1^4*u2^2*v1^10*y1+3*u1^4*u2*v1^11*x1-2*u1^3*u2^3*v1^10*y1+9*u1^3*u2^3*v1^5*x1^6+12*u1^3*u2^2*v1^11*x1-2*u1^3*u2*v1^12*y1-18*u1^3*u2*v1^11*x1^2-6*u1^3*v1^12*x1*y1+9*u1^2*u2^3*v1^11*x1-2*u1^2*u2^2*v1^12*y1-29*u1^2*u2^2*v1^11*x1^2+2*u1^2*u2*v1^13*x1+7*u1^2*u2*v1^11*x1^3-4*u1^2*v1^12*x1^2*y1+2*u1^2*v1^10*x1^4*y1+4*u1^2*v1^8*x1^6*y1-9*u1*u2^3*v1^11*x1^2+2*u1*u2^2*v1^13*x1+5*u1*u2^2*v1^11*x1^3-2*u1*u2*v1^14*y1-12*u1*u2*v1^13*x1^2+22*u1*u2*v1^11*x1^4+8*u1*u2*v1^9*x1^6-6*u1*v1^14*x1*y1+20*u1*v1^12*x1^3*y1-12*u1*v1^10*x1^5*y1-9*u1^7*u2^2*v1^5*x1^3-38*u1^5*u2^5*v1^5*x1^2+3*u1^2*u2^2*v1^6*x1^6*y1-20*u1^2*u2*v1^12*x1*y1-u1^2*u2*v1^6*x1^7*y1-14*u1*u2^2*v1^12*x1*y1-12*u1*u2*v1^10*x1^4*y1+8*u1*u2*v1^8*x1^6*y1 <> 0
. the three points A, B and C are not collinear
. the line AC is not perpendicular to the line AB
. the line AC is not perpendicular to the line BC

QED.

Theorem([arbitrary(C,G,A), oncircle(A,C,G,B), perpfoot(A,C,G,H,H), perpfoot(A,C,B,E,E), perpfoot(B,C,A,D,D), parallel(D,A,J,G), online(B,I,A), intersection(B,E,D,A,F), perpfoot(B,C,G,J,J), perpendicular(B,I,I,G), midpoint(F,G,M), online(I,J,H), online(I,J,M)],[parallel(B,E,H,G)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, M} are reassigned

Theorem: If the points C, G, and A are arbitrary, the point B is on the circumcircle of the triangle ACG, H is the perpendicular foot of the line AC to the line GH, E is the perpendicular foot of the line AC to the line BE, D is the perpendicular foot of the line BC to the line AD, the line DA is parallel to the line JG, `the point A is on the line B` || (I) , the two lines BE and DA intersect at F, J is the perpendicular foot of the line BC to the line GJ, `the line B` || (I) || ` is perpendicular to the line ` || (I) || G , M is the midpoint of F and G, `the point H is on the line ` || (I) || J , and `the point M is on the line ` || (I) || J , then the line BE is parallel to the line HG.

Proof:

Status: used = 31806, alloced = 23808, time = 7.862
char set produced: [7 y1 2] [4 x2 1] [3 y2 1] [5 x3 1] [3 y3 1] [7 x4 1] [4 y4 1] [8 x5 1] [4 y5 1] [10 x6 1] [4 y6 1] [10 x7 1] [6 y7 1] [3 x8 1] [2 y8 1]
pseudo-remainder: [6 y3 1] = -u2*y3 + ... (5 terms)
pseudo-remainder: [8 x3 1] = -u1*x3*y2 + ... (7 terms)
pseudo-remainder: [9 y2 1] = u1^2*v1^2*y2 + ... (8 terms)
pseudo-remainder: [12 x2 1] = -u1^3*v1*x2 + ... (11 terms)

`The theorem is true under the following subsidiary conditions:`
. the three points A, C and G are not collinear
. the line AC is non-isotropic
. the line BC is non-isotropic
. the line BE is not parallel to the line DA
. the line AC is not perpendicular to the line CG
. the line AB is not perpendicular to the line CG
. the line BC is not perpendicular to the line CG
. the line BE is not perpendicular to the line CG
. the line AB is not parallel to the line HJ

QED.

Theorem([arbitrary(C,G,A), oncircle(A,C,G,B), perpfoot(A,C,G,H,H), perpfoot(A,C,B,E,E), perpfoot(B,C,A,D,D), parallel(D,A,J,G), online(B,I,A), intersection(B,E,D,A,F), perpfoot(B,C,G,J,J), parallel(B,E,H,G), midpoint(F,G,M), online(I,J,H), online(I,J,M)],[perpendicular(B,I,I,G)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, M} are reassigned

Theorem: If the points C, G, and A are arbitrary, the point B is on the circumcircle of the triangle ACG, H is the perpendicular foot of the line AC to the line GH, E is the perpendicular foot of the line AC to the line BE, D is the perpendicular foot of the line BC to the line AD, the line DA is parallel to the line JG, `the point A is on the line B` || (I) , the two lines BE and DA intersect at F, J is the perpendicular foot of the line BC to the line GJ, the line BE is parallel to the line HG, M is the midpoint of F and G, `the point H is on the line ` || (I) || J , and `the point M is on the line ` || (I) || J , then `the line B` || (I) || ` is perpendicular to the line ` || (I) || G .

Proof:

char set produced: [7 y1 2] [4 x2 1] [3 y2 1] [5 x3 1] [3 y3 1] [7 x4 1] [4 y4 1] [8 x5 1] [4 y5 1] [10 x6 1] [4 y6 1] [10 x7 1] [6 y7 1] [3 x8 1] [2 y8 1]
pseudo-remainder: [6 y6 2] = -y6^2 + ... (5 terms)
pseudo-remainder: [12 x6 2] = -v1^2*x6^2 + ... (11 terms)
pseudo-remainder: [98 y5 2] = -x1^5*y5^2*u2 + ... (97 terms)
pseudo-remainder: [212 x5 2] = u1^2*x1*v1*x5^2*y1*u2 + ... (211 terms)
pseudo-remainder: [700 y2 2] = -u1^6*u2^2*y2^2*v1^2 + ... (699 terms)
pseudo-remainder: [440 x2 2] = -v1^2*x2^2*u1^5*u2^2*x1 + ... (439 terms)
pseudo-remainder: [244 y1 7] = u1^8*v1*y1^7 + ... (243 terms)

`The theorem is true under the following subsidiary conditions:`
. the three points A, C and G are not collinear
. the line AC is non-isotropic
. the line BC is non-isotropic
. the line BE is not parallel to the line DA
. the line AC is not perpendicular to the line CG
. the line AB is not perpendicular to the line CG
. the line BC is not perpendicular to the line CG
. the line BE is not perpendicular to the line CG
. the line AB is not parallel to the line HJ

QED.

Theorem([arbitrary(C,A,G), oncircle(A,C,G,B), perpfoot(A,C,G,H,H), perpfoot(A,C,B,E,E), perpfoot(B,C,A,D,D), parallel(D,A,J,G), intersection(B,E,D,A,F), perpfoot(B,C,G,J,J), perpendicular(B,I,I,G), parallel(B,E,H,G), midpoint(F,G,M), online(I,J,H), online(I,J,M)],[online(B,I,A)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, M} are reassigned

Theorem: If the points C, A, and G are arbitrary, the point B is on the circumcircle of the triangle ACG, H is the perpendicular foot of the line AC to the line GH, E is the perpendicular foot of the line AC to the line BE, D is the perpendicular foot of the line BC to the line AD, the line DA is parallel to the line JG, the two lines BE and DA intersect at F, J is the perpendicular foot of the line BC to the line GJ, `the line B` || (I) || ` is perpendicular to the line ` || (I) || G , the line BE is parallel to the line HG, M is the midpoint of F and G, `the point H is on the line ` || (I) || J , and `the point M is on the line ` || (I) || J , then `the point A is on the line B` || (I) .

Proof:

char set produced: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [8 x4 1] [4 y4 1] [7 x5 1] [4 y5 1] [12 x6 1] [6 y6 1] [2 x7 1] [6 y7 1] [2 x8 1] [3 y8 1]
char set recomputed: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [12 x4 1] [4 y4 1] [8 x5 1] [4 y5 1] [2 x6 1] [10 y6 1] [348 x7 2] [33 y7 1] [2 x8 1] [3 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [46 x7 1] = -u1^3*u2^2*v1^2*x7 + ... (45 terms)
pseudo-remainder: [46 x6 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 y5 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 x5 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 y4 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 x4 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 y3 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 x3 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 y2 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 x2 0] = u1^3*u2^3*v1*y1 + ... (45 terms)
pseudo-remainder: [46 y1 2] = -u1^3*y1^2*u2^3 + ... (45 terms)
the thoerem is possibly false: further decomposition in progress
char set produced: [4 x1 2] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 x5 1] [4 y7 2] [2 x8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [4 x5 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y4 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x4 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y3 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x3 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y2 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x2 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y1 1] = y1*u2 + ... (3 terms)
pseudo-remainder: [2 x1 1] = x1*y7 + ... (1 terms)
the thoerem is possibly false: further decomposition in progress
char set produced: [2 u2 1] [6 y3 1] [2 x4 1] [1 y4 1] [7 x5 1] [7 y5 1] [2 x6 1] [2 y6 1] [7 x7 1] [7 y7 1] [2 x8 1] [3 y8 1]
char set produced: [1 u1 1] [1 x1 1] [2 y1 1] [1 x2 1] [1 y2 1] [1 x3 1] [1 y3 1] [1 x4 1] [1 y4 1] [1 x5 1] [2 y5 1] [1 x6 1] [1 y6 1] [1 x7 1] [2 y7 1] [1 x8 1] [2 y8 1]
char set produced: [1 u1 1] [1 x1 1] [2 y1 1] [1 x2 1] [1 y2 1] [1 x3 1] [1 y3 1] [1 x4 1] [1 y4 1] [1 x5 1] [2 y5 1] [1 x6 1] [1 y6 1] [1 x7 1] [2 y7 1] [1 x8 1] [2 y8 1]
char set produced: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [12 x4 1] [10 y4 1] [12 x5 1] [14 y5 1] [2 x6 1] [10 y6 1] [5 x7 1] [31 y7 1] [2 x8 1] [14 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [46 x7 1] = u1^4*y1*u2*v1*x7 + ... (45 terms)
pseudo-remainder: [42 y1 3] = -u1^3*u2*y1^3*v1 + ... (41 terms)
char set produced: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [12 x4 1] [10 y4 1] [12 x5 1] [14 y5 1] [2 x6 1] [10 y6 1] [5 x7 1] [33 y7 1] [2 x8 1] [14 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [50 x7 1] = u1^2*u2^3*v1*x7*y1 + ... (49 terms)
pseudo-remainder: [41 y1 3] = -u1^2*u2^2*y1^3*v1 + ... (40 terms)
further decomposition in progress 7
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [50 x7 1] = u1^2*u2^3*v1*x7*y1 + ... (49 terms)
pseudo-remainder: [41 y1 3] = -u1^2*u2^2*y1^3*v1 + ... (40 terms)
char set produced: [3 x1 2] [6 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 x5 1] [2 y5 1] [2 x6 1] [14 y6 1] [1 x7 1] [2 y7 1] [2 x8 1] [12 y8 1]
char set produced: [1 v1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 x5 1] [1 y5 1] [3 y7 2] [2 x8 1] [2 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [4 x5 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y4 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x4 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y3 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x3 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y2 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x2 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y1 1] = y1*u2 + ... (3 terms)
pseudo-remainder: [2 v1 0] = -u2*y7 + ... (1 terms)
further decomposition in progress 9
char set produced: [2 u2 1] [6 y3 1] [2 x4 1] [1 y4 1] [7 x5 1] [7 y5 1] [2 x6 1] [2 y6 1] [7 x7 1] [7 y7 1] [2 x8 1] [3 y8 1]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [5 x5 1] [5 y5 1] [2 x6 1] [1 y6 1] [4 x7 1] [4 y7 1] [2 x8 1] [2 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [8 x7 1] = u2^2*y1*x7 + ... (7 terms)
pseudo-remainder: [6 y3 0] = -u1*v1*u2^2 + ... (5 terms)
pseudo-remainder: [6 x3 0] = -u1*v1*u2^2 + ... (5 terms)
pseudo-remainder: [6 y2 0] = -u1*v1*u2^2 + ... (5 terms)
pseudo-remainder: [6 x2 0] = -u1*v1*u2^2 + ... (5 terms)
pseudo-remainder: [6 y1 1] = -u1*y1*u2^2 + ... (5 terms)
pseudo-remainder: [4 x1 1] = u2*v1*u1*x1 + ... (3 terms)
further decomposition in progress 13
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 x5 1] [2 x6 1] [4 y7 2] [2 x8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [4 x5 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y4 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x4 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y3 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x3 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y2 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 x2 0] = y1*u2 + ... (3 terms)
pseudo-remainder: [4 y1 1] = y1*u2 + ... (3 terms)
pseudo-remainder: [2 x1 1] = x1*y7 + ... (1 terms)
pseudo-remainder: [1 y1 1] = -y1
pseudo-remainder: [2 x1 1] = x1 + ... (1 terms)
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
Status: used = 52322, alloced = 23808, time = 9.796000000000001
char set produced: [1 O 0]
char set produced: [1 u1 1] [1 x1 1] [2 y1 1] [1 x2 1] [1 y2 1] [1 x3 1] [1 y3 1] [1 x4 1] [1 y4 1] [1 x5 1] [2 y5 1] [1 x6 1] [1 y6 1] [1 x7 1] [2 y7 1] [1 x8 1] [2 y8 1]
char set produced: [1 u1 1] [1 x1 1] [2 y1 1] [1 x2 1] [1 y2 1] [1 x3 1] [1 y3 1] [1 x4 1] [1 y4 1] [1 x5 1] [2 y5 1] [1 x6 1] [1 y6 1] [1 x7 1] [2 y7 1] [1 x8 1] [2 y8 1]
char set produced: [1 O 0]
char set produced: [2 u2 1] [6 y3 1] [2 x4 1] [1 y4 1] [7 x5 1] [7 y5 1] [2 x6 1] [2 y6 1] [7 x7 1] [7 y7 1] [2 x8 1] [3 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [11 x7 1] = u1^2*y1*x7 + ... (10 terms)
pseudo-remainder: [8 u2 1] = u1*x1*y1*u2 + ... (7 terms)
char set produced: [2 u2 1] [6 y3 1] [2 x4 1] [1 y4 1] [7 x5 1] [7 y5 1] [2 x6 1] [2 y6 1] [7 x7 1] [7 y7 1] [2 x8 1] [3 y8 1]
char set produced: [1 v1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 x5 1] [1 y5 1] [3 y7 2] [2 x8 1] [2 y8 1]
further decomposition in progress 10
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [6 x7 1] = x6^3*y1*x7 + ... (5 terms)
pseudo-remainder: [5 x5 0] = -y6*x1*x6^2*u2 + ... (4 terms)
pseudo-remainder: [5 y4 0] = -y6*x1*x6^2*u2 + ... (4 terms)
pseudo-remainder: [5 x4 0] = -y6*x1*x6^2*u2 + ... (4 terms)
pseudo-remainder: [5 y3 0] = -y6*x1*x6^2*u2 + ... (4 terms)
pseudo-remainder: [5 x3 0] = -y6*x1*x6^2*u2 + ... (4 terms)
pseudo-remainder: [5 y2 0] = -y6*x1*x6^2*u2 + ... (4 terms)
pseudo-remainder: [5 x2 0] = -y6*x1*x6^2*u2 + ... (4 terms)
pseudo-remainder: [5 y1 1] = x6^3*y1*u2 + ... (4 terms)
pseudo-remainder: [2 v1 0] = -y6*x1*x6^2*u2 + ... (1 terms)
char set produced: [1 v1 1] [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [7 x5 1] [6 y5 1] [2 x6 1] [1 y6 1] [7 x7 1] [6 y7 1] [2 x8 1] [1 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [12 x7 1] = -u2^2*y1*x7 + ... (11 terms)
pseudo-remainder: [11 y3 0] = u1*y1*u2^2 + ... (10 terms)
pseudo-remainder: [11 x3 0] = u1*y1*u2^2 + ... (10 terms)
pseudo-remainder: [11 y2 0] = u1*y1*u2^2 + ... (10 terms)
pseudo-remainder: [11 x2 0] = u1*y1*u2^2 + ... (10 terms)
pseudo-remainder: [11 y1 1] = u1*y1*u2^2 + ... (10 terms)
pseudo-remainder: [4 x1 1] = u1*x1*y4*u2 + ... (3 terms)
pseudo-remainder: [4 v1 0] = -u1^2*y4*u2 + ... (3 terms)
further decomposition in progress 11
char set produced: [1 v1 1] [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [7 x5 1] [6 y5 1] [2 x6 1] [1 y6 1] [7 x7 1] [6 y7 1] [2 x8 1] [1 y8 1]
further decomposition in progress 16
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x5 1] [2 y5 1] [1 y6 1] [2 x7 1] [2 y7 1] [2 x8 1] [2 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [4 x7 1] = y1*x7 + ... (3 terms)
pseudo-remainder: [4 x5 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 y3 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 x3 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 y2 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 x2 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 y1 1] = -u1*y1 + ... (3 terms)
pseudo-remainder: [2 x1 1] = x1*v1 + ... (1 terms)
further decomposition in progress 18
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [4 x7 1] = y1*x7 + ... (3 terms)
pseudo-remainder: [4 x5 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 y4 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 y3 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 x3 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 y2 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 x2 0] = -u1*y1 + ... (3 terms)
pseudo-remainder: [4 y1 1] = -u1*y1 + ... (3 terms)
pseudo-remainder: [2 x1 1] = x1*v1 + ... (1 terms)
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [5 x4 4] [5 x5 1] [5 y5 1] [2 x6 1] [1 y6 1] [2 x8 1] [2 y8 1]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [9 x5 1] [9 y5 1] [2 x6 1] [1 y6 1] [9 x7 1] [9 y7 1] [2 x8 1] [2 y8 1]
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: [1 v1 1] [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y4 1] [1 y5 1] [1 y6 1] [2 x7 1] [1 y7 1] [2 x8 1] [1 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [2 x7 1] = -y1*x7 + ... (1 terms)
pseudo-remainder: [2 y1 1] = u1*y1 + ... (1 terms)
char set produced: [1 v1 1] [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y4 1] [1 y5 1] [1 y6 1] [2 x7 1] [1 y7 1] [2 x8 1] [1 y8 1]
char set produced: [1 v1 1] [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y5 1] [1 y6 1] [2 x7 1] [1 y7 1] [2 x8 1] [1 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [2 x7 1] = -y1*x7 + ... (1 terms)
pseudo-remainder: [2 y1 1] = u1*y1 + ... (1 terms)
char set produced: [1 v1 1] [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y5 1] [1 y6 1] [2 x7 1] [1 y7 1] [2 x8 1] [1 y8 1]
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: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 y5 1] [2 x6 1] [1 y6 1] [4 x7 1] [4 y7 1] [2 x8 1] [2 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [8 x7 1] = v1^2*y1*x7 + ... (7 terms)
pseudo-remainder: [8 y5 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y3 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 x3 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y2 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 x2 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y1 1] = -y1*x5^2*u1 + ... (7 terms)
pseudo-remainder: [4 x1 1] = u1*x1*v1*x5 + ... (3 terms)
further decomposition in progress 3
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [8 x7 1] = v1^2*y1*x7 + ... (7 terms)
pseudo-remainder: [8 y4 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y3 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 x3 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y2 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 x2 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y1 1] = -y1*x5^2*u1 + ... (7 terms)
pseudo-remainder: [4 x1 1] = u1*x1*v1*x5 + ... (3 terms)
char set produced: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [9 x5 1] [9 y5 1] [4 y6 1] [9 x7 1] [9 y7 1] [2 x8 1] [6 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [18 x7 1] = -u2^2*y1*x7 + ... (17 terms)
pseudo-remainder: [19 y3 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 x3 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 y2 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 x2 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 y1 1] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [10 x1 1] = u1*x1*y4*u2 + ... (9 terms)
further decomposition in progress 9
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [18 x7 1] = -u2^2*y1*x7 + ... (17 terms)
pseudo-remainder: [19 y3 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 x3 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 y2 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 x2 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 y1 1] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [10 x1 1] = u1*x1*y4*u2 + ... (9 terms)
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [4 y5 2] [1 y6 1] [2 x7 1] [2 y7 1] [2 x8 1] [2 y8 1]
char set produced: [1 v1 1] [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y5 1] [1 y6 1] [2 x7 1] [1 y7 1] [2 x8 1] [1 y8 1]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [9 x5 1] [9 y5 1] [9 x6 1] [15 y6 1] [9 x7 1] [9 y7 1] [9 x8 1] [17 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [18 x7 1] = -u2^2*y1*x7 + ... (17 terms)
pseudo-remainder: [19 y3 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 x3 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 y2 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 x2 0] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [19 y1 1] = u1*y1*u2^2 + ... (18 terms)
pseudo-remainder: [10 x1 1] = u1*x1*y4*u2 + ... (9 terms)
further decomposition in progress 8
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [4 y5 2] [2 x6 1] [1 y6 1] [2 x7 1] [2 y7 1] [2 x8 1] [2 y8 1]
char set produced: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [4 y5 2] [2 x6 1] [1 y6 1] [2 x7 1] [2 y7 1] [2 x8 1] [2 y8 1]
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: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [5 y5 1] [5 x6 1] [8 y6 1] [17 x7 1] [20 y7 1] [5 x8 1] [11 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [40 x7 1] = u2^2*v1^2*y1*x7 + ... (39 terms)
pseudo-remainder: [39 y3 0] = -u2^3*x5*u1*v1 + ... (38 terms)
pseudo-remainder: [39 x3 0] = -u2^3*x5*u1*v1 + ... (38 terms)
pseudo-remainder: [39 y2 0] = -u2^3*x5*u1*v1 + ... (38 terms)
pseudo-remainder: [39 x2 0] = -u2^3*x5*u1*v1 + ... (38 terms)
pseudo-remainder: [39 y1 1] = -y1*u2^2*x5^2*u1 + ... (38 terms)
pseudo-remainder: [22 x1 1] = u2^2*u1*v1*x5*x1 + ... (21 terms)
further decomposition in progress 6
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y4 1] [2 y5 1] [2 x6 1] [1 y6 1] [4 x7 1] [4 y7 1] [2 x8 1] [2 y8 1]
pseudo-remainder: [4 y7 1] = -u2*y7 + ... (3 terms)
pseudo-remainder: [8 x7 1] = v1^2*y1*x7 + ... (7 terms)
pseudo-remainder: [8 y5 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y4 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y3 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 x3 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y2 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 x2 0] = -u1*u2*v1*x5 + ... (7 terms)
pseudo-remainder: [8 y1 1] = -y1*x5^2*u1 + ... (7 terms)
pseudo-remainder: [4 x1 1] = u1*x1*v1*x5 + ... (3 terms)
further decomposition in progress 5
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: [1 O 0]
char set produced: [1 O 0]
char set produced: [2 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [4 y5 2] [2 x6 1] [2 x7 1] [2 y7 1] [2 x8 1] [3 y8 1]
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, C and G are not collinear
. the line AD is non-isotropic
. the line BC is non-isotropic
. x7 <> 0
. v1-y7 <> 0
. u1*u2^2-u2^2*x7+u2*v1^2-v1^2*x7 <> 0
. -u2^2*y7+u1*u2*v1-v1^2*y7+v1^3 <> 0
. the line AG is non-isotropic
. the line CG is non-isotropic
. the line AC is not perpendicular to the line CG
. the line AG is not perpendicular to the line AC
. u2^2*x7+v1^2*x7+u2*v1^2-v1^2*x1-u2*y1*v1 <> 0
. v1*u1^2-u1*u2*v1-u1*v1*x1+u1*y1*u2+y1*v1^2+x1*u2*v1 <> 0
. -u1*v1*x1+u1*u2*v1-u1*y1*u2-x1*u2*v1-y1*v1^2+v1*x1^2 <> 0
. -v1^2*x1*y1-x1*v1*u1^2+u1^2*v1*u2-u1^2*y1*u2+x1^2*v1*u1-u2*v1*u1*x1 <> 0
. -u1*v1*x1+u1*u2*v1-u1*y1*u2+y1^2*v1+v1*x1^2-y1*v1^2-x1*u2*v1 <> 0
. -u2^2*v1*u1*x1^2*y7-u2*v1^4*x1^2+v1^4*x1^3+2*u2^2*v1^2*x1^2*u1-3*x1*v1^2*u2^2*u1^2-v1^2*u1*x1*u2^3+u1^2*u2^2*v1*x1*y7+u1*u2*v1^3*x1*y7+u1^2*v1^3*x1*y7+u2^2*v1^2*x1*y1*y7-u2*u1^2*v1^3*y7-y1*v1^5*x1+u1^2*v1^2*u2^3+u1^3*u2^2*v1^2-u1*v1^3*x1^2*y7+v1^4*x1*y1*y7+u2*u1^2*y1*v1^2*y7+u1*u2^3*v1*x1*y7+u1*v1^3*x1^2*y1-u1^2*u2^3*v1*y7+u1^2*u2^3*y1*y7-u1^3*u2^2*y1*v1-u1^2*u2^3*v1*y1-u2^2*v1^3*x1*y1+u2*v1^3*x1^2*y1-y1*v1^3*x1*u1^2-u1*v1^4*x1^2+v1^4*u2*u1*x1-u1^3*v1^2*u2*x1+2*u1^2*v1^2*x1^2*u2-u1*u2*v1^2*x1^3+u1^2*v1*x1*u2^2*y1-2*y1*v1^3*u2*u1*x1 <> 0
. y4*u2-x4*v1+u2*v1 <> 0
. u2^2*y7-2*u2*x4*y7+u1*y4*u2+x4^2*y7+y4^2*y7-x4*u1*y4 <> 0
. u1*u2^2-u2^2*x7-2*u1*x4*u2+2*u2*x4*x7+x4^2*u1-x4^2*x7-y4^2*x7 <> 0
. -u2^2*x7+2*u2*x4*x7-x4^2*x7-y4^2*x7+u1*u2^2-2*u1*x4*u2+y4*u2*v1+x4^2*u1-y4*x4*v1 <> 0
. -v1*u2^2+u2^2*y7+2*u2*x4*v1-2*u2*x4*y7+u1*y4*u2+x4^2*y7-x4^2*v1-x4*u1*y4+y4^2*y7 <> 0
. the three points A, C and D are not collinear
. the line AD is not perpendicular to the line AC
. x6^2+y6^2 <> 0
. the line AC is not perpendicular to the line FG
. x5^2+v1^2 <> 0
. -x5^2*x7+x5^2*u1+v1^2*x5-v1^2*x7 <> 0
. u1*v1*x5-v1^2*y7+v1^3-x5^2*y7 <> 0
. the line AC is not parallel to the line GJ
. the line AC is not perpendicular to the line CJ
. the line AC is not perpendicular to the line GJ
. -2*y8+v1 <> 0
. the line AC is not perpendicular to the line BE
. -x6^2*x7+x1*x6^2-x7*y6^2 <> 0
. -y7*x6^2-y7*y6^2+y6*x1*x6 <> 0
. -u2^2*x6+2*u2*x6*x4-x6*x4^2-y4^2*x6+u1*u2^2-2*u1*x4*u2+y4*u2*v1+x4^2*u1-y4*x4*v1 <> 0
. u2^3*y6-u2^3*y4-3*u2^2*x4*y6+2*u2^2*x4*y4+3*u2*x4^2*y6-x4^2*y4*u2-x4^3*y6+y4^2*y6*u2-y4^3*u2-y4^2*x4*y6+u1*y4*u2^2-2*y4*u1*x4*u2+y4^2*u2*v1+y4*x4^2*u1-y4^2*x4*v1 <> 0
. v1*u2^2-y4*u2*x5-u2*x4*v1+x4*v1*x5-u2*v1*x5 <> 0
. -u2*y4*y5+u2*v1^2-u2*v1*y5-v1^2*x4+x4*v1*y5 <> 0
. u2^2*y5+u1*y4*u2-2*u2*x4*y5+y4^2*y5+x4^2*y5-x4*u1*y4 <> 0
. u1*u2^2-2*u1*x4*u2+x4^2*u1-u2^2*x5+2*u2*x4*x5-x5*x4^2-x5*y4^2 <> 0
. u1*u2^2-u2^2*x5-2*u1*x4*u2+2*u2*x4*x5+x4^2*u1-x5*x4^2-x5*y4^2+y4*u2*v1-y4*x4*v1 <> 0
. u2^2*x5^2-2*u2*x5^2*x4+x4^2*x5^2+y4^2*x5^2-2*y4*x5*u2*v1+2*y4*x5*x4*v1+u2^2*v1^2-2*u2*v1^2*x4+x4^2*v1^2 <> 0
. -v1*u2^2+u2^2*y5+2*u2*x4*v1+u1*y4*u2-2*u2*x4*y5-x4^2*v1+x4^2*y5-x4*u1*y4+y4^2*y5 <> 0
. -u2^2*x5^2*x7+u2^2*x5^2*u1+2*u2*x5^2*x4*x7-2*u2*x5^2*x4*u1-x4^2*x5^2*x7+x4^2*x5^2*u1-y4*x5^2*u2*v1+y4*x5^2*x4*v1-y4^2*x5^2*x7+2*y4*x5*x7*u2*v1-2*y4*x5*x7*x4*v1+u2^2*v1^2*x5-2*u2*v1^2*x4*x5-v1^2*x7*u2^2+2*u2*v1^2*x7*x4+x4^2*v1^2*x5-x4^2*v1^2*x7 <> 0
. u2^2*u1*v1*x5-u2^2*v1^2*y7+u2^2*v1^3-u2^2*x5^2*y7+2*u2*x5^2*x4*y7+2*u2*v1^2*x4*y7-2*u2*y4*x5*v1^2-2*u2*v1^3*x4-2*u2*x5*u1*x4*v1-u2*x5^2*u1*y4+2*u2*y4*x5*v1*y7-2*y4*x5*v1*x4*y7+v1^3*x4^2+y4^2*x5^2*v1-y4^2*x5^2*y7+2*v1^2*x4*x5*y4-x5^2*x4^2*y7-v1^2*x4^2*y7+x5*x4^2*u1*v1+x5^2*x4*u1*y4 <> 0
. -2*x8*u2^2+4*x8*u2*x4-2*x8*x4^2-2*x8*y4^2+u1*u2^2-2*u1*x4*u2+y4*u2*v1+x4^2*u1-y4*x4*v1 <> 0
. 2*u2^3*y8-u2^3*v1-6*u2^2*x4*y8+3*u2^2*x4*v1-u2^3*y4+6*u2*x4^2*y8-3*u2*x4^2*v1+2*u2^2*x4*y4-2*x4^3*y8+x4^3*v1-x4^2*y4*u2+2*y4^2*u2*y8-2*y4^2*x4*y8-y4^3*u2+u1*y4*u2^2-2*y4*u1*x4*u2+y4*x4^2*u1 <> 0
. the line AC is not perpendicular to the line FJ
. -2*y8+y6 <> 0
. -2*x8+x5 <> 0
. u2*v1*x5-x4*v1*x5+y4*u2*x5-u2*v1*x6+x4*v1*x6 <> 0
. -u2^2*v1*y6+y4*v1*u2^2+2*u2*v1*x4*y6-y4*u2*x4*v1-x4^2*v1*y6-y4*x5*u2*v1+y4*x5*x4*v1-y4^2*u2*x5 <> 0
. -2*u2*y8+u2*v1+2*x4*y8-x4*v1-y4*x6+y4*u2 <> 0
. -2*u2*v1*x8+2*x4*v1*x8+y4*u2*x5-x4*v1*x5+u2*v1*x5 <> 0
. -2*v1*u2^2*y8+u2^2*v1^2+4*u2*x4*v1*y8-2*u2*v1^2*x4-2*x4^2*v1*y8+x4^2*v1^2+y4*v1*u2^2+y4*x5*x4*v1-y4*u2*x4*v1-y4*x5*u2*v1-y4^2*u2*x5 <> 0

QED.

Theorem([arbitrary(C,A,G), oncircle(A,C,G,B), perpfoot(A,C,G,H,H), perpfoot(A,C,B,E,E), perpfoot(B,C,A,D,D), online(B,I,A), intersection(B,E,D,A,F), perpfoot(B,C,G,J,J), perpendicular(B,I,I,G), parallel(B,E,H,G), midpoint(F,G,M), online(I,J,H), online(I,J,M)],[parallel(D,A,J,G)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, M} are reassigned

Theorem: If the points C, A, and G are arbitrary, the point B is on the circumcircle of the triangle ACG, H is the perpendicular foot of the line AC to the line GH, E is the perpendicular foot of the line AC to the line BE, D is the perpendicular foot of the line BC to the line AD, `the point A is on the line B` || (I) , the two lines BE and DA intersect at F, J is the perpendicular foot of the line BC to the line GJ, `the line B` || (I) || ` is perpendicular to the line ` || (I) || G , the line BE is parallel to the line HG, M is the midpoint of F and G, `the point H is on the line ` || (I) || J , and `the point M is on the line ` || (I) || J , then the line DA is parallel to the line JG.

Proof:

char set produced: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [8 x4 1] [4 y4 1] [35 x5 1] [4 y5 1] [12 x6 1] [6 y6 1] [7 x7 1] [4 y7 1] [2 x8 1] [3 y8 1]
Status: used = 75549, alloced = 23808, time = 11.590000000000003
char set recomputed: [7 y1 2] [1 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [12 x4 1] [4 y4 1] [25 x5 1] [4 y5 1] [2 x6 1] [10 y6 1] [12 x7 1] [4 y7 1] [2 x8 1] [3 y8 1]
pseudo-remainder: [5 y7 1] = -u2*y7 + ... (4 terms)
pseudo-remainder: [10 x7 1] = -u1*y4*x7 + ... (9 terms)
pseudo-remainder: [40 y4 1] = u1^3*v1*u2*y4 + ... (39 terms)
pseudo-remainder: [32 x4 1] = -v1^2*u1^3*x4 + ... (31 terms)
pseudo-remainder: [22 y1 2] = -y1^2*v1^2*u1^2 + ... (21 terms)

`The theorem is true under the following subsidiary conditions:`
. the three points A, C and G are not collinear
. the line CG is non-isotropic
. the line AG is not perpendicular to the line AC
. v1*u1^2-u1*u2*v1-u1*v1*x1+u1*y1*u2+y1*v1^2+x1*u2*v1 <> 0
. -u1*v1*x1+u1*u2*v1-u1*y1*u2-x1*u2*v1-y1*v1^2+v1*x1^2 <> 0
. -u1^2*v1*x1*u2+u1^2*v1*u2^2-u1^2*y1*u2^2+x1^2*v1*u2*u1-u1*v1^2*x1*y1-y1*v1^2*u2*u1-u1*x1*v1^3+u1*v1^3*u2-x1*v1*u2^2*u1+x1^2*v1^3-u2*v1^2*x1*y1+y1*v1^2*x1^2-y1*v1^4-u2*x1*v1^3 <> 0
. the line AC is not perpendicular to the line AB
. the line AC is not perpendicular to the line BC

QED.