Theorems

1. Theorem([arbitrary(H,B,C), oncircle(B,C,H,G), intersection(E,H,B,C,I), oncircle(B,C,H,E), oncircle(B,C,H,F), intersection(B,C,G,F,J), midpoint(B,C,D), intersection(H,G,E,F,D)],[midpoint(I,J,D)])
   Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned
   
   
   Theorem: If the points H, B, and C are arbitrary, the point G is on the circumcircle of the triangle BCH, `the two lines EH and BC intersect at ` || (I) , the point E is on the circumcircle of the triangle BCH, the point F is on the circumcircle of the triangle BCH, the two lines BC and GF intersect at J, D is the midpoint of B and C, and the two lines HG and EF intersect at D, then `D is the midpoint of ` || (I) || ` and ` || J .
   
   Proof:
   
   char set produced: [14 x1 2] [4 y1 1] [7 y2 2] [6 x3 1] [3 y3 1] [26 x4 2] [6 y4 1] [8 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = -x5 + ... (2 terms)
   pseudo-remainder: [8 y4 1] = u2^2*y4 + ... (7 terms)
   pseudo-remainder: [21 x4 1] = -v1*x4*u2^2 + ... (20 terms)
   pseudo-remainder: [21 y3 0] = u2^3*y1 + ... (20 terms)
   pseudo-remainder: [21 x3 1] = -u2^2*y1*x3 + ... (20 terms)
   pseudo-remainder: [36 y2 2] = u2^3*u1*y2^2 + ... (35 terms)
   pseudo-remainder: [58 y1 1] = -v1*u2^2*u1*y2*y1 + ... (57 terms)
   pseudo-remainder: [80 x1 1] = 2*v1*x1*u1^2*u2^3 + ... (79 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 x5 1] = -v1*x5 + ... (1 terms)
   pseudo-remainder: [8 y4 1] = u2^2*y3*y4 + ... (7 terms)
   pseudo-remainder: [18 x4 1] = v1^2*x4*u2 + ... (17 terms)
   pseudo-remainder: [18 y3 1] = u2^2*y3*y1 + ... (17 terms)
   pseudo-remainder: [21 x3 1] = v1*x3*u2^2*y1 + ... (20 terms)
   Status: used = 692, alloced = 3072, time = 4.476999999999999
   pseudo-remainder: [36 y2 2] = -u2^3*u1*y2^2 + ... (35 terms)
   pseudo-remainder: [58 y1 1] = v1*u2^2*u1*y2*y1 + ... (57 terms)
   pseudo-remainder: [80 x1 1] = -2*v1*x1*u1^2*u2^3 + ... (79 terms)
   the thoerem is possibly false: further decomposition in progress
   char set produced: [1 u2 1] [4 x1 2] [3 y1 1] [4 y2 2] [1 x3 1] [3 y3 1] [4 x4 2] [4 y4 1] [1 x5 1] [7 y5 1] [1 x6 1] [2 y6 1]
   char set produced: [1 v1 1] [1 y1 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y4 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   the thoerem is possibly false: further decomposition in progress
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = x3 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   char set produced: [2 u2 1] [3 y1 1] [2 x3 1] [1 y3 1] [6 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [9 x1 1] [8 y1 1] [7 y2 2] [6 x3 1] [5 y3 1] [19 x4 2] [6 y4 1] [53 x5 1] [50 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = -x5 + ... (2 terms)
   pseudo-remainder: [50 x4 1] = 4*v1*x4*u1^2*u2^2 + ... (49 terms)
   pseudo-remainder: [50 y3 0] = -2*v1*u1^2*u2^3 + ... (49 terms)
   pseudo-remainder: [50 x3 1] = 4*v1*u1^2*u2^2*x3 + ... (49 terms)
   pseudo-remainder: [57 y2 2] = -4*u2^3*u1^3*y2^2 + ... (56 terms)
   pseudo-remainder: [77 y1 0] = 4*v1*u2^4*u1^4 + ... (76 terms)
   pseudo-remainder: [77 x1 0] = 4*v1*u2^4*u1^4 + ... (76 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [53 x4 1] = 4*v1^2*x4*u1^2*u2 + ... (52 terms)
   pseudo-remainder: [53 y3 1] = 4*v1*u1^2*u2^2*y3 + ... (52 terms)
   pseudo-remainder: [57 x3 0] = 2*u1^3*u2^2*v1^3 + ... (56 terms)
   pseudo-remainder: [57 y2 2] = 4*u1^3*y2^2*u2^2 + ... (56 terms)
   pseudo-remainder: [77 y1 0] = -4*v1*u1^4*u2^3 + ... (76 terms)
   pseudo-remainder: [77 x1 0] = -4*v1*u1^4*u2^3 + ... (76 terms)
   the thoerem is possibly false: further decomposition in progress
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [4 y3 1] [4 y4 1] [8 y5 1] [2 x6 1] [1 y6 1]
   char set recomputed: [2 u2 2] [1 v1 1] [1 y1 1] [3 y3 1] [2 y4 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 u2 1] = u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y4 0] = u2*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = u2*y3 + ... (1 terms)
   pseudo-remainder: [3 y1 0] = -v1*u2 + ... (2 terms)
   pseudo-remainder: [3 v1 1] = -v1*u2 + ... (2 terms)
   the thoerem is possibly false: further decomposition in progress
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [4 y3 1] [4 y4 1] [8 y5 1] [2 x6 1] [1 y6 1]
   Status: used = 3272, alloced = 5506, time = 4.648
   char set produced: [1 v1 1] [1 y1 1] [1 y2 1] [1 y3 1] [1 y4 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   the thoerem is possibly false: further decomposition in progress
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   char set produced: [2 u2 1] [3 y1 1] [2 x3 1] [1 y3 1] [6 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 v1 1] [1 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y4 1] [1 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [1 v1 1] [1 y1 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [9 x1 1] [8 y1 1] [7 y2 2] [6 x3 1] [5 y3 1] [2 x4 1] [2 y4 1] [25 x5 1] [24 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = -x5 + ... (2 terms)
   pseudo-remainder: [24 x3 1] = 4*v1*u1^2*u2*x3 + ... (23 terms)
   pseudo-remainder: [24 y2 2] = -4*u1^3*y2^2*u2^2 + ... (23 terms)
   pseudo-remainder: [34 y1 0] = 4*v1*u1^4*u2^3 + ... (33 terms)
   pseudo-remainder: [34 x1 0] = 4*v1*u1^4*u2^3 + ... (33 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [25 y3 1] = 4*v1*u1^2*u2*y3 + ... (24 terms)
   pseudo-remainder: [24 y2 2] = 4*v1*u1^3*y2^2*u2 + ... (23 terms)
   pseudo-remainder: [34 y1 0] = -4*v1*u1^4*u2^2 + ... (33 terms)
   pseudo-remainder: [34 x1 0] = -4*v1*u1^4*u2^2 + ... (33 terms)
   the thoerem is possibly false: further decomposition in progress
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [24 x3 1] = -4*v1*u1^2*u2*x3 + ... (23 terms)
   pseudo-remainder: [24 y2 2] = 4*u1^3*y2^2*u2^2 + ... (23 terms)
   pseudo-remainder: [34 y1 0] = -4*v1*u1^4*u2^3 + ... (33 terms)
   pseudo-remainder: [34 x1 0] = -4*v1*u1^4*u2^3 + ... (33 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [25 y3 1] = -4*v1*u1^2*u2*y3 + ... (24 terms)
   pseudo-remainder: [24 y2 2] = -4*v1*u1^3*y2^2*u2 + ... (23 terms)
   pseudo-remainder: [34 y1 0] = 4*v1*u1^4*u2^2 + ... (33 terms)
   pseudo-remainder: [34 x1 0] = 4*v1*u1^4*u2^2 + ... (33 terms)
   char set produced: [9 x1 1] [8 y1 1] [7 y2 2] [6 x3 1] [5 y3 1] [12 x4 1] [12 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = -x5 + ... (2 terms)
   pseudo-remainder: [6 x3 1] = v1*x3*u1 + ... (5 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [5 y3 1] = v1*u1*y3 + ... (4 terms)
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x3 1] [1 y3 1] [6 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = -v1*x1
   further decomposition in progress 10
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = v1*x1
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [4 y3 1] [4 y4 1] [8 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [1 v1 1] [1 y1 1] [2 x2 1] [1 y2 1] [1 y3 1] [1 y4 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   further decomposition in progress 11
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [4 y3 1] [4 y4 1] [8 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [2 u2 1] [3 y1 1] [2 x3 1] [1 y3 1] [6 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 v1 1] [1 y1 1] [1 y2 1] [1 y3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = -x5 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   further decomposition in progress 12
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [9 x1 1] [8 y1 1] [2 x2 1] [5 y2 2] [6 x3 1] [5 y3 1] [2 x4 1] [5 y4 2] [19 x5 1] [16 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [5 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = -v1*x1
   further decomposition in progress 12
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = v1*x1
   char set produced: [2 u2 1] [3 y1 1] [2 x3 1] [1 y3 1] [2 x4 1] [6 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = -v1*x1
   further decomposition in progress 15
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = v1*x1
   char set produced: [2 u2 1] [3 y1 1] [3 y2 1] [3 y3 1] [3 y4 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y3 1] = -y3 + ... (2 terms)
   pseudo-remainder: [2 y2 0] = u1*y5 + ... (1 terms)
   pseudo-remainder: [2 y1 0] = u1*y5 + ... (1 terms)
   pseudo-remainder: [2 u2 0] = u1*y5 + ... (1 terms)
   further decomposition in progress 17
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = v1*u1 + ... (2 terms)
   char set produced: [2 u2 1] [3 y1 1] [2 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = x3 + ... (2 terms)
   pseudo-remainder: [1 y1 0] = -x5
   pseudo-remainder: [1 u2 0] = -x5
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y4 0] = u1*y3 + ... (1 terms)
   pseudo-remainder: [2 x4 0] = u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 x3 0] = -v1*x5
   pseudo-remainder: [1 y1 0] = -v1*x5
   pseudo-remainder: [1 u2 0] = -v1*x5
   further decomposition in progress 19
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = x3 + ... (2 terms)
   pseudo-remainder: [1 y1 0] = -x5
   pseudo-remainder: [1 u2 0] = -x5
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y4 0] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [2 x4 0] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 x3 0] = v1*x5
   pseudo-remainder: [1 y1 0] = v1*x5
   pseudo-remainder: [1 u2 0] = v1*x5
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [4 y3 1] [4 y4 1] [8 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [4 y3 1] [4 y4 1] [8 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [2 u2 1] [3 y1 1] [2 x3 1] [1 y3 1] [6 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 v1 1] [1 y1 1] [2 x2 1] [1 y2 1] [1 y3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = -x5 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   further decomposition in progress 18
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   char set produced: [1 O 0]
   char set produced: [1 v1 1] [1 y1 1] [2 x2 1] [1 y2 1] [1 y3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [1 v1 1] [1 y1 1] [1 y2 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   further decomposition in progress 17
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y5 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [1 y2 1] [3 y3 1] [3 y4 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y3 1] = -y3 + ... (2 terms)
   pseudo-remainder: [2 y2 0] = u1*y5 + ... (1 terms)
   pseudo-remainder: [2 x2 0] = u1*y5 + ... (1 terms)
   pseudo-remainder: [2 y1 0] = u1*y5 + ... (1 terms)
   pseudo-remainder: [2 u2 0] = u1*y5 + ... (1 terms)
   further decomposition in progress 19
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = v1*u1 + ... (2 terms)
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = x3 + ... (2 terms)
   pseudo-remainder: [1 x2 0] = -x5
   pseudo-remainder: [1 y1 0] = -x5
   pseudo-remainder: [1 u2 0] = -x5
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y4 0] = u1*y3 + ... (1 terms)
   pseudo-remainder: [2 x4 0] = u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 x3 0] = -v1*x5
   pseudo-remainder: [1 x2 0] = -v1*x5
   pseudo-remainder: [1 y1 0] = -v1*x5
   pseudo-remainder: [1 u2 0] = -v1*x5
   further decomposition in progress 19
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = x3 + ... (2 terms)
   pseudo-remainder: [1 x2 0] = -x5
   pseudo-remainder: [1 y1 0] = -x5
   pseudo-remainder: [1 u2 0] = -x5
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y4 0] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [2 x4 0] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 x3 0] = v1*x5
   pseudo-remainder: [1 x2 0] = v1*x5
   pseudo-remainder: [1 y1 0] = v1*x5
   pseudo-remainder: [1 u2 0] = v1*x5
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [2 x4 1] [5 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = -v1*x1
   further decomposition in progress 20
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = v1*x1
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [3 y2 1] [3 y3 1] [2 x4 1] [3 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 y2 1] [3 y3 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -v1*u1 + ... (2 terms)
   further decomposition in progress 18
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = v1*u1 + ... (2 terms)
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [2 x4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = -v1*x1
   further decomposition in progress 18
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = -x3 + ... (2 terms)
   pseudo-remainder: [1 u2 0] = x1
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = v1*x1
   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] [1 y1 1] [2 x2 1] [1 y2 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   further decomposition in progress 18
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 v1 0] = -u2 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [2 y5 1] = -y5 + ... (1 terms)
   pseudo-remainder: [1 y3 1] = -y3
   char set produced: [1 O 0]
   char set produced: [1 v1 1] [1 y1 1] [2 x2 1] [1 y2 1] [1 y3 1] [2 x4 1] [1 y4 1] [1 y5 1] [2 x6 1] [1 y6 1]
   Status: used = 14660, alloced = 13188, time = 5.444
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [1 y2 1] [3 y3 1] [2 x4 1] [3 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -v1*u1 + ... (2 terms)
   further decomposition in progress 16
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = v1*u1 + ... (2 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]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 y2 1] [3 y3 1] [3 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -v1*u1 + ... (2 terms)
   further decomposition in progress 9
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = v1*u1 + ... (2 terms)
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [2 x3 1] = -2*x3 + ... (1 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = 2*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = -v1
   further decomposition in progress 9
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x5 1] = x5 + ... (2 terms)
   pseudo-remainder: [2 x3 1] = -2*x3 + ... (1 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -2*y3 + ... (1 terms)
   pseudo-remainder: [1 u2 0] = v1
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 y2 1] [3 y3 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 u2 1] [2 x1 1] [2 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [2 x4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 y2 1] [3 y3 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [1 y2 1] [3 y3 1] [2 x4 1] [3 y4 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 x4 0] = u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -v1*u1 + ... (2 terms)
   further decomposition in progress 6
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 x4 0] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = v1*u1 + ... (2 terms)
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 y2 1] [3 y3 1] [3 y4 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -v1*u1 + ... (2 terms)
   further decomposition in progress 4
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [3 y2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 x2 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 y1 0] = v1*u1 + ... (2 terms)
   pseudo-remainder: [3 u2 0] = v1*u1 + ... (2 terms)
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 y2 1] [3 y3 1] [2 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 y2 1] [3 y3 1] [2 y4 1] [2 x5 1] [3 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 u2 1] [3 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = x3 + ... (2 terms)
   pseudo-remainder: [1 x2 0] = -x5
   pseudo-remainder: [1 y1 0] = -x5
   pseudo-remainder: [1 u2 0] = -x5
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = -y5 + ... (2 terms)
   pseudo-remainder: [2 y4 0] = u1*y3 + ... (1 terms)
   pseudo-remainder: [2 x4 0] = u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms)
   pseudo-remainder: [1 x3 0] = -v1*x5
   pseudo-remainder: [1 x2 0] = -v1*x5
   pseudo-remainder: [1 y1 0] = -v1*x5
   pseudo-remainder: [1 u2 0] = -v1*x5
   further decomposition in progress 3
   pseudo-remainder: [3 x6 1] = 2*x6 + ... (2 terms)
   pseudo-remainder: [3 y4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x4 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 y3 0] = -u1 + ... (2 terms)
   pseudo-remainder: [3 x3 1] = x3 + ... (2 terms)
   pseudo-remainder: [1 x2 0] = -x5
   pseudo-remainder: [1 y1 0] = -x5
   pseudo-remainder: [1 u2 0] = -x5
   pseudo-remainder: [3 y6 1] = 2*y6 + ... (2 terms)
   pseudo-remainder: [3 y5 1] = y5 + ... (2 terms)
   pseudo-remainder: [2 y4 0] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [2 x4 0] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms)
   pseudo-remainder: [1 x3 0] = v1*x5
   pseudo-remainder: [1 x2 0] = v1*x5
   pseudo-remainder: [1 y1 0] = v1*x5
   pseudo-remainder: [1 u2 0] = v1*x5
   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]
   
   `The theorem is true under the following subsidiary conditions:`
   . the three points B, C and H are not collinear
   . the line EH is not parallel to the line BC
   . y3 <> 0
   . u1-x3 <> 0
   . 2*u1-u2 <> 0
   . -v1*x3+v1*u1-u1*y3 <> 0
   . 4*u1^2-4*u2*u1+v1^2+u2^2 <> 0
   . the line BH is not perpendicular to the line BC
   . the line BH is not perpendicular to the line CH
   . -2*x6+u1 <> 0
   . the three points B, D and H are not collinear
   . -2*x2+u1 <> 0
   . -2*y2+v1 <> 0
   . -v1^3-v1*u2^2-4*u1*v1*x2-4*u2*u1*y2+4*v1*u2*u1 <> 0
   . 4*v1*u1^2*u2-5*v1*u1*u2^2-4*v1*u1^2*x2-v1*x2*u2^2+4*x2*u2*v1*u1-u2^3*y2-u1*v1^3+2*v1^3*u2+2*v1*u2^3-v1^3*x2-4*y2*u1^2*u2+4*y2*u1*u2^2-v1^2*y2*u2 <> 0
   . the three points B, E and H are not collinear
   . the three points C, E and H are not collinear
   . the line BH is not perpendicular to the line EH
   . -2*x4+u1 <> 0
   . -2*y4+v1 <> 0
   . the three points B, F and H are not collinear
   . the three points C, F and H are not collinear
   . the three points B, G and H are not collinear
   . the three points C, G and H are not collinear
   . the line BH is not perpendicular to the line GH
   . u1-2*x5 <> 0
   . -2*y5+v1 <> 0
   . the three points B, H and J are not collinear
   . the three points C, H and J are not collinear
   . v1*u1-y4*u1+2*x4*y2-v1*x4-u1*y2 <> 0
   . v1*x4+2*y4*x2-2*x4*y2-v1*x2-y4*u1+u1*y2 <> 0
   . the line BH is not parallel to the line FE
   . the line BH is not perpendicular to the line FE
   . u2^3*y2*y5-2*v1^2*u1*u2^2-v1^2*u2^2*x2+5*v1*u1*u2^2*y5-4*y2*u1*u2^2*y5+v1*x2*u2^2*y5+2*v1^2*u2*u1*x2+v1*u2^2*u1*y2-4*x2*v1*u1*u2*y5+4*v1*u1^2*x2*y5-2*v1*u2*y2*u1^2-2*v1^2*u1^2*x2-y2*u1*v1^3-4*v1*u1^2*u2*y5+v1^3*u1*y5+4*u1^2*u2*y2*y5+y2*v1^2*u2*y5+v1^3*x2*y5+v1^2*u2^3-v1^4*x2-2*v1*u2^3*y5-2*v1^3*u2*y5+v1^4*u2+2*v1^2*u1^2*u2 <> 0
   . 2*v1*u1^2*u2^2-v1^3*u2*u1-u2^4*y2+v1*u2^4-2*u1^2*u2^2*y2+v1^3*u2^2+3*y2*u1*u2^3-y2*v1^2*u2^2-3*v1*u1*u2^3+2*x2*v1*u1*u2^2-2*v1*x2*u1^2*u2+u2*y2*u1*v1^2-4*u1^2*u2*v1*x5+5*u2^2*u1*v1*x5+4*u1^2*v1*x2*x5+u2^2*v1*x2*x5-4*u2*u1*v1*x2*x5+y2*u2^3*x5+u1*v1^3*x5-2*v1^3*u2*x5-2*u2^3*v1*x5+v1^3*x2*x5+4*y2*u1^2*u2*x5-4*y2*u2^2*u1*x5+y2*v1^2*u2*x5 <> 0
   . -y4*u1-v1*x1+v1*u1 <> 0
   . the line BH is not perpendicular to the line GF
   . v1*u1-u1*y5-v1*x4 <> 0
   . the line BH is not perpendicular to the line FJ
   . v1*u1-u1*y5-v1*x1 <> 0
   . the line BH is not perpendicular to the line GJ
   . v1*u1-v1*x1+2*y2*x1-y4*u1-u1*y2 <> 0
   . -2*y2*x1+2*y4*x2-v1*x2+v1*x1-y4*u1+u1*y2 <> 0
   
   QED.


2. Theorem([arbitrary(H,B,C), oncircle(B,C,H,G), intersection(E,H,B,C,I), oncircle(B,C,H,E), intersection(B,C,G,F,J), midpoint(B,C,D), intersection(H,G,E,F,D), midpoint(I,J,D)],[oncircle(B,C,H,F)])
   Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned
   
   
   Theorem: If the points H, B, and C are arbitrary, the point G is on the circumcircle of the triangle BCH, `the two lines EH and BC intersect at ` || (I) , the point E is on the circumcircle of the triangle BCH, the two lines BC and GF intersect at J, D is the midpoint of B and C, the two lines HG and EF intersect at D, and `D is the midpoint of ` || (I) || ` and ` || J , then the point F is on the circumcircle of the triangle BCH.
   
   Proof:
   
   char set produced: [14 x1 2] [4 y1 1] [7 y2 2] [6 x3 1] [3 y3 1] [23 x4 1] [6 y4 1] [3 x5 1] [3 y5 1] [3 x6 1] [3 y6 1]
   pseudo-remainder: [12 y4 2] = v1*u1*y4^2 + ... (11 terms)
   pseudo-remainder: [26 x4 2] = v1*x4^2*u2^2 + ... (25 terms)
   pseudo-remainder: [600 y3 2] = u2^5*y3^2*v1*u1 + ... (599 terms)
   pseudo-remainder: [202 x3 2] = 4*v1^3*x3^2*u1*u2^3 + ... (201 terms)
   pseudo-remainder: [402 y2 4] = 4*u2^5*u1^3*y2^4*v1 + ... (401 terms)
   pseudo-remainder: [38 y1 2] = -4*u2^3*u1^2*v1^3*y1^2 + ... (37 terms)
   pseudo-remainder: [31 x1 2] = 32*u1^4*u2*v1^2*x1^2 + ... (30 terms)
   the thoerem is possibly false: further decomposition in progress
   char set produced: [1 u2 1] [4 x1 2] [3 y1 1] [4 y2 2] [1 x3 1] [3 y3 1] [4 x4 1] [7 y4 1] [1 x5 1] [5 y5 1] [1 x6 1] [2 y6 1]
   char set produced: [1 v1 1] [3 x1 1] [1 y1 1] [1 y2 1] [2 x3 1] [1 y3 1] [1 y4 1] [3 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [12 y4 2] = v1*u1*y4^2 + ... (11 terms)
   pseudo-remainder: [6 v1 1] = v1*u1^2*u2 + ... (5 terms)
   char set produced: [2 u2 1] [8 x1 2] [4 y1 1] [4 y2 2] [6 x3 1] [1 y3 1] [2 x4 1] [6 y4 1] [1 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [9 x1 1] [4 y1 1] [2 x2 1] [5 y2 2] [6 x3 1] [5 y3 1] [2 x4 1] [11 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [9 x1 1] [8 y1 1] [7 y2 2] [6 x3 1] [5 y3 1] [53 x4 1] [50 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [12 y4 2] = v1*u1*y4^2 + ... (11 terms)
   pseudo-remainder: [554 x4 2] = 64*u1^6*u2^4*v1^3*x4^2 + ... (553 terms)
   pseudo-remainder: [149 y2 2] = 2*v1^4*y2^2*u1^3*u2^5 + ... (148 terms)
   
   `The theorem is true under the following subsidiary conditions:`
   . the three points B, C and H are not collinear
   . the line EH is not parallel to the line BC
   . 4*u1^2-4*u2*u1+v1^2+u2^2 <> 0
   . the line BH is not perpendicular to the line BC
   . -4*v1^3*x2^2*u1-4*v1^3*u1^2*u2+8*v1*u1^3*u2^2+4*v1^3*x2*u1^2+4*v1*x2*u1*u2^3+8*v1*u2*u1^2*x2^2+u2^3*y2*v1^2+v1^3*u1*u2^2-8*u2^2*y2*u1^3-4*v1*u1^2*u2^3+4*v1^3*x2*u2*u1+4*u2^3*y2*u1^2-2*u2^2*y2*u1*v1^2-8*v1^2*y2*u1^2*x2-8*v1*x2*u1^3*u2-v1^3*x2*u2^2+u1*v1^5-4*v1*x2^2*u1*u2^2-4*v1*x2*u1^2*u2^2-v1^5*x2+4*u2*u1^2*y2*v1^2+v1^4*y2*u2-2*v1^4*y2*u1 <> 0
   . the line BH is not perpendicular to the line GH
   
   QED.


3. Theorem([arbitrary(H,B,C), oncircle(B,C,H,G), intersection(E,H,B,C,I), oncircle(B,C,H,F), intersection(B,C,G,F,J), midpoint(B,C,D), intersection(H,G,E,F,D), midpoint(I,J,D)],[oncircle(B,C,H,E)])
   Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned
   
   
   Theorem: If the points H, B, and C are arbitrary, the point G is on the circumcircle of the triangle BCH, `the two lines EH and BC intersect at ` || (I) , the point F is on the circumcircle of the triangle BCH, the two lines BC and GF intersect at J, D is the midpoint of B and C, the two lines HG and EF intersect at D, and `D is the midpoint of ` || (I) || ` and ` || J , then the point E is on the circumcircle of the triangle BCH.
   
   Proof:
   
   char set produced: [14 x1 2] [4 y1 1] [402 y2 4] [6 x3 1] [3 y3 1] [23 x4 1] [6 y4 1] [3 x5 1] [3 y5 1] [3 x6 1] [3 y6 1]
   pseudo-remainder: [12 y2 2] = v1*u1*y2^2 + ... (11 terms)
   pseudo-remainder: [12 y1 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 x1 0] = v1*u1^2*u2 + ... (11 terms)
   the thoerem is possibly false: further decomposition in progress
   char set produced: [1 u2 1] [4 x1 2] [3 y1 1] [14 y2 2] [1 x3 1] [3 y3 1] [4 x4 1] [7 y4 1] [1 x5 1] [5 y5 1] [1 x6 1] [2 y6 1]
   char set produced: [1 v1 1] [1 y1 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [3 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [12 y3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 x3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 y1 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 v1 2] = -y2*u1*v1^2 + ... (11 terms)
   the thoerem is possibly false: further decomposition in progress
   pseudo-remainder: [12 y3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 x3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 y1 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 v1 2] = -y2*u1*v1^2 + ... (11 terms)
   char set produced: [14 x1 2] [4 y1 1] [4 y2 1] [2 x3 1] [2 y3 1] [14 x4 2] [4 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [12 y2 2] = v1*u1*y2^2 + ... (11 terms)
   pseudo-remainder: [19 y1 0] = 2*v1*u1^4*u2 + ... (18 terms)
   pseudo-remainder: [19 x1 0] = 2*v1*u1^4*u2 + ... (18 terms)
   the thoerem is possibly false: further decomposition in progress
   char set produced: [1 O 0]
   char set produced: [14 x1 2] [4 y1 1] [3 x2 2] [6 x3 1] [5 y3 1] [42 x4 1] [11 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [12 x2 2] = v1*u1*x2^2 + ... (11 terms)
   pseudo-remainder: [11 y1 0] = 4*v1*u1^2*u2 + ... (10 terms)
   pseudo-remainder: [11 x1 0] = 4*v1*u1^2*u2 + ... (10 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: [9 x1 1] [4 y1 1] [2 x2 1] [67 y2 2] [6 x3 1] [5 y3 1] [2 x4 1] [11 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [9 x1 1] [8 y1 1] [7 y2 2] [6 x3 1] [5 y3 1] [12 x4 1] [12 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [12 y2 2] = v1*u1*y2^2 + ... (11 terms)
   char set produced: [1 O 0]
   char set produced: [1 v1 1] [1 y1 1] [1 y2 1] [1 y3 1] [1 y4 1] [3 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [12 y4 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 y3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 y2 2] = v1*u1*y2^2 + ... (11 terms)
   pseudo-remainder: [6 y1 0] = v1*u1^2*u2 + ... (5 terms)
   pseudo-remainder: [6 v1 1] = v1*u1^2*u2 + ... (5 terms)
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [2 x3 1] [1 y3 1] [4 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [12 v1 2] = -y2*u1*v1^2 + ... (11 terms)
   pseudo-remainder: [2 u2 2] = y2*u1*u2^2 + ... (1 terms)
   char set produced: [1 v1 1] [1 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [3 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   pseudo-remainder: [12 y3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 x3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 x2 2] = v1*u1*x2^2 + ... (11 terms)
   pseudo-remainder: [6 y1 0] = -y2*u1^2*u2 + ... (5 terms)
   pseudo-remainder: [6 v1 2] = -y2*u1*v1^2 + ... (5 terms)
   further decomposition in progress 17
   pseudo-remainder: [12 y3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 x3 0] = v1*u1^2*u2 + ... (11 terms)
   pseudo-remainder: [12 x2 2] = v1*u1*x2^2 + ... (11 terms)
   pseudo-remainder: [6 y1 0] = -y2*u1^2*u2 + ... (5 terms)
   pseudo-remainder: [6 v1 2] = -y2*u1*v1^2 + ... (5 terms)
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 v1 2] [4 x1 2] [4 y1 1] [2 x2 1] [2 y2 1] [2 x3 1] [2 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [14 x1 2] [4 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [3 y3 1] [2 x4 1] [4 y4 1] [3 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 v1 2] [2 x1 1] [2 y1 1] [4 y2 1] [2 x3 1] [2 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [9 x1 1] [8 y1 1] [4 y2 1] [2 x3 1] [2 y3 1] [14 x4 2] [4 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [12 y2 2] = v1*u1*y2^2 + ... (11 terms)
   pseudo-remainder: [19 y1 0] = 2*v1*u1^4*u2 + ... (18 terms)
   pseudo-remainder: [19 x1 0] = 2*v1*u1^4*u2 + ... (18 terms)
   further decomposition in progress 12
   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: [5 v1 8] [31 x1 1] [28 y1 1] [16 x2 1] [2 y2 1] [18 x3 1] [15 y3 1] [3 x4 1] [2 y4 1] [15 x5 1] [18 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [9 x1 1] [8 y1 1] [3 x2 2] [6 x3 1] [5 y3 1] [34 x4 1] [10 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   pseudo-remainder: [12 x2 2] = v1*u1*x2^2 + ... (11 terms)
   pseudo-remainder: [11 y1 0] = 4*v1*u1^2*u2 + ... (10 terms)
   pseudo-remainder: [11 x1 0] = 4*v1*u1^2*u2 + ... (10 terms)
   further decomposition in progress 15
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [1 v1 1] [1 y1 1] [2 x2 1] [2 x3 1] [1 y3 1] [4 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [1 y6 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 v1 2] [2 x1 1] [2 y1 1] [2 x2 1] [2 y2 1] [2 x3 1] [2 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   Status: used = 112028, alloced = 24916, time = 15.848999999999998
   char set produced: [1 O 0]
   char set produced: [9 x1 1] [8 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [3 y3 1] [9 x4 1] [8 y4 1] [3 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 v1 2] [2 x1 1] [2 y1 1] [4 y2 1] [2 x3 1] [2 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 u2 1] [1 x1 1] [2 y1 1] [3 y2 1] [2 x3 1] [1 y3 1] [1 x4 1] [2 y4 1] [1 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [2 v1 2] [2 x1 1] [2 y1 1] [4 y2 1] [2 x3 1] [2 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [3 u2 2] [5 v1 4] [6 x1 1] [6 y1 1] [3 x2 2] [54 y2 4] [6 x3 1] [5 y3 1] [12 x4 1] [33 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [2 u2 1] [1 x1 1] [2 y1 1] [3 x2 2] [2 x3 1] [1 y3 1] [1 x4 1] [4 y4 1] [1 x5 1] [2 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   char set produced: [9 x1 1] [8 y1 1] [2 x2 1] [5 y2 2] [6 x3 1] [5 y3 1] [2 x4 1] [10 y4 1] [5 x5 1] [6 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [3 v1 4] [9 x1 1] [8 y1 1] [4 x2 1] [2 y2 1] [8 x3 1] [6 y3 1] [2 y4 1] [6 x5 1] [8 y5 1] [2 x6 1] [2 y6 1]
   char set produced: [1 O 0]
   
   `The theorem is true under the following subsidiary conditions:`
   . the three points B, C and H are not collinear
   . the line EH is not parallel to the line BC
   . 2*u1-u2 <> 0
   . 4*u1^2-4*u2*u1+v1^2+u2^2 <> 0
   . the line BH is not perpendicular to the line BC
   . the line BH is not perpendicular to the line CH
   . -2*x2+u2 <> 0
   . -2*y2+v1 <> 0
   . -2*u1*y2-v1*x2+u2*y2+v1*u1 <> 0
   . -v1^3-v1*u2^2-4*u1*v1*x2-4*u2*u1*y2+4*v1*u2*u1 <> 0
   . the three points B, E and H are not collinear
   . the line BH is not perpendicular to the line EH
   . -2*x4+u2 <> 0
   . -u2+u1+x1 <> 0
   . the line BH is not perpendicular to the line GH
   . x5-u2+u1 <> 0
   . the line BH is not perpendicular to the line GF
   
   QED.


4. Theorem([arbitrary(E,H,B,C), intersection(E,H,B,C,I), oncircle(B,C,H,E), oncircle(B,C,H,F), intersection(B,C,G,F,J), midpoint(B,C,D), intersection(H,G,E,F,D), midpoint(I,J,D)],[oncircle(B,C,H,G)])
   Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned
   
   
   Theorem: If the points E, H, B, and C are arbitrary, `the two lines EH and BC intersect at ` || (I) , the point E is on the circumcircle of the triangle BCH, the point F is on the circumcircle of the triangle BCH, the two lines BC and GF intersect at J, D is the midpoint of B and C, the two lines HG and EF intersect at D, and `D is the midpoint of ` || (I) || ` and ` || J , then the point G is on the circumcircle of the triangle BCH.
   
   Proof:
   
   char set produced: [7 v2 2] [3 x1 1] [1 y1 1] [62 x2 2] [6 y2 1] [24 x3 1] [6 y3 1] [3 x4 1] [4 y4 1] [3 x5 1] [3 y5 1]
   pseudo-remainder: [20 y3 2] = -y3^2*u2*v1 + ... (19 terms)
   pseudo-remainder: [47 x3 2] = -4*u2^3*x3^2*v1 + ... (46 terms)
   pseudo-remainder: [846 y2 2] = 8*u2^6*u3*v1*y2^2 + ... (845 terms)
   pseudo-remainder: [1036 x2 2] = -8*v1^3*u2^3*x2^2*u1^2 + ... (1035 terms)
   pseudo-remainder: [1160 y1 2] = -32*u1^4*u2^3*u3*v1*y1^2 + ... (1159 terms)
   pseudo-remainder: [271 x1 2] = 8*u1*v1^3*x1^2*u2^3 + ... (270 terms)
   pseudo-remainder: [189 v2 9] = u2^2*v2^9 + ... (188 terms)
   the thoerem is possibly false: further decomposition in progress
   char set produced: [1 u3 1] [4 v2 2] [1 x1 1] [1 y1 1] [11 x2 2] [5 y2 1] [4 x3 1] [9 y3 1] [1 x4 1] [15 y4 1] [1 x5 1] [3 y5 1]
   char set produced: [1 O 0]
   char set produced: [2 u2 1] [4 y1 1] [21 x2 2] [6 y2 1] [2 x3 1] [6 y3 1] [3 x4 1] [4 y4 1] [2 x5 1] [3 y5 1]
   char set produced: [2 v1 2] [5 v2 2] [3 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [12 x3 1] [13 y3 1] [3 x4 1] [3 y4 1] [2 x5 1] [3 y5 1]
   char set produced: [1 O 0]
   char set produced: [1 O 0]
   char set produced: [7 v2 2] [3 x1 1] [1 y1 1] [18 x2 1] [22 y2 1] [80 x3 1] [98 y3 1] [3 x4 1] [3 y4 1] [2 x5 1] [3 y5 1]
   pseudo-remainder: [20 y3 2] = -y3^2*u2*v1 + ... (19 terms)
   pseudo-remainder: [1984 x3 2] = -u1^8*u2^7*v1^5*x3^2 + ... (1983 terms)
   pseudo-remainder: [922 v2 4] = -u1^9*u2^8*v1*v2^4 + ... (921 terms)
   
   `The theorem is true under the following subsidiary conditions:`
   . the line EH is not parallel to the line BC
   . the three points B, E and H are not collinear
   . -v1*u2*u1+4*v1*u1^2+3*v2*v1^2-3*u1*u3*v1+v1*u2*u3+u1*v2*u2+v1^3 <> 0
   . v1*u1^4*u2^3-4*u2^2*u3*v1^5+3*u1^3*u2^2*v1^3+4*u2^3*u1^2*v1^3+3*u1^2*v1^5*u2+4*v1^5*u2^2*u1-u2^2*u1^4*u3*v1+v1^7*u1+u1^3*u2^2*u3^2*v1-u1^4*v2*u2^3-v2*v1^6*u1-3*v2*v1^2*u1^3*u2^2-2*v1^2*u1^3*u2*u3*v2-3*v1^5*u1^2*u3+v1^3*u1^2*u3^3-v1^3*u1^3*u3^2-4*u1*u2*u3*v1^4*v2+u1^2*u2*u3^2*v1^2*v2+u1^2*u2^2*u3*v1^2*v2-7*v1^6*u3*v2+3*u3^3*v1^5-4*u1*u2^3*u3*v1^3+6*u1*u2^2*u3^2*v1^3-4*u1*u2^2*v1^4*v2-2*u1*u2*u3^3*v1^3-3*u1*u2*u3*v1^5-4*u1^2*u2^3*v1^2*v2-9*u1^2*u2^2*u3*v1^3+4*u1^2*u2*u3^2*v1^3-3*u1^2*u2*v1^4*v2-4*u1^2*u3*v1^4*v2-4*u2^2*u3*v1^4*v2+3*u2*u3^2*v1^4*v2+2*v1^4*u1*u3^2*v2-2*v1^3*u1^3*u2*u3-u1^3*v1*u2^3*u3-u3*v1^7 <> 0
   . the line BC is not perpendicular to the line EH
   
   QED.